Proposal for Incremental Formal Verification


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

Full Text: PDF(1.1MB)>>
Buy this Article

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.

open access publishing via