Research on Development of Formal Logic Design Verifier for Microprocessors

微处理器形式逻辑设计验证器的开发研究

• 批准号: 07558155
• 负责人: YAJIMA Shuzo
• 金额: $ 1.41万
• 依托单位: KYOTO UNIVERSITY
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (A)
• 财政年份: 1995
• 资助国家: 日本
• 起止时间: 1995 至 1996
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07558155/
• 关键词: Formal design verification; Function level design; temporal logic; First-order Predicate logic; model checking; logic function manipulation; binary decision diagram; マイクロプロセッサ; 調理関数処理; 二分モーメントグラフ; 三分決定グラフ; 機能レベル検証; 算術演算回路検証

The aim of this research is to develop a formal verifier for large sequential circuits, in particular, microprocessors. Although arithmetic circuits such as multipliers are crucial components in microprocessor designs, it was a hard problem to verify them. We developed a new algorithm using binary moment diagrams, and showed that it is possible to verify multipliers, which were typical hard problems in formal verification. Furthermore, we developed a new efficient algorithm for formal verification based on linear time temporal logic, which can describe temporal properties more easily than the other temporal logics. In order to deal with circuits at function level than at logic level, we took a logic known as quantifier-free first-order predicate logic with equality. We introduced temporal operators similar to those of the above linear time temporal logic, and proved that its validity checking problem is decidable. We improved this algorithm in terms of required time and space, and implemented the algorithm to show its effectiveness. Furthermore we showed that the optimal variable ordering problem of binary decision diagrams is NP-complete. We also investigated the computational power of a variant binary decision diagrams which have nondeterministic nodes.

本研究的目的是开发大型顺序电路的正式验证器，特别是微处理器。虽然乘法器等算术电路是微处理器设计中的关键部件，但验证它们却是一个难题。我们开发了一种使用二元矩图的新算法，并证明了在形式化验证中典型的难题乘子验证是可能的。此外，我们开发了一种新的基于线性时间时间逻辑的形式验证算法，该算法比其他时间逻辑更容易描述时间属性。为了在功能级而不是逻辑级处理电路，我们采用了一种称为无量词的一阶等价谓词逻辑。我们引入了类似于上述线性时间时间逻辑的时间算子，并证明了其有效性检验问题是可判定的。从所需的时间和空间两个方面对该算法进行了改进，并对算法进行了实现，验证了算法的有效性。进一步证明了二元决策图的最优变量排序问题是np完全的。我们还研究了一种具有不确定性节点的变型二元决策图的计算能力。

项目成果

K. Hamaguchi: "Efficient Construction of Binary Moment Digarams for Verifying Arithmefic Circuits." 1995 IE^3/ACM International Conference an Computer-Aided Design. 78-82 (1995)

K. Hamaguchi：“用于验证算术电路的二进制矩量图的有效构建”。