Research on a synthesis and verification tool for high performance asynchronous circuits
| Project/Area Number |
12680334
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | National Institute of Informatics (2002)
Tokyo Institute of Technology (2000-2001) |
|---|
Principal Investigator |
YONEDA Tomohiro National Institute of Informatics, Infrastructure Systems Research Division, Professor, 情報基盤研究系, 教授 (30182851)
|
|---|
| Project Period (FY) |
2000 – 2002
|
| Project Status |
Completed (Fiscal Year 2002)
|
| Budget Amount *help |
¥3,700,000 (Direct Cost: ¥3,700,000)
Fiscal Year 2002: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2001: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2000: ¥2,500,000 (Direct Cost: ¥2,500,000)
|
|---|
| Keywords | Asynchronous Circuits / Formal Verification / Ternary dual-rail code / High level synthesis / Bounded delay model / Time Petri Nets / Partial Order Reduction / 3値論理回路 / 3線式符号 |
|---|
| Research Abstract |
Using dual-rail coding for data-path circuits is one of the major approaches for asynchronous circuit design. This approach requires a lot of C elements, which are memory devices, in control circuits, and it causes several problems in synthesis and verification, such as increase of state spaces, degradation of performance, and so on. Thus, this project proposes using three-rail coding instead of dual-rail coding to implement circuits without C elements. Actually, we have selected a ternary code for such the three-rail coding, and have developed two procedures to obtain basic ternary gates from given truth tables based on the ternary code. Furthermore, some optimization technique has also been developed.
On the other hand, when we want to verify an asynchronous circuit including data-paths, we usually do the abstraction of the circuit to remove most of those data-paths. This is because verifying the circuit without abstraction requires checking the whole data values that the data-paths take, and this makes it too difficult to describe specifications and traverse its huge state space. This project also proposes to verify data-paths partially using some specific or random values with verifying the control parts formally as usual. This allows us to do the verification of a given circuit without abstraction which still gives us rather reliable results. For this purpose, we have extended the existing model (a time Petri net) such that it can handle producing and comparing data. In addition, in order to avoid the state explosion problem, a partial order reduction algorithm, which can efficiently prune away the state spaces unnecessary for the verification and synthesis, for such an extended time Petri net has been developed. According to several benchmark circuits, it has been found to outperform a verifier based on the existing model.
|
Report
(4 results)
Research Products
(2 results)
