Assertions, event regions

SystemVerilog
, ,
1

Hello!

I have a few questions about timing and logic operators usage in assertions.

First example

Is there any difference in this code between syntax?


a && b && c && d |->  v
a ##0 b  ##0 c  ##0 d |->  v

And some similar question, I did some research in variable assertions, and found Ben Cohen example code from that topic :
https://verificationacademy.com/forums/systemverilog/usage-variable-delay-sva

Let’s take this one:


property p_range_equivalent; // Equivalent implementation
 int local_v; // this is an internal local variable defined by the tool
 $rose(a) |-> (1, local_v = v-N)
  ##N 1'b1 ##0 first_match((1, local_v=local_v - 1)[*0:$] ##1 (b || local_v<=0))
  ##0 b;
endproperty

I don’t understand why we need to write this code
…##N 1’b1 ##0 first_match…
Is it not similar like ##N first_match ?
And as I ask before can we write && b, instead ##0 b.

Thanks ! And have a nice day!

2

In reply to maxiale:

Is there any difference in this code between syntax?


a && b && c   |->  v
a ##0 b  ##0 c   |->  v

There is NO difference from a simulation point of view.
The difference is in the interpretation or reading of the sequence. Specifically,

"a && b && c " reads like a 3-input AND gate. 
"a ##0 b  ##0 c   " reads as a series (or sequence) of ON/OFF switches: 
____________/ __________/ _______/ _______ 
            a           b        c          
or in English, "a",  and then immediately "b", and then immediately "c", ...

And some similar question, I did some research in variable assertions, and found Ben Cohen example code from that topic :
https://verificationacademy.com/forums/systemverilog/usage-variable-delay-sva
Let’s take this one:


property p_range_equivalent; // Equivalent implementation
int local_v; // this is an internal local variable defined by the tool
$rose(a) |-> (1, local_v = v-N)
##N 1'b1 ##0 first_match((1, local_v=local_v - 1)[*0:$] ##1 (b || local_v<=0))
##0 b;
endproperty

I don’t understand why we need to write this code
…##N 1’b1 ##0 first_match…
Is it not similar like ##N first_match ?
And as I ask before can we write && b, instead ##0 b.

You are correct that 
 ##N 1'b1 ##0 first_match((.. // IS the same as 
 ##N first_match((..
When I wrote the code, my train of thoughts was like this: 
 $rose(a) |-> (1, local_v = v-N)  ##N 1'b1 ##0 first_match((..
Following a rose(a), I set the local variable and then wait for N cycles. 
At that "stepping stone" (the ##N 1'b1 ) I then continue (with the ##0 )with this complex iterations with repeats and tests.  Thus, in my mind, I visualized the (##N 1'b1) as a pause or "stepping stone".  
But, you are correct, it could have been replaced with 
 ##N first_match((..

Defining properties is more about specifying requirements; syntax have connotations in the expressions of these requirements.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr