<i>CirOPT</i> : Toward Effective Combinational Equivalence Checking via Compiler Optimization

Combinational equivalence checking (CEC) is essential for verifying the correctness of circuit designs. With the growing complexity of circuits, effective verification techniques have become increasingly critical. Recently, a conjunctive normal form (CNF)-based approach, converting circuits to CNF for Boolean satisfiability (SAT) solvers, has shown competitive performance compared to state-of-the-art hybrid SAT sweeping approaches. The capability of this CNF-based approach depends on effective CNF conversion. This work presents <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">CirOPT</i>, which is the first CNF conversion method using compiler optimization to equivalently simplify circuits. Extensive experiments are conducted on a broad range of real-world benchmarks, which are far more than the number of benchmarks typically used in empirical studies. The results reveal that, when paired with the state-of-the-art CNF SAT solver <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">Kissat</i>, <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">CirOPT</i> considerably outperforms existing approaches in CEC.