CondEC: Equivalence Checking under Conditions

If you find this project useful, please give us a star🌟.

Wenbin Che, Changyuan Yu, Hongce Zhang^✉️

The Hong Kong University of Science and Technology (Guangzhou)

^✉️Corresponding Author

Description

CondEC is a constraint-aware framework for conditional equivalence checking, where functional equivalence is required only under user-specified conditions rather than over the entire input space. Unlike conventional combinational equivalence checking, which assumes full input-space equivalence and treats constraints as auxiliary Boolean logic, CondEC explicitly incorporates functional constraints into the equivalence checking workflow. This enables efficient verification of designs whose equivalence holds only in semantically meaningful operating modes.

Setup

Dependencies:

• C++17 compiler (e.g., g++)
• CaDiCaL (v3.0.0)
• AIGER library sources (included: aiger.c/.h)

Install CondEC and CaDiCaL from the project root:

git clone https://github.com/WBChe/CondEC
cd ./CondEC
git clone https://github.com/arminbiere/cadical.git
cd ./cadical
git checkout 7b99c07f0bcab5824a5a3ce62c7066554017f641
./configure && make
cd ..

Quickstart

Build:

make

Run:

./condec <aigfile> [-option]

Common options:

• -h print help
• -q quiet mode (only prints final result and time)

Example:

./condec benchmarks/aig/aa1_cond.aig

Experiment

CondEC has been evaluated on a diverse set of industrial-style and competition benchmarks, including constrained datapath and arithmetic-intensive designs. Batch evaluation uses test.sh and processes all benchmarks/aig/*.aig files. It writes a CSV summary to results.csv.

./test.sh

For SAT solver (ensure the solver is properly installed and the paths in the .sh scripts are correctly configured):

./test_kissat.sh # for kissat test

./test_cadical.sh # for cadical test

For ABC (ensure ABC is installed):

abc -c "&r benchmarks/aig-and-output/*.aig; &cec -m;" # for one test

./test_abc-cec.sh # for all test

Acknowledgment

Our work is primarily based on the following codebases. We are sincerely grateful for their work.

• CaDiCaL SAT solver
• AIGER circuit format and parser