SVA repetetive condition

SystemVerilog
1

I have the following requirement when the sequence(SEQ) condition happens to look at signal during the simulation time. Following code check it once. How can check repetitively?


property x;
   @(posedge clk)
   (SEQ) |-> (signal);
endproperty
2

In reply to asvn:

"property x"is just a property declaration; it does absolutely nothing!
Do do something, you need the assertion of that property.


// for checks at all clocking events (all cycles)
ap_x: assert property(x);

// for check once
initial ap_x: assert property(x);

//  For check once after 10 clocks
initial begin
  repea(10) @(posedge clk);
  ap_x: assert property(x);
end

Ben systemverilog.us

3

In reply to ben@SystemVerilog.us:

Hi ben yes I called assert property but I want to check assertion result whenever the first condition(SEQ) happens without giving a defined number of time.

When the SEQ conditon happens and the signal is 1, assertion is passed and do not check it again when the same condition happens a time later.

4

In reply to ben@SystemVerilog.us:

In reply to asvn:
"property x"is just a property declaration; it does absolutely nothing!
Do do something, you need the assertion of that property.


// for checks at all clocking events (all cycles)
ap_x: assert property(x);
// for check once
initial ap_x: assert property(x);
//  For check once after 10 clocks
initial begin
repea(10) @(posedge clk);
ap_x: assert property(x);
end

Ben systemverilog.us

Hi Ben,

I used assert property. I want to check all the simulation time whenever the first condition happens.

For example;
Time 0 10 20 30 40 50
SEQ 0 1 0 1 1 0
signal 0 1 0 1 1 0

this assertion just check it only how can I check during the simulation time.

5

In reply to asvn:
Am not clear on the requirements. When you say
“check all the simulation time whenever the first condition happens”
Do you mean that once Seq happens then signal is always true at every clocking event?
If
So, use the always in SVA.

 
initial begin
 wait(Seq.triggered); // check of endpoint for sequence Seq
 ap_x : assert property (@(posedge clk) always signal);

You need to clarify your requirements, sorry, but I am not clear.
Look at the “always” or s_always construct.
Ben systemverilog.us

6

In reply to ben@SystemVerilog.us:

In reply to asvn:
Am not clear on the requirements. When you say
“check all the simulation time whenever the first condition happens”
Do you mean that once Seq happens then signal is always true at every clocking event?
If
So, use the always in SVA.

 
initial begin
wait(Seq.triggered); // check of endpoint for sequence Seq
ap_x : assert property (@(posedge clk) always signal);

You need to clarify your requirements, sorry, but I am not clear.
Look at the “always” or s_always construct.
Ben systemverilog.us

Hi Ben,

The sequence conditon happens more time so it can happen time 10, time 50 or time80. I want to check signal value whenvever sequence conditon happens like time 10, time 50 and time 80.

Time ------0------10------20-----50-----70-----80-------
SEQ ------0------OK------0------OK------0-----OK-------
SIGNAL ------0-------1------0-------1-------0-----1--------

In the above whenever SEQ happens OK, I want to check signal value.

7

In reply to asvn:

In reply to ben@SystemVerilog.us:
Hi Ben,
The sequence conditon happens more time so it can happen time 10, time 50 or time80. I want to check signal value whenvever sequence conditon happens like time 10, time 50 and time 80.
Time ------0------10------20-----50-----70-----80-------
SEQ ------0------OK------0------OK------0-----OK-------
SIGNAL ------0-------1------0-------1-------0-----1--------
In the above whenever SEQ happens OK, I want to check signal value.

I think this is what concurrent assertion does, when you put:


property x;
   @(posedge clk)
   (SEQ) |-> (signal);
endproperty
ap_x: assert property(x);
[\systemverilog]

It checks at every posedge clk, when SEQ is true, signal should be asserted. you can actually view it in the waveform.
8

In reply to David Liu:

The assertion you wrote does what you want.
@(posedge clk). (SEQ) |-> (signal);
At every clocking event thare is an attempt at Tha assertion, if the attempt succeeds, the thread continues until the end point of the Seq. If there is an endpoint {the sequence of the antecedent matches} then the consequent is tested.

What do you see wr?
Ben systemverilog.us

9

In reply to ben@SystemVerilog.us:

On your assertion “SEQ) |-> (signal);” you did not specify what your SEQ is and that matters.
This is particularly true for antecedents that are multiple threads. For example:


 a ##[1:10] b |-> c;
  1. In this case, that each attempt (i.e., at each clocking event) if a==1’b1, then “c” can only be true when all the threads of the sequence have been tested (11 cycles total) and for every thread where b==1, c must be equal to 1’b1.
  2. The threads of the antecedent include {a ##1 b) or {a ##2 b) or … ({a ##10 b)
  3. These overlaps of threads for multiple successful attempts can create confusion because the “b” and the “c” are seen by all the assertions that are in progress.
  4. An assertion of the form “a ##[1:$] b |-> c;” can never succeed since an infinite number of threads must be tested, and each of those threads must succeed truly of vacuously.

Ways to resolve these issues include:


$rose(a} ##1 b[->1] |-> c;  // preferred
     (a} ##1 b[->1] |-> c;  / if needed for every "a"
first_match($rose(a) ##[1:10] b) |-> c; // another option
// In the above case, multiple in-progress assertions can be terminated by a single occurenc of c==1. 
For example: if a==1 at cycles 1 and 3, and b==1 at cycle 6 then those two in-progress assertions will be terminated at cycle 6 with a pass or fail, depending on the value of "c"

For uniqueness on assertions see my answers and the following links in that link at
https://verificationacademy.com/forums/systemverilog/assertion-expected-data-check/review-users-question

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

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
10

In reply to ben@SystemVerilog.us:

In reply to David Liu:
The assertion you wrote does what you want.
@(posedge clk). (SEQ) |-> (signal);
At every clocking event thare is an attempt at Tha assertion, if the attempt succeeds, the thread continues until the end point of the Seq. If there is an endpoint {the sequence of the antecedent matches} then the consequent is tested.
What do you see wr?
Ben systemverilog.us

Hi Ben,
After thinking about it a second time, I am a little confused, please help me clarify
I am trying to achieve: whenever there is a SEQ, signal should follow the SEQ from the same cycle.( it might not be the original intent from the original author, but let’s say I just want to assert signal follows SEQ) For example(wave 1).

wave 1
SEQ |----------|__|----------------------------------|
signal|----------||----------------------------------|
clk |----------||----------||----------|_____

wave 2
SEQ |----------||-----------------------------|____________
signal__________|----------|_|----------|
clk |----------||----------||----------|

wave 1 is the behavior I want, at posedge of clk, when SEQ is 1, signal is 1. (I probably need another assert to say when SEQ=0 , signal is 0)

so by saying:

if the attempt succeeds, the thread continues until the end point of the Seq. If there is an endpoint {the sequence of the antecedent matches} then the consequent is tested

Do you mean, Seq is actually a sequence? so it might be a[1:10]b? Or it might be simply SEQ signal in my case? If that is the case, I think my understanding is here.

thanks

11

In reply to David Liu:

You need to look into what a sequence is, the timing for the sampling of signals, when an antecedent completes, what matching and no-matching means and its implications on properties.
There are several books (including mine) and free materials on sva.

Do some studying!
Ben systemverilog.us

12

In reply to ben@SystemVerilog.us:

Hi Ben,

Case 1 : -
I have two signals a and b. Now during a window frame when a is high , I need to check whether pulse b came or not only(IT SHOULD COME ONLY ONCE IN EVERY WINDOW) during this window frame.Also the window frame that is when a is high is variable also ,it needs to check every time.

Case 2 : - (Another case )
There is condition that n should come after 1 clock cycle of m has occured.But the catch is , the very first pulse of m needs to be ignored by the assertion logic ,and the next all pulses needs to be taken care of.

Thanks

13

In reply to pk_94:


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
  timeunit 1ns;     timeprecision 100ps;    
  bit clk, a, b, m, n;  
  /* Case 1 : -
Now during a window frame when a is high,
 check whether pulse b COMEs ONLY ONCE IN EVERY WINDOW.
Also the window frame that is when a is high is variable */
// sequence_expr ::=
// .. | sequence_expr within sequence_expr
//    | sequence_expr intersect sequence_expr
// NOTE: The "within" does not work because once a single occurrence of b 
//        (i.e., the b[->1]) happens inside the $fell(a)[->1], the 
//        consequent is satisfied.  Thus there could be other b's 
ap_b_within_a: assert property(@ (posedge clk)  // DO MOT USE THIS !!! 
                 $rose(a) |-> b[->1] within $fell(a)[->1]);  

// NOTE: The b[=1] is equivalent to !b[*0:$] ##1 b ##1!b[*0:$]
// Thus, we're looking for a single occurrence of "b insode the  $fell(a)[->1]
ap_b_in_a_frame: assert property(@ (posedge clk) 
                       $rose(a) |->   b[=1] intersect $fell(a)[->1]);

/*Case 2 : - (Another case )
n should come after 1 clock cycle of m has occurred.
The very first pulse of m needs to be ignored by the assertion logic. */ 
// Supporting logic eases this process 

initial begin
  while (m==0) begin
    @(posedge clk);
  end
  while (m==1) begin
    @(posedge clk);
  end

  forever @ (posedge clk) ap_m_n: assert property(@ (posedge clk) m |=> n);  
end


  //default clocking @(posedge clk); 
  //        endclocking
  initial forever #10 clk=!clk; 
  
  
  initial begin 
    bit va, vb, vn, vm; 
    repeat(200) begin 
      @(posedge clk);   
      if (!randomize(va, vb, vn, vm)  with 
      { va dist {1'b1:=4, 1'b0:=1};
      vb dist {1'b1:=1, 1'b0:=2};      
    }) `uvm_error("MYERR", "This is a randomize error")
    a <= va; 
    b <= vb;
    n <= vn;
    m <= vm;
  end 
  $stop; 
end 
endmodule

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

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
14

In reply to ben@SystemVerilog.us:

Thanks for the reply ben. Can you please explain the meaning of the following : -

                               $fell(a)[->1]

As $fell checks the dessertion of the signal from previous clock edge and current clock edge. But what the above expression is for ?

Thanks

15

In reply to pk_94:

Study the goto operator!


a[->1] // is same as: 
!a[*0:$] ##1 a

Study SVA if you intend to use it.
Ben Ben@systemverilog.us