Higher Level Design and Verification Support Systems for Hardware

硬件的更高级别设计和验证支持系统

基本信息

批准号：
13558028
负责人：
TANIGUSHI Kenichi
金额：
$ 3.26万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (B)
财政年份：
2001
资助国家：
日本
起止时间：
2001 至 2004
项目状态：
已结题

项目摘要

This research aims to establish methods for high-level design and verification of hardware and to develop their support systems. The objective of the verification consists of two aspects : to ensure time constraints and to ensure functional properties.In order to ensure the time constraints, we have proposed three methods : a method for symbolic model checking for some class of finite state machines with integer variables, a method to check timeliness properties of a given system represented in a network of timed automata, and a method to detect time-action-lock in a timed automaton. The method for symbolic model checking can input a CTL like expression and it can prove that a BJD (Black Jack Dealer) circuit always decides cards properly, in a few seconds. The method to check timeliness properties can verity that a given network of timed automata has timeliness properties such as throughput, jitter, and latency. The time-action-lock checker proves the deadlock problem by reducing the problem into a decision problem of rational Presburger sentences.In order to ensure the functional properties, we have developed a verification support system for a functional programming language ML. A specification description of a component of a general hardware can represented in a state machine model with clocks and also in a module signature scheme in ML. The later enables us to verify functional properties of a hardware component (module) using a verification support systems. We also give a simple language converter for verification of the functional properties. Future work involves developing an integrated developing environment along the proposed methods.

这项研究旨在建立高级设计和硬件验证并开发其支持系统的方法。验证的目的由两个方面组成：确保时间限制并确保功能属性。为了确保时间限制，我们提出了三种方法：一种用于检查具有INTEGER变量的某些有限状态机器的符号模型的方法，用于检查在自动化的自动化网络中的及时系统的及时效率的方法，可以检测到时间和时间 - 并检测到时间 - 且可以检测到一定的时间。符号模型检查的方法可以输入CTL表达式，并且可以证明BJD（Black Jack经销商）电路始终在几秒钟内正确地决定卡。检查及时性属性的方法可能会使给定的定时自动机网络具有及时性属性，例如吞吐量，抖动和延迟。时间行动锁检查器通过将问题减少到理性的前堡句子的决策问题来证明了僵局问题。为了确保功能属性，我们为功能编程语言ML开发了验证支持系统。通用硬件组件的规范说明可以在带时的状态机模型中表示，也可以在ML中的模块签名方案中表示。以后使我们能够使用验证支持系统验证硬件组件（模块）的功能属性。我们还提供了一个简单的语言转换器来验证功能属性。未来的工作涉及沿建议的方法开发一个综合发展的环境。