DFT设计中的Formal Check验证技术与实践

1. 项目概述

在芯片设计领域，DFT（Design for Testability）技术是确保芯片可测试性的关键环节。作为一名从业多年的DFT工程师，我经常需要面对一个核心问题：如何在插入测试电路的同时，确保原始功能电路不受影响？这正是Formal Check（形式验证）流程存在的意义。

想象一下，你花了数月时间设计了一个精密的PLL控制电路，却在DFT插入阶段因为测试寄存器的引入导致功能失效 - 这种情况在实际项目中并不罕见。Formal Check就像一位严格的"电路校对员"，它能通过数学方法证明DFT修改前后的电路在功能上是否等价。不同于仿真验证需要大量测试向量，Formal Check能穷举所有可能状态，确保万无一失。

2. DFT插入流程与验证需求

2.1 RTL Flow的双重验证

在RTL级别的DFT插入流程中，我们需要进行两次关键的形式验证：

1. RTL级别验证：

• 对比对象：原始Function RTL vs 插入MBIST/EDT后的DFT RTL
• 验证重点：测试逻辑的插入是否正确，是否引入非预期的功能修改
• 典型问题：测试寄存器默认值设置错误导致功能模式异常

2. Netlist级别验证：

• 对比对象：后端综合网表 vs 完成Scan Insertion后的DFT网表
• 验证重点：扫描链插入是否影响时序路径，测试复用逻辑是否正确实现
• 典型问题：扫描链stitch错误导致功能路径被切断

重要提示：RTL Flow中两次验证缺一不可。我曾遇到一个案例，RTL验证通过但网表验证失败，最终发现是综合优化移除了关键的测试控制逻辑。

2.2 Netlist Flow的集中验证

对于Netlist Flow，验证相对集中但挑战更大：

1. 单次网表级验证：

• 对比对象：原始综合网表 vs 完整DFT网表（含MBIST/OCC/EDT）
• 特殊挑战：需要处理多组网表的整合验证
• 典型问题：不同综合策略导致的逻辑锥不一致

在实际操作中，我推荐采用以下验证策略：

• 对memory BIST：重点验证BIST控制器与memory接口的隔离性
• 对logic测试：验证OCC时钟切换和EDT压缩逻辑的透明性
• 对scan链：验证stitch后的扫描路径不影响功