Applying SMT in symbolic execution of microcode

Author

Franzén, Anders ; Cimatti, Alessandro ; Nadel, Alexander ; Sebastiani, Roberto ; Shalev, Jonathan

Author_Institution

DISI, Univ. Trento, Trento, Italy

fYear

2010

fDate

20-23 Oct. 2010

Firstpage

121

Lastpage

128

Abstract

Microcode is a critical component in modern microprocessors, and substantial effort has been devoted in the past to verify its correctness. A prominent approach, based on symbolic execution, traditionally relies on the use of boolean SAT solvers as a backend engine. In this paper, we investigate the application of Satisfiability Modulo Theories (SMT) to the problem of microcode verification. We integrate MathSAT, an SMT solver for the theory of Bit Vectors, within the flow of microcode verification, and experimentally evaluate the effectiveness of some optimizations. The results demonstrate the potential of SMT technologies over pure boolean SAT.

Keywords

Boolean functions; computability; firmware; multiprocessing systems; program verification; MathSAT; SMT solver; SMT technology; backend engine; bit vectors; boolean SAT solvers; microcode verification; microprocessors; satisfiability modulo theory; symbolic execution; Cognition; Computers; Data structures; Engines; Instruments; Microarchitecture; Program processors;

fLanguage

English

Publisher

ieee

Conference_Titel

Formal Methods in Computer-Aided Design (FMCAD), 2010

Conference_Location

Lugano

Print_ISBN

978-1-4577-0734-6

Electronic_ISBN

978-0-9835678-0-6

Type

conf

Filename

5770940