Decision Procedures for Quantifier-free Bit-vectors of Symbolic Length

languages, can be used to reason about parametric circuits such as
mutlipliers, caches and arbiters. In order to support the verification
of these generic hardware descriptions, I have developed a formal
syntax, a formal semantics, several decision procedures and methods
for widening their scope.

My decision procedures are based on an extended version of propositional
tableaux (similar in some ways to Wolper's linear temporal logic
tableaux) and conditional term rewriting. In addition to emphasizing
proofs as the product of successful runs of the decision procedures,
my decision procedures can provide counter-models to false properties.

In this talk, I will describe the bit-vector satisfiability problems
decided, and how they apply to parametric circuits. I will also sketch
how a problems in a more expressive language of extended bit-vectors
(including arbitrary arrays of bits and their operations), can be
solved with my decision procedures for the flat bit-vector languages.
In addition, I contrast my framework with that of other formalisms
(which have comparable decision procedures) for describing parametric
circuits (such as M2L, WS1S, and LIFs).