HORUS: is semi-formal verification the future of simulation?

During the design process of an IP, its functional verification is considered a long and painful task. Assertion-based verification of logic and temporal properties can be performed with a variety of methods that can save considerable time.

The traditional design flow

The approach we developed is illustrated by the figure hereafter. The left part of the diagram shows the usual design flow together with the various levels of simulation-based verification, and the right part exhibits the same verification steps with assertions.

This second approach complements, possibly replaces, the time-consuming test vector elaboration, and helps interpret the results. At all levels of the design flow, assertions help describe:

The HORUS environment

From declarative assertions written in PSL or in SVA, synthesizable designs are automatically produced in Verilog or in VHDL for:

The HORUS technology is now integrated inside Dolphin Integration tools (article in French)

The main advantages of HORUS are:

Verifying and monitoring properties

There is a crucial need of expressing logical and temporal properties all along the specification, verification and test process. Two IEEE standard languages (PSL and SVA) are widely used to express such properties. These properties are more concise and accurate than waveforms, but can nevertheless be illustrated and graphically validated using waveforms.

In the example below, which is a simplified actual industrial problem, two nodes communicate via a data translator, according to a protocol characterized by various properties.

Two of them can be given as example:

A property that expresses a relation on the signals that interconnect the translation module and the receiving node, can be seen both as:

Modular Monitors and Generators

The approach proposed by the TIMA laboratory is based on a library (VHDL or Verilog) of primitive components, one for each PSL primitive operator, and an interconnection scheme, both of them formally proven correct. The proof of correctness has been performed using theorem proven techniques for monitors, and model-checking for generators. This approach leads to optimised and synthesizable VHDL or Verilog descriptions.

On the previous example, monitors built on properties P1 and P2 can be connected to the Design Under Test; the signals of the DUT involved in the property are mapped on the property input ports:

The component for property P1 is the interconnection of the primitive components contained in the property: always, implies, next and before. The monitor of P2 is built in the same way.
The generator construction method is similar, except that a random number generation device is added to each primitive component.
These components can be used for different purposes:

This approach has been extended to asynchronous monitors: for communication verification in multiclock systems (GALS), and for critical systems monitoring.

References