Drill 1. kick is always a one-cycle pulse.
Drill 2. strobe, once it rises, is high for exactly 3 cycles and then low.
Drill 3. valid, ready and an 8-bit data: while valid waits for ready, data does not change.
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: pulses and stability. Each drill has its own signals.
module tb_sva_pulse;
logic clk = 0, rst_n = 0;
always #5 clk = ~clk;
logic kick = 0; // drill 1: kick is always a one-cycle pulse
logic strobe = 0; // drill 2: strobe is high for exactly 3 cycles
logic valid = 0, ready = 0; // drill 3: data holds while valid waits for ready
logic [7:0] data = 0;
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 pulse(int width);
@(negedge clk) kick = 1;
repeat (width) @(negedge clk);
kick = 0;
repeat (2) @(negedge clk);
endtask
task automatic strobe_for(int width);
@(negedge clk) strobe = 1;
repeat (width) @(negedge clk);
strobe = 0;
repeat (3) @(negedge clk);
endtask
task automatic offer(logic [7:0] d, int wait_cycles, bit change);
@(negedge clk) valid = 1; data = d;
repeat (wait_cycles) begin @(negedge clk); if (change) data = data + 1; end
ready = 1; @(negedge clk) ready = 0; valid = 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 (3) pulse(1);
repeat (2) strobe_for(3);
offer(8'h10, 0, 0); offer(8'h20, 3, 0);
c1 = f1; c2 = f2; c3 = f3;
pulse(2); // planted: kick held for 2 cycles
strobe_for(2); // planted: a strobe one cycle short
offer(8'h30, 2, 1); // planted: data changes while waiting
wrong = verdict("drill 1, one-cycle pulse", c1, f1 - c1)
+ verdict("drill 2, strobe exactly 3 wide", c2, f2 - c2)
+ verdict("drill 3, data stable while stalled", c3, f3 - c3);
if (wrong != 0) $fatal(1, "FAIL: %0d of 3 drills wrong", wrong);
$display("PASS: all 3 drills right");
$finish;
end
endmodule$rose(kick) |-> !kick?It contradicts itself. $rose(kick) means kick is 1 in this cycle, so !kick in the same cycle can never hold and every pulse fails. The low cycle is the next one: |=>.
One set of answers, run through the same grader:
// SVA drills: pulses and stability. Each drill has its own signals.
module tb_sva_pulse;
logic clk = 0, rst_n = 0;
always #5 clk = ~clk;
logic kick = 0; // drill 1: kick is always a one-cycle pulse
logic strobe = 0; // drill 2: strobe is high for exactly 3 cycles
logic valid = 0, ready = 0; // drill 3: data holds while valid waits for ready
logic [7:0] data = 0;
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(kick) |=> !kick // ANSWER
) else f1++;
ap_drill2: assert property (@(posedge clk) disable iff (!rst_n)
$rose(strobe) |-> strobe ##1 strobe ##1 strobe ##1 (strobe == 0) // ANSWER
) else f2++;
ap_drill3: assert property (@(posedge clk) disable iff (!rst_n)
(valid && !ready) |=> $stable(data) // ANSWER
) else f3++;
// The grader: legal traffic first, then one planted bug per drill.
task automatic pulse(int width);
@(negedge clk) kick = 1;
repeat (width) @(negedge clk);
kick = 0;
repeat (2) @(negedge clk);
endtask
task automatic strobe_for(int width);
@(negedge clk) strobe = 1;
repeat (width) @(negedge clk);
strobe = 0;
repeat (3) @(negedge clk);
endtask
task automatic offer(logic [7:0] d, int wait_cycles, bit change);
@(negedge clk) valid = 1; data = d;
repeat (wait_cycles) begin @(negedge clk); if (change) data = data + 1; end
ready = 1; @(negedge clk) ready = 0; valid = 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 (3) pulse(1);
repeat (2) strobe_for(3);
offer(8'h10, 0, 0); offer(8'h20, 3, 0);
c1 = f1; c2 = f2; c3 = f3;
pulse(2); // planted: kick held for 2 cycles
strobe_for(2); // planted: a strobe one cycle short
offer(8'h30, 2, 1); // planted: data changes while waiting
wrong = verdict("drill 1, one-cycle pulse", c1, f1 - c1)
+ verdict("drill 2, strobe exactly 3 wide", c2, f2 - c2)
+ verdict("drill 3, data stable while stalled", 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, one-cycle pulse: ok
drill 2, strobe exactly 3 wide: ok
drill 3, data stable while stalled: ok
PASS: all 3 drills rightA width rule needs a terminator. $rose(strobe) |-> strobe [*3] checks that strobe lasted at least 3 cycles and says nothing about the fourth; adding ##1 (strobe == 0) closes it. The reveal writes the run out as strobe ##1 strobe ##1 strobe, the form Verilator 5.048 checks reliably; strobe [*3] ##1 (strobe == 0) passed this grader too, but the repetition lessons showed cases where the compact form missed a break. And the terminator is (strobe == 0), not !strobe, because Verilator rejects ! straight after ##1.
Stability is a level rule: every cycle that valid waits without ready, the next cycle's data must match. (valid && !ready) |=> $stable(data) renews the obligation each waiting cycle, which is exactly what the spec says.
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.