The Questa Formal suite of applications complements traditional RTL code modeling by formally analyzing object behavior to detect possible states that might lead to an error. This approach identifies errors that were missed in the simulation and ensures that control logic units operate completely correctly.

Questa Formal can be used to formally verify individual blocks of a design as soon as they are ready and before they are integrated into the SoC and before the infrastructure (testbench) for the simulation is developed. By analyzing the same RTL description as the simulation system as well as full integration with the USDB (Unified Coverage Database), Questa Formal is an excellent tool for finding and fixing bugs and, ultimately, accelerating the completeness of functional coverage.

How formal verification works

Questa Formal analyzes the behavior of the object under test and identifies all the states that the object can go into from its current state. This approach explores the full "breadth" of the set of states, in contrast to traditional simulation, which analyzes the "depth" of an object's progression from the current state as influenced by the test vectors it's fed.

In this way, Questa Formal makes it possible to detect all the errors that occur when the current state switches to all possible contiguous states, without using test actions to detect those errors. This ensures that all possible combinations of input stimuli can be tested to make sure the object is functioning correctly. At the same time, this approach essentially detects hard-to-reach states in the simulation, speeding up the achievement of completeness of coverage.

Automatics

Automatic "push-button solution"

.

The Questa Formal is an easy-to-use, next-generation suite of applications for verifying complex "hidden" errors. For example, the Questa X-Check application uses formal algorithms to exhaustively solve the uncertain signal state propagation problem X for two variants, optimistic and pessimistic. This problem cannot be solved by traditional modeling.