We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
HVoC: a Hybrid Model Checking - Interactive Theorem Proving Approach for Functional Verification of Digital Circuits.
- Authors
Minhas, Mishal Fatima; Hasan, Osman; Abed, Sa'ed
- Abstract
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.
- Subjects
DIGITAL electronics; SOFTWARE verification; COMPUTATIONAL complexity; SCALABILITY
- Publication
Journal of Electronic Testing, 2021, Vol 37, Issue 4, p561
- ISSN
0923-8174
- Publication type
Article
- DOI
10.1007/s10836-021-05956-y