Why do we use $rose() in assertion?

SystemVerilog
,
1

I’m trying to understand the behavior of $rose(expr) in assertion.

the $rose is defined as true if expr has changed value and is 1in the current cycle.
So I made a simple example for understanding why we have to use $rose(expr).

for example)

`timescale 1ns/1ps

module ex2;       
reg clk;  
reg a;    
reg b;    
          
initial begin     
clk = 0;  
a= 0;     
          
#4.5;     
#2 a = 1; 
#7 a = 1; 
#1 a = 0; 
end       
          
initial begin     
b = 0;    
#11 b = 1;
#2  b = 1;
#1   b = 0;       
end       
          
       
always #1 clk = ~clk;      
initial begin     
#100;     
$finish;  
end       
          
          
property impli_p; 
@(posedge clk)    
  a |-> ##3 b;    
endproperty       
          
property rose_p;  
@(posedge clk)    
  $rose(a) |-> ##3 b;      
endproperty       
          
check02 : assert property (impli_p);
check03 : assert property (rose_p);
endmodule

I get the assertion fail when I execute the assertion.

# vsim -voptargs=+acc=npr
# run -all
# ** Error: Assertion error.
#    Time: 15 ns Started: 9 ns  Scope: ex2.check02 File: testbench.sv Line: 43
# ** Error: Assertion error.
#    Time: 17 ns Started: 11 ns  Scope: ex2.check02 File: testbench.sv Line: 43
# ** Error: Assertion error.
#    Time: 19 ns Started: 13 ns  Scope: ex2.check02 File: testbench.sv Line: 43
# ** Note: $finish    : testbench.sv(29)
#    Time: 100 ns  Iteration: 0  Instance: /ex2

I didn’t get understand the behavior of $rose(). what’s the difference between check02 and check03? why does check02 make the assertion fail?

2

In reply to UVM_LOVE:

if I get it right, ‘check02’ assert that every posedge of clock, if ‘a’ so after 6ns ‘b’.
‘check03’ assert that if ‘a’ was 0’ in the previous clk posedge, and it '1 now, so after 6ns ‘b’.

‘check02’ assert that as long as a=1, always b will be 1 after 3 posedge of clock.
‘check03’ assert that always when ‘a’ was '0 at the prev cycle, and now it is '1,3 cycles later ‘b’ will be '1.

They completely different cases, don’t they?