Clock Delay Range Operator issue in SVA

SystemVerilog
,
2

In reply to MayurKubavat:
From my SVA Handbook 4th Edition, 2016 ISBN 978-1518681448:
An assertion of a property that has an antecedent with an infinite range, and without a first_match operator, will never succeed, but can fail (a first_match ignores the other matches). Consider the following example that has the form of your assertion:

ap_never_succeed_multithreaded_and_not_unique: assert property( a ##[2:$] b |=> c);

An assertion started with a multi-threaded sequence has the following criteria for its outcome:
 All threads must be exercised in search of a matched antecedent /consequent pair, unless the assertion fails. In that case, the search is short-circuited (i.e., stopped).

  • The assertion is considered failed if there is a matched antecedent with a failed consequent.
     For the assertion to be successful, two requirements must be met:
  1. There must be no failure in the search of a matched antecedent with a consequent.
  2. All threads of the antecedent and consequent must be successful. There are two types of successes: vacuous and nonvacuous.
    a. VACUOUS SUCCESS:
    i. If all the threads of the antecedent result in a no match, then the assertion is considered vacuously true (also referred to as vacuous success, or simply vacuous).
    ii. Vacuity can also occur if a thread has a matched (i.e., true) antecedent but its consequent is vacuous (see 3.9 for discussion of vacuous properties).
    b. PASS / NON-VACUOUS: For a nonvacuous pass (or success), there must be at least one matched antecedent with its successful nonvacuous property, which represents the consequent. There must also be no failures in the consequent. Some threads may however be vacuous.

Bottom line: An antecedent with an infinite range (delay range or repetition range) will initiate an infinite number of threads. For the assertion to not fail, all threads of the antecedent and consequent must be evaluated. Since there are an infinite number of threads to be tested, the assertion can never successfully terminate. However, a failure of a matched antecedent / consequent pair will cause the assertion to fail.

There are cases where all threads in an antecedent must be tested. In your case, do the following:

ap_can_succeed_and_unique: assert property(
first_match($rose(a) ##[2:$] b) |=> c); // One choice. 
ap_can_succeed_and_unique2: assert property(
$rose(a) ##2 b[->1] |=> c); // Use the goto operator.

Another note: Consider using a $rose, as a general advice. Thus,


property prop_name(bit [23:0] ADDR_, int POS_);
      @(posedge HCLK) disable iff(!HRESETn)
         first_match( $rose((HTRANS == 2) && (HADDR == ADDR) && !HWRITE) ##1 // $rose needed ??
         !HREADYOUT[*0:16] ##1 (HRDATA[(( ADDR_    - (int' (ADDR_   /4)*4))*8) +: 8] == 8'h55) ##[0:$]
 
         (HTRANS == 2) && (HADDR == ADDR_ + 1) && !HWRITE ##1 
          !HREADYOUT[*0:16] ##1 (HRDATA[(((ADDR_+1) - (int'((ADDR_+1)/4)*4))*8) +: 8] == 8'hAA))
      |->
         ##[1:$] EndLockCheck ##0 Lock[POS_];
endproperty

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us