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

assertions (e.g., a4 ) are legal outside procedural code, but immediate assertions
would be illegal there. Immediate assertion a1 and deferred assertions a2 and a4
are checked whenever either a or b changes value, while concurrent assertions a3
and a5 are checked only at the clock event clk , which occurs when clk changes
value.
Concurrent assertions use sampled values of their variables. For design signals,
the sampled value is the value of the variable at the beginning of the simulation
step, before any values change in the time step. Therefore, in waveforms it looks as
if concurrent assertions used past values of design signals from the preceding time
steps. This is described in detail in Sect. 4.4.3 .
Assertion Statements
Assertion statements specify properties on the behavior of signals. There are three
major assertion statements in SVA: assertions (the keyword assert ), assumptions
(the keyword assume ), and cover statements (the keyword cover ). Each type of
statement directs what to do with the specified property. These statements may be
immediate, deferred, or concurrent.
An assert statement makes sure that the design behaves as the properties in the
statement prescribe. Its purpose is to check the correctness of the system. An assume
statement states assumptions, specifying properties that should hold to enable the
proper functioning of the system. Its purpose is to ensure that the checking is
conducted under a system or environment that complies with the stated conditions.
A cover statement checks that the behavior it specifies is actually exhibited while
testing the system. Unlike assert statements, the interest lies in detecting only
selective cases from all possible cases of valid behavior.
In the following example, the same condition is used in all three types of
assertions ( a1 , m1 , c1 ) to depict the difference in motivation.
bit ok;
// ...
a1: assert property (@clk ok);
m1: assume property (@clk ok);
c1: cover property (@clk ok);
The difference between a1 and m1 is as follows: a1 states that ok must be 1'b1
for correct behavior. It is a property that the design is obliged to satisfy. m1 states
that it can be taken for granted that ok is 1'b1 . Assertions are checked while taking
into account assumptions. Typically, but not necessarily, assumptions are written on
primary inputs of the design, characterizing the behavior of the environment of the
design.
The cover statement c1 states that there exists some valid system behavior
where ok gets value 1'b1 . This does not prevent the system from having other
valid behaviors where this condition does not hold. Cover statements are usually
written to ascertain that there exist tests exercising specific scenarios.
SVA assertion statements are further discussed in Chaps. 4 and 18 .