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（Black Jack Dealer）电路总是在几秒钟内正确决定牌。检查及时性属性的方法可以验证给定的定时自动机网络是否具有及时性属性，例如吞吐量、抖动和延迟。时间-动作-锁检查器通过将问题简化为有理Presburger语句的决策问题来证明死锁问题。为了保证函数式属性，我们开发了函数式编程语言ML的验证支持系统。通用硬件组件的规范描述可以用带有时钟的状态机模型以及机器学习中的模块签名方案来表示。后者使我们能够使用验证支持系统来验证硬件组件（模块）的功能属性。我们还提供了一个简单的语言转换器来验证功能属性。未来的工作涉及按照所提出的方法开发集成开发环境。