A study on debug techniques for digital systems exploiting formal verification methods

随着先进的工艺和器件技术实现了系统级芯片（System-on-Chip）的集成化，许多与SoC相关的技术得到了研究。计算机辅助设计（CAD）也已成为SoC设计中不可或缺的，以减少设计周期，并保证设计的正确性。在这项研究中，我们已经研究了非常大规模的数字系统的调试流程和调试技术，利用形式验证技术的分析，设计时，需要分析，因为错误的设计或修改的规格。在传统的研究中，寄存器传输级（RTL）设计处理的设计语言。然而，在这项研究中，我们不仅处理了RTL设计，而且还处理了数字系统的硬件和软件混合的系统级设计。本文从以下几个方面进行了研究，以建立超大规模数字系统的调试框架。（1）面向系统级设计的程序切片技术及其在系统验证中的应用（2）面向系统级设计的抽象求精性质验证方法（3）面向硬件的C基设计的等价性验证方法。（4）算术电路的调试方法（1）、（2）和（3）是用于高级设计的技术，并且它们在所有功能单元（例如算术单元）都是正确电路的假设下分析或调试整个系统。(4)是对运算器进行独立调试的技术，通过研究，以上技术得到了初步的建立。通过综合运用这些技术，我们相信不仅可以减少调试时间，而且可以减少整个系统LSI设计所花费的时间。此外，我们相信这些技术也使系统LSI在未来的半导体技术中充分利用巨大的晶体管资源。

As advanced process and device technologies have realized System-on-Chip, in which whole system is integrated, many techniques related to SoC have been studied. Computer Aided Design (CAD) has also become indispensable for SoC designs to reduce the design period and to guarantee the correctness of the design.In this study, we have studied on the debug flow and debug techniques of very large scale digital systems by exploiting formal verification techniques for the analysis of the designs when the analysis is required because of faults of designs or modification of the specification. In the conventional studies, register transfer level (RTL) designs were handled for the design language. In this study, however, we have handled not only RTL designs but also system level designs in which hardware and software of the digital systems are mixed. Therefore, the consistent debug framework from specification level has been established.We have studied in terms of the following aspects to establish the debug framework for very large scale digital systems.(1)Program slicing technique for system level designs and its application for system verification(2)Property verification method with abstraction refinement for system level designs(3)Equivalence verification method for hardware oriented C-based designs.(4)Debug methodology for arithmetic circuits(1), (2), and (3) are the techniques for high level design and they analyze or debug the whole system on the assumption that all functional units, such as arithmetic units, are correct circuits. (4) is the technique which debugs the arithmetic units independently.Throughout the study, the above techniques have been established. By using those techniques together, we believe that the time spent for not only debug but also whole system LSI design can be reduced. In addition, we believe those techniques also enable the system LSIs which thoroughly utilize enormous transistor resources in the future semiconductor technology.