How to create an assertion that checks for if a signal is not high for more than 3 consecutive cycles?

Question

I am trying to write an assertion for my SystemVerilog design which checks if a signal is never high for more than 3 cycles (implicitly it must be de-asserted eventually). My signal is called "req" and I thought about doing something like this:

sequence req_three_seq;
   req ##[1:2] (~req);
endsequence

property reg_three_prop;
   @(posedge clk)
   disable iff (reset)
   (req) |-> req_three_seq;
endproperty

What can I do instead to create the assertion I need?

Answer 1

You could always add a helper block, something along the lines of:

reg [3:0] req_three_buf = 0;
always_ff @(posedge clk) begin
    req_three_buf = {req_three_buf[2:0], req};
end

property reg_three_prop;
    req_three_buf != '1;
endproperty

Also, you could wrap the block and property in an ifdef, so that you do not pull the additional block and signal into synthesis.