Memory models for the formal verification of assembler code using bounded model checking

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.