How to write assertions to check that first time when a is asserted it is preceded by the b?

SystemVerilog
, ,
1

write a assertion for the following condition:
If sig_a is asserted for the first time then it must have been preceded by sig_b.


property check_a;
@(posedge clk) $rose(a) |-> ($past(b) == 1'b1);
endproperty

If I write as above, then it is evaluated for all the cases whenever a is transited from 0 to 1. I want to check only for the first occurance of above condition. After that I want to disable it, how to do it?

Thanks in advance,
Manoj

2

In reply to Manoj J:

You can’t do this using only a property. You’ll have to track the fact that you saw ‘a’ in a different variable and use that inside the assertion:


property check_a;
  @(posedge clk)
    $rose(a) && !seen_a |-> ($past(b) == 1'b1);
endproperty

Tracking whether you’ve seen ‘a’ is also easy:


always @(posedge clk or negedge rst_n)
  if (!rst_n)
    seen_a <= 0;
  else 
    if (a)
      seen_a <= 1;

A lot of problems require support code for assertions and this is one of them, because you want to share information across assertion attempts. You can only do this using global state.

3

In reply to Tudor Timi:

Thanks for the clarification !!