Design and implementation of formal verification methodology using Boolean satisfiability

Abstract

Functional verification is an important phase in the design flow of digital circuits as it is used to verify a design when changes occur. It ensures that the functionality of the original design is not affected by the changes. Logic simulation is a widely used technique for the verification of a design. Formal verification is an alternative technique for logic simulation as it is impossible to verify the overall design completely and detect design bugs by logic simulation since the quality of simulation results deeply depend on given input patterns.

To address this, formal verification uses mathematical techniques to compare the original representation to the new representation. Formal verification method breaks the designs into mathematical representations and then formally proves that the two design representations are equivalent. Formal verification is realized on top of the basic Boolean reasoning techniques such as binary decision diagram (BDD), automatic test-pattern generation (ATPG) and Boolean satisfiability (SAT) as logic circuits compute Boolean functions.

In this report, a design methodology for formal verification of digital combinational circuit using Boolean satisfiability had been proposed and a new formal verification tool Verification-Satisfiability (VeriSat) had been implemented.