Range Allocation for Equivalence Logic
The range allocation problem was recently introduced as part of an efficient decision procedure for deciding satisfiability of equivalence logic formulas with or without uninterpreted functions. These type of formulas are mainly used when proving equivalence or refinement between systems (hardware designs, compiler’s translation, etc). The problem is to find in polynomial time a small finite domain for each of the variables in an equality formula φ, such that φ is valid if and only if it is valid over this small domain. The heuristic that was presented for finding small domains was static, i.e. it finds a small set of integer constants for each variable. In this paper we show new, more flexible range allocation methods. We also show the limitations of these and other related approaches by proving a lower bound on the size of the state space generated by such procedures. To prove this lower bound we reduce the question to a graph theoretic counting question, which we believe to be of independent interest.
KeywordsState Space Equivalence Logic Small Domain Boolean Variable Boolean Formula
Unable to display preview. Download preview PDF.
- BD94.J.R. Burch and D.L. Dill, “Automatic Verification of Microprocessor Control”, In Computer-Aided Verification CAV’ 94.Google Scholar
- BDL96.Clark W. Barrett, David L. Dill and Jeremy R. Levitt, “Validity Checking for Combinations of Theories with Equality”, In Formal Methods in Computer Aided Design FMCAD’ 96.Google Scholar
- BV00.R. E. Bryant and M. N. Velev, “Boolean satisfiability with transitivity constraints”, In Computer-Aided Verification CAV 2000.Google Scholar
- GSZAS98.A. Goel, K. Sajid, H. Zhou, A. Aziz and V. Singhal, “BDD Based Procedures for a Theory of Equality with Uninterpreted Functions”, In Computer-Aided Verification CAV’ 98.Google Scholar
- PRSS98.A. Pnueli, Y. Rodeh, M. Seigel and O. Shtrichman, “Deciding Equality Formulas by Small Domain Instantiations”, In Computer-Aided Verification CAV’ 99.Google Scholar
- PSS98.A. Pnueli, M. Siegel and O. Shtrichman, “Translation Validation for Synchronous Languages”, In International Colloquium on Automata, Languages and Programming ICALP’ 98.Google Scholar
- RS01.Y. Rodeh and O. Shtrichman, “Finite Instantiations in Equivalence Logic with Uninterpreted Functions”, In Computer-Aided Verification CAV’ 01.Google Scholar