Hierarchical Formal Verification of Hardware

Scaling hardware formal verification (FV) has been an ongoing challenge due to the state space explosion problem. In this paper, we introduce a bottom-up verification methodology that leverages design hierarchy by using sound abstractions at each level in the hierarchy to decompose the overall FV problem into a set of smaller, more manageable FV tasks. We use the recently proposed Instruction-Level Abstraction (ILA) as a complete specification at each level of the design hierarchy. We then utilize ILA-based verification methods to check correctness of modules composed at that level. The ILA specification includes an interface specification for each module and interface checks for verifying correct inter-module communication. This approach enables compositional verification with the following guarantee: if each hardware component refines its ILA specification and passes the interface checks, then the RTL composition refines the ILA composition. We then show how this compositional verification methodology facilitates a bottom-up hierarchical verification approach, where the specification at one level serves as the implementation at the next higher level. We demonstrate the increased scalability of our methodology through several case studies, including complex modules in two deep learning accelerators (FlexASR and NVDLA) where verification fails to complete on the flat designs.