16nm技术的形式验证流程、优势和调试-电子发烧友网

必须优化正式验证流程中的初始网表，因此测试设计需要额外的逻辑。在这里，我们提供16 nm节点的形式验证流程和调试技术。

形式验证是比较用硬件描述语言（HDL）编写的两个设计以确保它们在功能上等效的过程。作为功能验证的一个子集，it 提供了在不使用仿真的情况下检查两个设计的功能等效性的关键第一步。

这些功能等价物中的第一个称为参考设计/黄金设计，其中基于传输级（RTL）代码（如Verilog，System Verilog或VHDL）的模型用作参考网表。该网表根据第二种设计中的相应网表进行验证，称为实现或修订设计（图 1）。为简单起见，在本文的其余部分中，参考/黄金设计将称为“初始设计”，而实现设计/修订设计称为“目标设计”。

图1.形式验证方法的表示

下表显示了可用于比较初始设计与目标设计的组合。

表 1.初始设计与目标设计

此过程要求初始网表经过不同级别的优化，这反过来又需要额外的测试设计（DFT）逻辑。尽管有这些要求，但形式验证过程不应改变设计的逻辑功能。

形式验证的类型

通常使用两种形式验证技术：

等价性检查 – 逻辑等效性检查是一种技术，它采用两种可以具有相同或不同抽象级别（即算法、RTL 或门级）的设计，并检查它们之间的任何功能差异。

等价性检查进一步分为组合或顺序检查。组合等价性检查包括通过将从初始设计一对一的翻牌映射到目标设计来检查组合逻辑，而如果一对一翻牌映射之间存在不同的组合逻辑，但如果给定相同的输入，设计仍应能够产生相同的输出，则使用顺序等价检查。通常，如果 SoC 或 ASIC 设计经历了各种转换，如重定时、节能设计优化等，则使用顺序等效性检查。

属性检查或基于断言的验证（ABV） –属性检查或 ABV 检查行为是否可行，并使用属性检查器工具来证明设计符合其所有规范。属性检查使用数学程序来证明设计的准确性。

属性检查通常使用两种属性语言：间隔时态逻辑（ITL）和系统验证断言（SVA）。一旦这些被编码，它们就可以传递给数学工具，数学工具预测结果是保持或失败。持有ITL/SVA意味着所有属性都已经过检查，并保留了初始设计的属性。ITL/SVA失败意味着设计行为不是有意的，并且目标设计存在冲突。

形式验证的要求

功能等效性检查通常需要使用相同的测试向量对两个HDL设计进行仿真。但是，随着ASIC技术的缩小和电路复杂性的增加，不可能使用仿真来验证电路功能，因为仿真可能会运行数月。因此，形式化验证通过节省仿真运行时间以及这些扩展仿真的巨大资源需求起着非常重要的作用。

此外，由于设计要经历从综合、布局和布线、签核和工程变更单（ECO）的各个阶段，因此形式验证必须确保电路逻辑功能不会受到任何阶段的影响。

形式验证流程如下图所示。