Hardware Verification with respect to Program Specification

随着最近集成电路技术的发展，我们可以在一个芯片上集成100万个晶体管。为了设计如此庞大的电路，已经开发出高水平的设计方法，并将其应用于许多专用芯片。在高级设计中，使用编程语言对功能进行描述，并根据高级综合算法将描述自动转换为硬件模块。因此，需要在编程级对其进行修改和验证，并且需要高级别的验证方法。在本研究中，我们开发了几种基本算法来证明硬件模块相对于程序规格说明的正确性。首先，我们综述了未解释函数等价性的研究现状及其在软硬件验证中的应用。我们还检查了现有的等值系统，如svc、clvl等，并应用这些系统对arith…进行了验证。更多的Mtic电路，并显示了此类系统的局限性。我们还将等价性检查系统应用于并行电路和流水线电路的验证，在等价性检查中，算法使用逻辑公式来表示和判定等价性。为了加速决策过程，我们提出了一种基于新型现场可编程门阵列查找表结构的原型系统。我们设计了新的体系结构，并提出了新的体系结构的映射方法。在程序规范方面，提出了一种基于控制数据流图的数据路径优化方法。重点研究了数据路径的位宽问题，提出了整数运算的优化方法和浮点运算的误差估计方法。利用优化和估计算法，我们可以验证用C程序编写的专用电路。我们还进行了高层测试，并提出了一种用于片上系统设计的小面积开销的测试图压缩方法。较少

With the recent development of integrated circuit technology, we can integrate 1 million transistors in one chip. For the design of such huge circuits, high-level design methodologies have been developed and applied to many application specific chips. In the high-level design, programming languages are used to describe the functionality and the description is automatically converted to hardware modules based on high-level synthesis algorithms. So the modification and verification should be done at programming level and high-level verification methods are needed. In this research, we have developed several basic algorithms to show the correctness of hardware modules with respect to the program specification.At first, we have surveyed the current research on the equality with uninterpreted function and its application to software and hardware verification. We have also checked the current equality systems such as SVC, CLVL, etc. We have applied these systems for the verification of arith … More metic circuits and shown the limitation of such systems. We have also applied the equality checking systems for the verification of parallel and pipeline circuits.In the equality checking, the algorithm uses logic formulae to represent and decide the equality. For the acceleration of the decision procedure, we proposed a prototyping system based on new look-up-table architecture of Field Programmable Gate Array. We have devised the architecture and proposed a mapping method for the new architecture. The architecture is more area-efficient and faster compared to the usual loop-up-table architecture.For the program specification, we have proposed a control-data-flow graph based data-path optimization methods. Especially, we focused on the bit-width of data-paths and proposed an optimization method of integer operations and an error estimation method for floating point operations. With the optimization and estimation algorithms, we can verify application specific circuits written in C programs.We have also worked on the high-level test and proposed a test pattern compaction method with small area overhead for system-on-chip design. Less