DocumentCode
1747942
Title
SATIRE: A new incremental satisfiability engine
Author
Whittemore, Jesse ; Kim, Joonyoung ; Sakallah, Karem
Author_Institution
Michigan Univ., MI, USA
fYear
2001
fDate
2001
Firstpage
542
Lastpage
545
Abstract
We introduce SATIRE, a new satisfiability solver that is particularly suited to verification and optimization problems in electronic design automation. SATIRE builds on the most recent advances in satisfiability research, and includes two new features to achieve even higher performance: a facility for incrementally solving sets of related problems, and the ability to handle non-CNF constraints. We provide experimental evidence showing the effectiveness of these additions to classical satisfiability solvers.
Keywords
Boolean functions; automatic test pattern generation; circuit optimisation; computability; design for testability; electronic design automation; formal verification; logic CAD; logic testing; ATPG; SATIRE; electronic design automation; incremental satisfiability engine; incremental solution; logic design; logic testing; nonCNF constraints; optimization problems; verification; Algorithm design and analysis; Application software; Electronic design automation and methodology; Engines; Field programmable gate arrays; Large-scale systems; Pattern analysis; Permission; Test pattern generators; Timing;
fLanguage
English
Publisher
ieee
Conference_Titel
Design Automation Conference, 2001. Proceedings
ISSN
0738-100X
Print_ISBN
1-58113-297-2
Type
conf
DOI
10.1109/DAC.2001.156198
Filename
935567
Link To Document