Automated reasoning about hardware data types using bit-vectors of symbolic lengths
Eric C. R. Hehner, Mark Christopher Pichora · 2003
Fixed length bit-vectors are a data type commonly used in hardware description languages. In generalizing fixed length bit-vectors, to permit bit-vectors with symbolic lengths, we develop a formal semantics for bit-vector formulas, decision procedures for quantifier-free satisfiability of two sub-languages, and a method for expanding the scope of these decision procedures to include rudimentary expressions in a functional hardware description language. The main application for our decision procedures and methods is the design and verification of parametric circuits. Our semantics of bit-vector formulas is model theoretic, and therefore, our theory of bit-vectors is consistent and counter-model-oriented. In a manner similar to propositional linear temporal logic, we investigate an extension of propositional tableaux, called bit-vector tableaux, specifically equipped to produce counter-models in the event that the input formulas are satisfiable. For the sub-language of bit-vectors to which they apply, bit-vector tableaux constitute a sound and complete proof system, and a terminating procedure for tableau construction is presented and shown to be correct. We further improve the utility of bit-vector tableaux by applying integer-valued function constraints which may be used to restrict the set of possible counter-models. Ultimately periodic functions constraining the integer variables used in the tableau are analyzed by viewing the generated tableau as an automaton whose open branches are accepting states. A second decision procedure evolves from the tableau-based procedure by applying conditional term rewriting to a more natural bit-vector sub-language. As in the case of tableaux, our conditional term rewriting systems are shown to be semantically correct and functionally correct; functional correctness is a syntactic property relating to the proper translation of formulas to the format required for bit-vector tableaux. Each of our conditional term rewriting systems is also shown to be terminating and confluent. A framework of extended bit-vectors, similar to data types built from lists, pairs and booleans in the functional programming language ML, is described. Reasoning about extended bit-vector properties is done symbolically, using a method of simplifying the types of variables involved, in order to apply our bit-vector decision procedures. Methods for translating counter-models and decomposing extended bit-vector properties are also suggested.