README.org

• Certifaiger #+html: [[https://github.com/Froleyks/certifaiger][Certifaiger]] checks the correctness of witness circuits in [[https://github.com/arminbiere/aiger][AIGER]].

** Quickstart

#+begin_src bash git clone https://github.com/Froleyks/certifaiger cd certifaiger && make test #+end_src

Check out the step-by-step examples in [[https://github.com/Froleyks/certifaiger/blob/main/tests][tests]].

The [[https://github.com/Froleyks/certifaiger/blob/main/scripts/README.org][scripts]] directory includes additional usage examples. ** Motivation Model checking is an essential technique for hardware design. For unsafe circuits, those that violate the property being checked, it is usually easy to produce a trace to demonstrate the flaw. In cases where the model checking succeeds, a certificate should be produced that proves the property indeed holds for all possible traces. We propose /witness circuits/ as a format for these certificates. A witness circuit generalizes the concept of an inductive invariant.

Instead of searching for an inductive invariant in the model itself, we find a different circuit---the witness---that simulates part of the model and has an inductive invariant. ** Witness circuits To check if a witness circuit is valid for a given model, Certifaiger emits SAT checks for the simulation, inductiveness, and ranking obligations below. For an AIGER circuit $M$ we use $C, P, Q, R\{L\}, F\{L\}$ to refer to the symbolic formulas encoding that:

• All constraints hold.
• The safety property holds, i.e. all /bad/ signals are unset.
• The liveness property (combination of fairness and justice) holds.
• The latches in $L$ are in their reset.
• The latches in $L_1$ are equal to their /next/ state functions applied to $L_0, I_0$. The two copies of the latches and inputs also implicitly define two temporal copies of the other formulas, i.e., $R_0$, $R_1$, $C_0$, $C_1$, \dots

These formulas can be encoded as combinatorial AIGER circuits by replacing latches with inputs, resulting in a DAG with a single output and leaves ending in inputs or constants.

Note that we use a (slightly) modified version of the AIGER 1.9 format. Models and witnesses may use /reset functions/, that is, latches may be reset to other latches or gates, instead of just constants (or staying uninitialized).

For a model $M$ and witness circuit $W$, let $R, C, F, P, Q, I, L$ and their primed versions be the formulas from above and the sets of all inputs and latches in the respective circuit. Let $K$ be the mapped shared latches between model and witness. Certifaiger uses three time points $s,t,u$ and checks: *** Simulation | Reset | R_{s}{K} \wedge C_{s} \rightarrow R'{s}{K} \wedge C'{s} | | Transition | F_{st}{K} \wedge C_{s} \wedge C_{t} \wedge C'{s} \rightarrow F'{st}{K} \wedge C'{t} | | Safety | C{s} \wedge C'{s} \wedge P'{s} \rightarrow P_{s} | | Liveness | \wedge_{i\in s,t}(C_{i} \wedge C'{i} \wedge P'{i}) \wedge F'{st}{L'} \rightarrow \wedge{q\in Q}(q'{st}\rightarrow q{st}) | *** Inductive | Base | R'{s}{L'} \wedge C'{s} \rightarrow P'{s} | | Inductive | F'{st}{L'} \wedge C'{s} \wedge C'{t} \wedge P'{s} \rightarrow P'{t} | *** Ranked | Decrease | \wedge_{i\in s,t}(C'{i} \wedge P'{i}) \wedge F'{st}{L'} \rightarrow Q'{ts} | | Closure | \wedge_{i\in s,t,u}(C'{i} \wedge P'{i}) \wedge F'{st}{L'} \wedge Q'{su} \rightarrow Q'{tu} | | Consistent | \wedge{i\in s,t,u}(C'{i} \wedge P'{i}) \wedge F'{st}{L'} \wedge F'{tu}{L'} \wedge Q'{st} \wedge Q'{tu} \rightarrow \wedge_{q\in Q'}(q'{st}\rightarrow q'{tu}) |

Here $Q'$ is used as the disjunction of all signals in one liveness property (fairness + justice). If a witness simulates a model, its safety and liveness imply the same properties in the model. An inductive circuit is safe, and a ranked circuit is live.

The validity of these formulas is checked by encoding their negation into combinatorial circuits, translating them to CNF using [[https://github.com/arminbiere/aiger][aigtocnf]], and checking unsatisfiability with [[https://github.com/arminbiere/kissat][Kissat]] or any other SAT solver. When built with make lrat-trim, [[https://github.com/arminbiere/cadical][CaDiCaL]] is used instead and LRAT proofs are streamed directly into [[https://github.com/arminbiere/lrat-trim][lrat-trim]]. For even higher assurance, the fully verified [[https://github.com/lammich/lrat_isa][lrat_isa]] offers similar performance, but requires the Boost library to build.

The entire certificate check is coNP in the size of the circuits. ** Witness Format Witness circuits are normal AIGER circuits in either ASCII or binary format.

Requiring the witness circuit to keep the same variable names for their intersection $K$ would lead to gaps in the indexing. This, in turn, would prohibit storing the witness in the binary format since it requires the inputs and latches to be indexed consecutively before any gate. Instead, the witness can store an explicit mapping of its inputs and latches to the simulated literals in the model in its symbol table. Other information may be stored, but for elements of $K$ the /name/ must start with '=' followed by the simulated literal in the model. #+begin_example l0 = 2 l1 = 4 c WITNESS o0 model.aig shasum 9f1747da5a7dd981c9dac13f4077c8e31c9ce50d #+end_example

Certifaiger also allows latches and inputs to be mapped to gates in the witness circuit, which might be necessary for certifying certain techniques (e.g. retiming). However, since those cannot be expressed in the symbol table, the mapping has to be specified in a comment as follows: #+begin_example c MAPPING 2 12 2 17 4 #+end_example The number after MAPPING specifies the size of the mapping, and the following lines list witness literals followed by simulated model literals.

The /Intervention/ mapping is similar and allows a witness to define its liveness signals as edge predicates in the state space. Whenever a witness liveness signal q'_{ij} is encoded in the conditions above, the right-hand side is replaced with the left-hand side in copy j. To define intervention mappings, use '<' in the symbol table or a comment beginning with INTERVENTION.

To allow translation between the ASCII and binary formats without breaking the mapping, Certifaiger enforces consecutive indexing for inputs and latches, even in ASCII format.

While not required, it is recommended to include a comment starting with 'WITNESS' followed by the property being certified and the name of the model file. Additionally, a hash may be included.

If no mapping information is found, Certifaiger assumes that the first $n$ inputs in the model are simulated by the first $n$ inputs in the witness, and the first $m$ latches by the first $m$ latches in the witness. The default intervention replaces, the next-state function literal of each latch with the latch value in the next (second index) state. The safety property is the conjunction of all negated bad signals. For old AIGER files without bad or justice properties, outputs are treated as bad signals. Check out the [[https://github.com/Froleyks/certifaiger/blob/main/tests][tests]] directory. ** Stratified Reset A circuit is said to be stratified if the syntactic dependency graph induced by its reset function is acyclic. This is usually not a big restriction and fairly common in practice. Since in the original AIGER format latches can only be reset to constants, stratification is trivial. The /semantic dependency graph/ is the subset of the syntactic dependency graph, where an edge $(a, b)$ indicates that an assignment exists where a change in $b$ would imply a change in $a$.

If the witness circuit is stratified, the Reset check above ensures that the set of shared latches $K$ is at the bottom of the semantic dependency graph of $R'$, i.e., the reset of the latches in $K$ in the intersection depends only on inputs and latches in the intersection. It follows that any reset of $K$ can be extended to a reset of $L'$.

If the witness circuit is not stratified, it is not guaranteed that a partial reset can be extended, and Certifaiger will fail. ** References The theory this tool is based on is detailed in our papers. Furthermore, we demonstrate how to certify the combination of different preprocessing techniques and safety and liveness model checking algorithms with witness circuits. | Progress in Certifying Hardware Model Checking Results | Yu, Biere, Heljanko | CAV21 | | Stratified Certification for K-Induction | Yu, Froleyks, Biere, Heljanko | FMCAD22 | | Towards Compositional Hardware Model Checking Certification | Yu, Froleyks, Biere, Heljanko | FMCAD23 | | Certifying Phase Abstraction | Froleyks, Yu, Biere, Heljanko | IJCAR24 | | Introducing Certificates to the Hardware Model Checking Competition | Froleyks, Yu, Preiner, Biere, Heljanko | CAV25 | | Hardware Model Checking Certification with Certifaiger and Cerbtora | Froleyks, Yu | IJCAR26 | | Liveness Proofs for Hardware Model Checking | Froleyks, Yu, Bogaerts, Biere, Heljanko | CAV26 |