Level-Up - From Bits to Words

• Matthias Güdemann University of Applied Sciences Munich HM
• Klaus Riedl University of Applied Sciences Munich HM

Resumo

Model checking based on SAT solving has been successfully applied to hardware and software verification. Most of the time the verification is done on the single bit-level using Boolean logic to represent operations on atomic data types. With the extension of SAT solving to SMT solving, there exist solvers which can use more abstract reasoning on the word-level. SMT solvers support richer theories and allow for adding additional lemmas that can speed up verification. In this paper we show how a combination of bit and word-level analysis can speed up the verification of hardware models specified on the word-level. We combine the analysis efficiency of SAT solvers to identify bit-level information that is added to the word-level model. Effectively we use different bit-level invariant generation to augment word-level models. We validate the approach on the HWMCC word-level benchmarks using different integration strategies and state-of-the-art model-checkers.

Palavras-chave: Verification, SAT solvers