Introduction - SVA: The Power of Assertions in SystemVerilog - page 26

1 checker mytrig ( sequence trig, property prop, event clk);
2 a1: assert property (@clk trig |-> prop);
3 c1: cover property (@clk trig);
4 endchecker : mytrig
5 module m( input logic done, ready, clock, output logic idle);
6 ...
7 assign idle = done || !ready;
8 mytrig check_consistency(done, idle, posedge clock);
9 endmodule :m

Fig. 1.13 Asimple checker

The example shown in Fig. 1.13 illustrates the concept of checker .
mytrig is a checker which gets three arguments: trig , prop , and clk . trig
should be a sequence, prop should be a property, and clk should be an event.
mytrig consists of assertion a1 checking that whenever trig happens prop is
true (operator |-> , called overlapping suffix implication ), and a cover statement
c1 monitoring whether trig happens.
The checker is instantiated in module m ,Line 8 , with actual arguments done ,
idle , and posedge clock . Even though done and idle are signals, it is valid
to pass them to the checker as actual arguments because Boolean expressions are
special cases of sequences and properties.
We describe checkers and their use in Chaps. 9 , 23 and 24 .

1.6 SVA and PSL

Besides SVA, PSL (Property Specification Language) [ 6 ] is another standard
assertion specification language that is widely used in the industry. The goal of
PSL is to provide a language subset for assertions that could work in conjunction
with a variety of languages. To that end, the syntax is designed to be as neutral as
possible, customized with a syntactic flavor for the individual language hosting the
PSL features, such as SystemVerilog flavor and VHDL flavor. The semantics related
to the integration of PSL with the host language is left open for the tools to define,
to suit the environment of the tool.
Many of the PSL language features are semantically equivalent to those of SVA,
but there are some differences of importance. One of the PSL features is the Optional
Branching Extension (OBE) which defines operators for temporal properties in
terms of branching time. The OBE features are meant only for formal verification
and do not fit the simulation paradigm. SVA does not have the notion of branching
time [ 35 ]; the time used in SVA is always linear (see Chap. 21 ), but all the linear time
operators in SVA can be simulated. The OBE operators in PSL cannot be simulated.