Knowledge Center

Formal Verification

Formal verification involves a mathematical proof to show that a design adheres to a property

Description

There are several types of formal methods used to verify a design.

The first is equivalence checking. This takes two designs, that may be at the same or different levels of abstraction and finds functional differences between them. Equivalence checking can be further broken down into two principle domains—combinatorial equivalence checking, often just called equivalence checking, and sequential equivalence checking.

Combinatorial equivalence checking is used to show that a design after logic synthesis is the same as the input RTL description. It is also used to show that no functionality has been affected when test logic or other gate-level transformations are made. It compares the combinatorial logic between corresponding registers in the original description.

Sequential equivalence checking is an emerging technology that can take two designs that have fundamentally different timing, enabling an un-timed or partially timed model to be compared against an RTL model, or between RTL models that have undergone retiming or other transformation to improve power or other design qualities. This is a necessary technology for mass adoption of high-level synthesis.

The other main branch of formal verification is property checking. A property defines a behavior that must be present in a design, or a behavior that must not be possible. A third option is called a fairness condition that would ensure that each of several options is not treated unfairly, in arbitration for example.

In some cases it may be difficult to prove a property and instead of providing a full proof, a bounded proof is all that is possible. A bounded proof may say that the behavior is, or isn’t, possible within a defined number of clocks, or from a specific starting state, or when certain constraints are applied to the system.

The Formal Verification Capability Maturity Model (Formal CMM) has been proposed by Oski Technology as a way to define the progression of formal verification methodologies as “Levels,” each with different goals, training, and tool requirements.

The first level is automatic formal checks which focus on small, specific problems. The second level introduces formal apps, where a user specifies something about design intent and the tool generates assertions. At the third level, targeted assertions are written. These first three levels aim to reduce the time to finding first bug.

The next two levels are more advanced and focus on time to last bug. The fourth level begins to use formal block-level verification as a replacement for simulation, where the size of the DUT is typically a block or a module or a small IP. The fifth level builds on level four and aims to prove that the system architecture is correct for specific requirements such as cache coherence or to prove that the system will not deadlock.

These five levels represent the state of the industry today; developments may call for additional levels to be added in the future.