System verilog assertion to check that signal 'a' takes a value only when it has taken some other particular value before

SystemVerilog
,
1

Hello,

  I wish to learn how can I write a system verilog assertion to check that :

For example :

signal ‘a’ takes a value '‘d2’ only when it has already had the value '‘d1’ anytime before, during the simulation.

Thanks in advance!

2

In reply to Saraswati:

I can easily spoonfeed you the answer, but it would be more beneficial for you if I explain the technique and then you do the research to write the code.

In SVA, within a declared property, you store the value of that signal in a local property variable. You then check in the consequent if within a region of cycles the signal value ==the local variable.
Ben systemverilog.us

3

In reply to ben@SystemVerilog.us:

Hi Ben,
I think you didn’t get my request correctly.
I will elaborate by giving an example :

signal = {0,1,3,8,9,2,…}

Now, I want to check that if this signal takes the value of 2, then, sometime before(no fixed time, so “0:$”) it has had the value of 1 as well.

/////////////////////
In your previous answer it isn’t clear to me as to how do you store the value of the signal (in this case 1) without using an ‘if condition’ ?

/////////////////////

Just on the side-lines, I used a checker to solve the problem :

/////////////////////
bit valid_signal = 'b0;

always @(*) begin
if (signal == 'd1)
begin
valid_signal = 'b1;
end

  if (signal == 'd2)
     begin
        ASSERT_RXOVER_MSG_AFTER_START_MSG: assert (valid_signal  == 'b1);
        
     end

end
/////////////////////

This works fine, but still I would like to know the alternative in SVA.

Thanks a lot!

4

In reply to Saraswati:

You need to write the assertion in a forward-looking manner, meaning that if some condition (a sequence)now then a future condition (a property or sequence) later. DO this instead of thinking of "if a condition now, then a previous condition must have occurred.


    bit clk, a, b; 
    int d1=1, d2=2;  
    // signal 'a' takes a value ''d2' only when it has already had the value 
    // ''d1' anytime before, during the simulation. 
    // Assertion wirtten in a more generic manner for the values of "a"
    // If you want specific values, you can use the "let"
    // let d1=1; let d2=2; // no not declare d1 and d1 as variables 
    ap_d1d2: assert property(@ (posedge clk)
             a==d1 |=> strong(##[1:$] a==d2));   
    // or the following 
    ap_d1d2_b: assert property(@ (posedge clk)
              a==d1 |=> strong(a==d2[->1]));

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
5

In reply to ben@SystemVerilog.us:

Hi Ben,
In the solution you provided, it takes the assumption that if a==d1 then eventually a==d2.
But what if a was never equal to d1, then the assertion will never be checked.

I feel like it can be solved by introducing a bit valid in the testbench and then set it to 1 whenever a==d1.

property p1;
@(posedge clk) (a==d2) |-> valid;
endproperty

Let me know if I am wrong somewhere.
Thanks,

6

In reply to devil47:
I think this is what you mean

 
bit latched_a; // latched when a==d1

property p1;
@(posedge clk) latched_a && (a==d2) |-> valid;
endproperty
7

In reply to ben@SystemVerilog.us:

In reply to devil47:
I think this is what you mean

 
bit latched_a; // latched when a==d1
property p1;
@(posedge clk) latched_a && (a==d2) |-> valid;
endproperty

Hi Ben,
I meant more along these lines. Because it may be possible that a==d1 never occurred.
So, when a==d2 occurs it should make sure that a==d1 occurred in the past.


bit latched_a; //latched when a==d1

property p1;
@(posedge clk) (a==d2) |-> latched_a;
endproperty
8

In reply to devil47:
That looks OK
Ben

9

In reply to ben@SystemVerilog.us:

In reply to Saraswati:
I can easily spoonfeed you the answer, but it would be more beneficial for you if I explain the technique and then you do the research to write the code.
In SVA, within a declared property, you store the value of that signal in a local property variable. You then check in the consequent if within a region of cycles the signal value ==the local variable.
Ben systemverilog.us

Hello Ben,

Please write such an example for me. I want to do exactly what you said, but I did not use until now neither if conditions in properties nor property local variables.

An example, if it is helpfull for you to understand my need: if a 1 bit signaled toggled (let’s say from low to high, but the level reached by signal can be kept into a variable), and its high value is steady high for 8 clock cycles, it MUST be steady high another 90 clock cycles.

If example above is not clear, I have another one: if a signal changed his value, it must be steady for 30 clock cycles in that value.

Whichever of two above examples you solve, it is very beneficial for me because you will initiate me in building such type of SV Assertions.

Thanks in advance.
Alexandru

10

In reply to alexandru_dinu:


module top;
  timeunit 1ns;  timeprecision 100ps;    
  `include "uvm_macros.svh"   import uvm_pkg::*;
  bit clk, c, d, reset_n=1'b1;
  int a, d2, d1; 
  // signal 'a' takes a value ''d2' only when it has already 
  // had the value ''d1' anytime before, during the simulation.
  // In other words, Once a new occurrence of a==d1 then sometime later 
  //  a==d2 with NO other a being equal to the stored value of d1. d1 is a one clock cycle duration.
  initial forever #10 clk = !clk;
  
  // @rose 0f a==d1, save d1. Starting from next cycle 'a' should not equal to that 
 // saved value until a==d2
  // Error flagged if a==stored value. 
  property p_a_is_d1_thend2; 
    bit[2:0] v; 
    @(posedge clk) disable iff(reset_n==0)  
      ($rose(a==d1), v=d1) |-> ##1  a!=v[*1:$] ##0 a==d2;  
  endproperty 
  ap_a_is_d1_thend2: assert property(p_a_is_d1_thend2);  

  // WITH ISSUES 
  // @rose 0f a==d1, save d1. Starting from next cycle 'a' should not equal to that 
 // saved value ANDed with a==d2
  // ISSUE: Error is NOT flagged if a==stored value before a==d2. 
  property p_HAS_ISSUES_a_is_d1_thend2; 
    bit[2:0] v; 
    @(posedge clk) disable iff(reset_n==0)  
      ($rose(a==d1), v=d1) |-> ##1  (a==d2 && a!=v)[->1]; 
  endproperty 
  ap_HAS_ISSUES_a_is_d1_thend2: assert property(p_HAS_ISSUES_a_is_d1_thend2);  

  /*  if c 1 bit signaled toggled (let's say from low to high, but the level reached by signal can be kept into a variable),
   and its high value is steady high for 8 clock cycles, it MUST be steady high another 90 clock cycles. */
   property p_c8_90; 
    bit[2:0] v; 
    @(posedge clk) disable iff(reset_n==0)  
      ($changed(c), v=c) ##1 c==v[*8] |->  ##1 c==v[*90];
  endproperty 
  ap_c8_90: assert property(p_c8_90);   
  

  initial begin
    repeat (200) begin
      @(posedge clk);
      if (!randomize(a, d1, d2, c) with {
        a  dist {1 := 1, 2 := 4, 3:= 4 };
        d1 dist {1 := 1, 2 := 2, 7:= 2 };
        d2 dist {5 := 1, 6 := 2, 7:= 2 };
        c  dist {1'b1 := 1, 1'b0 := 15 };
      })
        `uvm_error("MYERR", "This is a randomize error");
    end
    $finish;
  end
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
11

In reply to ben@SystemVerilog.us:

Thank you very much. Your complete two examples really put me on track in considering this type of SV Assertions.

Best regards,
Alexandru

12

In reply to alexandru_dinu:

Do read my paper
Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2

You’ll gain a lot of insights into SVA.