Development of ASIC Design Support System

ASIC设计支持系统的开发

基本信息

批准号：
05558031
负责人：
TANIGUCHI Kenichi
金额：
$ 2.5万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Developmental Scientific Research (B)
财政年份：
1993
资助国家：
日本
起止时间：
1993 至 1994
项目状态：
已结题

项目摘要

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

(1) 对于设计高可靠的ASIC（专用IC），重要的是我们能够形式化地证明实现的正确性并且我们能够自动化一些设计步骤。在这项研究中，我们提出了一种开发正确 ASIC 的设计方法，并开发了一个设计支持系统。(2) 在所提出的方法中，我们按如下方式设计 ASIC。(a) 首先，我们使用代数规范描述抽象级别的规范语言ASL，然后我们将规范逐步细化为更具体的级别规范。(b)为了有效地证明每个设计步骤的正确性，我们开发了一个验证器。我们限制描述的风格。验证者对于仅受全称量词限制的 prenex 范式 Presburger 句子有一个有效的决策过程。在我们的方法中，设计者只给出原语的断言和一些定理。然后，验证者机械地检查给定的断言是否保持不变。(c)一般来说，为了提高电路的效率，我们需要对上述步骤获得的状态图进行变换。我们给出了一些转换规则。我们还开发了一个交互式转换支持工具。(d)最后，我们使用我们的电路生成器获得具体的电路图。电路生成器将获得的状态图转换为SFL描述，并使用日本NTT公司开发的合成器PARTHENON生成具体电路。我们的设计支持系统由上述验证器、交互式转换支持工具和电路生成器组成。(3)我们使用一些实际示例（例如 CPU 和排序电路）评估了我们方法的实用性。

项目成果

期刊论文数量（29）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

村上尚,北道淳司,森岡澄夫,西川清史,谷口健一: ""代数的手法を用いた同期式順序回路の設計支援機能の統合"" 1995年電子情報通信学会春期大会(A121). 基礎/境界. 121- (1995)

Hisashi Murakami、Junji Kitamichi、Sumio Morioka、Kiyoshi Nishikawa、Kenichi Taniguchi：“使用代数方法集成同步时序电路的设计支持功能”1995 IEICE 春季会议 (A121) (1995)。

DOI：
发表时间：
期刊：
影响因子：
0
作者：
通讯作者：

Sumio Morioka, Junji Kitamichi, Higasino Teruo and Kenichi Taniguchi: ""Facilities for State Diagran Transformation in Hardware Design Support System based on Algebraic Method"" Proceedings of the 8th Karuizawa Workshop on Circuits and Systems. (1995)

Sumio Morioka、Junji Kitamichi、Higasino Teruo 和 Kenichi Taniguchi：“基于代数方法的硬件设计支持系统中的状态图变换设施”第 8 届轻井泽电路与系统研讨会论文集。

DOI：
发表时间：
期刊：
影响因子：
0
作者：
通讯作者：

北嶋暁,森岡澄夫,北道淳司,東野輝夫,谷口健一: ""代数的言語ASLによる回路設計支援システムにおけるAFL記述への詳細化とその変更およびそれらの正しさの検証"" 情報処理学会第49回全国大会(4L-07). Vol.6. 99-100 (1994)

Akira Kitajima、Sumio Morioka、Junji Kitamichi、Teruo Higashino、Kenichi Taniguchi：“使用代数语言 ASL 对电路设计支持系统中的 AFL 描述进行细化和修改，并验证其正确性”日本信息处理学会第 49 届全国大会（4L-07）。第6卷99-100（1994）。