Symbolic Simulation and Its Application to VLSI System Verification

本研究以符号模拟作为正式验证复杂IC设计的基础。符号仿真与经典仿真的不同之处在于，在仿真器运行过程中，用户不仅可以设置输入为0或1，还可以设置布尔变量。本研究利用现有的仿真技术，采用行为方法进行电路验证。在这种情况下，验证者应用逻辑仿真来计算电路对一系列选择的刺激的响应，以检测所有可能的设计错误。研究任务包括：选择一组可以挫败恶意对手试图挫败验证者的模拟模式；基于二元决策图，确定操作布尔公式的结构和算法；并对仿真系统的使用进行了研究，作为调试和设计的辅助。

This research is on symbolic simulation as a basis for formally verifying complex IC designs. Symbolic simulation differs from classical simulation in that during simulator operation the user can set inputs not only to 0 or 1 but also to Boolean variables. The research exploits existing simulation technology by taking a behavioral approach to circuit verification. In this, the verifier applies logic simulation to compute the circuit's response to a series of stimuli chosen to detect all possible design errors. Research tasks include: selecting a set of simulation patterns which can defeat a malicious adversary attempting to foil the verifier; determining structures and algorithms, based on binary decision diagrams, for manipulating Boolean formulas; and investigating the use of the simulation system as an aid to debugging and design.