Four properties cover most RTL control bugs. Each row names the rule and what a violation means.
Template | Rule | Violation means |
|---|---|---|
Handshake response | Each eligible client's request gets its own grant within 1 to 3 cycles | A lost, misrouted or late answer |
Mutual exclusion |
| Two drivers on one bus |
Reset exit | State is idle at the first active sampling edge | Reset left a bad state |
Stability | Config holds while write enable is low | A stray write or a driver fight |
The checker module below observes all four properties on one clock and reset. Response windows are tracked separately per client. This arbiter gives client 0 strict priority: client 1 becomes eligible when req1 && !req0. This checks service opportunities, not starvation freedom; sustained client-0 traffic may legally block client 1.
Output | Meaning |
|---|---|
| No matching client grant within three cycles of an eligible request |
| Two grants high together |
| Non-idle state at the first active sampling edge |
| Config changed with write enable low |
| Reset release checked and state idle |
The trace below drives the arbiter twice: a normal request, then the same request with the force_both test hook, which makes the arbiter grant both clients.
Each slot shows the values sampled at one rising edge, numbered from 0.
Slots 1 and 2: req0 is sampled in slot 1 and the registered gnt0 answers in slot 2. One grant at a time, so $onehot0 holds.
Slot 4: req0 again, this time with force_both.
Slot 5: gnt0 and gnt1 are both high. This is the edge where $onehot0({gnt1, gnt0}) fails.
Slot 6: mutex_viol is high. The checker is a register, so its flag lands one cycle after the violating edge; an SVA tool reports the failure at slot 5 itself.
Check the reset state at the first active edge, before that edge's nonblocking assignments. A legal request on this edge may move the machine immediately afterwards; requiring IDLE one cycle later would reject that legal activity.
// snippet
// Same-edge sampling observes the reset state before normal transitions.
assert property (@(posedge clk)
$rose(rst_n) |-> state_q == ST_IDLE);
assert property (@(posedge clk) disable iff (!rst_n)
req0 |-> ##[1:3] gnt0);
assert property (@(posedge clk) disable iff (!rst_n)
(req1 && !req0) |-> ##[1:3] gnt1);
assert property (@(posedge clk) disable iff (!rst_n)
!cfg_we |=> $stable(cfg_q));The procedural checker remembers reset and write-enable history. A register change is qualified by the enable on the edge that caused it, not by the current enable. Request-age bits preserve overlapping response windows; a grant satisfies existing windows for that client but not a new same-edge request.
Only mutex_viol. The handshake window is still satisfied, so hs_viol stays low.
No. The checker samples IDLE at the first active edge, before the accepted request changes state. reset_ok pulses once; normal state transitions may then proceed.
The arbiter, the four-property checker, and the testbench. It answers eight requests, writes config twice, resets twice, then forces one double-grant.
// Two-client arbiter with registered grants, a config register, and a tiny state.
// force_both is a test hook: with req0 high it drives the deliberate double-grant.
module arb2 (
input logic clk, rst_n,
input logic req0, req1, force_both, cfg_we,
input logic [7:0] cfg_d,
output logic gnt0, gnt1,
output logic [1:0] state,
output logic [7:0] cfg_q
);
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
gnt0 <= 1'b0; gnt1 <= 1'b0; state <= 2'd0; cfg_q <= 8'd0;
end else begin
gnt0 <= req0;
gnt1 <= (req1 && !req0) || (force_both && req0);
if (req0 || req1) state <= 2'd1;
else state <= 2'd0;
if (cfg_we) cfg_q <= cfg_d;
end
end
endmodule
// One checker for the four template properties. Each monitor mirrors the
// standard SVA shapes: per-client response windows, grant mutex,
// first-active-edge reset state, and previous-enable register stability.
module prop_checker (
input logic clk, rst_n,
input logic req0, req1, gnt0, gnt1, cfg_we,
input logic [1:0] state,
input logic [7:0] cfg_q,
output logic hs_viol, mutex_viol, reset_viol, stab_viol, reset_ok
);
logic [2:0] pending0, pending1;
logic prev_rst_n, prev_we;
logic [7:0] prev_cfg;
wire [1:0] grant_vec = {gnt1, gnt0};
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
pending0 <= '0; pending1 <= '0; hs_viol <= 1'b0; mutex_viol <= 1'b0;
reset_viol <= 1'b0; stab_viol <= 1'b0; reset_ok <= 1'b0;
prev_rst_n <= 1'b0; prev_we <= 1'b0; prev_cfg <= 8'd0;
end else begin
hs_viol <= 1'b0; mutex_viol <= 1'b0; reset_viol <= 1'b0; stab_viol <= 1'b0; reset_ok <= 1'b0;
hs_viol <= (pending0[2] && (gnt0 !== 1'b1)) ||
(pending1[2] && (gnt1 !== 1'b1));
if (gnt0 === 1'b1) pending0 <= {2'b00, req0};
else pending0 <= {pending0[1:0], req0};
if (gnt1 === 1'b1) pending1 <= {2'b00, (req1 && !req0)};
else pending1 <= {pending1[1:0], (req1 && !req0)};
if ($isunknown(grant_vec) || !$onehot0(grant_vec)) mutex_viol <= 1'b1;
if (!prev_rst_n) begin
if (state === 2'd0) reset_ok <= 1'b1;
else reset_viol <= 1'b1;
end
prev_rst_n <= rst_n;
if (prev_rst_n && !prev_we && cfg_q !== prev_cfg) stab_viol <= 1'b1;
prev_we <= cfg_we;
prev_cfg <= cfg_q;
end
end
endmodule
Eight requests, four per client: every grant lands one cycle later, inside the window.
One deliberate violation: the forced double-grant raises mutex_viol exactly once, and nothing else fires.
Two resets each exit to idle. Config held 0x3C across traffic, and the second reset cleared it.
Directed checker regressions: a misrouted grant and a stray write must be detected; an immediate post-reset request must remain legal.
Testbench run with Icarus Verilog 13.0 (2026-10-16): prints PASS. It answers eight requests, writes config twice, resets twice and forces one double-grant; only the mutex check fires, once. The directed fault regressions (a misrouted grant and a stray write) are detected. These are simulation checks, not a formal proof.