Certifaiger

Certifaiger checks the correctness of witness circuits in AIGER.

Quickstart

git clone https://github.com/Froleyks/certifaiger
cd certifaiger && make
# if resets are not stratified: make qbf
./build/check examples/01_model.aag examples/06_witness.aag

Check out the step-by-step example.

The scripts directory includes addititonal usage exapmles.

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 performs five checks. For an AIGER circuit $M$ we use $R, C, P$, F to refer to the symbolic formulas encoding that:

• The latches in $L$ are in their reset.
• All constraints hold.
• The property holds on the inputs and latches in $I ∪ L$, i.e. the bad or output is not set.
• The latches in $L₁$ are equal to the next of the matching latch in $L₀$. The two copies of the latches and inputs also implicitly define two temporal copies of the other formulas, i.e., $R₀$, $R₁$, $C₀, 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:

Reset	R{K} ∧ C ⇒ R’{K} ∧ C’
Transition	F{K} ∧ C0 ∧ C1 ∧ C0’ ⇒ F’{K} ∧ C1’
Property	(C ∧ C’) ⇒ (P ⇒ P’)
Base	R’ ∧ C’ ⇒ P’
Step	P0’ ∧ F’ ∧ C0’ ∧ C1’ ⇒ P1’

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.

Stratification

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$.

In case both circuits are stratified, the Reset check above ensures that the set $M$ is at the bottom of the semantic dependency graph of either circuit, 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$ and $L’$.

If either circuit is not stratified, it is not guaranteed that a partial reset can be extended. Therefore, Certifaiger implements the stronger check Reset^∃ if the polynomial stratification test fails.

Reset∃

$R(L) ⇒ ∃(L’ \setminus L): R’(L’)$

The explicit quantifier is necessary as otherwise every extension to $L’$ of a reset in $C$ (reduced to $M$) would need to be a valid reset in $C’$. This very strong condition would be unlikely to hold if $C’$ introduces any additional latches. Since the formula is checked for validity, we have the quantifier alternation ∃\forall when encoding Reset^∃ and are no longer in coNP. In practice, Certifaiger encodes Reset^∃ as a QAIGER circuit which is then translated to QCIR and checked with QuAbS. Certifaiger will pick the appropriate Reset check without further interaction; however, note that the tool will return exit code 15 if a QAIGER formula was produced. See check_certificate.sh for more details.

Witness Format

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

To allow the translation between the two 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 first bad or in the absence of that the first output is certified. Check out the examples directory.

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 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 et al.	FMCAD22
Towards Compositional Hardware Model Checking Certification	Yu, Froleyks & Biere et al.	FMCAD23
Certifying Phase Abstraction	Froleyks, Yu & Biere et al.	IJCAR24