![[Moi Meme]](m1.jpg)
I have graduated. I am currently employed at OANDA.
New: Twig a bit-vector decision procedure tool (an early unstable release).
Automated reasoning about hardware data types using bit-vectors of symbolic length
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 strongly-typed functional programming language ML, is described. Reasoning about extended bit-vector properties is done symbolically, using a method of simplifying the types of variables used in the properties, in order to apply our bit-vector decision procedures. Methods for translating counter-models and decomposing extended bit-vector properties are also suggested.
Body of the thesis
This is available in three formats:
Appendices of the thesis
This part is rather dry in any case, and I do not recommend that you print it. It is also available in three formats:
Questions? e-mail me: mpichora at cs dot utoronto dot ca