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

In reply to mlsxdx:



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