Memory models for the formal verification of assembler code using bounded model checking
Memory models for the formal verification of assembler code using bounded model checking
复制标题
使用有界模型检查对汇编代码进行形式化验证的内存模型
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
M. Zambaldi
中科院分区：
文献类型：
--
作者：
W. Ecker;Volkan Esen;T. Steininger;M. Zambaldi
使用硬件验证工具对汇编代码进行形式验证需要内存组件，例如保存代码本身和处理后的数据。由于要证明的变量数量通常随着数据大小和地址空间的增加而增加，因此可以快速达到正式工具的复杂性边界。由于有界模型检查（BMC）总是涉及一定的时间窗口，因此存储器访问的数量是有限的，因此就地址空间和门数的大小而言，可以优化所应用的存储器。在本文中，我们介绍了各种内存模型，它们通过应用此类优化来降低形式证明的复杂性。我们提供了具有地址空间或可存储数据量限制的模型示例。我们的分析表明，这些模型显着提高了性能，同时使用我们内部的 BMC 工具验证给定处理器单元的指令集
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 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