SVA: throughout vs until

SystemVerilog
, ,
1

Hi,
I guess I have a fundamental misunderstanding, but I am not sure what it is - I hope someone can clarify.
Consider a property “request req_i must remain high until acknowledge ack_o becomes active, and then request req_i must become inactive”
This can be written a as:

property AP_req_ack0 ;
      $rose(req_i) |-> (req_i throughout ack_o[->1]) ##1 !req_i  ;      
   endproperty : AP_req_ack0

There is also the property operator “until_with”. I tried to re-write the above property as

property AP_req_ack ;
      $rose(req_i) |-> req_i until_with ack_o ##1 !req_i ;
   endproperty : AP_req_ack

However, this doesn’t behave in the same way. The req_i until ack_o seems to work OK, but it doesn’t then check !req_i.
Regards,
Steven

2

In reply to moogyd:

…
There is also the property operator “until_with”. I tried to re-write the above property as

property AP_req_ack ;
$rose(req_i) |-> req_i until_with ack_o ##1 !req_i ;
endproperty : AP_req_ack

However, this doesn’t behave in the same way. The req_i until ack_o seems to work OK, but it doesn’t then check !req_i.

The until_with is a property operator:
property_expr until_with property_expr

An until property of one of the overlapping forms (i.e., until_with, s_until_with) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until, and including a clock tick at which property_expr2 evaluates to true. Thus, for

 (req_i throughout ack_o[->1]) ##1 !req_i

You are requiring that the property (which is a sequence in this case, but a sequence can be a property)req_i==1 until the property (ack_o[->1]) ##1 !req_i) completes. Thus, you are requiring that req_i==1 when it completes AND also in that SAME last cycle req_i==0. Sorry,but that ain’t going to happen!!!
The req_i until ack_o seems to work OK because in the last cycle there is no test for req_i.
An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true
:)
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

3

In reply to ben@SystemVerilog.us:
Hi Ben,
Actually, the throughout version behaves as I expect (and wanted).
For the throughout property example, I explicitely added the parentheses to ensure the correct behaviour - I already came across this “gotcha”


// Need to be careful with () here. It seems that the "##1" may have higher precendence than the "throughout"
   property AP_req_ack0 ;
      $rose(req_i) |-> (req_i throughout ack_o[->1]) ##1 !req_i  ;      
   endproperty : AP_req_ack0

So the req_i througout only applies to ack_o[->1]

I am still not sure about the until_with version.
Basically, it works (i.e reports a failure) if the req_i becomes inactive before the ack_o becomes active (the until_with part).
However, if I change the stimulus such that the req_i stays high after ack_o, the “throughout” version correctly reports a failure, but the “until_with” version does not, which implies it is not “moving on” to the !req_i check.
At some point in your email, you state that:

You are requiring that the property (which is a sequence in this case, but a sequence can be a property)…

Is the converse true? i.e. is it correct to treat

req_i until_with ack_o

as a sequence? If not, I guess using the ##1 is invalid in this case?
One interesting thing I noticed is that if I try to add parantheses to the property

   property AP_req_ack1 ;
     $rose(req_i) |-> (req_i until_with ack_o) ##1 !req_i ;
   endproperty : AP_req_ack1

I get complilation error. With Aldex Riviera Pro (EDA playground)

ERROR VCP2000 “Syntax error. Unexpected token: ##[O_HASHHASH]. Expected tokens: ‘;’.” “testbench.sv” 69 48
FAILURE “Compile failure 1 Errors 0 Warnings Analysis time: 0[s].”
Exit code expected: 0, received: 1

(Also checked the incisive)
Again, this implies that there is some fundamental difference between the throughout and until_with operators
Thanks,
Steven

4

In reply to moogyd:

In reply to ben@SystemVerilog.us:
Actually, the throughout version behaves as I expect (and wanted).
For the throughout property example, I explicitely added the parentheses to ensure the correct behaviour - I already came across this “gotcha”


// Need to be careful with () here. It seems that the "##1" may have higher precedence than the "throughout"
property AP_req_ack0 ;
$rose(req_i) |-> (req_i throughout ack_o[->1]) ##1 !req_i  ;      
endproperty : AP_req_ack0

So the req_i througout only applies to ack_o[->1]

You are correct about the precedence rules. From my book, I am showing below those rules:

703×636 56 KB

I am still not sure about the until_with version.
Basically, it works (i.e reports a failure) if the req_i becomes inactive before the ack_o becomes active (the until_with part).
However, if I change the stimulus such that the req_i stays high after ack_o, the “throughout” version correctly reports a failure, but the “until_with” version does not, which implies it is not “moving on” to the !req_i check.

1800 says: An until property of one of the overlapping forms (i.e., until_with, s_until_with) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until, and including a clock tick at which property_expr2 evaluates to true.
Thus, if property_expr1 evaluates to false (your req_i) then the property expression with the until_with fails. However, if req_i stays high after ack_o, I would have expected a failure. Can you share the test code?

At some point in your email, you state that:
Is the converse true? i.e. is it correct to treat

req_i until_with ack_o

as a sequence? If not, I guess using the ##1 is invalid in this case?

The converse is NOT true. If you look at the BNF for a property you’ll see

property_expr ::=
     sequence_expr
  | strong ( sequence_expr )
  | weak ( sequence_expr )
  | ( property_expr )....

But the BNF for a sequence does NOT show a sequence as a property as a possibility.
Actually, that makes sense because of the hierarchy of operators: sequences are built out of expressions (a sequence of 1 terms is the expression). Properties are built out of sequences. Concurrent assertions are built out of properties.

One interesting thing I noticed is that if I try to add parentheses to the property

   property AP_req_ack1 ;
$rose(req_i) |-> (req_i until_with ack_o) ##1 !req_i ;
endproperty : AP_req_ack1

I get complilation error. With Aldex Riviera Pro (EDA playground)

The simulation tools are correct, you cannot concatenate a property with a sequence. The (req_i until_with ack_o) is a property. However, you can concatenate a sequence with a property with the followed-by operators

 property_expr ::= // among other things 
  sequence_expr #-# property_expr
| sequence_expr #=# property_expr

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

5

In reply to ben@SystemVerilog.us:
Hi Ben,
My test code is available on EDA playground throughout_vs_until_with.
Thanks,
Steven

6

In reply to moogyd:
consider the code at Edit code - EDA Playground


ap_untilw: assert property(
	$rose(a) |-> b until_with c ##1 !b) 
	 $display("ap_untilw passed, b=%b at %t", $sampled(b), $time);  	
	
	ap_until_eq: assert property($rose(a) |-> b[*1:$] ##0 c ##1 !b) ; // equivalent assertion

b must hold only at the beginning of c ##1 !b, i.e., the moment of the truth of the property c ##1 !b. Thus the property expression 2 when it completes i
(b && c ##1 !b).
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

7

Thanks a lot Ben!
The observed behavior makes more sense now. Although it also shows that I only have quite a superficial understanding of SVA :-(
Steven
p.s. Just out of interest, the example https://www.edaplayground.com/x/39YH behaves differently with Incisive and Riviera Pro. There are different messages in the log.

8

In reply to moogyd:

Thanks a lot Ben!
The observed behavior makes more sense now. Although it also shows that I only have quite a superficial understanding of SVA :-(
Steven
p.s. Just out of interest, the example https://www.edaplayground.com/x/39YH behaves differently with Incisive and Riviera Pro. There are different messages in the log.

The different messages is because Riviera displays all messages, vacuous and non-vacuous, whereas Incisive displays only the non-vacuous passes. There should be a switch for Riviera to suppress the vacuous pass action blocks.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

9

In reply to ben@SystemVerilog.us:

ap_untilw: assert property(
	$rose(a) |-> b until_with c ##1 !b) 
	 $display("ap_untilw passed, b=%b at %t", $sampled(b), $time);  	
 
	ap_until_eq: assert property($rose(a) |-> b[*1:$] ##0 c ##1 !b) ; // equivalent assertion

In the above example, there is no clock referred for the property. Will it not get any compilation issue?

10

In reply to Anudeep J:

You either need to add a clocking event or use a default clocking.

 
// what I usually use
default clocking @(posedge clk); endclocking

//override the default 
ap_untilw: assert property(@(posedge clk2) 
	$rose(a) |-> b until_with c ##1 !b) 
	 $display("ap_untilw passed, b=%b at %t", $sampled(b), $time);  	
 
	ap_until_eq: assert property($rose(a) |-> b[*1:$] ##0 c ##1 !b) ; // equivalent assertion

Ben systemverilog.us