Higher Level Design and Verification Support Systems for Hardware

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

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.