학술논문
Memory models for the formal verification of assembler code using bounded model checking
Document Type
Conference
Author
Source
Seventh IEEE International Symposium onObject-Oriented Real-Time Distributed Computing, 2004. Proceedings. Object-oriented real-time distibuted computing Object-Oriented Real-Time Distributed Computing, 2004. Proceedings. Seventh IEEE International Symposium on. :129-135 2004
Subject
Language
Abstract
The formal verification of assembler code using hardware verification tools requires memory components, which e.g. hold the code itself and the processed data. Since the count of variables to be proven usually rises with both data-size and address-space, complexity boundaries of formal tools can be reached quickly. Since bounded model checking (BMC) always involves a certain time window and therefore the count of memory accesses is limited, it is possible to optimize the applied memory as far as the address-space and the size in the count of gates is concerned. We introduce various memory models, which decrease the complexity of formal proofs by applying such optimizations. We provide examples of models with limitations either of the address-space or the amount of storable data. Our analysis shows that these models remarkably enhance the performance, while verifying the instruction-set of a given processor-unit with our in-house BMC-Tool.