使用符号模拟的单元库验证

自逻辑合成和组合方法出现以来，标准单元库一直是芯片设计的主流。单元库IP通常包含描述单元功能的Verilog模型、原理图派生的晶体管级网络列表、位置和路由视图、物理布局视图、布局后提取的网络列表以及特征时序和功率模型。芯片设计团队在他们的芯片设计、验证和功率性能区域(PPA)优化项目时间表的不同阶段使用电子设计自动化(EDA)工具链中调用各种单元视图。

细胞库团队维护一个丰富的基础设施，该基础设施将细胞设计、表征、模型生成和验证联在一起，以提供客户设计团队所需的高质量和一致性的细胞库IP。该基础设施的基础是利用基于二进制矢量的模拟来验证电池功能并执行时序和功率特性的方法学。对于典型的标准单元产品，例如多输入逻辑门或锁存器和触发器，二进制矢量模拟传统上提供了足够的逻辑覆盖完整性。

然而，在过去的10年里，两大行业趋势使二进制矢量模拟方法变得紧张。首先，随着芯片复杂性的增加，对更复杂的单元功能的需求也相应地增加到单元库中。除了标准单元之外，库现在还包含复杂的宏，例如保留触发器、多位存储元素、同步器和计数器等等。对于这些类型的单元格，功能验证的完整性超出了应用大量二进制输入向量的范围。这些向量组合还必须考虑到这些复杂状态元素中对存储节点逻辑值的依赖关系。如果单元有任何反馈或管道深度，则这种将内部状态节点依赖项与二进制输入向量组合进行卷积的验证挑战会加剧。

其次，低功耗设计的行业趋势导致芯片设计具有多个电源域，每个包含单独的电压电源，其值可以独立调整，甚至完全关闭。这样一个重要的特性必须通过整个设计层次结构集成到每个组件和代表性模型中，向下延伸到各个单元库模型。在这种情况下，电池Verilog模型必须考虑各种开/关电源状态条件，包括捕捉电源和接地连接错误反转的可能性。

充分验证功耗感知库单元模型，同时考虑内部状态依赖关系和所有可能的输入向量组合的任务变得越来越具有挑战性，并增加了测试逃脱的风险。因此，单元库团队已经探索了正式的验证技术，以实现全功能的验证覆盖。

近二十年来，形式化验证技术一直是芯片设计验证的固有组成部分，因为测试覆盖完整性问题在更大的设计中遇到，具有更高的引脚数和更复杂的逻辑锥和状态依赖关系，远远早于对单元库验证的需求。

大多数标准形式化技术在设计表示之间推断正确的寄存器映射，以确定状态点逻辑等价性，这是在基于合成的流程中可以实现的任务，用于门级设计，其中这些寄存器由离散的单元库flop或latch表示，但不适用于由晶体管级电路组成的扁平设计。更先进的技术，如模型检查和属性证明，也受到限制，因为它们不能直接与包含晶体管元件的全定制电路设计一起工作。

一种已被证明能很好地用于晶体管级网表的形式化方法是符号模拟。该技术还支持行为RTL和可合成RTL，因此非常适合验证通常包含不常用可合成RTL建模的电路的定制设计。

符号模拟涉及用符号变量替换应用于每个设计输入引脚的二进制值。

图1:符号模拟提供高覆盖率的功能验证

输入引脚符号在整个设计中传播，在每个连接晶体管电路拓扑的本地通道的输出端生成布尔逻辑最小项，在每个单元输出引脚处最终生成布尔逻辑方程。由于每个符号包含了0、1、X甚至三态Z的所有可能性，形式验证完整性要求仿真周期数至少等于设计的管道深度。因此，符号模拟通常用于验证通常具有低顺序深度的内存，如sram、多端口寄存器文件、CAMs和rom。

图2:符号模拟传播示例

当参考RTL模型和实现的单元示意图网表都进行符号模拟时，在各自的单元输出引脚处产生的逻辑方程可以通过形式等价逻辑证明相互检查。如果存在不匹配，则通过二进制矢量模拟自动生成一个反例，供用户通过波形进行调试。如果参考设计视图和实现设计视图是等效的，就没有相关的波形需要检查，因此覆盖率分析用于补充符号模拟，以提供设计验证完整性的度量。覆盖度量包括验证输出方程中显示的所有输入符号，所有设计内部网络都是符号的，并且在两个设计表示形式中都有完整的代码覆盖。

符号模拟技术可以将单元验证的范围扩展到逻辑功能等价之外。虽然输入引脚符号是用完整的二进制甚至四元逻辑值编码的，但也可以将其他属性附加到这些符号上。功率感知验证最相关的是将每个引脚的功率域信息嵌入到其各自的符号中。使用该设备，可以动态检查包含多个功率域的电路，以查看功率域接口是否存在电气危险。这种检查包括检测丢失的电压电平移位器，由于电源门控而导致的功率域之间的不正确隔离，多过渡故障或承载相同逻辑值的不同电源电压源之间不需要的隐蔽路径。

图3:电气危险检查的符号模拟

虽然这类电路电气验证已经通过静态网表检查器或基于矢量的模拟进行了探索，但前者只能捕获基于连接的电气规则违规行为，而向量集限制了后者检测瞬态违规行为的能力。这些限制都不适用于动态符号模拟，它总是暴露出电气规则违反测试逃脱固有的其他技术。

符号模拟是一种经过验证的自定义电路形式验证技术。从历史上看，它一直被用于验证大型设计，如sram，但一些库单元的复杂性，结合电源意识验证完整性要求，以检查输入和电源引脚上的所有逻辑条件，以及内部状态节点依赖关系，现在已经使符号模拟成为单元库功能验证的一个有吸引力的解决方案。此外，这种形式化技术扩展了电源感知验证的范围，超出了纯逻辑验证，还包括用于电气危险检测的形式化电路检查。

Synopsys对此的ESP的工具已被行业标准解决方案定制电路正式验证。它采用符号模拟的形式等价性检查和电气危险检测。