Title :
SATIRE: A new incremental satisfiability engine
Author :
Whittemore, Jesse ; Kim, Joonyoung ; Sakallah, Karem
Author_Institution :
Michigan Univ., MI, USA
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;
Conference_Titel :
Design Automation Conference, 2001. Proceedings
Print_ISBN :
1-58113-297-2
DOI :
10.1109/DAC.2001.156198
