Systemverilog Assertion to validate clock cycle count for data reading

SystemVerilog
1

Hello everyone, Hope you all are doing well.
I was facing some problems with my assertions and can’t seem to find what is wrong.

	property out_ready_p;
		int len, count = 0;
		@(posedge clk) disable iff (reset)
		$rose(ready) |-> 							// Activates when ready rises
		##[1:$] (read, count=count+1)[*2] 			// read can be asserted any time after ready is asserted, First two packets will be DA and SA
		##1 (read, len=port, count=count+1) 		// 3rd packet contains length information
		##1 (read, count=count+1)[*1:$] 			// Continue count whenever read is HIGH
		##1 (!ready, $display($time, "ns |out_intf_%d| found read and ready LOW", ID))  // Untill ready is found LOW
		##0 (len+4 == count, $display("OutMon%d Count %0d || Len %d", ID, count, len)); // Check if read was HIGH for len+4 clock cycles, before ready is asserted LOW
	endproperty
	
	out_ready_check: assert property (out_ready_p);

The problem is, if count doesn’t match len+4 the assertion does not fail, it remains active. I wanted it to fail. Also the 2nd last display executes 16 times for some reason.

Could anyone kindly let me know what am I doing wrong here.

2

Creating a property where the antecedent starts out with an unbounded ##[1:$] never can fail; it forever keeps looking for success.

I’m guessing ready must remain asserted while read can go high and low nonconsecutively. Then you want the count to be checked when ready goes low. You need to be much more precise describing your requirements.

It would help tremendously if you could create a testbench for the case you think should fail, and a case that should pass.