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. 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.