北京智芯微电子科技有限公司 段丽莹 胡 毅 郝 燚 甘 杰 冯文楠 唐晓柯

随着系统级芯片（System on Chip，SoC）中输入/输出（I/O）接口数量和复用功能的不断增加，I/O复用电路的验证变得越来越复杂，并且需要耗费大量时间。本文针对I/O复用电路的特点，提出一种基于静态形式验证的高效验证方法，在验证早期对I/O复用进行了复用功能验证和连接性验证，同时也进行了翻转覆盖率收集。与传统基于动态验证的方法相比，本方法可以将验证时间缩短一半以上，显著提升了设计质量和开发效率。

芯片验证是芯片开发流程中必不可少的环节，芯片验证的目标是全面，快速，简单并高效。随着芯片设计技术和制造工艺技术的发展，主流系统级芯片（System on Chip，SoC）的集成度不断增加，使芯片具有越来越复杂的功能；同时，芯片面积和物理边界在不断减小。在这种环境下，芯片的输入/输出（I/O）接口面临着功能需求增加与面积限制的矛盾。为解决这一问题，现今的SoC中普遍采用了I/O复用技术。传统方法使用系统级仿真验证来验证I/O复用功能，需要在系统级别编写场景测试例（case），然后可以配合进行相关的断言验证。然而随着SoC复杂度的提升，I/O接口的数量和复用功能也都随之增加，从芯片级别对I/O复用进行验证需要编写复杂的测试例组合并且花费大量时间。如何实现I/O复用电路的高效验证成为了芯片验证工作中的一个重大挑战。

静态形式化验证（formal）方法是通过形式数学方法来证明断言或属性，以确保RTL代码的正确性。……