Development of ASIC Design Support System

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

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