Certifaiger checks the correctness of witness circuits in AIGER.

git clone https://github.com/Froleyks/certifaiger
cd certifaiger && make
./bin/check examples/01_model.aag examples/06_witness.aag

Check out the step-by-step example.

The scripts directory includes additional usage examples.

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.

To check if a witness circuit is valid for a given model, Certifaiger performs five checks. For an AIGER circuit $M$ we use $C, P, R\{L\}, F\{L\}$ to refer to the symbolic formulas encoding that:

• All constraints hold.
• The property holds, i.e. the bad or output is not set.
• 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, …$

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. Our witness circuits may require the use of 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 $M’$, let $R, C, F, P, I, L$ and their primed version be the formulas from above and the set of all inputs and latches in the respective circuit, $K$ is the intersection of latches and inputs between the two. The five checks are:

For a witness and model that pass the first three checks, the witness is said to simulate the model. The last two check the inductiveness of the property in the witness circuit.

The validity of these formulas is checked by encoding their negation into combinatorial circuits, translated to CNF using aigtocnf, and checking unsatisfiability with Kissat or any other SAT solver. The produced certificates of unsatisfiability may additionally be checked by a verified proof checker. The entire certificate check is coNP in the size of the circuits.

Witness circuits are normal AIGER circuits in either ASCII or binary format.

Both the Reset and Transition checks are defined on the set of intersecting inputs and latches $M$. Requiring the witness circuit to keep the same variable indexing for $M$ would lead to gaps in the variable 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 $M$ the name must start with ‘=’ followed by the simulated literal in the model.

l0 = 2
l1 = 4
c
WITNESS o0 model.aig shasum 9f1747da5a7dd981c9dac13f4077c8e31c9ce50d

Certifaiger also allows to map latches and inputs 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:

c
MAPPING 2
12 2
17 4

Where, the number after MAPPING specifies how big the mapping is, and the lines following it list witness literal followed by simulated model literal.

To allow the translation between the ASCI and binary format 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 disjunction of all bads and outputs is certified. Check out the examples directory.

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 stratifed, the Reset check above ensures that the set of shared latches $M$ is at the bottom of the semantic dependency graph of $R’$, i.e., the reset of the latches in $M$ depends only on $M$. It follows that any reset of $M$ 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.

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 model checking algorithms with witness circuits.