Boolean and Word Level Integrated Engines for Hybrid Checking

Bowling 1 DIT-PRJ-03-005

Status NOT active project
DISI role Coordinator
Project type Industrial Project
Dimension International
Acquisition date 2003-02-25
Start date 2003-02-25
End date 2004-02-25
SAP code 40100605

Project details

Project astract Aim of this project is the investigation of extend SAT-based techniques that avoid flattening by working directly at a level of expressivity higher than boolean reasoning. This will enable to develop SAT-based tools for formal equivalence and property checking, able to scale up in the analysis of larger RTL designs. The investigation will rely on a representation formalism based on Hybrid Formulas, i.e. boolean combinations of both boolean propositions and propositions in more expressive theories. Typically such theories are decidable fragments of first-order theories (e.g. equality, linear and non-linear arithmetic over integers, uninterpreted functions), and allow us to directly represent abstract, structural and word-level information available in the RTL designs (e.g. memory stores, modular structure, word-level arithmetics). This project will target the development of a Hybrid SAT Solver, able to decide the satis- fiability of hybrid formulae. The hybrid SAT solver will be developed by extending state-of-the-art SAT procedures for boolean reasoning (that are extremely effective in dealing with the truly boolean components of the design) with dedicated reasoners for dealing with the non-boolean, mathematical theories. Key issue is the tight integration of the reasoners for the extended theories within the boolean SAT solver, in such a way that the ability to reason efficiently with boolean formulae is retained and fully exploited, and the complexity of (more expensive) reasoning in the extended theories is controlled as much as possible. Such hybrid SAT solver can be used for the development of SAT-based Hybrid Formal Checkers, such as Equivalence Checkers, Bounded Model Checkers, and Inductive Invariant Checkers, that are able to formally analyze designs at RTL avoiding boolean flattening. 1 The main objectives of the project can be outlined along the following lines: first, the identification of a general framework for hybrid SAT reasoning, which allows for a principled integration of a large class of mathematical theories of interest; second, the develpment of a hybrid SAT solver, tuned to efficiently reason about a wide class of theories needed to avoid boolean flattening of RTL designs; third, the development of hybrid formal checkers, based on the hybrid SAT solver defined at previous point, that are tuned to the specific problem being tackled (e.g. equivalence checking, bounded model checking, invariant checking).
Keywords formal verification
Fundings 21010 €
Partners
  • DIT
  • ITC-Irst, SRA Division
  • ITC-Irst

DISI Sub-project details

Project astract Same as the general project
Fundings 10505 €
Manager Roberto Sebastiani