Drill 1. state is an enum of IDLE, REQ, WAIT and DONE. Legal moves: IDLE to IDLE or REQ, REQ to WAIT or IDLE, WAIT to WAIT or DONE, DONE to IDLE.
Drill 2. req and gnt are 4-bit vectors: at most one grant at a time, and only to a requester.
Drill 3. wreq[0] and wgnt[0]: a request held high is granted within 4 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: FSMs and arbiters. Each drill has its own signals.
module tb_sva_fsm;
logic clk = 0, rst_n = 0;
always #5 clk = ~clk;
typedef enum logic [1:0] {IDLE, REQ, WAIT, DONE} state_e;
state_e state = IDLE; // drill 1: only legal moves (IDLE->IDLE/REQ, REQ->WAIT/IDLE, WAIT->WAIT/DONE, DONE->IDLE)
logic [3:0] req = 0, gnt = 0; // drill 2: at most one grant, and only to a requester
logic [3:0] wreq = 0, wgnt = 0; // drill 3: a held request is granted within 4 cycles
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 walk(state_e s[$]);
foreach (s[i]) begin @(negedge clk) state = s[i]; end
@(negedge clk) state = IDLE;
repeat (2) @(negedge clk);
endtask
task automatic arb(logic [3:0] r, logic [3:0] g);
@(negedge clk) req = r; gnt = g;
@(negedge clk) req = 0; gnt = 0;
endtask
task automatic wait_for(int lat);
@(negedge clk) wreq[0] = 1;
repeat (lat) @(negedge clk);
wgnt[0] = 1; @(negedge clk) wgnt[0] = 0; wreq[0] = 0;
repeat (6) @(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;
walk('{IDLE, REQ, WAIT, WAIT, DONE});
walk('{IDLE, REQ, IDLE});
arb(4'b0011, 4'b0001); arb(4'b1000, 4'b1000); arb(4'b0000, 4'b0000);
wait_for(0); wait_for(4);
c1 = f1; c2 = f2; c3 = f3;
walk('{IDLE, REQ, DONE}); // planted: REQ jumps to DONE
arb(4'b0101, 4'b0100); arb(4'b0010, 4'b0001); // the second grant goes to a non-requester
wait_for(6); // planted: granted after 6 cycles
wrong = verdict("drill 1, legal moves only", c1, f1 - c1)
+ verdict("drill 2, grants are one-hot and earned", c2, f2 - c2)
+ verdict("drill 3, granted within 4 cycles", c3, f3 - c3);
if (wrong != 0) $fatal(1, "FAIL: %0d of 3 drills wrong", wrong);
$display("PASS: all 3 drills right");
$finish;
end
endmodule$onehot(gnt) do it?No. $onehot rejects the idle cycle with no grant, which is legal; $onehot0 allows it. And neither says the grant went to a requester: that needs (gnt & ~req) == 0 beside it.
One set of answers, run through the same grader:
// SVA drills: FSMs and arbiters. Each drill has its own signals.
module tb_sva_fsm;
logic clk = 0, rst_n = 0;
always #5 clk = ~clk;
typedef enum logic [1:0] {IDLE, REQ, WAIT, DONE} state_e;
state_e state = IDLE; // drill 1: only legal moves (IDLE->IDLE/REQ, REQ->WAIT/IDLE, WAIT->WAIT/DONE, DONE->IDLE)
logic [3:0] req = 0, gnt = 0; // drill 2: at most one grant, and only to a requester
logic [3:0] wreq = 0, wgnt = 0; // drill 3: a held request is granted within 4 cycles
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)
(state == IDLE |=> state inside {IDLE, REQ}) and // ANSWER
(state == REQ |=> state inside {WAIT, IDLE}) and // ANSWER
(state == WAIT |=> state inside {WAIT, DONE}) and // ANSWER
(state == DONE |=> state == IDLE) // ANSWER
) else f1++;
ap_drill2: assert property (@(posedge clk) disable iff (!rst_n)
$onehot0(gnt) && (gnt & ~req) == 0 // ANSWER
) else f2++;
ap_drill3: assert property (@(posedge clk) disable iff (!rst_n)
wreq[0] |-> ##[0:4] wgnt[0] // ANSWER
) else f3++;
// The grader: legal traffic first, then one planted bug per drill.
task automatic walk(state_e s[$]);
foreach (s[i]) begin @(negedge clk) state = s[i]; end
@(negedge clk) state = IDLE;
repeat (2) @(negedge clk);
endtask
task automatic arb(logic [3:0] r, logic [3:0] g);
@(negedge clk) req = r; gnt = g;
@(negedge clk) req = 0; gnt = 0;
endtask
task automatic wait_for(int lat);
@(negedge clk) wreq[0] = 1;
repeat (lat) @(negedge clk);
wgnt[0] = 1; @(negedge clk) wgnt[0] = 0; wreq[0] = 0;
repeat (6) @(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;
walk('{IDLE, REQ, WAIT, WAIT, DONE});
walk('{IDLE, REQ, IDLE});
arb(4'b0011, 4'b0001); arb(4'b1000, 4'b1000); arb(4'b0000, 4'b0000);
wait_for(0); wait_for(4);
c1 = f1; c2 = f2; c3 = f3;
walk('{IDLE, REQ, DONE}); // planted: REQ jumps to DONE
arb(4'b0101, 4'b0100); arb(4'b0010, 4'b0001); // the second grant goes to a non-requester
wait_for(6); // planted: granted after 6 cycles
wrong = verdict("drill 1, legal moves only", c1, f1 - c1)
+ verdict("drill 2, grants are one-hot and earned", c2, f2 - c2)
+ verdict("drill 3, granted within 4 cycles", 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, legal moves only: ok
drill 2, grants are one-hot and earned: ok
drill 3, granted within 4 cycles: ok
PASS: all 3 drills rightOne implication per row of the table, joined with and because the drill has one slot: (state == IDLE |=> state inside {IDLE, REQ}) and .... In a real checker, write one assertion per row instead, so a failure names its source state; the FSM cookbook does exactly that.
Grants combine mutual exclusion and conservation: $onehot0(gnt) && (gnt & ~req) == 0. A one-hot grant to a non-requester passes mutual exclusion alone, which is why the second term exists.
A bounded wait is a range at the end of the consequent, wreq[0] |-> ##[0:4] wgnt[0]. Its antecedent is the level, which is right here: the obligation should renew each cycle the request waits.
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.