Why do we use $rose() in assertion?

Question

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?

Answer 1

Solution

OE93

Full Access

10 posts

June 08, 2023 at 6:47 am

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?

Languages & Standards

Methodologies

Techniques & Tools

Universal Verification Methodology (UVM)

Featured Courses

Additional Courses

Formal-Based Techniques

Analog/Mixed Signal

UVM Forum

SystemVerilog Forum

Coverage Forum

Additional Forums

Implementation Patterns

Specification Patterns

Pattern Resources

UVM Cookbook

Coding Guidelines & Deployment

Coverage Cookbook

Featured & On-Demand

On-Demand Library

Recording Archive

Conferences & WRG

Siemens EDA Learning Center

Blog & News

Verification Horizons Publication

About Us

Training

Solution

Portfolio

Explore

Siemens

Contact