DocumentCode :
2380144
Title :
SWORD: A SAT like prover using word level information
Author :
Wille, Robert ; Fey, Görschwin ; Grobe, Daniel ; Eggersgluss, Stephan ; Drechsler, Rolf
Author_Institution :
Institute of Computer Science, University of Bremen, 28359, Germany
fYear :
2007
fDate :
15-17 Oct. 2007
Firstpage :
88
Lastpage :
93
Abstract :
Solvers for Boolean Satisfiabilily (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.
Keywords :
Arithmetic; Boolean functions; Computer science; Data structures; Degradation; Digital circuits; Formal verification; Integer linear programming; Robustness; Surface-mount technology;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Very Large Scale Integration, 2007. VLSI - SoC 2007. IFIP International Conference on
Conference_Location :
Atlanta, GA, USA
Print_ISBN :
978-1-4244-1709-4
Electronic_ISBN :
978-1-4244-1710-0
Type :
conf
DOI :
10.1109/VLSISOC.2007.4402478
Filename :
4402478
Link To Document :
بازگشت