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

SystemVerilog
, ,
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.