Managing Complexity through Abstraction: A Refinement-Based Approach to Formalize Instruction Set Architectures
Managing Complexity through Abstraction: A Refinement-Based Approach to Formalize Instruction Set Architectures
复制标题
通过抽象管理复杂性：一种基于细化的指令集架构形式化方法
DOI：
10.1007/978-3-642-24559-6_39
复制
发表时间：
2011
影响因子：
1.8
通讯作者：
D. May
中科院分区：
文献类型：
--
作者：
F. Yuan;Stephen Wright;K. Eder;D. May
验证处理器的功能正确性需要对其指令集体系结构（ISA）进行声音和完整的规范。当前的工业实践是使用自然语言在非正式的情况下以添加半正式表示法来描述处理器的ISA，以捕获说明的功能意图。这留下了错误和不一致的范围。在本文中，我们提出了一种使用正式方法b的逐步完善和正式证明来指定，设计和构建声音和完整ISA的方法。我们讨论自动生成的证明义务如何有助于确保正式ISA模型的自矛盾，以及如何在此建模框架内执行ISA的理想特性。我们已经在Event-B中开发了一个通用的ISA建模模板，以促进重复使用。重复使用此类模板的关键值是增加模型完整性。我们的方法现在被用来正式化XMOS XCORE处理器的ISA，以确保Xcore的文档与硅的文档匹配，并且硅与建筑意图匹配。
Verifying the functional correctness of a processor requires a sound and complete specification of its Instruction Set Architecture (ISA). Current industrial practice is to describe a processor's ISA informally using natural language often with added semi-formal notation to capture the functional intent of the instructions. This leaves scope for errors and inconsistencies. In this paper we present a method to specify, design and construct sound and complete ISAs by stepwise refinement and formal proof using the formal method Event-B. We discuss how the automatically generated Proof Obligations help to ensure self-consistency of the formal ISA model, and how desirable properties of ISAs can be enforced within this modeling framework. We have developed a generic ISA modeling template in Event-B to facilitate reuse. The key value of reusing such a template is increased model integrity. Our method is now being used to formalize the ISA of the XMOS XCore processor with the aim to guarantee that the documentation of the XCore matches the silicon and the silicon matches the architectural intent.