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
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;
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
DOI :
10.1109/VLSISOC.2007.4402478