Need to Use Variable in Assertions ## Delay

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.

In reply to Digesh:

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.

You need to first clarify your requirements about the relationships between x1 and x2.

  1. x2 always follows x1 // Normal behavior
  2. 2 occurrences of x2 after x1 // Error behavior
  3. Other relationships

Once this is done, you can easily write assertions. Understand your requirements!
:)
Ben Cohen SystemVerilog.us

In reply to ben@SystemVerilog.us:

In reply to Digesh:
You need to first clarify your requirements about the relationships between x1 and x2.

  1. x2 always follows x1 // Normal behavior
  2. 2 occurrences of x2 after x1 // Error behavior
  3. Other relationships

Once this is done, you can easily write assertions. Understand your requirements!
:)
Ben Cohen SystemVerilog.us

x2 always follows x1 is normal condition. 2 transition on x1 before they reach x2 is also normal condition in such condition you should expect same 2 transition on x2. Now if you think of error behavior it can be like you said 2 occurrences of x2 after x1 other error condition I think of are :

  1. transition on x2 only
  2. transition on x1 only
  3. n number of transition on x1 but m transition on x2 where (m !== n)

Please let me know if you are having hard time understanding my point. I can draw some diagram that way you it will be easy for you to understand me.

In reply to Digesh:

In reply to ben@SystemVerilog.us:
x2 always follows x1 is normal condition. 2 transition on x1 before they reach x2 is also normal condition in such condition you should expect same 2 transition on x2. Now if you think of error behavior it can be like you said 2 occurrences of x2 after x1 other error condition I think of are :

  1. transition on x2 only
  2. transition on x1 only
  3. n number of transition on x1 but m transition on x2 where (m !== n)

I’ll give you guidelines in writing the needed assertions.

  1. FOR “2 transition on x1 before they reach x2 is also normal condition in such condition you should expect same 2 transition on x2”, see my solution with the use of ticket, now_serving.
    Counting number of events on clock a, while clock o is forbidden - SystemVerilog - Verification Academy
  2. FOR “n number of transition on x1 but m transition on x2 where (m !== n)”, you can use the module variables int ticket, now_serving as the difference should be zero at the end of simulation, or at times determined by you.
  3. FOR “2 occurrences of x2 after x1 // Error behavior”. Use something like
    rose(x1) |-> strong(x2[->1] ##1 !x2[*0:] ##1 $rose(x1));
    BTW, this is in conflict with your first requirement “2 transition on x1 before they reach x2”

Ben Cohen

In reply to ben@SystemVerilog.us:

In reply to Digesh:
I’ll give you guidelines in writing the needed assertions.

  1. FOR “2 transition on x1 before they reach x2 is also normal condition in such condition you should expect same 2 transition on x2”, see my solution with the use of ticket, now_serving.
    Counting number of events on clock a, while clock o is forbidden - SystemVerilog - Verification Academy
  2. FOR “n number of transition on x1 but m transition on x2 where (m !== n)”, you can use the module variables int ticket, now_serving as the difference should be zero at the end of simulation, or at times determined by you.
  3. FOR “2 occurrences of x2 after x1 // Error behavior”. Use something like
    rose(x1) |-> strong(x2[->1] ##1 !x2[*0:] ##1 $rose(x1));
    BTW, this is in conflict with your first requirement “2 transition on x1 before they reach x2”

Ben Cohen

Hi Ben ,
Thanks for reply I have already implemented this check as per below.

property pipe_dly_chk(clk,rst,variable,signal1,signal2);
int v_b;
@(clk) disable iff(rst)
if(variable == 0)
(($changed(signal1))|-> (signal2 == signal1))
else
(($changed(signal1), v_b=signal1) |->(pipe_dly_seq(variable,1)) |-> (signal2 == v_b ));
endproperty : pipe_dly_chk

sequence pipe_dly_seq(max_count, expr);
integer count;
(expr,count = max_count) ##0 (count > 0,count = count - 1)[*0:$] ##1 (count == 0);
endsequence :pipe_dly_seq

DELAY_CHK : assert property (pipe_dly_chk(clk,enable_condition,(2 * delay_depth_in_terms_of_clk),signal1,signal2))
else
error_msg

always @(signal1)begin
sig1_cnt = sig1_cnt + 1;
end

always @(signal2)begin
sig2_cnt = sig2_cnt + 1;
end

final begin
if(enable_condition)begin
CNT_CHK: assert (sig1_cnt == sig2_cnt) else $display(“sig1_cnt:%d and sig2_cnt:%d count mismatch”,sig1_cnt,sig2_cnt);
end
end

Let me know if you think of any better solution than this.

In reply to Digesh:

You need to build a testbench for the assertions and see if it meets your requirements.
As you may have noticed, I typically use the randomize with weighted distributions to generate the test signals. For example:


import uvm_pkg::*; `include "uvm_macros.svh" 
module m; 
	bit clk, a, din;  
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;   

 initial begin 
     repeat(200) begin 
       @(posedge clk);   
       if (!randomize(a, din)  with 
           { a dist {1'b1:=1, 1'b0:=3};
             din dist {1'b1:=1, 1'b0:=2};

           }) `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
endmodule  

In my 4th edition of the SVA book, I have a chapter thta addresses building a testbench for assertions, and explain the use of typical constraints.

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

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

What if the requirement is to pass a range of delay as input variables? For example in the following assertion
$rose (sigA) |-> ##[min_cycle_response:max_cycle_response] ($fell(sigB)) ;

passing delay as parameters from the module seem to work. Is there another way or are there any disadvantage using parameter instead of input ?

Example:
module event_sigA_assertion #(parameter int min_cycle_response=0,max_cycle_response=0 )
(
input ref_clk,
input assert_enable,
input sigA,
input sigB
);
property p_event_clear_reset_assert;
@(posedge ref_clk)
disable iff (!assert_enable)
$rose (sigA) |-> ##[min_cycle_response:max_cycle_response] ($fell(sigB)) ;
endproperty
endmodule

If the 2 ranges (min and max) are small, you can use the generate with 2 loops that will create multiple assertions. You can also use a property with local variables; that can be tricky, but the following looks OK to me.


import uvm_pkg::*; `include "uvm_macros.svh" 
module m5067; 
	parameter N=0;  // <--- Parameter, used for testing a simple assertion 
	bit clk, a, b, c; 
	bit[2:0] v=3, v0=0, v1=3;
	default clocking @(posedge clk); endclocking
    initial forever #10 clk=!clk;     

 
    // ap_range: assert property($rose(a) |-> ##[v0:v1] b); // WANT
     ap_range_fix: assert property($rose(a) |-> ##[N:3] b); // Simple, fixd range 
     property p_range_equivalent; // Equivalent implementation
                                  // Range defined by module variables v0 and v1
      int lv0, lv1; // this is an internal local variable defined by the tool 
       ($rose(a), lv0=v0, lv1=v1 )
          |->  
      	    ##0 first_match((1'b1, lv0=lv0-1'b1, lv1=lv1- 1'b1) [*0:$] ##1 lv0<=0)
            ##0 first_match( (1, lv1=lv1- 1'b1)[*0:$] ##1  (b || lv1<=0))
			##0 b;
     endproperty
     ap_range_equivalent: assert property(p_range_equivalent); 
    
  initial begin // Testing of assertions 
     repeat(200) begin 
       @(posedge clk);   
       #1 if (!randomize(a, b, c)  with 
           { a dist {1'b1:=1, 1'b0:=5};
       		 b dist {1'b1:=10, 1'b0:=4};
       		 c dist {1'b1:=3, 1'b0:=1};})
       	          `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
endmodule 

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

  • SVA 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:

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

Hello Ben,

I am a big fan of you. Your way of solving problems via SVA is amazing. I have a question:
If the variable delay can be achieved by passing parameters then why do we need to do this lengthy workaround?

I’ll be looking forward to your humble response.

Thank you,

Regards,
Muneeb Ulla Shariff

In reply to muneebullashariff:
Parameters work because they are static after elaboration.
I am not trying to stop you from asking questions, but one good advice that was given to me was to test certain theories or problems to better understand the legality of code.
You your specific question on parameters, see my example at

Thanks for being a “fan”
:)
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us


In reply to ben@SystemVerilog.us:

In reply to muneebullashariff:
Parameters work because they are static after elaboration.
I am not trying to stop you from asking questions, but one good advice that was given to me was to test certain theories or problems to better understand the legality of code.
You your specific question on parameters, see my example at
Edit code - EDA Playground
Thanks for being a “fan”
:)
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us


Hey Ben,

Many thanks for your reply. I ran the code on edaplayground and got a good feel of the problem. However, I do have a question:

In what scenarios do we need to use parameterized delays and when do we need to use this variable delay (workaround)?

Thank you,

Regards,
Muneeb Ulla Shariff

In reply to muneebullashariff:

In what scenarios do we need to use parameterized delays and when do we need to use this variable delay (workaround)?

  1. Parameterized delays or repeat operators are typically used when configurations or modes can change prior to a simulation run, but are stable (no change) during the simulation. Modes can be things like low/hi power mode (affects response times), Design A vs Design B (e.g., fast or slow multiplier or IP), interface spec changes (may affect when expected information is received).
  2. Dynamic variable that define delays, though not often used, can be used as a substitute for parameterized delays when within a simulation run one may want to test different configurations or modes. Another example may be when the testbench informs the test interface the length of a message; this is done as a setup prior to the transmission or receipt of the message. The assertion can then may use of the value of that variable to adjust for the verification process.

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


In reply to ben@SystemVerilog.us:

Is it possible to use a variable along with $past construct ?

property sig_high_check;
int high_value;
@(posedge clk)
($rose(signal_b), high_value = signal_a_reg) |-> $past($rose(signal_a),high_value);
endproperty

Throws error - variable can’t use along with $past.

In reply to princedavidt:

In reply to ben@SystemVerilog.us:
Is it possible to use a variable along with $past construct ?
property sig_high_check;
int high_value;
@(posedge clk)
($rose(signal_b), high_value = signal_a_reg) |-> $past($rose(signal_a),high_value);
endproperty
Throws error - variable can’t use along with $past.

The issue is not the $past, but your syntax in the use of the $past.
The syntax of the function is: [1]
$past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])
More explanation from my SVA Handbook 4th Edition

Here is what I believe you wanted to express:



import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    timeunit 1ns;     timeprecision 100ps;  
	bit clk, a, b, e;  
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;  
  property p; 
    bit d;
    ($rose(a), d=b) |-> $past($rose(b)) ##0 d==e;  
  endproperty 
  ap: assert property(p);                         

 initial begin 
     repeat(20) begin 
       @(posedge clk);   
       if (!randomize(a, b, e)  with 
           { a dist {1'b1:=1, 1'b0:=3};
             b dist {1'b1:=1, 1'b0:=2};

           }) `uvm_error("MYERR", "This is a randomize error")
       end 
       $stop; 
    end 
endmodule   

You can simulate this at Edit code - EDA Playground

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


In reply to ben@SystemVerilog.us:

Hi Ben,

Thank you for your response.

  1. What is the varible e ? why it’s used in your code

Few clarifications

  1. sig_a ( 1 bit) is input, sig_b ( 1 bit) is output when ever there is change in sig_b,(rise or fall) sig_a should have risen or fell, before the programmed number of cycles. Mentioned only positive case above.

  2. Valiable delay ( programmed numbebr of cycles) is bit [7:0] for both rise duration and fall duration for sig_a

Confused on the implementation as per the syntax mentioned in

($rose(a), d= delay) |=> $past (a==b, d,1,@(rose(b))); // Is the correct usage
or
($rose (b), d= delay ) |=> $past(a==b, d, 1 , @(rose(b)));

Expression 1 checks a==b, before d cycles, 1 is enable condition, @ clocking event , which is rise of signal b.

~Thanks
pdt

I misinterpreted your requirements.
Getting back to your code:

($rose(a), d= delay) |=> $past (a==b, d,1,@(rose(b))); // Is the correct usage

That is the ICORRECT usage of $past because the # of ticks must be static, Youe have it as “d”, which is a variable and is dynamic, known at runtime, not elaboration time.
Per spec, and explained in my book http://systemverilog.us/vf/svabk4_past.pdf

The syntax of the function is: [1]
$past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])
expression1 represents the expression being sought.
The three optional arguments define the following:
expression1 and expression2 can be any expression allowed in assertions.
number_of_ticks specifies the number of clock ticks in the past. number_of_ticks must be one or greater, and must be static (i.e., known at elaboration time). If number_of_ticks is not specified, then it defaults to 1. If the specified clock tick in the past is before the start of simulation, the returned value from the $past function is a value of X

As a guideline, it is best to write assertions that go forward, meaning
antecedent |-> present_or_future_expectations
instead of
antecedent |-> some_past_occurences

Hopefully, you also read my paper that explains the engine behind SVA. You should be able to write the assertions using a task.
PAPER: Understanding the SVA Engine + Simple alternate solutions - SystemVerilog - Verification Academy
Abstract: Understanding the engine behind SVA provides not only a better appreciation and limitations of SVA, but in some situations provide features that cannot be simply implemented with the current definition of SVA. This paper first explains, by example, how a relatively simple assertion example can be written without SVA with the use of SystemVerilog tasks; this provides the basis for understanding the concepts of multithreading and exit of threads upon a condition, such as an error in the assertion. The paper then provides examples that uses computational variables within threads; those variables can cause, in some cases, errors in SVA. The strictly emulation model with tasks solves this issue.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


In reply to ben@SystemVerilog.us:

hi,
I have used your above suggested code to delay using particular variable, but i am facing an issue like my assertion is getting active second time immediately where I’m not expecting and remain in active state only. Please find below code . Thanks in advance.

property to_dly_p7;
int count_p7;
@(posedge clk32r20 )
disable iff (!rst32kn)
((apcState == LD_PLL_DLY), count_p7=(reg_t_pll_delay*10)+1’b1) |=> (1, count_p7=count_p7-1’b1)[*0:$] ##1 count_p7==0 ##1 ((apcState == LD_TO_DLY) and op_signals_to_dly_p7);
endproperty
assert property ( to_dly_p7 );

The above assertion is getting active (apcState == LD_TO_DLY) at this state not remain in active.

In reply to naga vardhini:

  1. ) SVA easy solutions for dynamic range delays and dynamic repeat delays.
    Dynamic range delays and dynamic repeat delays.in SVA are complex to solve. An interesting simple response using a package was provided at
    SVA: Package for dynamic and range delays and repeats | Verification Academy

  2. use above solution. However on your code you need a first_match
    Antecedent |->
    first_match((1, count_p7=count_p7-1’b1)[*0:$] ##1 count_p7==0)
    ##1 ((apcState == LD_TO_DLY) and op_signals_to_dly_p7);
    Ben systemverilog.us