USAT: An Integrated Platform for Satisfiability Solving and Model Checking
Weimin Wu, Min-Chuan Chen · 2008
A platform named USAT that integrates several gate-level and RTL satisfiability solvers is described. USAT has a unified circuit model that can represent both gate-level and RTL circuits. USAT integrates other solvers by translating between various circuit formats via the unified circuit model. USAT also includes a circuit generator that can generate RTL circuits with specific features specified by users. USAT also has a native ATPG-based solver that can solve satisfiability problem at both gate-level and RTL. The effectiveness of USAT is demonstrated by applications in bounded model checking.