2004 Fiscal Year Final Research Report Summary
Higher Level Design and Verification Support Systems for Hardware
| Project/Area Number |
13558028
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 展開研究 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
TANIGUSHI Kenichi Osaka University, Graduate School of Information Science and Technology, Professor, 大学院・情報科学研究科, 教授 (00029513)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
HIGASHINO Teruo Osaka University, Graduate School of Information Science and Technology, Professor, 大学院・情報科学研究科, 教授 (80173144)
KATAMICHI Junii University of Aizu, School of Computer Science and Engineering, Associate Professor, コンピュータ理工学部, 助教授 (20234271)
OKANO Kozo Osaka University, Graduate School of Information Science and Technology, Associate Professor, 大学院・情報科学研究科, 助教授 (70252632)
YAMAGUCHI Hirozumi Osaka University, Graduate School of Information Science and Technology, Research Associate, 大学院・情報科学研究科, 助手 (80314409)
MORIOKA Sumio Sony Corporation, Information technologies laboratories, Researcher, ユビキタス技術研究所, 研究員
|
|---|
| Project Period (FY) |
2001 – 2004
|
| Keywords | High-Leveled Design / Verification of Functional Properties / Verification of Timeliness / Verification Support System / Register Transfer Level / Behavioral Level / Time-Action-Deadlock |
|---|
| Research Abstract |
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.
|
Research Products
(12 results)
