Clarification on first_match()

SystemVerilog
,
1

Hello,

I have a question about first_match() usage in concurrent assertions.

There is a scenario, where upon satisfying a condition (say sig1 && !sig2), sig3[1:0] is supposed to be 01 after four clock cycles. I have written the property as below:

property my_prop;
@(posedge clk) disable iff(reset)
(sig1 && !sig2) |-> (##4 (sig3 == 2’b01));
endproperty

This is working fine, and the assertion is passing after 4 clock cycles when both the conditions are met (antecedent true at 1st cycle, consequenct at 5th cycle). But the issue is that the antecedent holds true in 2nd, 3rd, 4th clock cycles also but consequent doesn’t need to be true in 6th, 7th, 8th cycles and because of which, I see false assertion failures.

To avoid this, I have enclosed antecedent in first_match() operator, but it is not working.
I tried first_match with the consequent too and it doesn’t work either.

Let me know if my understanding of first_match() is correct or wrong. If correct, I’d follow up with tool vendor on this. If wrong, please suggest the best method to resolve this.

Thanks,

PS: Note that I can’t use $rose(sig1) or $fell(sig2) as such as there is no certain order of whether sig1 roses first or sig2 falls first. It depends on the configuration.

2

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
3

In reply to ben@SystemVerilog.us:

Hello Ben,

Thanks for the solution and the clarification about first_match(). Your solution works perfectly fine.

Thanks