使用 VC Formal 进行 DFT 时钟验证

SNUG China 2018 2018 9 页

使用 VC Formal 进行 DFT 时钟验证

论文信息

项目	内容
作者	Wei Huang、Feng Huang、Thenappan Nachiappan、Vishal Agarwal（NVIDIA 半导体科技上海有限公司）
会议	SNUG China 2018
页数	9 页

摘要

DFT 时钟设计对于多种 DFT 特性（如扫描、MBIST 和 DFD）至关重要。传统上我们使用仿真工具创建测试平台来监测和检查某些特定的时钟行为。然而，基于仿真的验证的痛点是仿真激励难以提供足够的覆盖率。因为在扫描或某些 DFT 模式下，功能逻辑值将是未知的，而基于仿真的验证在穷举验证这些未知空间方面存在局限性。因此，由于这些覆盖率漏洞，很容易出现流片后失效。

本文提出了一种新的时钟验证方法——使用 VC Formal 属性验证（FPV，Formal Property Verification）通过形式化技术来验证时钟逻辑。我们将使用一个 GPU IP 来介绍如何通过基于断言的形式化测试平台来实现这一点，并列出一些结果数据。

1. 引言

1.1 形式验证简介

形式验证（FV）是使用工具对设计可能的行为空间进行数学分析，而非对特定值计算仿真结果。

形式验证已不再仅仅用于发现缺陷——当前 FV 被视为防止关键任务区域出现缺陷的必备手段。FV 实际上应该被看作一个与设计交互、验证和理解设计的通用工具包。从早期开发一直到流片后调试过程，在每个设计阶段适当利用形式化方法都可以提高设计吞吐量、增强设计信心并缩短上市时间。

仿真 vs 形式验证： - 仿真验证特定输入组合下的行为——它是采样式的。 - 形式验证穷举分析所有可能输入下的行为——它是完备的。

1.2 DFT 时钟挑战简介

DFT 时钟设计的复杂性源于多种 DFT 模式（扫描、MBIST、DFD 等）对时钟行为的不同要求。在功能模式下，时钟路径由功能逻辑控制；在 DFT 模式下，时钟路径由 DFT 逻辑接管。这些模式之间的切换逻辑、时钟门控信号、以及多时钟域之间的交互使得时钟行为的验证变得极为复杂。

传统仿真方法的主要局限： - 未知值（X）传播：在扫描模式下，功能逻辑输出为未知值（X），仿真无法准确预测 X 传播的行为。 - 覆盖率漏洞：仿真激励无法覆盖所有可能的模式切换序列。 - 状态空间爆炸：DFT 模式配置的组合数量巨大。

2. 动机

选择形式验证来验证 DFT 时钟的主要动机是：

- DFT 时钟路径的正确性对于芯片的可测试性至关重要。错误的时钟行为可能导致扫描测试失败，甚至损坏芯片。 - 仿真在 X 处理和覆盖率完备性方面存在根本性局限。 - 形式验证可以穷举验证所有 DFT 模式配置下的时钟行为，提供 100% 的覆盖率。 - VC Formal 的 FPV 功能提供了成熟的断言语言（SVA）和自动化证明引擎。

3. 形式化时钟验证

3.1 VC Formal 版本

本工作使用的 VC Formal 版本支持完整的 SVA 断言语言，以及约束求解和属性证明引擎。

3.2 VC Formal 流程概述

形式化时钟验证流程包括以下步骤：

1. 设计编译：将 RTL 设计读入 VC Formal，建立形式化模型。 2. 约束编写：定义时钟和复位行为、DFT 模式配置的合法范围、输入信号的假设。 3. 属性编写：使用 SVA 编写待验证的时钟属性（assert 断言）。 4. 形式化证明：VC Formal 穷举分析设计空间，证明或反驳每个属性。 5. 结果分析：对于被反驳的属性（counterexample），分析波形追踪并修复设计问题；对于被证明的属性，确认无缺陷。

3.3 VC Formal 环境设置

形式化环境设置包括： - 定义时钟信号和复位信号 - 约束 DFT 模式选择信号的合法组合 - 建立扫描使能、测试模式等控制信号的行为模型 - 对功能逻辑中的无关部分进行"黑盒化"处理以减少验证空间

3.4 VC Formal 约束编码

约束（constraints/assumptions）限定了形式化引擎的搜索空间，确保只探索合法的输入行为。约束的编写需要特别小心——过于严格的约束可能排除真实的缺陷场景，而过于宽松的约束可能导致虚假的 counterexample。

关键约束包括： - 时钟频率和相位关系 - DFT 模式之间的合法切换序列 - 扫描使能信号的时序关系

3.5 VC Formal FPV 编码

属性（assertions）定义了待验证的正确行为。本文针对 DFT 时钟验证定义的关键属性包括：

- 时钟门控信号在所有 DFT 模式下不会意外关闭 - 时钟路径在所有模式配置下保持完整 - 模式切换期间不产生毛刺 - 多个时钟域之间的相位关系在 DFT 模式下正确 - 扫描移位和捕获期间的时钟行为符合规范

3.6 VC Formal 运行时间

在 NVIDIA GPU IP 的实际运行中，VC Formal 在数小时内完成了对所有 DFT 时钟属性的形式化证明。对于大型设计（> 10M 门），采用分层验证策略——先验证叶子模块的独立时钟属性，再验证顶层集成的跨模块时钟行为。该策略有效控制了形式化引擎的搜索空间，使证明时间保持在可管理范围内。

4. 结论

本文提出了使用 VC Formal 进行 DFT 时钟验证的新方法。通过将形式化方法应用于传统上由仿真覆盖的 DFT 时钟验证领域，我们实现了：

1. 100% 覆盖率：对所有可能的 DFT 模式配置和切换序列进行穷举验证。 2. X 处理完备性：形式化引擎天然处理未知值场景，无需担心仿真中的 X 乐观或悲观问题。 3. 早期缺陷发现：在 NVIDIA GPU IP 的实际应用中，形式化验证发现了仿真遗漏的多处 DFT 时钟缺陷。 4. 可复用性：建立的形式化验证环境可以在项目之间复用，减少后续项目的验证工作量。

该方法展示了形式验证从"发现缺陷"向"防止缺陷"转变的趋势——通过在设计阶段系统性地使用形式化方法，可以在流片前建立对 DFT 时钟正确性的高度信心。

参考文献

1. VC Formal User Guide, Synopsys 2. DFT Compiler User Guide, Synopsys

核心概念

概念	说明
VC Formal	Synopsys 形式验证工具，支持 FPV 属性验证
形式验证 Formal Verification	穷举分析设计所有可能行为的数学化验证方法
FPV 形式属性验证	使用 SVA 断言进行属性证明的形式验证方法
DFT 可测试性设计	芯片可测试性设计，时钟验证是 DFT 质量的关键环节
SVA SystemVerilog 断言	SystemVerilog 断言语言，用于编写形式验证属性和约束

图片索引

本文共 6 张图片，存放于原文 _images/ 目录。

第 1 页： -

第 6 页： -

第 7 页： -

第 8 页： - - -

使用 VC Formal 进行 DFT 时钟验证