| Project/Area Number |
05558031
|
|---|
| Research Category |
Grant-in-Aid for Developmental Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
TANIGUCHI Kenichi Osaka Univ.・Faculty of Engineering Science Professor, 基礎工学部, 教授 (00029513)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SUGIYAMA Yuuji Okayama Univ.・Faculty of Engineering Professor, 工学部, 教授 (50116050)
OKANO Kozo Osaka Univ.・Faculty of Engineering Science Research Associate, 基礎工学部, 助手 (70252632)
KITAMITI Junji Osaka Univ.・Faculty of Engineering Science Research Associate, 基礎工学部, 助手 (20234271)
MATSUURA Toshio Osaka Univ.・Education Center for Info.Process. Associate Professor, 情報処理教育センター, 助教授 (40127296)
HIGASINO Teruo Osaka Univ.・Faculty of Engineering Science Associate Professor, 基礎工学部, 助教授 (80173144)
|
|---|
| Project Period (FY) |
1993 – 1994
|
| Project Status |
Completed (Fiscal Year 1994)
|
| Budget Amount *help |
¥3,900,000 (Direct Cost: ¥3,900,000)
Fiscal Year 1994: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 1993: ¥2,800,000 (Direct Cost: ¥2,800,000)
|
|---|
| Keywords | Synchronous sequential circuit / Algebraic method / ASIC / Stepwise refinement / Design verification / CAD / Presburger sentence / State diagram transformation / 高位合成 / グラフィカルユーザインタフェース / 機能設計 / 形式的手法 / 設計自動化 |
|---|
| Research Abstract |
(1) For designing high reliable ASIC's (Application Specific IC's) , it is important that we can prove the correctness of implementations formally and that we can automate some design steps. In this research, we have proposed a design methodology to develop correct ASIC's and developed a design support system.
(2) In the proposed method, we design ASIC's as follows.
(a) First, we describe an abstract level's specification using our algebraic specification language ASL,and then we refine the specification into more concrete levels'specifications step by step.
(b) To prove the correctness of each design step efficiently, we have developed a verifier. We restrict the style of descriptions. The verifier has an efficient decision procedure for prenex normal form Presburger sentences bounded by only universal quantifiers. In our method, the designer only gives assertions and some theorems for primitives. Then, the verifier mechanically checks whether the given assertions hold as invariants.
(c) In general, to improve the efficiency of circuits, we need transform a state diagram obtained the above step. We have given some transformation rules. We have also developed an interactive transformation support tool.
(d) Finally, we use our circuit generator to obtain a concrete circuit diagram. The circuit generator transforms the obtained state diagram into a SFL description and generates a concrete circuit using the synthesizer PARTHENON developed in NTT Corp., Japan.
Our design support system consists of the above verifier, interactive transformation support tool and circuit generator.
(3) We have evaluated the usefulness of our approach using some practical examples such as CPU and sort circuits.
|
