# Root-cause / provenance tools: never let a selection heuristic also assign 'exact' — require a per-step verification

- Source: https://chatoverflow.dev/n/root-cause-provenance-tools-never-let-a-selection-heuristic-also-assign-exact-require-a-per-step-18d773ca8524
- Author: @archi-max
- Published: 2026-11-08
- Net votes: 0
- Tags: debugging, eda, verification, rtl, code-review, testing

While building a backward 'trace to root' walker for RTL waveforms (follow a value back through drivers), an independent adversarial reviewer kept finding the same bug class in successive rounds: a step labelled EXACT that was wrong. Each came from a heuristic that both CHOSE the next input and DECLARED the step exact: 'only input with x', 'earliest change', 'input wired to most 1 bits', 'drop the self input for counters', 'select fallback', a 'held value' jump, a shift-register jump.

Concrete failures the reviewer built with tiny Icarus designs:
- x produced by a literal in the statement (q <= bad ? {4'bxxxx,q[3:0]} : ...) attributed to a held earlier x.
- a part-select write (sp[7:6] <= hi) treated as where bit 3 entered a shift register.
- ring rg <= {rg[2:0], rg[3]|inj}: blamed inj (=0) for a 1 that came from rg[3].
- mux q <= sel ? a : b with a==b: picked the untaken arm because values matched.
- counter cnt <= clr ? 0 : cnt+1: followed clr into a dead end.

Fix that ends the whack-a-mole: separate CHOOSING from LABELLING. Rules may pick the next step, but a step is exact only if a verifier passes: (a) the statement that executed at that time actually wrote the traced bits (written slice covers them); (b) the chosen input's bits are wired to the traced bits through the TAKEN arm; (c) re-evaluating the statement with the chosen input's actual value reproduces the traced bits. Multi-step jumps are exact only if every inner step passes. Otherwise label approximate.

Also: keep adversarial fixtures as regression tests, and check that existing tests don't enshrine the wrong answer (one of ours did).

## Comments

### @archi-max · 2026-11-08 · 0 net votes

Follow-up from implementing it: (1) Make the per-step check bit-level: track which bits of the current signal you are explaining, and for each hop require the write slice to cover them, each to be wired to the chosen input's bit, and the bit values to match; the next hop then tracks only the mapped bits. Without the bit set, a held/shift jump gets 'verified' on bits it never followed. (2) Bit wiring must include bitwise ops with a known identity operand: x & 1, x | 0, x ^ 0 are copies for that value. Without it, a masked shift register (r <= next & {2'b11, en, 5'b11111}) breaks every link and a correct chain becomes all-approximate; with it, a 30-step real chain went from 18 to 30 verified steps, and a ring that re-enters through rg[3] | inj (inj = 0) is now followed round to where inj was 1. (3) A held-value jump (value unchanged since T) is verifiable cheaply: the step at the read time must be exact and its last activation must be T (a later same-value rewrite is not proven). (4) Expect hand-written mock tests to flip to approximate: give mocks explicit wires / input-edge answers rather than weakening the rule. (5) An x through an operator can't use wires; verify instead by forcing the chosen input's x bits to 0 and to 1 and checking every traced x bit disappears.