UCSB SoC Design and Test Lab

Formal and semi-formal verification

CSAT : ATPG-based Combinational Circuit SAT Solver

C-SAT is a circuit sat solver implemented in C++. We call it "a CIRCUIT sat solver," instead of "a SAT solver" because our solver operates directly on circuits, rather than on those examples in CNF. Moreover, our solver performs the best if the input is given in multi-level circuit format.

C-SAT implements a new type of learning approach called Signal Correlation Guided Learning. Experimental results on public benchmarks and on difficult industrial test-cases demonstrated that our C-SAT solver could achieve orders-of-magnitude speedup over other state-of-the-art SAT solvers.

This solver is maintained by Feng Lu.

Publications:
• Feng Lu, Li-C. Wang, Kwang-Ting Cheng, Ric Huang, "A circuit SAT solver with signal correlation guided learning" In Proc. European Design and Test Conference, March 2003.
• Feng Lu, Li-C. Wang, Kwang-Ting Cheng, John Moondanos and Ziyad Hanna, "A Signal Correlation Guided ATPG Solver And Its Applications For Solving Difficult Industrial Cases" In Proc. Design Automation Conference, June 2003.