Symbolic Procedures for a Theory of Equality
(joint work with Adnan Aziz, Anuj Goel and Khurram Sajid)
We present a novel approach of using BDDs for the problem of verifying formulas in the theory of quality with uniterpreted functions (UIFs). Burch and Dill have shown that pipeline verification can be reduced to such a verification problem, through an abstraction of arithmetic and memory units by UIFs.
Currently, all practical methods for verification in this theory proceed by case splitting on terms occuring in the formula; heuristic rewriting of subformulas is also performed. Based on experiences with analogous approaches for propositional verification, we predict that these techniques may not be viable as the examples get larger or more complex, especially when the examples are not hand designs but are outputs of automatic CAD tools, e.g. high-level synthesis tools. The situation may be similar to propositional logic checking, where the original tools were also based on case splitting (e.g. ATPG-based methods); they have now be largely supplanted by BDD-based methods. (ATPG-based methods still work better for satifiability problems, e.g. test generations for combinational stuck-at-faults).
Recently, Hojati and others presented a BDD-based method for the verification problem with UIFs. Their results were negative, and were directly caused by the absence of a good BDD variable ordering. Our experiments corroborate this. We have since developed a new approach for encoding the UIF verification problem with BDDs which results in significantly improved runtimes, and enjoys nice theoretical properties. We present this approach in this talk.