| 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)
|
|---|
| 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.
|
