Scalable Synthesis of Safety Games and Low-Power Retention Using Satisfiability Solving
Date Issued
2015
Date
2015
Author(s)
Chiang, Ting-Wei
Abstract
In the domain of electronic design automation (EDA), various tough combinatorial optimization and decision can be formulated as the satisfiability (SAT) problem and tackled by advanced SAT solvers. For the past decades, extensive efforts have been devoted to make SAT solver efficient. Many applications, such as formal verification and logic synthesis, adopt SAT solvers as the core engine and benefit greatly from the improvement of SAT solvers. In this thesis, we apply advanced SAT solving techniques to two applications, synthesis of reactive systems from safety specifications and retention register minimization in low-power design. For the former, we are inspired by the state-of-the-art model checking algorithm emph{property-directed reachability} (PDR, a.k.a. IC3) and propose a SAT-based synthesis algorithm that extends the PDR by adopting the concept of interactive SAT solving for two-level quantified Boolean formulas (2QBF). For the latter, we exploit incremental SAT solving, high level symbolic simulation and unsatisfiable (UNSAT) core analysis to greatly reduce runtime overhead. Experimental results show that our proposed algorithm for the former problem outperform the existing SAT-based and QBF-based algorithms by some margin and the method for the latter problem is effectively applicable to industrial designs.
Subjects
Satisfiability Problem
Synthesis of Reactive Systems
Property-directed Reachability
Incremental SAT Solving
Retention Register
Low-power Design
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-104-R02943088-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):351b5919a4903f9cc0368463380dfc62