Drill 1. A 2-stage pipe: whenever out_vld is high, dout equals din from 2 cycles earlier.
Drill 2. After every reset, valid must not be high until init_done has been seen.
Drill 3. Requests carry a 4-bit tag and data; responses may come back in any order. Each response's data equals the data its tag was sent with.
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: data and reset. Each drill has its own signals.
module tb_sva_data;
logic clk = 0, rst_n = 0;
always #5 clk = ~clk;
logic in_vld = 0, out_vld = 0; // drill 1: a 2-stage pipe: dout is din from 2 cycles earlier
logic [7:0] din = 0, dout = 0, d1 = 0;
logic v1 = 0;
logic init_done = 0, valid = 0; // drill 2: after every reset, no valid until init_done has been seen
logic req = 0, rsp = 0; // drill 3: each response carries its own tag's data
logic [3:0] req_tag = 0, rsp_tag = 0;
logic [7:0] req_data = 0, rsp_data = 0;
bit corrupt = 0;
int f1 = 0, f2 = 0, f3 = 0;
// A small design for drill 1: two flops, with a plantable bug.
always @(posedge clk) begin
d1 <= din; dout <= corrupt ? d1 ^ 8'h01 : d1;
v1 <= in_vld; out_vld <= v1;
end
// 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 pipe(logic [7:0] d, bit bad);
@(negedge clk) in_vld = 1; din = d; corrupt = 0;
@(negedge clk) in_vld = 0; din = 0; corrupt = bad;
repeat (3) @(negedge clk);
corrupt = 0;
endtask
task automatic send(logic [3:0] t, logic [7:0] d);
@(negedge clk) req = 1; req_tag = t; req_data = d;
@(negedge clk) req = 0;
endtask
task automatic answer(logic [3:0] t, logic [7:0] d);
@(negedge clk) rsp = 1; rsp_tag = t; rsp_data = d;
@(negedge clk) rsp = 0;
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;
pipe(8'h11, 0); pipe(8'h22, 0);
@(negedge clk) init_done = 1; @(negedge clk) init_done = 0;
@(negedge clk) valid = 1; @(negedge clk) valid = 0;
send(4'h1, 8'hA1); send(4'h2, 8'hB2); answer(4'h2, 8'hB2); answer(4'h1, 8'hA1); // out of order is legal
c1 = f1; c2 = f2; c3 = f3;
pipe(8'h33, 1); // planted: the pipe flips a bit
rst_n = 0; @(negedge clk) rst_n = 1; // a reset: init must be seen again
@(negedge clk) valid = 1; @(negedge clk) valid = 0; // planted: valid before init_done
send(4'h3, 8'hC3); answer(4'h3, 8'hC4); // planted: wrong data for tag 3
repeat (2) @(negedge clk);
wrong = verdict("drill 1, dout is din two cycles back", c1, f1 - c1)
+ verdict("drill 2, no valid before init_done", c2, f2 - c2)
+ verdict("drill 3, tagged data matches", c3, f3 - c3);
if (wrong != 0) $fatal(1, "FAIL: %0d of 3 drills wrong", wrong);
$display("PASS: all 3 drills right");
$finish;
end
endmodule$past not express it?The distance back differs for every response, because responses come back in any order. $past needs a constant depth. The data has to be remembered per tag, in a local variable or in modeling code.
One set of answers, run through the same grader:
// SVA drills: data and reset. Each drill has its own signals.
module tb_sva_data;
logic clk = 0, rst_n = 0;
always #5 clk = ~clk;
logic in_vld = 0, out_vld = 0; // drill 1: a 2-stage pipe: dout is din from 2 cycles earlier
logic [7:0] din = 0, dout = 0, d1 = 0;
logic v1 = 0;
logic init_done = 0, valid = 0; // drill 2: after every reset, no valid until init_done has been seen
logic req = 0, rsp = 0; // drill 3: each response carries its own tag's data
logic [3:0] req_tag = 0, rsp_tag = 0;
logic [7:0] req_data = 0, rsp_data = 0;
bit corrupt = 0;
int f1 = 0, f2 = 0, f3 = 0;
// A small design for drill 1: two flops, with a plantable bug.
always @(posedge clk) begin
d1 <= din; dout <= corrupt ? d1 ^ 8'h01 : d1;
v1 <= in_vld; out_vld <= v1;
end
// Your answers: one property per drill, plus any modeling code you need.
ap_drill1: assert property (@(posedge clk) disable iff (!rst_n)
out_vld |-> dout == $past(din, 2) // ANSWER
) else f1++;
logic seen_init = 0; // ANSWER
always @(posedge clk or negedge rst_n) // ANSWER
if (!rst_n) seen_init <= 0; else if (init_done) seen_init <= 1; // ANSWER
ap_drill2: assert property (@(posedge clk) disable iff (!rst_n)
valid |-> seen_init // ANSWER
) else f2++;
logic [7:0] sent [16]; // ANSWER
always @(posedge clk) if (req) sent[req_tag] <= req_data; // ANSWER
ap_drill3: assert property (@(posedge clk) disable iff (!rst_n)
rsp |-> rsp_data == sent[rsp_tag] // ANSWER
) else f3++;
// The grader: legal traffic first, then one planted bug per drill.
task automatic pipe(logic [7:0] d, bit bad);
@(negedge clk) in_vld = 1; din = d; corrupt = 0;
@(negedge clk) in_vld = 0; din = 0; corrupt = bad;
repeat (3) @(negedge clk);
corrupt = 0;
endtask
task automatic send(logic [3:0] t, logic [7:0] d);
@(negedge clk) req = 1; req_tag = t; req_data = d;
@(negedge clk) req = 0;
endtask
task automatic answer(logic [3:0] t, logic [7:0] d);
@(negedge clk) rsp = 1; rsp_tag = t; rsp_data = d;
@(negedge clk) rsp = 0;
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;
pipe(8'h11, 0); pipe(8'h22, 0);
@(negedge clk) init_done = 1; @(negedge clk) init_done = 0;
@(negedge clk) valid = 1; @(negedge clk) valid = 0;
send(4'h1, 8'hA1); send(4'h2, 8'hB2); answer(4'h2, 8'hB2); answer(4'h1, 8'hA1); // out of order is legal
c1 = f1; c2 = f2; c3 = f3;
pipe(8'h33, 1); // planted: the pipe flips a bit
rst_n = 0; @(negedge clk) rst_n = 1; // a reset: init must be seen again
@(negedge clk) valid = 1; @(negedge clk) valid = 0; // planted: valid before init_done
send(4'h3, 8'hC3); answer(4'h3, 8'hC4); // planted: wrong data for tag 3
repeat (2) @(negedge clk);
wrong = verdict("drill 1, dout is din two cycles back", c1, f1 - c1)
+ verdict("drill 2, no valid before init_done", c2, f2 - c2)
+ verdict("drill 3, tagged data matches", 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, dout is din two cycles back: ok
drill 2, no valid before init_done: ok
drill 3, tagged data matches: ok
PASS: all 3 drills rightA fixed-latency pipe is the one place $past shines: out_vld |-> dout == $past(din, 2). On a pipe that stalls, the lookback must count advancing beats instead, and the gated form or a small history in modeling code does that.
Drill 2 needs memory that survives the cycles between init_done and valid, and that forgets on reset. The modeling flop resets with rst_n; the grader pulses reset between the clean traffic and the planted bug, so a flop that never resets is caught as too loose.
Tagged matching is the textbook local-variable property. Verilator 5.048 did not hold local-variable values correctly, so the reveal keeps the sent data in an array indexed by tag, which works everywhere.
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.