4 point handshake assertions for a simple valid-ready protocol

SystemVerilog
,
1

Hi,
I am trying to verify a simple valid-ready protocol handshake that follows the 4 point handshake between valid and ready signals of 2 components that are trying to communicate on the interface.
I have come up with the following assertions. Could someone proof check if these are correct and correct if something is off, in the sense they translate to what is functionally desired?
It is assumed that when data is available , the sender would assert valid.

Assertions:

1. The receiver must assert ready in response once its ready and the sender must keep the valid asserted until the receiver asserts ready.
	
	Property p1; --> ready should eventually come once the valid is asserted
		@(posedge clk) disable iff (reset)
		$rose(valid) |-> ##[*0:$] ready
	endproperty 

	Property p2; -> once valid is asserted it must remain asserted until the ready is asserted
		@(posedge clk) disable iff (reset)
		$rose(valid) |-> valid throughout ready[->1];
	Endproperty
	
2. The sender must de-assert the valid once it sees the receiver assert ready.
	Property p3; -> once the ready is asserted, the sender must eventually deassert the valid
		@(posedge clk) disable iff (reset)
		$rose(ready) |-> ##[0:$] !valid
	endproperty
3. The receiver must keep the ready asserted until the sender de-asserts valid
	Property p4;
		@(posedge clk) disable iff (reset)
		$rose(ready) |-> ready throughout !valid[->1];
	endproperty
4. The receiver must de-assert the ready once it sees the de-assertion of valid 
	Property p5;
		@(posedge clk) disable iff (reset)
		$fell(valid) |-> ##[0:$] !ready 
	endproperty
2

yOU ARE MOSTLY correct. You often use the [*0:] when yiu really mean [*1:].
I also have a disdain for the use of the throughout because it is subject to interpretaion. I prefer the use of the intersect.

1. The receiver must assert ready in response once its ready and the sender must keep the valid asserted until the receiver asserts ready.
	
	Property p1; --> ready should eventually come once the valid is asserted
		@(posedge clk) disable iff (reset)
		$rose(valid) |-> ##[*0:$] ready
	endproperty 

	Property p2; -> once valid is asserted it must remain asserted until the ready is asserted
		@(posedge clk) disable iff (reset)
		$rose(valid) |-> valid throughout ready[->1];
// Throughout is same as (exp) [*0:$] intersect seq  
// tHIS IS THE SAME, BUT WITHOUTH having to clarify the meaning of ‘throughout’
           // $rose(valid) |-> valid[*1:$] intersect ready[->1]; // – my preference
	Endproperty
	
2. The sender must de-assert the valid once it sees the receiver assert ready.
	Property p3; -> once the ready is asserted, the sender must eventually deassert the valid
		@(posedge clk) disable iff (reset)
		$rose(ready) |-> ##[0:$] !valid;
// [Ben] You  mean !valid AFTER rose or rdy, 
//                     $rose(ready) |-> ##[1:$] !valid
	endproperty
3. The receiver must keep the ready asserted until the sender de-asserts valid
	Property p4;
		@(posedge clk) disable iff (reset)
		$rose(ready) |->  ready[*1:$] intersect  !valid[->1];  /[Ben]
 // ready throughout !valid[->1]; // The throughout is more English like, subject to interretation
	endproperty
4. The receiver must de-assert the ready once it sees the de-assertion of valid 
	Property p5;
		@(posedge clk) disable iff (reset)
		$fell(valid) |-> ##[1:$] !ready  // ##[0:$] !ready // iN same CYCLE? 
	endproperty
1 Like
3

Thanks @hdlcohen for your reply and pointing out the small mistakes.
It resolves the problem.