芯片设计之逻辑等价检查 (LEC)

　　设计芯片是一个复杂的过程。它从定义架构要求开始，然后是微架构开发，然后是 RTL 设计和功能验证。然后综合设计得到网表，交给后端团队进行后端流程。在后端流程中，网表在各个阶段经历各种变化，无论是在识别错误​​后对设计执行的工程变更单 （ECO），还是为时序收敛而修改单元。简而言之，该设计在进入最终流片阶段之前会进行多次更改。

　　为了在更改后验证设计，有必要通过提供测试用例来运行仿真，但由于设计的复杂性（复杂的设计需要更多的运行时间）以及设计更改的频率，这通常是不可能的。在这种情况下，设计要经过逻辑等效检查 （LEC），其中工具通过注入随机向量来验证设计。

　　业内有许多工具可用于检查逻辑等价性，但使用最广泛的是Cadence的Conformal和 Synopsys 的Formality。除了 LEC，这些工具还可以用于执行其他任务，例如 ECO。在本文中，我们将介绍 Conformal LEC 流程。

 

 

　　图 1一个典型的 Conformal LEC 流程包括一个设置模式和一个 LEC 模式。

　　一个典型的保形 LEC 平面运行流程主要由一个设置阶段和一个 LEC 模式组成。设置模式包括以下步骤：

　　黑盒规格

　　阅读图书馆和设计

　　设计约束规范

　　建模指令规范

　　切换到 LEC 模式

　　LEC 模式包括：

　　映射过程

　　比较过程

　　一、黑匣子规格

　　在典型的设计中，会有模拟块、存储器和数字块。内存和模拟块由不同的团队提供，在运行 LEC 时它们将被视为黑盒。如果设计中存在 IP，则 IP 验证由 IP 提供商执行，用户无需花费时间验证 IP。因此，即使 IP 也可以作为黑盒包含在内。

　　可以使用命令指定黑盒，如下图 2中的第 25 行所示。这必须在读取设计文件/库之前完成，以确保只读取 I/O 端口而不是整个设计。这样做会大大减少运行时间，并且在我们在大型设计上运行 LEC 时会有很大帮助。当一个模块被指定为黑盒时，Conformal 工具将验证连接——黑盒的输入和输出——但它不会验证黑盒内部的逻辑。　　

 

 

　　图 2可以使用此图像中显示的命令指定黑盒。

　　2. 阅读VHDL/Verilog 设计和库

　　除了 Verilog 和 VHDL 支持读取设计文件外，Conformal 工具还支持读取 Verilog 标准仿真库和 Liberty 格式库。该信息通过使用如下图 3中第 37 行和第 40 行所示的命令提供给工具。搜索路径和文件列表也可以使用适当的命令输入到工具中。

 

 

　　图 3上面显示的命令用于读取设计文件。

　　读入设计后，Conformal 中内置的硬件描述语言 （HDL） 规则检查插件可用于检查 lint 错误和警告。这些错误和警告可以根据严重程度进行报告，并且可以添加豁免。使用以下命令报告黄金和修订设计中的错误和警告消息：

　　报告规则检查 -design -error -warning -golden -verbose 》 rpt.rule.golden

　　报告规则检查 -design -error -warning -revised -verbose 》 rpt.rule.revised

　　3.设计约束规范

　　在设计中插入测试设计 （DFT） 后，将添加某些端口/引脚用于调试目的。例如，scan_in、scan_out、scan_mode 和 scan_enable。在比较 RTL 与 DFT-RTL 设计时，由于这些额外的端口，设计将是非等效的。因此，有必要将设计置于黄金设计和修订设计的通用功能模式中。这可以通过在设计中添加约束来实现。

　　例如，在下面的图 4中，左侧的触发器是黄金设计中的常规 D 触发器，而右侧的触发器是扫描插入后修订设计中的可扫描 D 触发器。黄金设计中的 D 输入是 D in的函数，而修订设计中的 D 输入是 D in、scan_in 和 scan_enable 的函数。因此，当工具将向量传递给两个触发器时，它们将被标记为不等价。但在功能模式下，scan_enable 将始终为零。因此，如果在 scan_enable 上添加约束以将其绑定到 1‘b0，则黄金设计和修订设计在功能模式下将相等。

　　添加引脚约束 0 scan_enable-revised

 

 

　　图 4这是扫描插入后黄金 DFF 与修订后 DFF 的样子。

　　4.建模指令规范

　　综合后，综合工具的网表输出将进行功率优化。因此，黄金设计中的任何时钟门控逻辑都将转换为基于锁存器的时钟门控，如下面的图 5所示。许多此类优化将由不同的工具完成，有必要仔细审查它们并添加建模指令以匹配两种设计。以下命令可用于为时钟门控优化添加建模指令：

　　设置展平模型-gated_clock

 

 

　　图 5这是黄金 DFF 与修订后 DFF 在功耗优化后的样子。

　　5.切换到LEC模式

　　添加所有设置约束和建模指令后，必须将工具切换到 LEC 模式以映射关键点和比较。这是通过使用以下命令完成的：

　　设置系统模式 lec

　　6. 映射过程

　　当工具设置为 LEC 模式时，工具会自动映射关键点，例如初级输入 （PI）、初级输出 （PO）、DFF、D 锁存器、黑盒、Z 门和切割门。首先，该工具使用基于名称的映射，然后是基于函数的映射。顾名思义，在基于名称的映射中，工具映射基于黄金和修订设计中的网络/变量的名称。在基于函数的映射中，该工具分析关键点的输入逻辑锥并基于它进行映射。基于名称的映射比基于函数的映射需要更少的运行时间，因此该工具会在切换到基于函数的映射之前尝试使用基于名称的映射来映射关键点。

　　必须映射所有关键点。但是第一次运行 LEC 时，并不是所有的关键点都会被映射。这是因为 IC 设计过程中使用的不同工具进行了优化。例如，综合工具根据设置将RTL中的寄存器/ dma_reg［0］［1］重命名为netlist中的/ dma_0_reg［1］。基于名称的映射将无法匹配此关键点，而基于函数的映射可能会或可能无法匹配此关键点，这取决于逻辑锥的复杂性。在这些情况下，应为工具提供重命名规则，以便映射这些关键点。以下重命名规则将解决上述未映射的关键点：

　　添加重命名规则 REG1 “%d_reg\［%d\］” “reg［@1］［@2］” -revised

　　7.比较过程

　　仅在映射的关键点上进行比较。因此，如前所述，重要的是应该映射所有关键点。该工具将尝试通过将所有输入组合传递给逻辑锥来证明等效性并检查输出行为。在比较过程之后，该工具会将关键点分类为等效点、反向等效点、非等效点和中止点。除等效关键点外的所有类别都应调试。如果所有比较点都相同，那么我们可以得出结论，黄金和修改后的设计是匹配的。

　　在LEC模式下可以使用如下命令调用比较过程，比较后会显示如图6所示的信息：

　　添加比较点-所有比较

 

 

　　图 6所示的 LEC 日志摘要是非等效的黄金和修订设计。

　　如上所述，每次设计更改时运行回归和其他复杂模拟并不是验证设计的有效方式。在这种情况下使用 LEC 工具表明，可以用更少的运行时间验证设计。按照上述步骤使用 Cadence Conformal 进行 LEC 将简化整个过程并显着减少调试时间。

　　Deekshith Krishnegowda 是 Marvell Technology 圣克拉拉办事处的 IC 设计工程师。