A Hybrid Model Checking - Theorem Proving based Approach for Formal Verification of Digital Circuits

Abstract

Verification of integrated circuits (ICs) using traditional simulation techniques has always suffered from incompleteness due to the ever increasing complexity of ICs and the limited computational resources and time. Formal verification has been extensively used for digital circuit verification to overcome the simulation limitations. However, the automated formal techniques, based on model checking and automated theorem proving usually have scalability issues for contemporary digital circuits. Whereas, the interactive theorem provers, based on higher-order-logic, require significant user guidance, which makes them unsuitable for industrial usage. To alleviate these issues, we propose a hybrid model checking - theorem proving based approach for the formal functional verification (FFV) of digital RTL circuits with both combinational and sequential logic. The main idea behind the proposed approach is to verify the equivalence of the structural and behavioral views of the combinational logic blocks in the design under verification using a higher-order-logic based approach. The obtained behavior is then verified along with the behavior of the sequential blocks to verify the behavior of the overall circuit in a model checker. This two-step process reduces the number of binary decision diagram (BDD) variables and nodes by replacing the structural implementation details composed of a large number of gates, with the corresponding behavior, which is comparatively compact, and thus improving the scalability of model checking. Our theorem proving step is automatic as well based on a formally verified library of generic combinational components. Thus, the proposed methodology offers automatic formal verification of RTL circuits with an improved scalability compared to traditional model checking. The proposed approach is realized using the HOL4 theorem prover and the nuXmv model checker and it supports completely automatic property generation and formal modeling of circuits to minimize the user intervention and time. For demonstration purpose, we verified several Verilog circuits, including a 2501-bit arithmetic circuit and multiple modules of the USB2.0 Design from the VCEGAR and OpenCores benchmarks. We have formally verified these circuits with a significant reduction in time, effort and resources. For example, the behavioral verification of 2501-bit arithmetic cir cuit took only 17.59 seconds to verify the model against the specified invari ant. Moreover, approximately 50% reduction in the memory usage, number of BDD variables and nodes is observed for an 8-bit ALU circuit by replacing the structural implementation with the corresponding behavior