Drill 1. a, b and c: after a rises, c must not come before b has come.
Drill 2. req and gnt: every gnt had a req 1 to 3 cycles before it.
Drill 3. start, beat and done: between a start and its done there are exactly 4 beat cycles.
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: ordering and counting. Each drill has its own signals.
module tb_sva_order;
logic clk = 0, rst_n = 0;
always #5 clk = ~clk;
logic a = 0, b = 0, c = 0; // drill 1: after a, no c until b has come
logic req = 0, gnt = 0; // drill 2: every gnt had a req 1 to 3 cycles before
logic start = 0, beat = 0, done = 0; // drill 3: exactly 4 beats between start and done
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 abc(bit c_first);
@(negedge clk) a = 1;
@(negedge clk) a = 0;
if (c_first) begin c = 1; @(negedge clk) c = 0; end
@(negedge clk) b = 1;
@(negedge clk) b = 0; c = 1;
@(negedge clk) c = 0;
repeat (2) @(negedge clk);
endtask
task automatic grant_after(int lat);
@(negedge clk) req = 1;
@(negedge clk) req = 0;
repeat (lat - 1) @(negedge clk);
gnt = 1; @(negedge clk) gnt = 0;
repeat (4) @(negedge clk);
endtask
task automatic burst(int n);
@(negedge clk) start = 1;
@(negedge clk) start = 0;
for (int i = 0; i < n; i++) begin beat = 1; @(negedge clk); beat = 0; @(negedge clk); end
done = 1; @(negedge clk) done = 0;
repeat (2) @(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 (2) abc(0);
grant_after(1); grant_after(3);
repeat (2) burst(4);
c1 = f1; c2 = f2; c3 = f3;
abc(1); // planted: c arrives before b
grant_after(5); // planted: a grant 5 cycles after its request
burst(3); // planted: only 3 beats
wrong = verdict("drill 1, no c before b", c1, f1 - c1)
+ verdict("drill 2, gnt had a recent req", c2, f2 - c2)
+ verdict("drill 3, exactly 4 beats", c3, f3 - c3);
if (wrong != 0) $fatal(1, "FAIL: %0d of 3 drills wrong", wrong);
$display("PASS: all 3 drills right");
$finish;
end
endmodulereq or from gnt?From gnt, looking back with $past. Starting from req with a window forward says every request is granted, which is a different rule and fails on requests that are never granted.
One set of answers, run through the same grader:
// SVA drills: ordering and counting. Each drill has its own signals.
module tb_sva_order;
logic clk = 0, rst_n = 0;
always #5 clk = ~clk;
logic a = 0, b = 0, c = 0; // drill 1: after a, no c until b has come
logic req = 0, gnt = 0; // drill 2: every gnt had a req 1 to 3 cycles before
logic start = 0, beat = 0, done = 0; // drill 3: exactly 4 beats between start and done
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(a) |=> !c until b // ANSWER
) else f1++;
ap_drill2: assert property (@(posedge clk) disable iff (!rst_n)
gnt |-> $past(req, 1) || $past(req, 2) || $past(req, 3) // ANSWER
) else f2++;
int unsigned beats = 0; // ANSWER
always @(posedge clk) // ANSWER
if (start) beats <= 0; else if (beat) beats <= beats + 1; // ANSWER
ap_drill3: assert property (@(posedge clk) disable iff (!rst_n)
done |-> beats == 4 // ANSWER
) else f3++;
// The grader: legal traffic first, then one planted bug per drill.
task automatic abc(bit c_first);
@(negedge clk) a = 1;
@(negedge clk) a = 0;
if (c_first) begin c = 1; @(negedge clk) c = 0; end
@(negedge clk) b = 1;
@(negedge clk) b = 0; c = 1;
@(negedge clk) c = 0;
repeat (2) @(negedge clk);
endtask
task automatic grant_after(int lat);
@(negedge clk) req = 1;
@(negedge clk) req = 0;
repeat (lat - 1) @(negedge clk);
gnt = 1; @(negedge clk) gnt = 0;
repeat (4) @(negedge clk);
endtask
task automatic burst(int n);
@(negedge clk) start = 1;
@(negedge clk) start = 0;
for (int i = 0; i < n; i++) begin beat = 1; @(negedge clk); beat = 0; @(negedge clk); end
done = 1; @(negedge clk) done = 0;
repeat (2) @(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 (2) abc(0);
grant_after(1); grant_after(3);
repeat (2) burst(4);
c1 = f1; c2 = f2; c3 = f3;
abc(1); // planted: c arrives before b
grant_after(5); // planted: a grant 5 cycles after its request
burst(3); // planted: only 3 beats
wrong = verdict("drill 1, no c before b", c1, f1 - c1)
+ verdict("drill 2, gnt had a recent req", c2, f2 - c2)
+ verdict("drill 3, exactly 4 beats", 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, no c before b: ok
drill 2, gnt had a recent req: ok
drill 3, exactly 4 beats: ok
PASS: all 3 drills rightOrdering with gaps is an until: from the cycle after a, !c holds until b. until lets c come in the same cycle as b or later; until_with would also forbid c on the b cycle. Pick by that one cycle.
Backward rules trigger on the effect and look back. gnt |-> $past(req, 1) || $past(req, 2) || $past(req, 3) is three fixed lookbacks, each one a constant, which $past requires.
Counting across a window is modeling code. A counter clears on start, counts beat, and the property at done is one comparison. Sequence forms such as beat [->4] ##1 done say something similar but stop scaling the moment the count is a parameter or the spec adds a timeout, and on Verilator 5.048 a goto followed by more steps missed its planted bugs.
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.