Strong and #-# of SVA

SystemVerilog
, , ,
1

Hi,
Please help. I am confused with #-# operator of SVA.
I thought the following two properties were equal.

// strong usage
$rose(s1) |-> strong(##[0:$] ##0 $rose(s2))

// #-# operator usage
$rose(s1) #-#        ##[0:$] ##0 $rose(s2)

However, it looks it is not correct.
The following tests were applied to these properties.

# === TEST 1 :         ________________
# s1 :  ______________|           _____
# s2 :  _________________________|  

# === TEST 2 :          _______________
# s1 :  _______________|               
# s2 :  _______________________________

I expected both property gets PASS in TEST 1 and FAIL in TEST 2 since s2 never goes high.
However, the result is

strong usage :
PASS in TEST 1, FAIL in TEST 2
(As expected)

#-# operator usage :
FAIL in TEST 1, FAIL in TEST 2
Looks fails at every clock cycle.

Here is EDA Playground link : https://www.edaplayground.com/x/vWKi

Is #-# operator different from strong? What is it and what is happening in the sim of the EDA Playground ?

2

property_expr ::=
…
| strong ( sequence_expr )
| sequence_expr #-# property_expr
| sequence_expr #=# property_expr
There is NO implication here. #-# is equivalent to ##0 if you substitute
property_expr with sequence.
So the #-# just says
sequence_expr is followed by a property_expr in a manner similar to
sequence ##0 sequence says a sequence followed by another sequence.
en Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

rose(s1) #-# ##[0:] ##0 $rose(s2)

1 Like
3

Thanks @ben2 ,

I understand that #-#, #=# don’t have meaning of implication unlike |->, |=>. Therefore, the check is done at every clock. A few articles says no vacuous pass with followed-by operator, #-#, #=#. But they are NOT implication property. So, check is done at every clock unless there is implication before them. Therefore, no vacuous pass in that sense. I misunderstood it and I thought strong attribute can be applied with #-#. I guess the person who created the following post made the same misunderstanding as me.

Usually, #-# is used to combine two properties as follows.

A |-> B #-# C |-> D

And, I think this is equivalent to the following two properties.

A |-> B
A ##0 B ##0 C |-> D

In this sense, followed-by operators are different from simple concatenation of implication.

A |-> B |-> C |-> D

is equal to

A |-> B
A ##0 B |-> C
A ##0 B ##0 C |-> D

I believe my understanding is correct now.

4

[YOU] Usually, #-# is used to combine two properties as follows.
[Ben] #-# is used to combine a sequence to a property

A |-> B #-# C |-> D  
    B is the sequene 
    C |-> D  is the property

A |-> B #-# C |-> D  is equivalent to 
A |-> (B #-# (C |-> D)))
      (B #-# C) |-> D   // ILLEGAL

All the other interpretations are incorrect

5

Hi @ben2 ,
I’m a bit confused.

What is the difference of the followings?

B #-# (C |-> D)

B ##0 C |-> D

Are these same? What is #-# for in that case?

6

Difference between

"B #-# (C |-> D)" and "B ##0 C |-> D"?
A: B #-# (C |-> D)
  B is a sequence
 (C |->D) is a property
if B==0 then ( B #-# (C |-> D)) property is false (Fails in an assertion)
(B #-# C) |-> D is illegal because (B #-# C) is a property
-----
B ##0 C |-> D
B ##0 C is a sequence and is an antecedent
D is sequence treated as a property in the consequent
if B==0 then (B ##0 C |-> D) property is vacuously true, (vacuous in an assertion)

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

7

Thanks @ben2 ,

Then, what about the case of (B == 1) and (C == 0)?
B ##0 C |-> D is obviously vacuous pass in this case.
Is B #-# (C |-> D) vacuous pass or fail?

8

If B==1, then you evaluate the property C |-> D
By now, you should know that if C==0 then property is vacuous.
Assertion is thus vacuously true