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.