Developmental Research on Interactive Logic Simulator-Verifier with High-Level Hardware Description

层次化设计方法从结构级到门级反复细化设计，适用于大规模逻辑电路的设计。在这种设计方法中，验证每个细化步骤并尽早发现设计错误是非常重要的。为了支持这样的验证步骤，我们已经研究了高级硬件描述语言，支持设计细化步骤，高速逻辑仿真算法，和形式化验证方法。基于这些研究结果，我们还开发了一个交互式逻辑模拟验证器。主要研究结果如下：1.高级硬件描述：为了支持精细化设计，我们开发了一种新的硬件设计语言HDL-R，它支持精细化设计中的多重抽象时间和对应规范。适合于从体系结构到寄存器传输级的可靠性设计.使用向量处理器的高速逻辑模拟：我们开发了新的逻辑模拟算法，称为向量并行方法和门分组方法。它们面向矢量处理器，实现了7.7M门评估/秒，与硬件仿真引擎相当.形式规格说明和验证：我们提出了一个新的并行系统模型，将时间和因果关系视为事件上的偏序。该模型使我们能够使用抽象数据类型代数地给出形式化规格说明，并进行形式化验证.图形工作站：我们提出并开发了多计算机多屏幕图形作为交互式逻辑模拟器验证器的工作站。它可以实现任何高分辨率屏幕上的技术限制的分辨率的CRT。

Hierarchical design method which repeats refinement of design from architectural level to gate level is suitable for designing of large scale logic circuits. In such a design methodology it is very important to verify each refinement step and to find out design error as early as possible. In order to support such verification step, we have researched on high-level hardware description languages which support design refinement step, high-speed logic simulation algorithms, and formal verification methods. Based on the results of these researches, we have also developed an interactive logic simulator-verifier. The major results of our researches are as follows.1. High-Level Hardware Description: In order to support refinement of design, we have developed a new hardware design language HDL-R which supports multiple abstracted time and specification of correspondence in refinement of design. It is suitable for reliable design through architecture to register transfer level design.2. High-Speed Logic Simulation Using a Vector Processor: We have developed new logic simulation algorithms named vector-parallel method and gate-grouping method. They are oriented to vector processors, and realized 7.7M gate evaluation/sec which is comparable to hardware simulation engines.3. Formal Specification and Verification: We proposed a new model for parallel systems which treats time and cause-effect relations as partial ordering over events. This model enables us to give formal specification algebraically using abstract data types and to make formal verification.4. Graphics Workstation: We have proposed and developed multicomputermultiscreen graphics as a workstation for the interactive logic simulatorverifier. It can realize any high resolution screen over technological limitation on resolutions of CRTs.