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）的各个阶段，因此形式验证必须确保威廉希尔官方网站 逻辑功能不会受到任何阶段的影响。

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

图2.形式验证流程图。

形式验证的步骤

在形式验证期间执行以下步骤：

读–读取步骤读取初始设计和目标设计以及所有相关技术库（图 3）。它进一步将设计划分为逻辑锥的关键等价检查概念和比较点：

常见比较点：输入黑匣子;寄存器或锁存器;主输出

不太常见的比较点：多驱动网络;圈;切割点

逻辑锥（图4）：驱动比较点的组合逻辑块

设置 – 综合工具提供所有自动设置信息，包括时钟门控和扫描插入，这些信息由形式验证识别。

火柴–匹配过程将首先尝试验证指导文件并应用已设置的任何指导。比赛还将尝试根据以下内容匹配比较点：

基于名称的算法

基于签名的分析

注意：然后报告任何不匹配的点。

？验证 – 验证周期验证参考设计的每个逻辑锥与相应实现设计的逻辑等效性。形式验证算法使用许多求解器来证明等价或不等价。有四种可能的结果：

成功：实现等效于引用

失败：实现不等于参考，这意味着存在逻辑差异或设置问题。

定论：没有点失败，但分析未完成，这可能是由于超时或复杂性。

未运行：由于流中的某些初始问题，验证无法运行。

调试-

检查是否有任何警告标志。

检查是否有任何被拒绝的 SVF 指导命令。

检查不匹配的比较点。

报告和修复分析

正式验证运行完成后，可以生成报告分析并在必要时执行修复。

下面的图 5 显示了匹配报告。这里总共报告了 30 个失败的比较点，包括 4 个黑匣子引脚 （BBPins）、17 个 D 触发器 （DFF） 和 9 个锁存器。此外，该报告指示验证失败（图 6）。

由于可能会发生从正常翻牌到多位翻牌的一些转换，从而导致翻牌被报告为非等效点，因此 DFF 表示潜在的修复。

图7.普通翻牌与多位翻牌。

好处

无需运行仿真。

功能检查可以通过在任何阶段之后获取网表来完成。

可以轻松识别错误。

结论

本文介绍了形式验证流程、形式验证中使用的技术以及 16 nm 技术节点的调试。形式验证可以轻松检测在时序修复、ECO 实现或任何后端过程中可能发生的任何错误或逻辑故障。

审核编辑：郭婷