Need to Use Variable in Assertions ## Delay

In reply to Dharak:

Hello!

I have faced the same problem :)

let’s say for example the interface is parametrized with parameter “sva_parameter”

and you want to wait no. of clock cycles equal to this parameter, then using ##sva_parameter will not be allowed!
then you need to make a sequence, this sequence will take the generic or the parameter as an input and it works!
Kindly check the following example:

sequence dummy_seq_1 (delay);
1 ##delay 1;
endsequence

property p1;
@(posedge clk)
(!signal_a ##2 signal_b) |-> dummy_seq_1(sva_parameter) |-> !signal_c ;
endproperty

assert property (p1)
uvm_report_info(“>> P1 << Pass”,“Check Pass”,UVM_NONE);
else
uvm_report_error(“>> P1 << Fail”,“Check Fail”,UVM_NONE);

It works :)

In reply to Elbosily:
Some comments


// 1) Following assertion can never fail because if the *0:$] and b==0
($rose(a), v=delay+1'b1) |-> (v>0, v=v-1'b1)[*0:$] ##1 v==0 ##0 b == 1;

// 2) Following assertion CAN fail because of the first_match() if b==0
($rose(a), v=delay+1'b1) |-> 
     first_match((v>0, v=v-1'b1)[*0:$] ##1 v==0) ##0 b == 1;

// 3) Consider the following example 
int v=5;
ap_1: assert property( x|-> ##2 b ##v c);  // illegal in 1800'2012

/* If the variable used to define the delay has values that are within a constraint
range, such as between 0 and 7 (or 15, or at most 32) one can use the generate statement, which appears much simpler than the use of local variables and the sequence_match_item. Example: */
generate for (genvar g_i=0; g_i<8; g_i++) begin
  ap_delay_gen: assert property (v==g_i && $rose(a) |-> ##g_i b);
end endgenerate 

// 4) When a parameter is used, the value is static (and does not change) after elaboration, prior to sim. 
                    

Ben SystemVerilog.us

In reply to ben@SystemVerilog.us:

(rose(a), v=delay+1'b1) |-> first_match((v>0, v=v-1'b1)[*0:] ##1 v==0) ##0 b == 1;

This worked.

In reply to sharadha:
I put a lot of thought into Mantis 5067 (for 1800’2018) where delays and repeat operators can use module variables as the value for the delays or repeat. I now believe that the best approach would be to specify something like the following:

  1. The range for the ​delay or ​repeat cannot be greater than 32, as specified by a bit vector of no more than 5 bits.
  2. The delay or repeat statement is in a sequence that is used as a property, and not as a sequence (e.g., no end points, no implication operator after the sequence).

Thus,


  bit[2:0] v=3;
  ap_delay: assert property( $rose(a) |-> d ##v b); 
// The compiler would automatically implement something like the following:
generate for (genvar g_i=0; g_i<8; g_i++) begin
      ap_delay_gen:  assert property ($rose(a) |-> d ##0 v==g_i |-> ##g_i b);    
end endgenerate   

The above approach is simple to implement, fits most application​s, and is more generic conceptually.
​The use of local variables is complex, but feasible. But the use of the generate statement is much easier to express and understand.
Ben Cohen http://www.systemverilog.us/

  • SystemVerilog Assertions Handbook, 3rd Edition, 2013
  • A Pragmatic Approach to VMM Adoption
  • Using PSL/SUGAR … 2nd Edition
  • Real Chip Design and Verification
  • Cmpt Design by Example
  • VHDL books

In reply to ben@SystemVerilog.us:

(rose(a), v=delay+1'b1) |-> (v>0, v=v-1'b1)[*0:] ##1 v==0 ##0 $rose(b);

I want to check b rose 6 cycle after a raises, and during 6 cycle b should be zero, should not toggle.
Please help me to implement this in assertion.

In reply to tirumalrao_m:

I want to check b rose 6 cycle after a raises, and during 6 cycle b should be zero, should not toggle.

Two solutions:

  1. fixed 6 cycles for rose(b)
  2. Delay-based on a variable
module m_rose; 
	bit clk, a, b; 
	bit[3:0] delay=6; 
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;   
	// I want to check b rose 6 cycle after a raises, 
        // and during 6 cycle b should be zero, should not toggle. 
	ap_ab: assert property(
			$rose(a) |=> !b[*5] ##1 $rose(b));  
	
	generate for (genvar g_i=0; g_i<16; g_i++) begin
	 if(g_i ==0)
                ap_delay_gen:  assert property ($rose(a) && g_i==delay
      		|=> !b[*g_i] ##1 $rose(b));  // same as |=> $rose(b)
	 else 
	 	ap_delay_gen:  assert property ($rose(a) && g_i==delay
      		|=> !b[*g_i-1'b1] ##1 $rose(b));    
        end endgenerate 

http://systemverilog.us/m_rose.sv with simple testbench

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

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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

In reply to ben@SystemVerilog.us:

Thank you, for your help.

I tried above thing but for me g_i is not fixed It will changes during run.
It depends on some other variable in the simulation and that variable changes based on setting.

In reply to tirumalrao_m:

In reply to ben@SystemVerilog.us:
I tried above thing but for me g_i is not fixed It will changes during run.
It depends on some other variable in the simulation and that variable changes based on setting.

You missed my main point on the generate. The following code generates 16 separate assertions: Thus, the variable can change value. Note that in eh antecedent I have
$rose(a) && g_i==delay, thus, if among those 16 assertions, the ones that don’t match the delay create vacuous assertions. The only one that matches and has a successful $rose fire.


generate for (genvar g_i=0; g_i<16; g_i++) begin
	 if(g_i ==0)
                ap_delay_gen:  assert property ($rose(a) && g_i==delay
      		|=> !b[*g_i] ##1 $rose(b));  // same as |=> $rose(b)
	 else 
	 	ap_delay_gen:  assert property ($rose(a) && g_i==delay
      		|=> !b[*g_i-1'b1] ##1 $rose(b));    
        end 
endgenerate 

Specifically, you would get



 genblock(0)ap_delay_gen:  assert property ($rose(a) && 0==delay
      		|=> !b[*0] ##1 $rose(b));  // same as |=> $rose(b)
 genblock(1)ap_delay_gen:  assert property ($rose(a) && 1==delay
      		|=> !b[*1-1'b1] ##1 $rose(b)); 
...
genblock(15)ap_delay_gen:  assert property ($rose(a) && 15==delay
      		|=> !b[*15-1'b1] ##1 $rose(b)); 

Here is the code and simulation results.

Code used for simulation

It looks like I could have done this instead, I don’t need the 0 case in this case. :


generate for (genvar g_i=1; g_i<16; g_i++) begin
	 ap_delay_gen:  assert property ($rose(a) && g_i==delay
      		|=> !b[*g_i-1'b1] ##1 $rose(b));    
        end 
endgenerate 

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

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448

In reply to ben@SystemVerilog.us:

Thank you, I think you are right, I Missed that condition in generator block.
I can use this.

But I Have around 102 to 203 clocks variable. this will generate around 203 assertion for single assertion.

In reply to tirumalrao_m:

The use of the generate is good for a small number of assertions.
You should be able to use a property with a local variable. Clarify your requirements and do a trial on a case. I’ll see if I can optimize it for you. Right now it is late for me, I can look at it in the morning.
Ben

In reply to ben@SystemVerilog.us:
If you don’t want to use the generate, you can do the following:


property p_delay; 
  int v; 
   ($rose(a), v=delay+1'b1) |-> 
     first_match((v>0 && !b, v=v-1'b1)[*0:$] ##1 v==0) ##0 $rose(b);
// New comment: No need for the first_match because of the v>0 test
//              Need of first_match() if we use the following instead 
//   first_match((!b, v=v-1'b1)[*0:$] ##1 v==0) ##0 $rose(b);
endproperty 
// You need the first_match() because without it, id no $rose(b) 
// the repeats keeps on counting forever. 

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

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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

In reply to ben@SystemVerilog.us:

I think this should work.
If first cycle value of b is zero, then b should have zero till end of count. at end it will check for rose of b.other wise assertion fails,(If I understood correctly)

correct me please.

In reply to tirumalrao_m:

Correct. Use my testbench model http://systemverilog.us/m_rose.sv (with the constrained-random tests (i.e., the randomized)) and verify that it is working as you think it should. You can modify the constraints to tune the testbench.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448

In reply to ben@SystemVerilog.us:

See my updated comment above on the use of first_match()

In reply to ben@SystemVerilog.us:

I tried to run that file as it is, it is not running as it needs uvm package.
I ma not using uvm, just system verilog for my env.
Let me try.

In reply to tirumalrao_m:
Try the following code: http://systemverilog.us/m_roseB.sv
You don’t need uvm; I just used it for the messaging. You can use $error.


module m_rose; 
	bit clk, a, b; 
	bit[3:0] delay=6; 
	int cycle=0;
	let VACUOUSOFF = 11; // assertion control type
	initial begin 
		$assertpasson(0); 
		$assertcontrol( VACUOUSOFF); //
	end
	always  @(posedge clk)  cycle <= cycle +1'b1; 
	
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;   
	// I want to check b rose 6 cycle after a raises, 
        // and during 6 cycle b should be zero, should not toggle. 
    property p_delay; 
     int v; 
     ($rose(a), v=delay+1'b1, $display("Cycle=%d, START, time=%t, DELAY= %d", cycle, $time, delay)) |-> 
      (v>0 && !b, v=v-1'b1)[*0:$] ##1 v==0 ##0 $rose(b);
    endproperty 
	ap_delay: assert property(p_delay) $display("Cycle=%d, PASS", $sampled(cycle));   
			else  $display("Cycle=%d, FAIL", $sampled(c

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

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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

In reply to ben@SystemVerilog.us:

ncsim: *E,MSSYSTF (./test_2.sv,8|14): User Defined system task or function ($assertpasson) registered during elaboration and used within the simulation has not been registered during simulation.
$assertcontrol( VACUOUSOFF); //
I am getting above error.

In reply to tirumalrao_m:
This forum’s emphasis in on language usage and purposely avoids addressing tool issues, as those should be addressed directly with the vendor.
On this particular note, my guess is that the simulator was commanded (or started) into an optimized mode versus a debug mode. You typically do not want to slow the simulator with lots of messages, particularly on PASSONs.
Ben Cohen
http://www.systemverilog.us/

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448

In reply to ben@SystemVerilog.us:

Hi ,

Thanks a lot for you solutions.
below code works for me.

property seq_a_b(a,sclk,b,delay);
int v,v2;
@(a or posedge sclk)
(rose(a), v=delay+1'b1) |-> (v>0 && !b, v=v-1'b1)[*0:] ##1 v==0 ##0 $rose(b);
endproperty : seq_a_b

Seems interesting topic. Is there any simple way to check signal pipeline variable delay. let’s consider 2 signals x1 and x2. Here x2 is delayed version on x1 and this delay is programmable with some variable. I don’t want to check value or state of x2 based on change on x1 because it may possible that x2 follows all transaction on x1 but there are also unexpected transaction x2 that are not there on x1 those transition also needs to be reported as error.