// If valid is asserted, data must not be X or Z

property PnotXorZ (clk, reset, valid, data);

@(posedge clk)

disable iff (reset)

valid |-> !$isunknown (data);

endproperty

 

// Assert that bus_data must be known when bus_valid is asserted

Ap_bus_data_valid: assert_property (PnotXorZ(clk250, reset, bus_valid, bus_data));

 

// Match when a response arrives within N cycles after a request

sequence Sreq_resp (clk, reset, request, response, N);

@(posedge clk)

request ##[1:N] response;

endsequence

 

// Collect coverage statistics for acknowledgements that come 1-10 cycles after requests

Cp_req_ack_10: cover property (Sreq_resp(clk250, reset, req, ack, 10));

Common Assertions

We will add more useful assertions here as we come across them. So please check back occasionally