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

Volume

4

fYear

2008

fDate

12-14 Dec. 2008

Firstpage

87

Lastpage

90

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Science and Software Engineering, 2008 International Conference on

Conference_Location

Wuhan, Hubei

Print_ISBN

978-0-7695-3336-0

Type

conf

DOI

10.1109/CSSE.2008.1352

Filename

4722570