Assertion to check signal change only once(1->0->1) between 2 events

SystemVerilog
,
5

In reply to ben@SystemVerilog.us:

Thanks for your detailed explanation on why within does not work as expected due to the unbounded expansion(##1 1[*0:$]).

I really appreciate that you bring deep insight on within & [->1] by doing the expansion of the formulation. Well, in my application, if the rising edge of e may or may not overlap with rising edge of b, will the following property work?


property b_chg_once_ac_within(s, e, b);
      @(posedge clk)
        $rose(s) |-> (##1 $fell(b)[->1] ##1 b[=1] ##[0:$] !b) intersect e[->1];
endproperty