Higher Level Design and Verification Support Systems for Hardware

点击翻译按钮获取中文摘要

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.