Part 4 · Assertions (SVA) · Intermediate
$countones, $onehot, $onehot0, $isunknown
Bit-counting and classification of a sampled vector, X handling, one-hot FSM and grant checks, and X-free payload assertions.
Classifying a single sampled vector
Unlike $rose or $past, these four functions look at one snapshot — no history involved. $countones(v) returns the number of bits that are exactly 1. $onehot(v) is true when exactly one bit is 1; $onehot0(v) relaxes that to at most one bit (zero or one) — the right check for grant vectors that may be idle. $isunknown(v) is true when any bit is X or Z.
X handling is the part interviews probe: $countones counts only solid 1s — X and Z bits contribute zero. Consequently $onehot(4'b1x00) is true (one solid 1; the X is not counted), which can mask a corrupted one-hot register. A robust one-hot check therefore pairs $onehot with !$isunknown.
X HANDLING REFERENCE
vector v $countones $onehot $onehot0 $isunknown
─────────────────────────────────────────────────────────
4'b0000 0 0 1 0
4'b0100 1 1 1 0
4'b0110 2 0 0 0
4'b1x00 1 1* 1* 1 * X masked!
4'b0x00 0 0 1* 1
4'bxxxx 0 0 1* 1
4'bz010 1 1* 1* 1
Rule: X/Z bits are simply NOT counted as ones.
$onehot/$onehot0 can return true on corrupted vectors —
always AND with !$isunknown when X-safety matters.One-hot FSM state check
// One-hot encoded FSM: exactly one state bit set, always X-free
typedef enum logic [3:0] {
S_IDLE = 4'b0001, S_FETCH = 4'b0010,
S_EXEC = 4'b0100, S_WB = 4'b1000
} state_e;
state_e state;
// Exactly one bit, and no X/Z anywhere in the register
assert property (@(posedge clk) disable iff (!rst_n)
$onehot(state) && !$isunknown(state));tick : 1 2 3 4 5
state (sampled): 0001 0010 0110 0x00 1000
$onehot : 1 1 0 0 1
$isunknown : 0 0 0 1 0
assertion : PASS PASS FAIL FAIL PASS
^ ^
two bits set ─┘ └─ X corruption caught only
because of !$isunknown;
$onehot0(0x00) alone = trueWhy this beats a default-case check in RTL: the assertion fires the very cycle the register is corrupted (by an SEU model, an X from an uninitialized path, or a decode bug), with a message pointing at the exact signal — instead of the FSM silently sitting in a dead state until a downstream timeout.
Arbiter mutual exclusion and X-free payloads
The grant vector of an arbiter is the canonical $onehot0 customer: zero grants is legal (no requester), two grants is a catastrophic bus conflict. A second classic is conservation: grants only go to requesters. The third is the X check on payloads — X on a data bus is only a bug when someone is consuming the data , so qualify it with valid. An unqualified !$isunknown(data) fires constantly on idle buses that legitimately float.
// 1. Never two grants in the same cycle (idle allowed)
assert property (@(posedge clk) disable iff (!rst_n)
$onehot0(gnt) && !$isunknown(gnt));
// 2. Conservation: every grant bit had a matching request
assert property (@(posedge clk) disable iff (!rst_n)
(gnt & ~req) == '0);
// 3. Payload X check — qualified by the implication
assert property (@(posedge clk) disable iff (!rst_n)
valid |-> !$isunknown(data) && !$isunknown(strb));
// 4. Exactly-one-grant only when someone requests
assert property (@(posedge clk) disable iff (!rst_n)
(|req) |-> $onehot(gnt) or ##1 $onehot(gnt));Arbiter mutual exclusion, 3 requesters
tick : 1 2 3 4 5 6
req (sampled) : 000 011 011 100 000 010
gnt (sampled) : 000 010 001 110 000 010
$onehot0(gnt) : 1 1 1 0 1 1
gnt & ~req : 000 000 000 010 000 000
check 1 : PASS PASS PASS FAIL PASS PASS
check 2 : PASS PASS PASS FAIL PASS PASS
^
tick 4: two grants AND a grant (bit1) without request —
both assertions fire the same cycle, naming the rule brokenCombining with implication
These functions return plain booleans, so they slot directly into implications as antecedent qualifiers or consequent checks. The pattern “property holds only while enabled” is just enable |-> $onehot(sel). Resist the temptation to bury the qualification inside a boolean (!enable || $onehot(sel)) — it evaluates identically here, but the implication form documents intent, shows up as a vacuous pass when disabled (visible in coverage), and extends naturally when the consequent later grows sequence operators.
// Mode-qualified one-hot: lane select must be one-hot only in
// striped mode; in mirror mode all-lanes (all ones) is also legal.
assert property (@(posedge clk) disable iff (!rst_n)
(mode == STRIPED) |-> $onehot(lane_sel));
assert property (@(posedge clk) disable iff (!rst_n)
(mode == MIRROR) |-> ($onehot(lane_sel) || lane_sel == '1));
// Population-count bound: at most 4 outstanding tags
assert property (@(posedge clk) disable iff (!rst_n)
$countones(tag_in_flight) <= 4);Interview angle
The high-frequency question is $onehot vs $onehot0: exactly-one versus at-most-one, with the arbiter grant vector as the example where idle must be legal. The differentiator question is X handling — most candidates do not know that $onehot(4'b1x00) is true, and explaining why you pair it with !$isunknown signals real-world scar tissue. Expect “write an assertion that the data bus is never X” as a trap: the correct answer qualifies with valid |-> and you should say why the unqualified version drowns you in failures on idle cycles.
Key takeaways
$countones counts solid 1s only; X and Z bits contribute nothing.
$onehot = exactly one bit; $onehot0 = at most one — grants use $onehot0, one-hot FSM state uses $onehot.
X can hide inside a passing $onehot — pair with !$isunknown for X-safe checks.
Qualify $isunknown payload checks with valid — X on an idle bus is not a bug.
These are single-snapshot classifiers; combine with implication to scope when they must hold.
Common pitfalls
Trusting $onehot alone on a state register — 4'b1x00 passes while the FSM is corrupted.
Asserting !$isunknown(data) unconditionally — fires every idle cycle on a floating bus.
Using $onehot on a grant vector that is legally idle — zero grants fails; you wanted $onehot0.
Forgetting conservation (gnt & ~req == 0) — one-hot grants to a non-requester still pass mutual exclusion.
Re-implementing $countones with a hand-rolled loop in a checker — slower and X-handling diverges.