Esterel EDA>Products>Design Verifier

Design Verifier*

Design Verifier™ is used to exhaustively verify complex functional properties, detect hard-to-find corner-case bugs, and explore complex design behaviors. Properties are either defined by the user or defined by automatic assertions extracted from designs.

Writing assertions together with specifications and design is an efficient and flexible way to document expected behavior, and to automate sanity checks. When refining or modifying the specification, proof engines included in Esterel Studio can check non-regression of design assertions and detect mistakes in seconds.

• Design Verifier implements a multiple-engine formal verification system.
• Design Verifier is completely integrated into the Esterel Studio IDE allowing users to be immediately productive.
• Design Verifier does not need any test benches or test vectors but performs formal analysis and model-checking of the design. It can be used right from the start of the design flow.
• When Design Verifier finds a possible fault, it produces a simulation scenario leading to the falsification of the assertion so that it can easily be simulated and the error diagnosed and corrected.

Formal property verification

To illustrate typical usage and capabilities of Formal Verification and Design Verifier, we use a FIFO example with concurrent read, write and bypass. You can download the FIFO Esterel Studio design document for reference.

Assertions can be directly embedded into Esterel Designs or Safe State Machines (SSM). Below three properties about a simple FIFO are embedded using Esterel assertions. In plain English the properties are:

• The FIFO read pointer is always less than or equal the write pointer.
• The FIFO never tries to simultaneously read and write the same memory address.
• The FIFO bypass logic does not read nor write the FIFO memory.

The first property is false the last two are valid.

Selection and verification of assertions

Direct root-cause analysis of counter-examples

The root-cause of assertion violations can be immediately analyzed using the interactive debugger and waveform display to replay the counter-example scenarios. To analyze the violated assertion, simply double click-on the counter-example scenario which will launch the simulator. A quick replay of the generated scenario leads us directly to the problem: the write pointer indeed may become smaller than the read pointer.

Properties as external observers

Properties can be defined as external observers using stand-alone Esterel Designs or SSMs. External observers are a way to perform black-box verification, where the verification observes only boundary signals and makes no assumptions about the internal state and variables of the design. The SSM below implements an observer for the FIFO that can be used to verify that only "read" are effective to leave FIFO "full" state. The observer will emit a dedicated output (called BUG here) if and only if the property is violated.

Automatic consistency assertions

Esterel Studio can generates automatic assertions to statically check that there cannot be signal collisions (called single signal check). In the FIFO example, the data out of the FIFO can be written either by the bypass logic or by the FIFO memory but not by both at the same time. The assertion can be selected and verified directly using the Design Verifier.

Design exploration

Design Verifier can help the user construct simulation scenarios to explore the functional behavior of designs. Functionality to be explored can be stated simply with signals, as in the illustration below meaning: "can the FIFO output "Full" be emitted". With this to prove,the Design Verifier will quickly generate an input sequence filling up the FIFO.

* ESTEREL STUDIO Design Verifier is based on the Prover Plug-In. Prover Plug-In is a trademark of Prover Technology AB in Sweden, the United States and in other countries.