权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

"A Study on design and verification of parallel sequential machines"

《并行顺序机的设计与验证研究》

基本信息

批准号：
11680358
负责人：
KENICHI Taniguchi
金额：
$ 2.18万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
1999
资助国家：
日本
起止时间：
1999 至 2000
项目状态：
已结题

项目摘要

(1) We have proposed a method to design an out-of-order pipelined CPU and to verify its correctness. An experimental result shows that our method is useful.(2) We have modeled TASV, which is an extended version of Alur's timed automata. The model has global variables. We have devised an efficient method to check deadlock freeness of the model which utilizes one-way reference relations of global variables.(3) We have proposed an automatic symbolic model checking method for an extended finite state machine (EFSM), which can decide temporal properties like "it eventually reaches desired states", "it is deadlock free", and so on. We have given a sufficient condition for the checking to be decidable. In an implementation of the method, we use a library for Presburger sentences to treat arbitrary precision integer registers.(4) We have also proposed an automatic symbolic model checking method for EFSMs, by extending the previous work. As an example, we have described a simple auction system in the model and checked some dynamic properties on it. We found that such properties can be checked on a PC within a few minutes.(5) We have introduced automatic verification tools into a laboratory work for undergraduates. In the laboratory work, students determine CPU instruction sets and CPU architectures, and then refine the CPU designs to a logic-design level. The final design has multi FSMs as a CPU controller. We have analyzed the workloads and investigated the correctness of the final CPUs. We found that the formal methods is useful to design correct sequential machines (especially parallel sequential machines).

(1)提出了一种乱序流水线CPU的设计方法，并验证了其正确性。实验结果表明，该方法是有效的。(2)我们建立了TASV模型，TASV是Alur时间自动机的扩展版本。该模型具有全局变量。我们设计了一种利用全局变量的单向引用关系来检测模型死锁是否有效的方法。(3)提出了一种扩展有限状态机（EFSM）的自动符号模型检验方法，该方法可以判定“最终达到预期状态”、“无死锁”等时间属性。我们给出了检验可判定的充分条件。在该方法的实现中，我们使用了Presburger语句库来处理任意精度的整数寄存器。(4)在此基础上，提出了一种EFSMs符号模型自动检测方法。作为一个例子，我们在模型中描述了一个简单的拍卖系统，并检查了它的一些动态特性。我们发现这些属性可以在几分钟内在PC上检查。(5)我们在本科生的实验室工作中引入了自动验证工具。在实验室工作中，学生确定CPU指令集和CPU架构，然后将CPU设计细化到逻辑设计水平。最终设计采用多个fsm作为CPU控制器。我们分析了工作负载并调查了最终cpu的正确性。我们发现形式化方法对于设计正确的顺序机（特别是并行顺序机）是有用的。