Drill 1. req_a and ack_a: whenever req_a rises, ack_a is high exactly 3 cycles later.
Drill 2. req_b and ack_b: once req_b is high it stays high until ack_b arrives, and still high in the ack_b cycle.
Drill 3. req_c and ack_c: req_c is a one-cycle pulse and ack_c comes some cycles later. An ack_c with no request outstanding is a bug.
Write the three assertions before opening the reveal. Copy the starter into the Code Lab, replace each 1'b1 with your property (add modeling code above it if you need state), and run it on Verilator with assertions on. The grader runs legal traffic, where your assertions must stay silent, then one planted bug per drill, which yours must report. If an answer uses a repetition, or a range followed by more steps, and the grader says it missed its bug, read the tool notes on the sequences pages: Verilator 5.048 misses some failures in those forms.
// SVA drill starter: write each property (and any modeling code), then run it.
// SVA drills: handshakes. Each drill has its own signals.
module tb_sva_handshake;
logic clk = 0, rst_n = 0;
always #5 clk = ~clk;
logic req_a = 0, ack_a = 0; // drill 1: ack exactly 3 cycles after req rises
logic req_b = 0, ack_b = 0; // drill 2: req held until ack, overlapping it
logic req_c = 0, ack_c = 0; // drill 3: req is a 1-cycle pulse; no ack without one outstanding
int f1 = 0, f2 = 0, f3 = 0;
// Your answers: one property per drill, plus any modeling code you need.
ap_drill1: assert property (@(posedge clk) disable iff (!rst_n)
1'b1 // replace 1'b1 with your property
) else f1++;
ap_drill2: assert property (@(posedge clk) disable iff (!rst_n)
1'b1 // replace 1'b1 with your property
) else f2++;
ap_drill3: assert property (@(posedge clk) disable iff (!rst_n)
1'b1 // replace 1'b1 with your property
) else f3++;
// The grader: legal traffic first, then one planted bug per drill.
task automatic hs_a(int lat);
@(negedge clk) req_a = 1;
@(negedge clk) req_a = 0;
repeat (lat - 1) @(negedge clk);
ack_a = 1; @(negedge clk) ack_a = 0;
repeat (3) @(negedge clk);
endtask
task automatic hs_b(bit early_drop);
@(negedge clk) req_b = 1;
repeat (2) @(negedge clk);
if (early_drop) begin req_b = 0; @(negedge clk); end
ack_b = 1; @(negedge clk) ack_b = 0; req_b = 0;
repeat (3) @(negedge clk);
endtask
task automatic hs_c(bit extra_ack);
@(negedge clk) req_c = 1;
@(negedge clk) req_c = 0;
@(negedge clk) ack_c = 1;
@(negedge clk) ack_c = 0;
if (extra_ack) begin @(negedge clk) ack_c = 1; @(negedge clk) ack_c = 0; end
repeat (3) @(negedge clk);
endtask
function automatic int verdict(string name, int clean, int caught);
if (clean != 0) begin $display("%s: wrong, it fired %0d times on legal traffic (too strict)", name, clean); return 1; end
if (caught == 0) begin $display("%s: wrong, it missed its planted bug (too loose)", name); return 1; end
$display("%s: ok", name);
return 0;
endfunction
initial begin
int c1, c2, c3, wrong;
repeat (2) @(negedge clk);
rst_n = 1;
repeat (3) hs_a(3);
repeat (2) hs_b(0);
repeat (2) hs_c(0);
c1 = f1; c2 = f2; c3 = f3;
hs_a(2); // planted: ack one cycle early
hs_b(1); // planted: req dropped before ack
hs_c(1); // planted: an ack nobody asked for
wrong = verdict("drill 1, ack exactly 3 cycles later", c1, f1 - c1)
+ verdict("drill 2, req held until ack", c2, f2 - c2)
+ verdict("drill 3, no orphan ack", c3, f3 - c3);
if (wrong != 0) $fatal(1, "FAIL: %0d of 3 drills wrong", wrong);
$display("PASS: all 3 drills right");
$finish;
end
endmoduleack_c |-> req_c?On a pulsed protocol req_c is already low when the legal ack arrives, so the assertion fires on good traffic. The pins no longer hold the protocol state; a flop of modeling code has to remember the outstanding request.
One set of answers, run through the same grader:
// SVA drills: handshakes. Each drill has its own signals.
module tb_sva_handshake;
logic clk = 0, rst_n = 0;
always #5 clk = ~clk;
logic req_a = 0, ack_a = 0; // drill 1: ack exactly 3 cycles after req rises
logic req_b = 0, ack_b = 0; // drill 2: req held until ack, overlapping it
logic req_c = 0, ack_c = 0; // drill 3: req is a 1-cycle pulse; no ack without one outstanding
int f1 = 0, f2 = 0, f3 = 0;
// Your answers: one property per drill, plus any modeling code you need.
ap_drill1: assert property (@(posedge clk) disable iff (!rst_n)
$rose(req_a) |-> ##3 ack_a // ANSWER
) else f1++;
ap_drill2: assert property (@(posedge clk) disable iff (!rst_n)
(req_b && !ack_b) |=> req_b // ANSWER
) else f2++;
logic outstanding = 0; // ANSWER
always @(posedge clk) // ANSWER
if (req_c) outstanding <= 1; else if (ack_c) outstanding <= 0; // ANSWER
ap_drill3: assert property (@(posedge clk) disable iff (!rst_n)
ack_c |-> outstanding || req_c // ANSWER
) else f3++;
// The grader: legal traffic first, then one planted bug per drill.
task automatic hs_a(int lat);
@(negedge clk) req_a = 1;
@(negedge clk) req_a = 0;
repeat (lat - 1) @(negedge clk);
ack_a = 1; @(negedge clk) ack_a = 0;
repeat (3) @(negedge clk);
endtask
task automatic hs_b(bit early_drop);
@(negedge clk) req_b = 1;
repeat (2) @(negedge clk);
if (early_drop) begin req_b = 0; @(negedge clk); end
ack_b = 1; @(negedge clk) ack_b = 0; req_b = 0;
repeat (3) @(negedge clk);
endtask
task automatic hs_c(bit extra_ack);
@(negedge clk) req_c = 1;
@(negedge clk) req_c = 0;
@(negedge clk) ack_c = 1;
@(negedge clk) ack_c = 0;
if (extra_ack) begin @(negedge clk) ack_c = 1; @(negedge clk) ack_c = 0; end
repeat (3) @(negedge clk);
endtask
function automatic int verdict(string name, int clean, int caught);
if (clean != 0) begin $display("%s: wrong, it fired %0d times on legal traffic (too strict)", name, clean); return 1; end
if (caught == 0) begin $display("%s: wrong, it missed its planted bug (too loose)", name); return 1; end
$display("%s: ok", name);
return 0;
endfunction
initial begin
int c1, c2, c3, wrong;
repeat (2) @(negedge clk);
rst_n = 1;
repeat (3) hs_a(3);
repeat (2) hs_b(0);
repeat (2) hs_c(0);
c1 = f1; c2 = f2; c3 = f3;
hs_a(2); // planted: ack one cycle early
hs_b(1); // planted: req dropped before ack
hs_c(1); // planted: an ack nobody asked for
wrong = verdict("drill 1, ack exactly 3 cycles later", c1, f1 - c1)
+ verdict("drill 2, req held until ack", c2, f2 - c2)
+ verdict("drill 3, no orphan ack", c3, f3 - c3);
if (wrong != 0) $fatal(1, "FAIL: %0d of 3 drills wrong", wrong);
$display("PASS: all 3 drills right");
$finish;
end
endmoduledrill 1, ack exactly 3 cycles later: ok
drill 2, req held until ack: ok
drill 3, no orphan ack: ok
PASS: all 3 drills right“Whenever req rises” is an edge, so $rose(req_a): a level antecedent would start a fresh attempt every cycle req_a stays high. “Exactly 3 cycles later” is the fixed delay ##3; a range would accept early acks. And $rose(req_a) |=> ##3 ack_a counts the delay twice, checking cycle T+4.
For drill 2, (req_b && !ack_b) |=> req_b says each cycle without the ack is followed by one with req_b still high, which carries req_b into the ack cycle. $rose(req_b) |-> req_b until_with ack_b says the same in one sentence. Neither demands that the ack ever comes: that is a separate bounded check.
Drill 3 needs state because the pins forget. A flop sets on the request and clears on the ack, and the property is one line on top. Modeling code next to an assertion is normal, and saying so is a senior signal.
Run with Verilator 5.048 (--binary --timing --assert, plus --coverage when a listing has a cover property) on 2026-10-18; every bench printed the PASS line shown. Verilator stops at the first $error or failing assertion without an action block, so the benches count failures in the action block. Icarus 13 has no concurrent assertions.
The starter was run with every property left as 1'b1, and its grader reported all three drills wrong; the revealed answers passed the same grader.