Clock Delay Range Operator issue in SVA

SystemVerilog
,
1

Hi,

I’m writing an SystemVerilog assertion where I need to use indefinite cycles for a event to happen. But, clock delay range operator gives me issue when used with $. See below snippet,

//This works fine(pass/fail happens)!
//As the delay between two reads vary, I need to use indefinite delay (using $) but
//as it does not work, I've been using 500 cycles assuming events will occure
//within this range.
property prop_name(bit [23:0] ADDR_, int POS_);
      @(posedge HCLK) disable iff(!HRESETn)

         (HTRANS == 2) && (HADDR == ADDR_    ) && !HWRITE ##1 
         !HREADYOUT[*0:16] ##1 (HRDATA[(( ADDR_    - (int' (ADDR_   /4)*4))*8) +: 8] == 8'h55) ##[0:500]

         (HTRANS == 2) && (HADDR == ADDR_ + 1) && !HWRITE ##1 
          !HREADYOUT[*0:16] ##1 (HRDATA[(((ADDR_+1) - (int'((ADDR_+1)/4)*4))*8) +: 8] == 8'hAA)
      |->
         ##[1:500] EndLockCheck ##0 Lock[POS_];
endproperty

//But this does not work
//This assertion gets activated but never passes/fails
property prop_name(bit [23:0] ADDR_, int POS_);
      @(posedge HCLK) disable iff(!HRESETn)

         (HTRANS == 2) && (HADDR == ADDR_    ) && !HWRITE ##1 
         !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
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

3

In reply to ben@SystemVerilog.us:

Hi Ben Cohen,

Thanks for the reply.

I’ve tried above suggestions, I still do not get pass/fail status for checks.

//Tried this. Does not give pass/fail satus
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

From your explanation, I know that this is a multi-threaded sequence, but in my simulation, I have only one reads on these AHB addresses, eliminating possibility of starting multi-thread in a property.

Also, consequent signal EndLockCheck goes high after few/200 cycles(That is why I’m using delay of 500 cycles in general). With these hard-coded cycle delays assertion either passes/fails, which is what I need. But when I replace 500 with $ in above checks, SVA does not give any results.

Any other explanation on why checks I wrote should not work might be useful.

4

In reply to MayurKubavat:

In reply to ben@SystemVerilog.us:
I’ve tried above suggestions, I still do not get pass/fail status for checks.

//Tried this. Does not give pass/fail satus
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

From your explanation, I know that this is a multi-threaded sequence, but in my simulation, I have only one reads on these AHB addresses, eliminating possibility of starting multi-thread in a property.

[Ben] Let me simplify your code using the “let” statement. What you have is


let a= $rose((HTRANS == 2) && (HADDR == ADDR) && !HWRITE);
let b= !HREADYOUT[*0:16];
let c= (HRDATA[(( ADDR_    - (int' (ADDR_   /4)*4))*8) +: 8] == 8'h55);
let d= (HTRANS == 2) && (HADDR == ADDR_ + 1) && !HWRITE;
let e= !HREADYOUT[*0:16];
let f= (HRDATA[(((ADDR_+1) - (int'((ADDR_+1)/4)*4))*8) +: 8] == 8'hAA)' 

property prop_name(bit [23:0] ADDR_, int POS_);
	@(posedge HCLK) disable iff(!HRESETn)
		first_match(a ##1 b ##1 c ##[0:$] d ##1 f) |-> ##[1:$] EndLockCheck ##0 Lock[POS_];
endproperty

…“eliminating possibility of starting multi-thread in a property.”
The above has a multi-threaded antecedent because of the (##[0:$] d)
That is whay you need the first_match().

Also, consequent signal EndLockCheck goes high after few/200 cycles(That is why I’m using delay of 500 cycles in general). With these hard-coded cycle delays assertion either passes/fails, which is what I need. But when I replace 500 with $ in above checks, SVA does not give any results.

You need to look at your consequent. Assume that at cycle 20 the first_match(antecedent) is a match. after that cycle, let’s say cycle 200, when EndLockCheck ##0 Lock[POS_] matches, you should get a PASS.
With the ##[1:$] in the consequent you will NEVER GET A FAIL.

  As you know, 
(##[1:$] w) // is same as 
##1 w or ##2 w or ##3 w or ..... ##infinity w

Thus if w==0 forever, the consequent will keep on testing for a possible cycle when w==1.

Any other explanation on why checks I wrote should not work might be useful.

Constrain your ##[1:$} to a fixed range; pick a reasonable max cycle.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us