Assertions - Properties

In these examples we have been using, the properties being asserted are specified in the assert property statements themselves. Properties may also be declared separately, for example:

property not_read_and_write;
not (Read && Write);endproperty assert property (not_read_and_write);

Complex properties are often built using sequences. Sequences, too, may be declared separately:

sequence request
Req;
endsequence

sequence acknowledge
##[1:2] Ack;
endsequence

property handshake;
@(posedge Clock) request |-> acknowledge;
endproperty

assert property (handshake);

Assertion Clocking

Concurrent assertions (assert property and cover property statements) use a generalised model of a clock and are only evaluated when a clock tick occurs. (In fact the values of the variables in the property are sampled right at the end of the previous time step.) Everything in between clock ticks is ignored. This model of execution corresponds to the way a RTL description of a design is interpreted after synthesis.

A clock tick is an atomic moment in time and a clock ticks only once at any simulation time. The clock can actually be a single signal, a gated clock (e.g. (clk && GatingSig)) or other more complex expression. When monitoring asynchronous signals, a simulation time step corresponds to a clock tick.

The clock for a property can be specified in several ways:

Explicitly specified in a sequence:

sequence s;
@(posedge clk) a ##1 b;
endsequence
property p;
a |-> s;
endproperty
assert property (p);

Explicitly specified in the property:

property p;
@(posedge clk) a ##1 b;
endproperty
assert property (p);

Explicitly specified in the concurrent assertion:

assert property (@(posedge clk) a ##1 b);

Inferred from a procedural block:

property p;
a ##1 b;
endproperty
always @(posedge clk) assert property (p);

From a clocking block (see the Clocking Blocks tutorial):

clocking cb @(posedge clk);
property p;
a ##1 b;
endproperty
endclocking
assert property (cb.p);

From a default clock (see the Clocking Blocks tutorial):

default clocking cb;

Handling Asynchronous Resets:

In the following example, the disable iff clause allows an asynchronous reset to be specified.

property p1;
@(posedge clk) disable iff (Reset) not b ##1 c;
endproperty

assert property (p1);

The not negates the result of the sequence following it. So, this assertion means that if Reset becomes true at any time during the evaluation of the sequence, then the attempt for p1 is a success. Otherwise, the sequence b ##1 c must never evaluate to true.