一种基于静态形式验证的I/O复用电路高效验证方法

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

随着系统级芯片（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代码的正确性。属性验证（formal property verification，FPV）是一种典型的静态形式验证方法，已经被证明是设计验证签收（signoff）的一种可信赖的方案。但是，随着设计逐渐变复杂，设计的容量和复杂度都会对使用形式化验证方法带来制限，如果没有任何人工抽取方法是无法实现全覆盖的验证。本文提出了使用静态验证工具VC Formal CC来完成I/O复用的单体和SoC级别的验证，无需搭建新的验证平台，也不需要编写专门的验证case。同时VC Formal CC可以产生覆盖率数据，并合并到芯片级的覆盖率数据中，有效提高了I/O复用电路验证的效率和完备性。

1 基于静态形式化验证的连接性检查

在芯片设计的验证中，连接验证是最基本的验证内容。连接可以通过形式化验证方法完成完全的验证，但是需要执行FPV设计人员将SoC分成不同的子系统，手动将不进行验证的模块黑盒化，并使用常量和假设来约束设计。因此，验证过程需要消耗大量的人力和时间。

连接性检查（Connectivity Check，CC）应用是在形式化验证的基础上建立的。与FPV相比，CC是一个自动check的工具，可以实现高效的验证工作。CC通过读取CSV表格自动提取设计并分析连接检查的需求。然后自动产生连接检查需要的断言和假定。因此理想化来说，CC执行属性检查，但是并不需要用户再建立检查器（checker）。该工具会帮助时钟产生，重置（reset）产生和断言产生。CC工具在设计提取方面具有强大的功能，能够解决庞大的SoC编译的问题。

静态验证工具VC Formal CC的目标应用包括结构检查和功能检查两方面。结构检查是检查从源到目标是否有一个结构连接/路径。功能检查是检查设计中的两个信号是否具有同样的值，注意是在特定的条件，比如数据选择器（multiplexer，MUX）逻辑。虽然传统方法中使用动态仿真也可以进行功能检查，但是它不能进行结构检查。

连接性检查有组合逻辑和时序逻辑两种应用场景。在组合逻辑的应用中可以验证SoC I/O连接，模块引脚复用/解复用，可配置多路复用，模块的连接和常值检查，在子模块间的直接连接等内容。在时序逻辑的应用中，VC Formal CC可以支持检查待延迟的路径，比如在源-目的路径上有触发器（FlipFlop），和使能（enbale）路径上有触发器的路径。在本工作中CC工具的使用主要是完成组合逻辑中的I/O复用进行的验证。

2 IO复用的电路特征以及验证目标

对于目前的SoC的焊盘（PAD）来说，大多数PAD属于通用I/O（genneral Purpose I/O，GPIO）。常见的GPIO型PAD单元均为双向I/O，除了输入/输出数据使能，还包括上下拉使能，驱动能力使能等。为了实现高集成度和尽可能小的芯片面积，有限的I/O就通过PINMUX模块和寄存器的不同配置来实现GPIO的复用。PAD的复用从功能角度具有以下两个特点：

（1）I/O复用情况复杂

实际上，SoC的每一个PAD在大部分的工作时间内都属于自己主要服务的模块，这是其最基本的属性。但除此之外，它们还承担着转接到其他模块并协助传输数据的任务。当I/O被切换到其它功能时，功能控制的选择、输入输出方向控制逻辑等都是通过相关寄存器的配置来实现。

（2）工作模式的不同

在SoC的开发中，还会加入可测性设计模块（Design For Test，DFT）。因此，I/O复用的电路也要把测试功能考虑进去。

图1 IO复用在系统级的验证对象

图2 VCForaml CC需要的CSV文件格式和TCL命令

简单来说，I/O复用实际上是利用一个巨大的MUX实现的。针对IO复用的结构，如果使用常规的验证方法，从搭建验证环境到验证case的完成，工作量很大，并且工时较长。而这种情况对于连接性检查工具CC check来说，正是它的优势所在。通过使用CC check，不需要搭建专门的验证环境，只需要提取验证要点，配置验证参数，验证工具可以自动生成测试向量，并进行验证。由此可以大幅提高I/O模块的验证效率，缩短产品开发周期。由于CC check使用的是静态的数学理论实现测试向量的生成，极大地提高了验证的完备性。

本工作的目标是在芯片级别验证从各IP模块经过PINMUX到IO PAD的验证。图1是系统级I/O复用验证对象示意图。其中灰色部分在连接性验证中都是黑盒化，蓝色部分是验证的对象。

3 VC Fomral CC在I/O复用中的验证流程

在进行连接性检查之前，虽然使用测试case对IO复用进行了部分功能的验证，但是对整个I/O复用的全部功能来说，这些验证是不充分的，因此使用CC check对剩余的连接性进行验证。在连接性检查完成后，使用VC Formal CC产生的覆盖率数据可以合并到芯片的覆盖率数据中，完善SoC系统的连接性验证。

使用VC Formal CC验证I/O复用的流程如下：

（1）首先要根据I/O复用的设计spec抽取生成CC check需要的CSV表格

项目开始前需要准备一个CSV表格，它是VC Foraml CC用来连接验证的输入格式。这个表格就是一个CC测试计划，如图2所示，它包括源信号，目的信号，使能条件，复位，不同的延迟设置等。

图3 CC check建立流程

（2）准备和运行TCL文件

在RTL和Formal流程中都是用的是工具命令语言（tool command language，TCL）。整个CC check流程建立中的设置如图3所示。其中，定义复位信息可以支持多复位设置，打开自动黑盒子功能可以在连接验证目标的基础上对设计进行提取。通过使用命令Check_fv，在产生断言后，会自动的执行check_fv和保存CC check的结果。

由于本SoC中的I/O复用模块完全由组合逻辑构成，所以在脚本中没有对时钟和进行设置。在进行SoC中的I/O复用部分的验证时，我们可以把不关心的连接验证的设计部分进行黑盒化处理，这样可以进一步减少VC fomal CC工具分析对象的数量，在满足验证完备性的前提下节省仿真时间。VC Formal CC中提供了自动识别黑盒化的命令。图4是本I/O复用验证中的部分黑盒化的list示意图。

图4 IO复用验证中部分黑盒化list

图5 使用Verdi GUI界面进行debug

（3）查看结果，debug，和锁定bug

在编译了RTL和CSV之后，VC Formal工具会为每个定义在CSV文件中的连接验证生成断言，在CSV文件中描述了n个连接检查，就有n个断言产生。

“check_fv”命令能够自动执行这些断言检查，在进行了第一个检查后，会发现有一些断言失败。我们查找了原因，一些是因为CSV文件中连接定义不正确，其余的是真正的RTL中的连接bug。

图6 IO复用验证的结果

图7 IO验证toggle结果

图8 未toggle的信号调查

表1 本次验证工作结果总结

表2 传统验证方法和本方法的对比

Debug的方法有两种，一种debug方法是使用命令行。在命令行中使用analyze_root_cause和report_root_cause两个命令，命令行会报出连接错误的原因。通过显示的描述可以查找断言fail的原因。另一种是使用VC Fomral CC的图形用户界面（Graphical User Interface，GUI），使用GUI可以同时观测电路和波形，更加快速和便利。这种图形化界面使得debug更直观和便捷。图5是一个fail的实例。通过GUI可以看到缺少一个enable的控制点（红圈部分）。这种属于CSV中enable定义不全。

4 验证结果

图6是本次IO复用CC Check验证的最后结果。CSV中定义的所有的验证项目全部pass。我们还可以把收集的覆盖率数据与SoC的仿真覆盖率数据合并在一起。通过GUI就可以直接的看到翻转（toggle）结果。图7是本工作中针对IO复用的CC check的覆盖率结果，结果显示有16个信号没有toggle。除此之外，其他信号全部都实现了toggle。图8是未toggle信号的列表，经过调查这些信号在IP内是被固定为常值的。

使用VC Formal CC容易地验证连接性，并且实现toggle的覆盖目标。研发人员可以在设计早期发现IO复用的连接错误。由于免去了搭建chip级验证环境和编写验证case，assertion的工作，大大提升了验证工作的效率，节省了产品开发时间。表1是对本次验证工作结果的总结。表2是使用传统验证方法和使用VC Formal CC工作量的比较。

总结：静态形式验证作为芯片signoff的重要方法已经被应用到先进SoC芯片的验证流程中，VC Formal CC更是简化了Formal执行者的工作量，可以节省大量的人工，并且在连接性的结构性检查中具有很大的优势。本文使用VC Fomral CC实现了IO复用的验证，在设计初期，不需要搭建验证环境，不需要编写验证case，就可以对IO复用功能进行验证，进而可以提前发现设计缺陷，缩短验证时间。