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.