Proposal for Incremental Formal Verification

Toru SHONAI  Kazuhiko MATSUMOTO  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E81-D   No.11   pp.1172-1185
Publication Date: 1998/11/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Computer Hardware and Design
Keyword: 
formal verification,  processor,  pipeline,  BDD,  theorem prover,  

Full Text: PDF>>
Buy this Article




Summary: 
A formal verification approach that combines verification based on binary decision diagrams (BDDs) and theorem-prover-based verification has been developed. This approach is called the incremental formal verification approach. It uses an incremental verifier based on BDDs and a conventional theorem-prover-based verifier. Inputs to the incremental verifier are specifications in higher-level descriptions given in terms of arithmetic expressions, lower-level design descriptions given in terms of Boolean expressions, and constraints. The incremental verifier limits the behavior of the design by using the constraints, and compares the partial behavior limited by the constraints with the specifications by using BDD-based Boolean matching. It also replaces the matched part of the lower design description with equivalent constructs in the higher descriptions. Successive uses of the incremental verifier with different constraints can produce higher design descriptions from the lower design descriptions in a step-by-step manner. These higher descriptions are then input to the theorem-prover-based verification which enables faster treatment of larger circuits. Preliminary experimental results show that the incremental verifier can successfully check the partial equivalence and replace the matched parts by higher constructs.