Difficulty: Easy · Puzzle 2 of 6 · Topic: Clocking Block Puzzles
For a req sampled high at cycle N, at which cycle must grant be 1 for this property to pass?
interface arb_if(input bit clk);
logic req, grant;
clocking cb @(posedge clk);
default input #0 output #0;
input req, grant;
endclocking
endinterface
module tb;
bit clk = 0;
arb_if vif(clk);
always #5 clk = ~clk;
property p_req_to_grant;
@(vif.cb) vif.cb.req |=> ##1 vif.cb.grant;
endproperty
ap: assert property (p_req_to_grant);
endmodule|=> already moves one cycle; ##1 adds another cycle.
1) The antecedent samples req high at cycle N.
2) |=> starts the consequent at cycle N+1.
3) ##1 inside the consequent delays the grant check by one more cycle, to N+2.
4) Checked in Verilator: with req sampled at t=15 (N), grant high at t=35 passes; grant high only at t=25 (N+1) fails at t=35.
5) The property demands grant at N+2, not N+1.Answer: grant must be 1 at cycle N+2. Candidates often misread this as the next cycle (N+1).
Checked by running the code in Verilator 5; the printed output supports the answer above. With req sampled at t=15, grant at N+2 (t=35) passes while grant only at N+1 (t=25) fails.
Double-counting the delay is the trap: |=> and ##1 each add one cycle. It is a one-step reading exercise once you know that.
How would you rewrite for exactly next-cycle grant expectation? Model answer: vif.cb.req |=> vif.cb.grant (or vif.cb.req |-> ##1 vif.cb.grant); both require grant at N+1.
Grant must be 1 at cycle N plus 2. The non-overlapped implication starts the consequent one cycle after the antecedent, and the ##1 inside the consequent adds one more. The trap is double counting the delay and expecting grant at N plus 1, or missing one of them. I would confirm it with a pass and a fail run, and check what the spec says before I trust the assertion.