Knowledge Center
Navigation
Knowledge Center

Formal Verification

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

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.


Multimedia

Billion-Gate Design Connectivity

Multimedia

Formal Signoff

Multimedia

Heterogeneous Computing Verification

Multimedia

Formal Datapath Verification

Multimedia

Planning Out Verification

Multimedia

ISO 26262 Statistics

Multimedia

Tech Talk: Traceability In Functional Safety

Multimedia

Tech Talk: FPGA RTL Checking

Multimedia

Tech Talk: Better Coverage

Multimedia

Tech Talk: Formal Discussion

Multimedia

Tech Talk: Formal Practices

Multimedia

Tech Talk: Formal Verification

Multimedia

Tech Talk: Debugging IP

Multimedia

Tech Talk: Security Risks In An SoC

Multimedia

Executive Briefing: Formal Attire


Related Entities