权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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)为了设计高可靠性的专用集成电路（Application Specific IC），重要的是我们可以正式证明实现的正确性，并且我们可以自动化一些设计步骤。在本研究中，我们提出了一种设计方法来开发正确的ASIC，并开发了一个设计支持系统。(2)在提出的方法中，我们对ASIC进行了如下设计。(a)首先，我们使用代数规范语言ASL描述抽象的层次规范，然后逐步将规范细化为更具体的层次规范。(b)为了有效地证明每个设计步骤的正确性，我们开发了一个验证器。我们限制了描述的样式。验证者对仅由全称量词限定的前缀范式Presburger句子有一个有效的判定过程。在我们的方法中，设计者只给出了原语的断言和一些定理。然后，验证器机械地检查给定的断言是否作为不变量成立。(c)一般来说，为了提高电路的效率，我们需要对上一步得到的状态图进行变换。我们给出了一些变换规则。我们还开发了一个交互式转换支持工具。(d)最后，我们利用电路发生器得到了具体的电路图。电路发生器利用日本NTT公司开发的PARTHENON合成器，将得到的状态图转换成SFL描述，并生成具体电路。我们的设计支持系统由上述验证器、交互式转换支持工具和电路生成器组成。(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
作者：
通讯作者：

森岡澄夫,北道淳司,東野輝夫,谷口健一: ""整数上の論理式の恒真性判定アルゴリズムを用いた組合せ論理回路の実現の正しさの証明"" 情報処理学会第49回全国大会(4L-01). Vol.6. 87-88 (1994)

Sumio Morioka、Junji Kitamichi、Teruo Higashino、Kenichi Taniguchi：“使用确定整数逻辑公式恒常性的算法实现组合逻辑电路的正确性证明”日本信息处理学会第 49 届全国大会 (4L-01)。第6卷。87-88（1994）

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）。