Assertion System Functions and Tasks - SVA: The Power of Assertions in SystemVerilog - page 142

has the same effect as

logic a, b, temp;
always @( posedge clk) begin
temp <= $sampled(b); a <= temp;
end
provided that a is not assigned elsewhere.
To understand this, we need to apply the definition of $past(b) —the sampled
value of b on the prior clock rise. The value of b immediately after the prior clock
rise is modeled by the variable temp , and a is equal to the sampled value of temp at
that time step, i.e., to the value of temp immediately before the clock rise.

t

7.2.1.3 Rose and Fell

Sampled value function $rose(e, @clk) returns true iff the Least Significant Bit
(LSB) of e has changed to 1, and false, otherwise. The sampled value function
$fell(e, @clk) returns true if the LSB of e has changed to 0, and false, otherwise.
More precisely

$rose(e, @clk)
$past(LSB(e),,,@clk)!== 1 && $sampled(LSB(e))=== 1 .
$fell(e, @clk)
$past(LSB(e),,,@clk)!== 0 && $sampled(LSB(e))=== 0 .

System functions $rose and $fell compare the past value with the current
sampled value of the expression. The clocking event argument is optional and if
omitted, its value is inferred from the context as explained in Sect. 7.2.1.5 .

Example 7.19. For the timing diagram in Fig. 7.2 , $rose(a, @( posedge clk))
returns true for time steps 30 < t 40 and 50 < t 60. For all other time steps, it
returns false .
$fell(a, @( posedge clk)) returns true for time steps 40 < t 50 and 70 <
t 80. For all other time steps, it returns false .

t

Example 7.20. If an expression changes its value from 3'b100 to 3'b001 , $rose
returns true , and fell returns false , since only the LSB counts. If an expression
changes its value from x to 1, $rose returns true , and if it changes its value from x
to 0, $fell returns true . If an expression becomes x , both $rose and $fell return
false .

t

Example 7.21. Assume that sig is of type bit . The assertion from Example 6.29
“signal remains high during 5 cycles” may be rewritten as follows using function
$rose :
a1: assert property (@( posedge clk) ##1 $rose(sig) |=> sig[ * 4]);
What happens if we omit the initial delay in assertion a1 ?
a2: assert property (@( posedge clk) $rose(sig) |=> sig[ * 4]);