TY - GEN
T1 - Memory models for the formal verification of assembler code using bounded model checking
AU - Ecker, Wolfgang
AU - Esen, Volkan
AU - Steininger, Thomas
AU - Zambaldi, Martin
PY - 2004
Y1 - 2004
N2 - 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. In this paper we introduce various memory models, which decrease the complexity of formal proofs by applying such optimizations. We will provide examples of models with limitations either of the address-space or the amount of storable data. Our analysis will show that these models remarkably enhance the performance, while verifying the instruction-set of a given processor-unit with our in-house BMC-Tool.
AB - 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. In this paper we introduce various memory models, which decrease the complexity of formal proofs by applying such optimizations. We will provide examples of models with limitations either of the address-space or the amount of storable data. Our analysis will show that these models remarkably enhance the performance, while verifying the instruction-set of a given processor-unit with our in-house BMC-Tool.
UR - http://www.scopus.com/inward/record.url?scp=4544365536&partnerID=8YFLogxK
U2 - 10.1109/ISORC.2004.1300338
DO - 10.1109/ISORC.2004.1300338
M3 - Conference contribution
AN - SCOPUS:4544365536
SN - 076952124X
SN - 9780769521244
T3 - Proceedings - Seventh IEEE International Symposium on Object-Oriented Real-Time Distributed Computing
SP - 129
EP - 135
BT - Proceedings - Seventh IEEE International Symposium on Object-Oriented Real-Time Distributed Computing
A2 - Gustafsson, J.
A2 - Aoki, T.
A2 - Lee, I.
T2 - Proceedings - Seventh IEEE International Symposium on Object-Oriented Real-Time Distributed Computing
Y2 - 12 May 2004 through 14 May 2004
ER -