HVoC: a Hybrid Model Checking - Interactive Theorem Proving Approach for Functional Verification of Digital Circuits

Automated formal verification techniques, based on model checking and theorem proving, usually have scalability issues for contemporary digital circuits. On the other hand, interactive theorem provers can overcome this issue, by verifying circuits using universally quantified variables, at the cost of significant skilled guidance. Leveraging upon the complimentary nature of the techniques, this paper presents a hybrid model checking - theorem proving approach for the formal functional verification of digital circuits (HVoC). The main idea is to first use a higher-order-logic theorem prover to replace the structural (RTL or gate level) implementations of the combinational modules with their, formally verified, corresponding behavior and then verify the complete behavioral implementation using a model checker. This kind of a 2-step process not only reduces the computational complexity, but, is also quite effective in terms of counterexample generation time. Our experiments on some benchmarks show an average $$50\%$$ reduction in analysis time.