טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentEmmer Moshe
SubjectBounded Model Checking at Word Level via Encoding into
Effectively Propositional Logic
DepartmentDepartment of Electrical Engineering
Supervisors Professor Yoram Moses
Professor Ofer Strichman
Full Thesis textFull thesis text - English Version


Abstract

Use of theorem proving in hardware and software verification is not new. A first classification of the use of theorem proving in formal verification would be to divide it into Higher-Order Logic (HOL) and First-Order Logic (FOL) theorem proving. Because HOL theorem proving is highly interactive and requires from the user both an expertise in theorem proving and a good familiarity of the design (or program) under verification, the use of higher-order theorem proving in hardware verification is limited to particular styles of design for which no good fully-automatic verification methods exist. Unlike HOL, there are highly efficient, fully automatic theorem-provers for FOL, so the potential of FOL for a wider use in formal verification is significantly higher.


Word-level bounded model checking and equivalence checking problems are naturally encoded in the theory of bit-vectors and arrays. The standard practice of deciding formulas of such theories in the hardware industry is either SAT- (using bit-blasting) or SMT-based methods. These methods perform reasoning on a low level but perform it very efficiently. To find alternative potentially promising model checking and equivalence checking methods, a natural idea is to lift reasoning from the bit and bit-vector levels to higher levels. Although this is not easy due to low level of hardware description languages, it was proposed to translate equivalence and model-checking problems involving memory designs into the Effectively Propositional (EPR) fragment of first-order logic.


The first experiments with using such a translation have been encouraging but raised some questions. Since the high-level encoding was incomplete (yet avoiding bit-blasting) some equivalences could not be proved. Another problem was that there was no natural correspondence between models of EPR formulas and bit-vector based models that would demonstrate non-equivalence and hence design errors. We address these problems by providing more refined translations of equivalence checking problems arising from hardware verification into EPR formulas. We provide a number of such translations and formulate their properties. All three translations are designed in such a way that models of EPR problems can be translated into bit-vector models demonstrating non-equivalence.


We also evaluate the best EPR solvers on industrial equivalence checking problems and compare them with SAT and SMT solvers designed and tuned for such formulas specifically. We present empirical evidence demonstrating that EPR-based methods and solvers are competitive. We report experimental results for these problems for several provers known to be strong in EPR problem solving.