Assertion to check number of clock pulses

In reply to ben@SystemVerilog.us:

Thank you Ben. I’m not sure how the tool is expanding the inner block, but the following is working.

property p1;
@(posedge clk)
$fell(a) |=> (##1 b && !a ##2 !b && !a)[*16] ##2 $rose(a);
endproperty