What is Formal Verification?
Formal verification is an alternative to verification through simulation. Verification through simulation applies a large number of input vectors to the circuit and then compares the resulting output vectors to expected values. As designs become larger and more complex and require more simulation vectors, regression testing with traditional simulation tools becomes a bottleneck in the design flow.
What is Formal Verification?
Formal verification is an alternative to verification through simulation. Verification through simulation applies a large number of input vectors to the circuit and then compares the resulting output vectors to expected values. As designs become larger and more complex and require more simulation vectors, regression testing with traditional simulation tools becomes a bottleneck in the design flow.
Formal Verification Process:
Design formality verification using equivalence checking is a four-phase process:
- Read and elaborate language descriptions into logical representations
Formality begins a verification by reading a set of user-defined design and library files and elaborates them into a format ready for equivalency checking that fully represents the logic of the user-defined top-level model. During this phase, you establish the reference and implementation designs, along with corresponding compare points and logic cones.
- Set up to preempt differences
There may be intended functional differences in the two designs being compared. In these cases, perform setup to account for these differences to avoid false-failures. An example is adding scan logic to the implementation design. You can still check that the non-scan functionality of the implementation design matches that of the reference design by setting a constant in the implementation design that disables the scan logic.
- Map corresponding signals between pairs of designs (Matching)
Prior to design verification, Formality tries to match each primary output, sequential element, black box input pin, and qualified net in the implementation design with a comparable design object in the reference design.
- Compare the logic cones that drive the mapped signals (Verification)
Verification is the primary function of equivalence checking. By default, Formality checks for design consistency when you verify a design or technology library.