芯技术 | IC设计:基于形式化方法的验证找bug
发布网友
发布时间：2024-10-24 09:47
共1个回答
热心网友
时间：1天前
硬件成为芯片世界的新货币，半导体行业不再仅是传统巨头的领域。随着软件公司的硬件开发团队兴起，以及开源架构的普及，使用开源框架和工具开发芯片成为主流。
尽管芯片设计变得更易实现，芯片验证却依然挑战重重。2020年研究指出，83%的FPGA设计和68%的ASIC设计在首次流片尝试中失败，68%的ASIC项目实际执行低于预期，这表明验证成本占项目总成本的约70%。
验证工程师与设计工程师的比例为5:1，意味着需要雇佣多出设计五倍的验证资源，而芯片重新流片的情况频繁发生。验证面临的挑战涉及成本上升、项目进度延迟和人员重新分配。
功能验证并非唯一挑战，ISO 26262、DO-254和DO-333等标准下的责任与可靠性同样重要。Meltdown和Spectre漏洞后的安全防护问题也日益突出。硬件开发和上市时间的竞争要求质量和可靠性同步提高。
软件动态仿真是传统的芯片验证主力，并在数字和模拟电路设计验证中占主导地位。硬件加速仿真虽初期成本高，但重视硅片质量的公司都在使用，它提供更高的速度，是一种更快的仿真形式。
动态仿真和硬件加速仿真利用测试案例，以输入序列或程序测试底层硬件。设计与实际行为不匹配时会被标记为设计或测试bug。测试案例只能显示bug的存在，不能证明其不存在。
形式化方法提供了一种基于证明的方法来验证bug的存在。它使用数学模型和断言或覆盖目标的证明，基于人工智能的搜索技术和逻辑推理，以符号化方式显示设计。形式化方法在硬件符号模型上工作，自动抽象设计空间的指数级复杂性，建立断言或覆盖属性的证明。
如果不能建立证明，工具会显示一个反例波形，就像在仿真中一样，用于修复设计bug。形式化工具的智能详尽搜索通常可以更快找到容易忽略的bug，且在许多情况下比仿真或模拟测试平台更容易发现更多bug。
在大型项目中，仿真是验证的主要技术。形式化方法的使用仍然限于解决简单问题，如项目早期的lint，或项目后期的SoC连接性检查。在项目生命周期的前五个步骤中，形式化方法发现bug，而仿真测试平台耗尽能力时，形式化方法通常在生命周期的最后阶段启动。
通过形式化验证发现1000万甚至1亿多次失败的关键在于一个良好的方。通过避免在设计开发的第一个小时内使用形式验证工具，检测设计更改的每次迭代中的bug，删除结构设计缺陷，证明设计正确性，完成流片。
形式验证的覆盖率和签核是通过工具提供的，从设计开发的第一个小时到完整的芯片测试，都可获得覆盖率信息。六维覆盖是确保签核质量的关键，包括需求驱动的目标、断言和覆盖点数量、检查器完整性、过度约束分析、代码覆盖率和场景覆盖。
形式化方法在IC设计验证中是一种强大的技术，设计验证小组正在逐步将其应用于实践中。形式化方法的使用有助于解决验证中的挑战，提供更可靠的芯片设计。
