Cerbotor checks the correctness of witnesses in the Btor2 format.
git clone https://github.com/Froleyks/cerbotor
cd cerbotor
cmake -DCMAKE_BUILD_TYPE=Release -DTOOLS=ON -B build
make -j$(nproc) -C build
./build/bin/check examples/model.btor2 examples/witness.btor2
#expected usage: ./<your_model_checker> <model> <witness>
./build/bin/fuzzer ./<your_model_checker>Model checking is an essential technique for hardware design. For unsafe designs, 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, Cerbotor performs five checks:
| 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’ |
Where
If a witness and model 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 Btor2, and checking unsatisfiability with Bitwuzla.
Witness circuits are normal Btor2 files.
Both the Reset and Transition checks are defined on the intersection between model and witness
1 sort bitvec 1 2 zero 1 3 state 1 =8 4 init 1 3 2 5 next 1 3 3 6 bad 3
If no mapping information is found, Cerbotor assumes that
the first
The theory this tool is based on is detailed in our papers. Beyond that, 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 |
Cerbotor itself depends on make, cmake, a c++ compiler, and git to fetch the btor2tools dependency. With cmake -DTOOLS=ON additional tools are built, namely fuzzbtor2 and the bitvector SMT solver bitwuzla. The latter brings the additional dependencies of meson and m4.
A static Cerbotor binary can be built with cmake -DSTATIC=ON.
Checkout the Dockerfile for more details or directly run the container:
docker build -t cerbotor .
docker run --rm cerbotor examples/model.btor2 examples/witness.btor2In addition to Cerbotor, the TOOLS option builds a number of useful scripts in the build/bin directory:
- check <model> <witness>
- checks the first line of the witness to decide if it is a Btor2 model to certify safety or a Btor2 trace to certify unsafety. Then runs Cerbotor and bitwuzla or btorsim respectively.
- generate [seed]
- Produces a random Btor2 model. Ensures that it is compatible with the current version of btor2sim.
- certified <model checker> <model>
- Runs the model checker and checks the produced certificate. The model checker is expected to take the first argument as the model path and write a (sat or unsat) certificate to the path provided in the second argument.
- fuzzer <model checker> [threads]
- Executes the model checker on random Btor2 models in multiple threads and checks the produced certificates. Error inducing models are collected in build/bugs.