Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 77

10 20 30 40 50 60 70 80 90 100

clk

rst

req

ack

Fig. 4.11 Assertion with reset

Example 4.9. An example of disable iff .
module reqgen( input logic busy, clk, rst, output logic req);
wire idle;
assign idle = !busy;
always @( posedge clk or posedge rst) begin
if (rst) req <= '0;
else req <= !busy;
end
req_when_idle: assert property (
@( posedge clk) disable iff (rst) idle |=> req)
$display("req_when_idle completed");
endmodule : reqgen
In the usual way, assertion req_when_idle is scheduled in the Observed
region as a result of the occurrence of its clock ( posedge clock) in the Active
region. None of the signals in the assertion expression, namely, idle and req ,
have any effect on the assertion outside the time slots in which the clock tick
occurs. The disable iff expression (rst) is an exception to this general rule.
req_when_idle is disabled in the time slot when signal rst becomes true. Its action
block is scheduled in the same Reactive region.

t

Unlike other expressions in the body of a concurrent assertion, the
disable iff expression is not sampled and can affect the result of the
assertion from any scheduling region in which it becomes true.

4.4.5 Boolean Expressions

Boolean expressions are elementary building blocks for assertions. There are two
places in an assertion statement where Boolean assertions are used: