在3D芯片设计中，多个晶片（Die）通过中介层（Interposer）堆叠连接，能大幅提升性能和集成度。但这种设计也带来了一个巨大的挑战：如何验证数以万计的信号连接是否正确？Xilinx团队用一套名为Formal App的自动化工具，将验证时间从数月缩短到几小时，并成功拦截了13个隐藏错误。以下是他们的实战经验。

---

传统仿真方法的困境

过去，Xilinx使用基于仿真的方法验证连接性。但面对3D IC设计时，问题来了：

• 规模爆炸：即使小型同质结构（Homogeneous）芯片也有上万条连接，异质结构（Heterogeneous）芯片更复杂。
• 效率低下：仿真需手动编写测试平台，覆盖所有场景需耗时数月。
• 风险高昂：一旦漏检一个连接错误，可能导致芯片返工，影响市场进度。

团队意识到，必须找到一种全覆盖且自动化的验证方案。

---

Formal App的核心思路：形式验证+自动化

Formal App的核心是形式验证（Formal Verification）——通过数学证明而非仿真，确保设计符合规范。具体实现分为三步：

1. 从Excel表格生成断言（Assertions）

• 输入：连接性规范表（Excel），明确每条信号的起点（Source）和终点（Destination）。
• 自动化脚本：用Perl解析表格，生成SystemVerilog断言。例如：

  CHECK_LVL_B2_10_to_LVL_B10_9_m0_to_s2:  
    assert property (dut.m0.slice.LVL_B2[10] == dut.s2.slice.LVL_B10[9]);

   
• 断言捆绑（Bundling）：将多个独立断言合并，减少验证次数。例如，将100条连接合并为1个断言组，运行效率提升50倍。

2. 黑盒化处理与层次保留

• Black Boxing：用工具bbgen剥离模块内部逻辑，仅保留接口，减少验证复杂度。
• 保持层次结构：尽管3D设计有4-8层嵌套，工具仍保留层次信息，确保与物理设计一致。

3. 一键式运行与结果解析

• 命令行启动：用户只需输入顶层模块名、配置文件路径等参数，工具自动调用Cadence Incisive Formal Verifier。
• 快速定位错误：若断言失败，工具生成反例（Counter Example），直接标出错误连接路径。

---

实战效果：从24小时到1小时

案例1：同质结构验证

• 设计：多个FPGA Die通过中介层连接。
• 挑战：24,863条连接，传统仿真需数周。
• 结果：
  • 初始单条断言验证耗时37秒，总时间约24小时。
  • 通过断言捆绑，将断言数从24,863降至91条，总时间缩短至1小时。

案例2：异质结构验证

• 设计：混合FPGA、处理器、高速接口等多种IP。
• 挑战：连接模式复杂且不重复。
• 结果：工具成功解析所有独特连接，发现13个设计错误，包括信号错位和规范表错误。

---

三大优势与未来扩展

1. 全覆盖验证：形式验证穷举所有可能场景，避免仿真遗漏。
2. 极简用户体验：工程师无需懂形式验证，像执行普通脚本一样操作。
3. 灵活适配：支持同质/异质结构、不同层数设计，适应快速迭代需求。

未来方向：

• 扩展至更多EDA工具链，如Synopsys VC Formal。
• 支持动态连接验证（如电源管理场景下的信号通断）。

---

总结：验证效率的革命

Formal App的成功证明，自动化和形式验证是解决超大规模芯片验证难题的关键。对于3D IC、Chiplet等先进封装技术，这类工具将成为避免“连接灾难”的标配。正如Xilinx团队所言：“过去认为‘设计即正确’的时代已结束，验证必须比设计更快更准。”

---

工具链速览：

• Cadence Incisive Formal Verifier：底层形式验证引擎。
• Perl脚本：自动化生成断言与结果解析。
• Excel模板：定义连接规范，人机双读。

参考文章
A Reusable, Scalable Formal App for Verifying Any Configuration of 3D IC Connectivity

数字芯片资料不定时更新，建议转存。
链接：https://pan.baidu.com/s/1QJXXQoU3Wly6KaGShT7jlg?pwd=3uMy提取码：3uMy复制这段内容打开「百度网盘APP即可获取」