SV assertion for verifying a sequence of events not working

SystemVerilog
2

In reply to Adarsh24:


// An assertion of the form 
    // seq |-> expr1 ## [1:$] seq2 
    // can only fail if expr1 is false.  <<<**********
    // If expr1==1 then there are an infinite number of possibilities 
    // for seq2 to be true. 
      seq |-> expr1 ## [1:$] seq2  // is equivalent to 
      seq |-> expr1 ##1 seq2 or
              expr1 ##2 seq2 or  
              ...
              expr1 ##n seq2; // n= $ 

    // The difference between something like 
            ##1  !c[->1]
            ##1  (reg2[17:1] == 17'h00000) [->1]
            ##1  (reg2[17:1] == 17'h1FFFF) [->1]
     // and this 
            ##[1:$] (!c) 
            ##[1:$] (reg2[17:1] == 17'h00000) 
            ##[1:$] (reg2[17:1] == 17'h1FFFF) 
    // is that with the goto operator, when 
            (!c)  // occurs
    // no other occurrences of !c is further tested. 
    // For example, the following 3 sequences are possibilities
            ##2 (!c) 
            ##4 (reg2[17:1] == 17'h00000) 
            ##6 (reg2[17:1] == 17'h1FFFF) 
    // or ..
            ##3 (!c) 
            ##5 (reg2[17:1] == 17'h00000) 
            ##6 (reg2[17:1] == 17'h1FFFF)
    // In essence, the use of the goto operator it is equivalent to 
            first_match(##[1:$] (!c))
            ##0 first_match(##[1:$] (reg2[17:1] == 17'h00000))
            ##0 first_match(##[1:$] (reg2[17:1] == 17'h1FFFF))
/////////////////////
// Taking the path out, I would write it as 
property example1;
        disable iff (!(testmode))
        @(posedge clk) (a && b) |-> (1, $display ("Checking SEQ1"))
            ##0 (c && (reg1[16:0] == 17'h0000F)) 
            ##1  !c[->1]
            ##1  (reg2[17:1] == 17'h00000) [->1]
            ##1  (reg2[17:1] == 17'h1FFFF) [->1]
            ##1  c[->1];
    endproperty

// BTW, you have too many ()s.  Use expr instead (expr) 
// You may also want to use the "let" on the path.  Thus,
let path=TB.TOP;
path.!c ##1 path.reg2

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) https://rb.gy/cwy7nb
  3. Papers: