Flexible and formal modeling of microprocessors with application to retargetable simulation
Flexible and formal modeling of microprocessors with application to retargetable simulation
复制标题
灵活、形式化的微处理器建模及其可重定向仿真的应用
DOI：
10.1109/date.2003.1253667
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
S. Malik
中科院分区：
文献类型：
--
作者：
W. Qin;S. Malik
考虑到特定于应用程序的处理器的增长，迫切需要一个可重新定位的建模框架，该框架能够准确捕获复杂的处理器行为并生成高效的模拟器。我们提出了操作状态机（OSM）计算模型作为该建模框架的基础。OSM模型将处理器分为两个交互层：操作层，其中操作语义和时序建模；硬件层，其中规范的硬件单元进行交互。这种声明性模型允许直接合成微体系结构模拟器，因为它封装了微处理器的精确并发语义。通过对StrongARM内核和PowerPC-750超标量处理器的实例分析，说明了该模型的实际应用价值。实验结果表明，OSM模型具有良好的建模生产力和建模效率。此建模框架的其他应用包括编译器所需的信息派生和处理器验证的形式化分析。
Given the growth in application-specific processors, there is a strong need for a retargetable modeling framework that is capable of accurately capturing complex processor behaviors and generating efficient simulators. We propose the operation state machine (OSM) computation model to serve as the foundation of such a modeling framework. The OSM model separates the processor into two interacting layers: the operation layer where operation semantics and timing are modeled, and the hardware layer where disciplined hardware units interact. This declarative model allows for direct synthesis of micro-architecture simulators as it encapsulates precise concurrency semantics of microprocessors. We illustrate the practical benefits of this model through two case studies - the StrongARM core and the PowerPC-750 superscalar processor The experimental results demonstrate that the OSM model has excellent modeling productivity and model efficiency. Additional applications of this modeling framework include derivation of information required by compilers and formal analysis for processor validation.