Regarding SVA properties

SystemVerilog
,
1

Hi,
I have a question regarding the below assertion property. what happens if the ##1 in line 5 is changes to ##0, i understand it is scheduled in the later region of the time stamp. But will the functional behavior be different?

Question 2:
what happens if the ##1 in Line 6 is changed to ##0? I am assuming the ##0 in line 6 would make the empty sequence match in same time stamp. But is there any behavior difference?


 property p_fifo_data_check;// Line1
 dataType data; // Line2
bit [0:$clog2(MAX_OUTSTANDING)] numAhead;// Line 3
 (start, data = dataIn, numAhead = outstanding)// Line 4
 ##1 (numAhead > 0 ##0 complete[->1], numAhead--)[*] //Line 5
 ##1 (numAhead == 0 ##0 complete[->1])// Line 6
 |-> // Line 7
 dataOut == data; // Line 8
 endproperty // Line 9
 a_fifo_data_check: assert property (p_fifo_data_check);// Line 10
2

I reformatted your property to something simpler to look at the construction, and its equivalent.


property p_fifo_data_check;// Line1
        int data; // Line2
        bit [0:2] numAhead;// Line 3
        ($rose(a), data = 3, numAhead = 2)// Line 4
        ##1 (numAhead > 0 ##2 1, numAhead--)[*] //Line 5
        ##1 (numAhead == 0 ##0 b[->1])// Line 6
             |-> // Line 7
                  data==3; // Line 8
    endproperty // Line 9
    a_fifo_data_check: assert property (p_fifo_data_check);// Line 10

    property p_fifo_data_check_eq;// Line1
        int data; // Line2
        bit [0:2] numAhead;// Line 3
        (($rose(a), data = 3, numAhead = 2)// Line 4
        ##1 (numAhead > 0 ##2 1, numAhead--)[*0] //Line 5
        ##1 (numAhead == 0 ##0 b[->1])) or 
// *******************************************************
        // 16.9.2.1 Repetition, concatenation, and empty matches
        // (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) `true).
// ******************************************************************************
        // Thus, above is same as 
        /* (($rose(a), data = 3, numAhead = 2)// Line 4
        ##0 1 //  (numAhead > 0 ##2 1, numAhead--)[*0] //Line 5
        ##1 (numAhead == 0 ##0 b[->1])) or  */ 
        // 
        (($rose(a), data = 3, numAhead = 2)// Line 4
        ##1 (numAhead > 0 ##2 1, numAhead--)[*1] //Line 5
        ##1 (numAhead == 0 ##0 b[->1])) or 
        //
        (($rose(a), data = 3, numAhead = 2)// Line 4
        ##1 (numAhead > 0 ##2 1, numAhead--)[*2] //Line 5
        ##1 (numAhead == 0 ##0 b[->1])) // or ... 
        // Line 6
             |-> // Line 7
                  data==3; // Line 8
    endproperty // Line 9
    a_fifo_data_check_eq: assert property (p_fifo_data_check_eq);// Line 10

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
…

  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:
3

In reply to ben@SystemVerilog.us:
One more note:
16.9.2.1 Repetition, concatenation, and empty matches
Using 0 as a sequence repetition number, an empty sequence (see 16.7) results, as in this example: a [*0]Because empty matches occur over an interval of zero clock ticks and are thus of length 0, they follow the set of concatenation rules specified below. In the following rules, an empty sequence is denoted as empty, and another sequence (which may be empty or nonempty) is denoted as seq.
— (empty ##0 seq) does not result in a match.
— (seq ##0 empty) does not result in a match.
— (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq).
— (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) true). For example, compare the following two sequences: a[*0] ##0 b true ##0 b
As defined by the preceding rules, the first sequence can never be matched: there is no point in time when the end point of the length-0 sequence a[*0] and the length-1 sequence ##0 b are aligned.
Now consider this example:
a ##1 b[*0] ##0 1 |-> 1
Look at it left-associatively, starting with “a ##1 b[*0]” standalone, rule 4 makes this equivalent to “a ##0 true”, which is a reasonable non-vacuous sequence.
Then the full sequence becomes “a ##0 true ##0 1”, which is the same as
“a ##0 1”.
Ben SystemVerilog.us

4

In reply to ben@SystemVerilog.us:


Ben,
May be i am still not getting the point, are you saying they both are equivalent?

property p_fifo_data_check;// Line1
 dataType data; // Line2
bit [0:$clog2(MAX_OUTSTANDING)] numAhead;// Line 3
 (start, data = dataIn, numAhead = outstanding)// Line 4
 **##1** (numAhead > 0 ##0 complete[->1], numAhead--)[*] //Line 5
 ##1 (numAhead == 0 ##0 complete[->1])// Line 6
 |-> // Line 7
 dataOut == data; // Line 8
 endproperty // Line 9
 a_fifo_data_check: assert property (p_fifo_data_check);// Line 10

equivalent to 

property p_fifo_data_check;// Line1
 dataType data; // Line2
bit [0:$clog2(MAX_OUTSTANDING)] numAhead;// Line 3
 (start, data = dataIn, numAhead = outstanding)// Line 4
 **##0** (numAhead > 0 ##0 complete[->1], numAhead--)[*] //Line 5
 ##1 (numAhead == 0 ##0 complete[->1])// Line 6
 |-> // Line 7
 dataOut == data; // Line 8
 endproperty // Line 9
 a_fifo_data_check: assert property (p_fifo_data_check);// Line 10
5

In reply to rag123:


property p_fifo_data_check;// Line1
  dataType data; // Line2
  bit [0:$clog2(MAX_OUTSTANDING)] numAhead;// Line 3
   (start, data = dataIn, numAhead = outstanding)// Line 4
   **##1** (numAhead > 0 ##0 complete[->1], numAhead--)[*] //Line 5
   ##1 (numAhead == 0 ##0 complete[->1])// Line 6
   |-> // Line 7
  dataOut == data; // Line 8
endproperty // Line 9

// Is equivalent to 
property p_fifo_data_check;// Line1
  dataType data; // Line2
  bit [0:$clog2(MAX_OUTSTANDING)] numAhead;// Line 3
   (start, data = dataIn, numAhead = outstanding)// Line 4
   // ##1 (numAhead > 0 ##0 complete[->1], numAhead--)[*0] //Line 5 is EMPTY, the [*0]
   ##0 (numAhead == 0 ##0 complete[->1])// Line 6, ##0 because is is ##{1-1)
// Because — (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq)
   or 
   (start, data = dataIn, numAhead = outstanding)// Line 4
   ##1 (numAhead > 0 ##0 complete[->1], numAhead--)[*1:$] //Line 5, [*]==[*0:$]
                                   // [*0] accounted above
   ##1 (numAhead == 0 ##0 complete[->1])// Line 6
   |-> // Line 7
  dataOut == data; // Line 8
endproperty // Line 9

Ben SystemVerilog.us

6

In reply to ben@SystemVerilog.us:

Thanks Ben :)