Auxiliary code helping in SVA

hello guys , i have the following signals

  • clock “active high”
  • request
  • ack

specs

  • 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?

thanks!!

/ 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);

see update above

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 .

always_ff(posedge clk) if(req) req_cnt <= req_cnt +1 if(ack) ack_cnt <= ack_cnt +1

ap_req_ack : assert property (@posedge clock) bit [31:0] req_count (req, req_count = req_cnt) |-> ##[2:8](ack && ack_cnt == req_count);

1 Like
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.

guys you did not get my question.

now assume i have 3 requests in 1st clk and 3rd clk and 5th clk
and grant is high in 7th clk for 1 clk cycle after than simulation is finished.

my assertions enable condition is request signal so now there will be 3 assertions opens…

the 3 assertions will pass however just only 1 grant no 3 grants , so is there any auxiliary code can handle this case?

when 3 requests and 1 ack , it must be only 1 pass and 2 fails

check the code here

your solution worked , check it here
EDA Playground Login Modal with display aux code 2

can you please explain to me this
bit [31:0] req_count (req, req_count = req_cnt) ?

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);

Then:
initial a_no_initial_ack: assert property (@(posedge clk) not (!req ##[0:$] ack));

a_req_ack: assert property(@(posedge clk) req |=> !req[*0:N] ack);

a_no_ack_wo_req: assert property(@(posedge clk)
not (ack ##1 !req[*0:$] ##1 ack));