Encoding of processor instruction sets with explicit concurrency control
Encoding of processor instruction sets with explicit concurrency control
复制标题
具有显式并发控制的处理器指令集编码
DOI：
10.1049/iet-cdt.2010.0158
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
A. Yakovlev
中科院分区：
文献类型：
--
作者：
A. Mokhov;A. Alekseyev;A. Yakovlev
在微体系结构的建模和综合中，迫切需要设计自动化。缺乏必要的自动化支持的领域之一是以各种设计优化标准为目标的指令代码的合成。本文旨在通过提供一套形式化的方法和软件工具来填补这一空白，该方法和软件工具用于在给定处理器被描述为指令集的情况下综合指令代码。该方法基于条件偏序图(CPOG)模型，该模型是一种有效描述和综合微控制器的形式化方法。它将一个系统描述为其行为场景或指令的功能组合，每个指令都是事件的偏序。为了区分CPOG中的指令，它们被赋予用布尔向量表示的不同编码。最终微控制器的大小和延迟在很大程度上取决于所选择的编码，因此有效的指令代码合成是至关重要的。文章指出，CPOG模型是一种非常方便的表示处理器指令集的形式化方法。它为几个编码问题的简明表述提供了基础，这些问题可归结为布尔可满足性(SAT)问题，并且可以被现代SAT解算器有效地解决。
There is a critical need for design automation in microarchitectural modelling and synthesis. One of the areas which lacks the necessary automation support is synthesis of instruction codes targeting various design optimality criteria. This paper aims to fill this gap by providing a set of formal methods and a software tool for synthesis of instruction codes given the description of a processor as a set of instructions. The method is based on the conditional partial order graph (CPOG) model, which is a formalism for efficient specification and synthesis of microcontrollers. It describes a system as a functional composition of its behavioural scenarios, or instructions, each of them being a partial order of events. In order to distinguish instructions within a CPOG they are given different encodings represented with Boolean vectors. Size and latency of the final microcontroller significantly depends on the chosen encodings, thus efficient synthesis of instruction codes is essential. The paper shows that the CPOG model is a very convenient formalism for efficient representation of processor instruction sets. It provides a ground for a concise formulation of several encoding problems, which are reducible to the Boolean satisfiability (SAT) problem and can be efficiently solved by modern SAT solvers.