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

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.

本研究的目的是建立高层次的硬件设计和验证的方法，并开发其支持系统。验证的目标包括两个方面：确保时间约束和确保功能特性。为了确保时间约束，我们提出了三种方法：一种用于对具有整数变量的某类有限状态机进行符号模型检验的方法，一种用于检验在时间自动机的网络中表示的给定系统的时间性属性的方法，以及一种在定时自动机中检测时间动作锁定的方法。符号模型检验的方法可以输入一个类似CTL的表达式，它可以证明一个BJD（黑杰克经销商）电路总是正确地决定卡，在几秒钟内。该方法可以验证给定的时间自动机网络是否具有吞吐量、抖动和延迟等时间特性。时间-动作-锁检查器通过将死锁问题归结为有理Presburger语句的判定问题来证明死锁问题。为了保证函数式程序设计语言ML的功能性，我们开发了一个验证支持系统。通用硬件组件的规范描述可以用具有时钟的状态机模型表示，也可以用ML中的模块签名方案表示。后者使我们能够使用验证支持系统来验证硬件组件（模块）的功能属性。我们还给出了一个简单的语言转换器的功能特性的验证。未来的工作涉及开发一个集成的开发环境，沿着所提出的方法。