$past in Systemverilog Assertions

SystemVerilog
, ,
1

Need to implement an assertion: If data_rd rose and (data[3:0] !=7) then 160 cycles before data[3:0] should have been 7

Implemented:

assert property (@(posedge clk) disable iff(rst) ($rose(data_rd) && (data[3:0] !=7)) |-> $past((data[3:0]==7),160));

Assertion got triggered for the first rise and non-7 data and passed successfully, but never got triggered later even though there were lot of non-7 data and all those were preceded by 7, 160cycles before.
Any idea why is this happening?

2

In reply to Tobi:

Each attempt is separate from others.
What I see wrong is that from time 0, $past(d, n) where n < 161 is the default value of d.
2 solutions:


// better
always @(posedge clk count <= count + 1'b1;

assert property (@(posedge clk) disable iff(rst) 
count > 160 ##0 ($rose(data_rd) && (data[3:0] !=7)) |-> $past((data[3:0]==7),160));


// Too many nonvacuous attempts 
assert property (@(posedge clk) disable iff(rst) 
##161 ($rose(data_rd) && (data[3:0] !=7)) |-> $past((data[3:0]==7),160));

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

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
  • 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
  • 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

See Paper: 1) VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
2) http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf

3

In reply to ben@SystemVerilog.us:

Thanks for the reply. I tried your solution but couldn’t detect any change.

I am not sure if that is the problem, because data_rd is a one cycle pulse. Also it arrives once every 160 cycles. So I am expecting it to trigger only once every 160 cycles.

waveform is like :
cycle:0: first data_rd pulse, data = 7
cycle:160: second data_rd pulse, data = 15 → assertion success
cycle:320: third data_rd pulse, data = 7
cycle:480: fourth data_rd pulse, data = 8 → no sign of assertion trigger

Also there was a failure case in between and assertion shown failed.
Assertion detects every failure but is not showing every success in waveform. Am I missing any detail about the $past construct? Did I miss something from your reply?

4

In reply to Tobi:
There is nothing wrong with your code.
The issue may be that the antecedent is never retriggered. Below is a test of your code with debug features added. Try this model with your simulator.


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    timeunit 1ns;     timeprecision 100ps;    
    bit clk, a, b, data_rd, rst=0;  
    bit[3:0]  data; 
    int count; 
    event e160, e_attempt; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    always  @(posedge clk)  begin 
        count <= count + 1'b1;
        if (count==160) -> e160;
    end 
    function void attempt();
      -> e_attempt;
    endfunction
    
    ap160: assert property (@(posedge clk) disable iff(rst) 
    count > 160 ##0 ($rose(data_rd) && (data[3:0] !=7), attempt())
                              |-> $past((data[3:0]==7),160)) 
              $display("PASS at cycle %d past(data[3:0])=%b",
                    $realtime, $sampled($past(data[3:0], 160)));
    
    
    initial begin 
        bit va, vb; 
        repeat(500) begin 
            @(posedge clk);   
            if (!randomize(data_rd, data)  with 
            { data_rd dist {1'b1:=1, 1'b0:=3};
              data dist {4:=1, 5:=2, 6:=1, 7:=4};      
        }) `uvm_error("MYERR", "This is a randomize error")
        a <= va; 
        b <= vb;
    end 
    $stop; 
end 
endmodule   

 ** Error: Assertion error.
#    Time: 3270 ns Started: 3270 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# PASS at cycle       3450 past(data[3:0])=0111
# ** Error: Assertion error.
#    Time: 3530 ns Started: 3530 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# PASS at cycle       3630 past(data[3:0])=0111
# PASS at cycle       3750 past(data[3:0])=0111
# ** Error: Assertion error.
#    Time: 3990 ns Started: 3990 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# ** Error: Assertion error.
#    Time: 4310 ns Started: 4310 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# PASS at cycle       4690 past(data[3:0])=0111
# ** Error: Assertion error.
#    Time: 4790 ns Started: 4790 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# ** Error: Assertion error.
#    Time: 4990 ns Started: 4990 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# PASS at cycle       5190 past(data[3:0])=0111
# PASS at cycle       5310 past(data[3:0])=0111
# PASS at cycle       5390 past(data[3:0])=0111
# ** Error: Assertion error.
#    Time: 5510 ns Started: 5510 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# PASS at cycle       5610 past(data[3:0])=0111
# ** Error: Assertion error.
#    Time: 5790 ns Started: 5790 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# ** Error: Assertion error.
#    Time: 5930 ns Started: 5930 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# PASS at cycle       6030 past(data[3:0])=0111
# ** Error: Assertion error.
#    Time: 6070 ns Started: 6070 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# PASS at cycle       6370 past(data[3:0])=0111
# PASS at cycle       6570 past(data[3:0])=0111
# ** Error: Assertion error.
#    Time: 6630 ns Started: 6630 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# ** Error: Assertion error.
#    Time: 6830 ns Started: 6830 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# PASS at cycle       7150 past(data[3:0])=0111
# ** Error: Assertion error.
#    Time: 7190 ns Started: 7190 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# ** Error: Assertion error.
#    Time: 7330 ns Started: 7330 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# PASS at cycle       7450 past(data[3:0])=0111
# ** Error: Assertion error.
#    Time: 7650 ns Started: 7650 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)
# PASS at cycle       7830 past(data[3:0])=0111
# ** Error: Assertion error.
#    Time: 7910 ns Started: 7910 ns  Scope: top.ap160 File: C:/ben_play/./past160.sv Line: 20 Expr: $past(data[3:0]==7,160)

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

See Paper: 1) VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
2) http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf

5

In reply to ben@SystemVerilog.us:

Replace $realtime with count.
I initially meant to put the time for the pass, but thought count would be more expressive.
But then did not correct the $display.
Ben