Systemverilog assertions

SystemVerilog
,
1

How to write the following property without Non Constant expression error?

property falling_check;
@(posedge clk) $rose(r) |-> ##[d:d+6] ($fell(f));
endproperty

2

Below is an assertion that works. Note tha the first_match() is needed because without it, the assertion will never fail.


import uvm_pkg::*; `include "uvm_macros.svh" 
module varm; 
	/* property falling_check;
@(posedge clk) $rose(r) |-> ##[d:d+6] ($fell(f));
endproperty*/ 
  bit clk, r, f, go=1, reject; 
  int d=2, count1, count2; 

  
  property p_falling_check;  
  	int v1, v2; 
  	 @(posedge clk) 
  	 	($rose(r), v1=d) |-> (first_match((1, v1=v1-1'b1) [*1:$] ##0 (v1==0, v2=6))  
  	 		 // intersect !$fell(f, @(posedge clk)) [*1:$]) ##0  // incorrect 
  	 	           intersect !f [*1:$]) ##0
   (first_match((1, v2=v2-1) [*1:$] ##0 v2==0) intersect  $fell(f, @(posedge clk)) [=1]) ;             
  endproperty
  ap_falling_check: assert property(@(posedge clk)p_falling_check); 
  


  initial forever #10 clk=!clk;  
  initial begin 
     repeat(200) begin 
       @(posedge clk);   
       #2 if (!randomize(r, f)  with 
           { r dist {1'b1:=1, 1'b0:=8};
       		 f dist {1'b1:=1, 1'b0:=5};})
       	          `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
	
	
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
3

In reply to ben@SystemVerilog.us:

Thankyou very much Ben, but for
@(posedge clk) $rose(r) ##[d:d+6] !f
the below didn’t work
property p_falling_check;
int v1, v2;
@(posedge clk)
(rose(r), v1=d) |-> (first_match((1, v1=v1-1'b1) [*1:] ##0 (v1==0, v2=6))
// intersect !fell(f, @(posedge clk)) [*1:]) ##0 // incorrect
intersect !f [*1:]) ##0 (first_match((1, v2=v2-1) [*1:] ##0 v2==0) intersect (!f, @(posedge clk)) [=1]) ;
endproperty
can you please help?

4

In reply to ranjithkumar d:

The model, repeated below, emulates "$rose(r) ##[d:d+6] !f ". Below are the simulation results

Model checks that between the rose of r and the 1st d (2 in my simulation) there is no f
That is presented in

(first_match((1, v1=v1-1'b1) [*1:$] ##0 (v1==0, v2=6))  
  	 		                       // intersect !$fell(f, @(posedge clk)) [*1:$]) ##0  // incorrect 
  	 	                           intersect !f [*1:$])

The model then states that thereafter, there is an occurrence of fell of f up to no more than 6 cycles.

(first_match((1, v2=v2-1) [*1:$] ##0 v2==0) intersect  $fell(f, @(posedge clk)) [=1])


import uvm_pkg::*; `include "uvm_macros.svh" 
module varm; 
	/* property falling_check;
@(posedge clk) $rose(r) |-> ##[d:d+6] ($fell(f));
endproperty*/ 
  bit clk, r, f, go=1, reject; 
  int d=2, count1, count2; 

  
  property p_falling_check;  
  	int v1, v2; 
  	 @(posedge clk) 
  	 	($rose(r), v1=d) |-> (first_match((1, v1=v1-1'b1) [*1:$] ##0 (v1==0, v2=6))  
  	 		                       // intersect !$fell(f, @(posedge clk)) [*1:$]) ##0  // incorrect 
  	 	                           intersect !f [*1:$]) ##0
  	 	                     (first_match((1, v2=v2-1) [*1:$] ##0 v2==0) intersect  $fell(f, @(posedge clk)) [=1]) ;             
  endproperty
  ap_falling_check: assert property(@(posedge clk)p_falling_check); 
  


  initial forever #10 clk=!clk;  
  initial begin 
     repeat(200) begin 
       @(posedge clk);   
       #2 if (!randomize(r, f)  with 
           { r dist {1'b1:=1, 1'b0:=8};
       		 f dist {1'b1:=1, 1'b0:=5};})
       	          `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
	
	
endmodule