Title slide: hardware model checking certification at two abstraction levels.
Four latches start at zero, selecting the initial graph state.
The selected inputs pick an outgoing edge of the current state.
The latch values update and the highlighted current state moves at the same time.
After five input choices, the reached state violates P, so the highlighted path is a bad trace.
At word level, the variables are bitvectors and the circuit operations include addition and multiplication.
A model checker returns a counterexample for unsafe answers or a witness circuit for safe answers.
Certifaiger and Cerbtora independently validate the model and witness circuit at the bit and word levels.
The witness simulates the model and carries an inductive safety property.
Reset, Transition, and Property establish the simulation relation.
Base and Step make the witness property inductive; together, these are the five conditions.
The model has eight states, with reset at 000 and the bad state marked at 111.
The complete eight-state model and the derived four-state witness now remain visible side by side.
The bit-level and word-level witnesses appear beside their models; no model information is removed.
Certifaiger checks the bit-level pair; Cerbtora checks the word-level pair.
The check command dispatches bad traces and witness circuits to their matching verification tools.
Unlike the bit-level SAT path, the Bitwuzla path still lacks a proof-checking endpoint.
The certified wrapper calls check and the model checker; fuzz adds the bit-level or word-level input generator above them.
Bit blasting translates both the word-level model and its certificate before Certifaiger checks their bit-level equivalents.
A bug in either translation becomes part of the trusted path, even when the final bit-level check succeeds.
These real fixes illustrate the extra implementation risk introduced by bitvector translation.
Formula generation is negligible, SAT features are essential, and LRAT proof checking raises CaDiCaL's PAR10 by a factor of 1.69.
Across all 47 certificates, word-level checking uses 23 percent less time in total.
Word-level witnesses are five times smaller in geometric mean, and smaller on 42 of 47 cases.