符号模拟

Symbolic Simulation

符号模拟将模拟验证从布尔值扩展到符号领域,是集成电路验证行业中的重要分支。符号方法将符号值加到待验证电路的基本输入端,依次计算每个结点的布尔函数,直到在电路的输出端得到由这些初始符号变量组成的布尔表达式,并判断其是否具有所期望的特征。该文介绍了符号模拟的发展过程、基本技术及其所面临的BDD爆炸问题,并对消除该问题的两种技术:近似值法和参数方法,进行了讨论。介绍了具有一定自动机处理能力的符号轨迹评价方法。

Symbolic simulator assigns symbolic variables to the inputs of both specification and implementation, propagates those to the outputs, builds the symbolic expressions for both circuits, and checks the corresponding signals. The paper introduces the history, basic technology, and the drawback of BDD blowup of symbolic simulation. The two techniques, approximate value method and parametric method, which are used to eliminate the BDD blowup problem, and symbolic trajectory evaluation（STE） is also introduced.