Assertion Disabling for specific time and reenable it

Hi,

I need help in the following scenario in writing assertion
From event “sig1”, i am checking sig1 and sig2 should be equal in 6 clock cycles. Within the 6 clock cycles “dis” signal is triggered high.
The check should be disabled when “dis” is high and when “dis” goes low the check should proceed where it left.

For example :
Event “sig1” happened at 1st cycle
“dis” signal is high at 3rd cycle and high for 2 clock cycles. – The check should be disabled only for 3 and 4th clock cycle
“dis” signal low at 5ht cycle – Once disable went low the check has to resume checking

I wrote below property which is disabling when dis is high.
property p1(sig1,sig2,dis)
@(posedge clk) disable iff(dis)
$rose(sig1) |-> ##[1:6] sig1==sig2 ;
endproperty

In reply to ashokgupta466:
UPDATEDThe requirements upon a rose(sig1) within 6 cycles where dis==0 sig1==sig2.
Basically, the 6 cycles are only those cycles where dis==0; if dis==1, the cycles are not counted, and the comparison is not made.
I started the model with a tas that is forked at every cycle. See my paper on understanding the SVA model, link below.
I then converted the task into a function where the property local variable is a struct, and I pass that struct to the function. The function updates the property local variable.
I fixed the bug that I reported earlier.

 

module top;
  timeunit 1ns;  timeprecision 100ps;    
  `include "uvm_macros.svh"   import uvm_pkg::*;
  bit clk, sig1, sig2, dis, reset_n=1; 
  int thecycle; 
  typedef struct {int count; bit s1; bit s2; bit pass; bit dis;} str_type; 
  event e1, e2; // for debug
  initial forever #10 clk = !clk;
  initial $timeformat(-9, 0, " ns", 10); 

  task automatic t();
    int count=1, cycles=0; 
    realtime start;
    bit pass;
    -> e1; 
    cycles=0; start=$realtime; // for debug 
    while (count <=6) begin  : while1
      cycles+=1; // keep track on the number of cycles for statistical purposes
      if(dis==0 && sig1==sig2) begin : if1 // pass 
        pass=1;
        break; 
      end : if1
      else begin : else1
        if(dis==0) count =count +1; 
        @(posedge clk); // keep cycling, no tests
      end : else1
    end : while1
    am_sig1sig2_pass2: assert(pass) $display("%t PASS start %t count=%d cycles=%d thecycle %d", $realtime, start, count, cycles, thecycle);
                           else $display("%t ******* FAIL *******  start %t count=%d cycles=%d thecycle %d", $realtime, start, count, cycles, thecycle);
    -> e2; 
  endtask 
  always @(posedge clk) 
     if($rose(sig1)) fork
      t();
     join_none 
 
  
  function str_type f(str_type d); // int count; bit s1; bit s2; bit pass; bit dis} str_type;  
      if(d.count <=6 && d.dis==0 && d.s1==d.s2) begin : if1 // pass 
        d.pass=1; 
        d.count+=1; 
      end : if1
      else begin : else1
        if(dis==0) d.count =d.count +1; 
      end : else1 
      return d; 
  endfunction

  property p1;  // int count; bit s1; bit s2; bit pass; bit dis} str_typ
    str_type v;
    @(posedge clk) disable iff(reset_n==0) 
    $rose(sig1) |-> 
      first_match((1, v.s1=sig1, v.s2=sig2, v.dis=dis, v.pass=0, v=f(v))[*1:$] ##0 v.count==7 || v.pass) ##0 v.pass;  
  endproperty  
   ap: assert property(p1);  

  initial begin
    bit vsig1, vsig2, vdis; 
    repeat (300) begin
      @(posedge clk);
      thecycle <= thecycle +1; 
      if (!randomize(vsig1, vsig2, vdis) with {
        vsig1  dist {1'b1 := 3, 1'b0 := 1};
        vsig2  dist {1'b1 := 1, 1'b0 := 3};
        vdis   dist {1'b1 := 3, 1'b0 := 1};
      }) `uvm_error("MYERR", "This is a randomize error");
      sig1 <= vsig1; sig2 <= vsig2; dis <= vdis; 
    end
  end
endmodule
 


 ** Error: Assertion error.
#    Time: 2970 ns Started: 2470 ns  Scope: top.ap File: s1s2dis.sv Line: 56 Expr: v.pass
#    Local vars : v = '{count:6, s1:0, s2:0, pass:0, dis:1}
#    2990 ns PASS start    2470 ns count=          6 cycles=         27 thecycle         149

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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 - SystemVerilog - Verification Academy
  2. Free books: * Component Design by Example https://rb.gy/9tcbhl
  1. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

In reply to ben@SystemVerilog.us:
A much simpler solution by my co-autho Srini,
Thnks Srini!


ap_simpler: assert property(@(posedge clk)  $rose(sig1) |-> 
                                    !dis && sig1==sig2 within !dis[->6]);

In reply to ben@SystemVerilog.us:

Hi Ben,

This solution has worked, Thanks a lot…

In reply to ashokgupta466:
An interesting comment from a colleague:
If the interpretation of the requirements are:

  1. After rising sig1 within 6 cycles where dis==0 then sig1==sig2.

ap_simpler: assert property(@(posedge clk)  $rose(sig1) |->
                                    !dis && sig1==sig2 within !dis[->6]);
// would succeed if !dis && sig1==sig2 happened only once. 

However,
2) After rising sig1 within 6 cycles where and when dis==0 then sig1==sig2
(i.e., sig1==sig2 in all 6 cases when dis ==0)


$rose(sig1) ##0 (dis==0)[->1:6] |-> sig1==sig2

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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
  1. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/