These four functions inspect a single sample with no history. $countones(v) returns the number of bits that are exactly 1.
$onehot(v) is true for exactly one set bit, and $onehot0(v) allows zero as well. $isunknown(v) is true when any bit is X or Z.
X and Z bits contribute zero to the count. That keeps the functions total, but it also lets corruption hide inside a passing check.
Vector | $countones | $onehot | $onehot0 | $isunknown |
|---|---|---|---|---|
| 0 | 0 | 1 | 0 |
| 1 | 1 | 1 | 0 |
| 2 | 0 | 0 | 0 |
| 1 | 1 | 1 | 1 |
| 0 | 0 | 1 | 1 |
| 0 | 0 | 1 | 1 |
| 1 | 1 | 1 | 1 |
The X rows are the lesson. $onehot(4'b1x00) is true while the register is corrupted, so pair every one-hot check with !$isunknown when X-safety matters.
4'b1x00. Does $onehot(state) catch it?No. The X bit is not counted, so the call returns true. Only the paired !$isunknown(state) term reports the corruption.
A one-hot FSM needs exactly one state bit set and no X anywhere.
// snippet
assert property (@(posedge clk) disable iff (!rst_n)
$onehot(state) && !$isunknown(state));An arbiter grant vector is the $onehot0 customer: idle with zero grants is legal, while two grants is a bus conflict. Conservation and X-freedom complete the set.
// snippet
assert property (@(posedge clk) disable iff (!rst_n)
$onehot0(gnt) && !$isunknown(gnt));
assert property (@(posedge clk) disable iff (!rst_n)
(gnt & ~req) == '0);
assert property (@(posedge clk) disable iff (!rst_n)
valid |-> !$isunknown(data));
assert property (@(posedge clk) disable iff (!rst_n)
(|req) |-> ##[0:1] $onehot(gnt));Check | Function | Why it matters |
|---|---|---|
Mutual exclusion |
| Two grants together means two drivers on one bus. |
Conservation |
| One-hot grants to a non-requester still pass mutual exclusion. |
Payload fitness |
| X on an idle bus is not a bug, so qualify with valid. |
These functions return plain booleans, so they drop into implications directly. Prefer enable |-> $onehot(sel) over burying the qualifier in a boolean OR.
The implication form reads as intent, shows a vacuous pass in coverage when disabled, and extends cleanly when the consequent grows sequence operators.
Need | Form |
|---|---|
Exactly one active line |
|
At most one, idle allowed |
|
Bounded population |
|
$onehot0, which accepts zero grants. $onehot rejects the idle cycle and reports a violation for correct behavior.
The first bench runs the real functions on Verilator: immediate $onehot and $onehot0 checks over all 16 binary patterns, and the two arbiter rules with a planted double grant and a planted grant to a non-requester.
module tb_counting;
logic clk = 0, rst_n = 0;
always #5 clk = ~clk;
logic [3:0] req = 0, gnt = 0;
int not_onehot = 0, not_onehot0 = 0, excl_fails = 0, conserve_fails = 0;
// Immediate checks over all 16 binary patterns.
task automatic classify(logic [3:0] v);
a_onehot: assert ($onehot(v)) else not_onehot++;
a_onehot0: assert ($onehot0(v)) else not_onehot0++;
endtask
// Arbiter rules: at most one grant, and only to a requester.
ap_excl: assert property (@(posedge clk) disable iff (!rst_n) $onehot0(gnt)) else excl_fails++;
ap_conserve: assert property (@(posedge clk) disable iff (!rst_n) (gnt & ~req) == '0) else conserve_fails++;
initial begin
for (int r = 0; r < 16; r++) classify(4'(r));
$display("16 patterns: $onehot failed %0d (12 expected), $onehot0 failed %0d (11 expected)", not_onehot, not_onehot0);
repeat (2) @(negedge clk);
rst_n = 1;
req = 4'b0011; gnt = 4'b0001; @(negedge clk); // legal
req = 4'b0000; gnt = 4'b0000; @(negedge clk); // legal: idle
req = 4'b0110; gnt = 4'b0110; @(negedge clk); // planted: two grants
req = 4'b0001; gnt = 4'b1000; @(negedge clk); // planted: one-hot, but to a non-requester
req = 0; gnt = 0;
repeat (2) @(negedge clk);
$display("arbiter: mutual exclusion %0d failure, conservation %0d failure", excl_fails, conserve_fails);
if (not_onehot != 12 || not_onehot0 != 11 || excl_fails != 1 || conserve_fails != 1) $fatal(1, "FAIL: %0d %0d %0d %0d", not_onehot, not_onehot0, excl_fails, conserve_fails);
$display("PASS: the classifiers matched the table, and each arbiter rule caught its planted grant");
$finish;
end
endmodule16 patterns: $onehot failed 12 (12 expected), $onehot0 failed 11 (11 expected)
arbiter: mutual exclusion 1 failure, conservation 1 failure
PASS: the classifiers matched the table, and each arbiter rule caught its planted grantThe X rows of the table need a 4-state simulator, and Verilator is 2-state. The listing below asks the course checks for Icarus 13, which runs these functions in immediate form.
module tb_vec_class_x;
logic [3:0] v;
int bad = 0;
initial begin
v = 4'b1x00; #1;
if ($countones(v) != 1 || $onehot(v) != 1 || $isunknown(v) != 1) bad++;
v = 4'b0x00; #1;
if ($countones(v) != 0 || $onehot(v) != 0 || $onehot0(v) != 1 || $isunknown(v) != 1) bad++;
v = 4'bxxxx; #1;
if ($countones(v) != 0 || $onehot(v) != 0 || $onehot0(v) != 1 || $isunknown(v) != 1) bad++;
v = 4'bz010; #1;
if ($countones(v) != 1 || $onehot(v) != 1 || $isunknown(v) != 1) bad++;
$display("4'b1x00: $onehot is %0d, $isunknown is %0d", $onehot(4'b1x00), $isunknown(4'b1x00));
if (bad == 0) $display("PASS: 4 X rows match the table above");
else $fatal(1, "FAIL: bad=%0d", bad);
$finish;
end
endmodule4'b1x00: $onehot is 1, $isunknown is 1
PASS: 4 X rows match the table aboveThe line printed before PASS is the whole lesson: $onehot(4'b1x00) is 1 while $isunknown is also 1. On Verilator the same X would have become 0 or 1 before any check saw it, so X-safety checks belong on a 4-state simulator.
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 X rows ran on Icarus 13 in immediate form; Verilator is 2-state, so $isunknown never fires there.