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 results expected from the IP (assert),
- the constraints on the inputs (assume).
The HORUS environment
From declarative assertions written in PSL or in SVA, synthesizable
designs are automatically produced in Verilog or in VHDL for:
- synchronous or asynchronous observation monitors,
- test sequence generators,
- interfaces and history tracing mechanisms
The HORUS technology is now integrated inside Dolphin Integration
(article in French
The main advantages of HORUS are:
- Same reusable properties through the design flow
- Standard input languages: PSL, SVA
- Formally proven construction method
- Synthesizable monitors and generators
- Simulation with standard design software
- FPGA emulation for accelerated simulation
- On-line checking of safety critical circuits
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:
- P1 : between the end of a transaction (END) and the beginning of
the next one (START), an error (ERROR) cannot occur
always (END -> next (START before ERROR))
- P2 : the data translator cannot be ready (READY) before being
! (READY until START)
A property that expresses a relation on the signals that interconnect the
translation module and the receiving node, can be seen both as:
- a functionality that the translation module should guarantee: assert P1
More precisely, this property specifies a functionality to be verified by simulation,
emulation, or formal proof, the coverage of which may be of interest. Such property
is associated with a monitor device.
- or a constraint on the inputs of the receiving mode, that features the
signals of the environment: assume P1
In that case, the property can be used to generate constrained tests. The corresponding
device is a test generator.
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
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:
- during design, in simulation and/or emulation for debug and circuit
- as embedded components, for critical systems behavior monitoring.
This approach has been extended to asynchronous monitors: for communication verification in multiclock
systems (GALS), and for critical systems monitoring.
- M.Liu, D.Borrione, P.Ostier, L.Fesquet: "PSL-based online monitoring of
digital systems". Proc. FDL'05, September 2005.
- D.Borrione, M.Liu, K.Morin-Allory, P.Ostier, L.Fesquet: "On-line
assertion-based verification with a proven correct library of monitors".
Proc. 3rd International Conference on Information
and Communication Technology (ICICT2005), December 2005.
- K.Morin-Allory, D.Borrione: "Proven correct monitors from PSL specifications".
Proc. DATE'2006, March 2006.
- K.Morin-Allory, L.Fesquet, D.Borrione: "Asynchronous Assertion Monitors for
multi-Clock Domain System Verification". Proc. IEEE International Workshop on
Rapid System Prototyping RSP'06, June 2006.
- K.Morin-Allory, D.Borrione: "On-line monitoring of properties built on regular
expressions". Proc. FDL'2006, September 2006.
- Y.Oddos, K.Morin-Allory, D.Borrione: "On-line vector generation from temporal
constraints written in PSL". Proc. VLSI-SoC'2006, October 2006.
- K.Morin-Allory, L.Fesquet, D.Borrione, B.Roustan: "Asynchronous Online-Monitoring
of Logical and Temporal Assertions". Proc. FDL'07, September 2007.
- K.Morin-Allory, E.Gascard, D.Borrione: "Synthesis of property monitors for on
line fault detection". Journal of Circuits, Systems, and Computers (JCSC), Vol. 16(6), December 2007.
- Y.Oddos, K.Morin-Allory, D.Borrione: "Assertion-Based Design with Horus".
Proc. MEMOCODE'2008, June 2008 (short paper).
- Y.Oddos, K.Morin-Allory, D.Borrione: "Assertion-Based Verification and On-line Testing in Horus".
Proc. IEEE International Design and Test Workshop (IDT'08), Monastir (Tunisia), December 2008.
- Y.Oddos: "Vérification semi-formelle et synthèse automatique de circuits à partir
de spécifications temporelles écrites en PSL".
PhD Thesis, Grenoble University, November 2009 (in French).