Title :
USAT: An Integrated Platform for Satisfiability Solving and Model Checking
Author :
Wu, Wei-Min ; Chen, Min-Chuan
Author_Institution :
Dept. of Comput. Eng., Beijing Jiaotong Univ., Beijing
Abstract :
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.
Keywords :
automatic test pattern generation; circuit CAD; computability; formal verification; ATPG-based solver; RTL circuits; RTL satisfiability USAT; RTL satisfiability solver; circuit formats; circuit generator; gate-level circuits; gate-level satisfiability solver; integrated platform; model checking; satisfiability problem; satisfiability solving; unified circuit model; Asia; Automatic test pattern generation; Circuits; Computer science; Data structures; Formal verification; NP-complete problem; Registers; Software engineering; Terminology; RTL (register transfer level); model checking; satisfiability;
Conference_Titel :
Computer Science and Software Engineering, 2008 International Conference on
Conference_Location :
Wuhan, Hubei
Print_ISBN :
978-0-7695-3336-0
DOI :
10.1109/CSSE.2008.1352