HORUS: Verifying properties using proven correct monitors



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 is currently extended to:

References