SWORD: A SAT like prover using word level information

Robert Wille, Görschwin Fey, Daniel Große, Stephan Eggersglüß, Rolf Drechsler

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Scopus citations

Abstract

Solvers for Boolean Satisfiability (SAT) are state-of-the-art to solve verification problems. But when arithmetic operations are considered, the verification performance degrades with increasing data-path width. Therefore, several approaches that handle a higher level of abstraction have been studied in the past. But the resulting solvers are still not robust enough to handle problems that mix word level structures with bit level descriptions. In this paper, we present the satisfiability solver SWORD - a SAT like solver that facilitates word level information. SWORD represents the problem in terms of modules that define operations over bit vectors. Thus, word level information and structural knowledge become available in the search process. The experimental results show that on our benchmarks SWORD is more robust than Boolean SAT, K*BMDs or SMT.

Original languageEnglish
Title of host publicationVLSI-SoC
Subtitle of host publicationAdvanced Topics on Systems on a Chip: A Selection of Extended Versions of the Best Papers of the Fourteenth Int. Conf. on Very Large Scale Integration of System on Chip (VLSI-SoC2007)
EditorsRicardo Reis, Paul Hasler, Vincent Mooney
Pages175-191
Number of pages17
DOIs
StatePublished - 2009
Externally publishedYes

Publication series

NameIFIP International Federation for Information Processing
Volume291
ISSN (Print)1571-5736

Fingerprint

Dive into the research topics of 'SWORD: A SAT like prover using word level information'. Together they form a unique fingerprint.

Cite this