Verifying micro-architecture simulators using event traces
Verifying micro-architecture simulators using event traces
复制标题
使用事件跟踪验证微架构模拟器
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Zhenlin Wang
中科院分区：
文献类型：
--
作者：
Hui Meen Nyew;Nilufer Onder;Soner Önder;Zhenlin Wang
当代微架构研究本质上依赖于周期精确的模拟器来测试新的想法。典型的模拟器实现涉及数万行高级代码。尽管可以应用通用软件工程验证和确认技术，但模拟器的复杂性使得使用形式化技术变得困难，并且需要特定于领域的知识作为验证过程的一部分。该域特定信息包括对流水线级和指令相对于这些级的时序行为进行建模。
我们提出了一种模拟器验证的方法，使用特定于域的信息，以有效地捕捉潜在的不匹配之间的假设的架构模型和它的模拟器。我们首先讨论如何模拟器生成的事件跟踪可以被送入一个自动生成的验证程序从一阶逻辑规范，以验证模拟器遵守的不变量。然后，我们展示了从跟踪中提取模拟器行为的技术，并以图形和规则的形式将结果呈现给用户。前者通过检查模型不变式来确保实现的正确性，而后者则试图推导出实现的扩展模型，从而更深入地了解实现了什么。
我们的技术适用于任何微体系结构模拟器。我们提出的应用程序，我们的技术，手写的模拟器，以及从一个架构规范语言生成的。
Contemporary micro-architecture research inherently relies on cycle-accurate simulators to test new ideas. Typical simulator implementations involve tens of thousands of lines of high-level code. Although general software engineering verification and validation techniques can be applied, the mere complexity of simulators makes using formal techniques difficult and calls for domain-specific knowledge to be a part of the verification process. This domain-specific information includes modeling the pipeline stages and the timing behavior of instructions with respect to these stages.
We present an approach to simulator verification that uses domain-specific information to effectively capture a potential mismatch between the assumed architecture model and its simulator. We first discuss how a simulator-generated event trace can be fed into an automatically generated verification program from a first-order logic specification to verify that the simulator obeys the invariants. We then show techniques that extract simulator behavior from traces and present the results to the user in the form of graphs and rules. While the former seeks an assurance of implementation correctness by checking that the model invariants hold, the latter attempts to derive an extended model of the implementation and hence enables a deeper understanding of what was implemented.
Our techniques are applicable to any micro-architecture simulator. We present the application of our techniques to hand-written simulators as well as to those generated from an architecture specification language.