what you need is a $rose.
$rose((sig1 && !sig2)) |-> (##4 (sig3 == 2’b01));
You need a first_match() in an antecedent for a sequence that has multiple possible matches.
For example:
$rose(a) ##[1:$]b |-> c;
// same as
($rose(a) ##1 b) or ($rose(a) ##2 b) or ... ($rose(a) ##n b) |-> c
For the property to be true, ALL possible threads must be tested, and must be true (or vacuously true) for a completion of true. Thus, you would need a first_match()
first_match(($rose(a) ##[1:$]b)) |-> c;
You also would have multiple matches for the repeat operator:
a ##1 b[*1:7] |-> c;
you do not need a first_match() for the consequent since a match completes the assertion.
But
a ##1 b[*1:7] |-> c ##d [*1:9] |->e;
needs first_match() for the 2 antecedents
Ben Cohen http://www.systemverilog.us/
- SystemVerilog Assertions Handbook, 3rd Edition, 2013
- A Pragmatic Approach to VMM Adoption
- Using PSL/SUGAR … 2nd Edition
- Real Chip Design and Verification
- Cmpt Design by Example
- VHDL books