Design and implementation of formal verification tool for combinational circuits using automatic test pattern generation

Abstract

Functional Verification or Logical Simulation is an important phase in Digital Design Flow. It is to ensure that the functionality of the design remains the same as the initial desired functionality at any point of time in the whole process, before advancing to the next level. If errors are detected in the early stages, they can be corrected and by doing this, unwanted cost can be reduced.

Due to the growing complexity of the digital design, verification has become the major bottleneck, leading to impractical exhaustive simulation. Formal Verification has been known as an alternative to logical simulation. In this approach, mathematical techniques are used to prove the properties of the design and it is equivalent to exhaustive simulation. Therefore a design error could be detected using formal verification where simulation cannot detect. Therefore Formal Verification is a better choice to detect any error in the design.

In this report, existing methodologies of Formal Verification and the Automatic Test Pattern Generation (ATPG) algorithms are studied. A hybrid approach to implement a new formal verification tool, D-Verify using ATPG algorithm for combinational circuits is being proposed, designed and implemented.