ack must come after request , no ack without request.
when i write that
there is a corner case that i have 3 requests and 1 ack,
A1: assert property(@(posedge clock) request |-> ##[2:8] ack));
the surprise that the 3 assertions are passed! , i searched internet i found the solution is auxiliary code.
can you help me writing auxiliary code with SVA to test when
3 requests and 1 ack, just only 1 pass and the other two fails?
/ ack must come after request , no ack without request.
bit past_req;
always_ff @(posedge clk) begin
if(req && !ack) past_req<=1;
else if(ack) past_req <=0;
end
//
a// DO NOT USE: p_no_req_ack: assert property (@(posedge clk) !req && !ack);
//
ap_req_ack: assert property (@(posedge clock) req |-> past_req ##[2:8] ack);
in your solution , past_req will set after once clock cycle . based on supporting logic. What if ack comes in one cycle later instead between ##[2:8]
Solution only works if next req does not come before ack .
ap_req_ack: assert property (@(posedge clock) req |-> past_req ##[2:8] ack);
in my solution , past_req will set after once clock cycle and stays at that level until reset by hte ack.
If ack comes in one cycle later instead between ##[2:8] then assertion ap_req_ack will fail.
Properties are provided in solution that are weak in nature. if the simulation is finished without grant , then simulation passes. You need to write the strong or keywork
ap_req_ack : assert property (@posedge clock) bit [31:0] req_count (req, req_count = req_cnt) |-> strong(##[2:8](ack && ack_cnt == req_count));
A possible solution w/o procedural code. I assume that both req and ack are single clock tick wide pulses. I.e.,
Assume_Req: assume property(@(posedge clk) req |=> !req);
Assume_Ack: assume property(@(posedge clk) ack |=> !ack);