在现代集成电路（IC）设计中，先进封装技术的应用越来越广泛。这些技术集成了多个IC和高带宽内存（HBM），导致了复杂的互连问题，给传统的验证方法带来了巨大的挑战。
传统验证方法依赖于手工过程和电子表格，对于具有超过500,000个连接的设计来说是不足够的。这种方法容易出错且效率低下，特别是在高性能计算和人工智能领域。
为了应对这些挑战，一种新的验证方法——形式验证正在逐渐兴起。形式验证通过数学分析来验证所有互连，确保设计的正确性和高效性。
现代IC封装设计面临的挑战
过去，IC封装设计相对简单，主要是将芯片凸点扩展到印刷电路板上。然而，随着异构集成和高级封装技术的发展，这项任务变得更为复杂，需要系统级的整合。
封装设计师现在需要处理来自多个工程师的多种输入，并确保电气和功能上的正确性。由于连接数量通常超过500,000个，手动验证已经变得不切实际。而依靠电子表格进行验证则容易出错且繁琐。
传统验证方法的局限性
传统验证方法难以跟上现代设计的步伐。功能验证需要模拟设计以确保其正常运行，这对于封装设计来说尤其困难。它要求每个芯片都有功能模型，还需要模型和测试平台。
当涉及到像HBM这样的芯片时，这些模型可能不易获得，即使获得了，封装设计师也缺乏适应和使用它们的专业知识。
布局与原理图验证（LVS）虽然有助于确保物理实现与源网表一致，但并不能验证设计的功能正确性。它可以检测短路和断开，但不能确认设计是否按预期工作。如果源网表本身存在错误，LVS也无法捕捉到这些错误，这可能会造成虚假的安全感。
形式验证：一种新的范式
形式验证提供了一种替代解决方案，通过数学分析来彻底验证所有互连。该方法只需要两个关键信息：
- 系统顶层模块及其连接信息
- 各芯片模块端口定义
形式验证不需要冗长的测试台或断言。它可以检测连接错误，确保连接的正确性，并识别潜在的短路。由于该方法使用数学分析考虑所有可能的刺激，因此可以证明连接的正确性，而不会遗漏任何场景。
Innovator3D IC 和 Check Connect
西门子EDA的Innovator3D IC（i3D）工具帮助工程师应对现代封装设计的复杂性。i3D从各种来源收集数据，例如芯片、BGA和网表数据，并允许创建系统连接。连接可以以多种格式导出，包括Verilog，用于验证目的。
Siemens的Check Connect是一个形式验证工具，用于验证封装设计的连接。它使用黄金参考模型，通常由设计团队在设计阶段通过广泛的仿真开发而成，并自动提取连接以验证设计。该工具与i3D封装设计工具一起生成Verilog网表，并验证连接。该工具还可以生成缺失端口报告，列出未被任何连接覆盖的端口，帮助识别参考模型或连接规范中的潜在问题。该工具非常快速，可以在几分钟甚至几秒内验证大量连接。测试案例显示，对于具有超过20,000个连接的设计，验证时间低至30秒，对于具有超过40,000个连接的设计，验证时间为56秒。
形式验证流程
形式验证流程的优点：
- 全面验证：形式方法通过数学分析所有可能的场景，确保连接的正确性。
- 早期检测：错误可以在原型制作后立即被检测到，节省时间和金钱。
- 自动化：整个流程是自动化的，从创建连接规范到验证包装输出连接。脚本简单且可以重用不同的项目。
- 速度快：自动并行算法可以在计算网格上验证大量的连接，在几分钟甚至几秒钟内完成。测试案例表明，对于具有超过20,000个连接的设计，验证时间低至30秒，对于具有超过40,000个连接的设计，验证时间为56秒。
- 提高可靠性：形式验证在航空航天和汽车等严格监管标准的行业中至关重要，因为它可以提供连接的全面分析，某些工具已通过ISO 26262认证。
结论
白皮书展示了形式验证是解决现代IC封装设计挑战的有效方法。通过自动化验证过程，它确保早期连接的正确性，从而提高质量和缩短上市时间。设置这些形式工具的学习曲线只需几分钟。这种方法有望成为现代IC封装设计流程中的重要组成部分。