Proposal for incremental formal verification

A formal verification approach that combines verification based on binary d ecision diagrams (BDDs) and theorem-prover-based verification has been deve loped. 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 specification s in higher-level descriptions given in terms of arithmetic expressions, lo wer-level design descriptions given in terms of Boolean expressions, and co nstraints. The incremental verifier limits the behavior of the design by us ing the constraints, and compares the partial behavior limited by the const raints 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 v erifier with different constraints can produce higher design descriptions f rom the lower design descriptions in a step-by-step manner. These higher de scriptions are then input to the theorem-prover-based verification which en ables faster treatment of larger circuits. Preliminary experimental results show that the incremental verifier can successfully check the partial equi valence and replace the matched parts by higher constructs.