基于形式化验证的芯片IO复用验证方法

摘要

本发明公开了一种基于形式化验证的芯片IO复用验证方法，包括如下步骤：S1、根据芯片规定定义，提炼芯片IO复用关系文件；S2、根据芯片IO复用关系文件，自动形成IO描述文件；S3、开启形式验证，同时导入芯片文件和IO描述文件到验证工具；S4、启动形式化验证，输出验证结果；S5、分析结果，判断是否为设计BUG。优点，本发明验证方法，相比传统的Uvm验证,基于形式化验证的IO复用验证技术使用简单，步骤简洁，大幅降低了工作量；该方法无需芯片系统级仿真运行，因而运行时间短，大幅提升了验证效率。

说明书

技术领域

本发明涉及一种基于形式化验证的芯片IO复用验证方法。

背景技术

验证是现代化芯片研制中非常重要、不可或缺的环节，其使命是确保设计功能符合设计预期，没有故障。通常在一个芯片研制项目中，芯片验证所耗费的时间和人力资源可占到70%。

主流的传统验证方法主要是以UVM(Universal Verification Methodology)和SystemVerilog为代表的验证方法学，通常采用随机约束+定向激励相结合的方式，在电路仿真中自动产生激励，驱动电路运行，完成验证功能。

目前形式化验证目前越来越受到关注，其主要思想是基于对芯片设计抽象出的数学表述和模型，根据设计规约对设计功能进行属性描述，并自动进行数学分析和证明。

而传统验证方法的缺点是1、UVM验证仿真时间长；2、工作量大，完备性难以保证。由于UVM验证需要驱动芯片仿真运行，而现代芯片规模急剧扩增，目前大型的服务器级CPU芯片已可达百亿门规模，在一定的仿真计算资源条件下，随着芯片规模的提升，其系统级仿真运行的时间大幅提升。由于UVM传统方式验证，需要对每一个功能项搭建验证场景，提供验证激励，分析输出结果并判断是否符合预期，现在芯片规模急剧提升，集成度越来越高，内部部件之间的相互联系越发复杂化，所需验证的功能项也出现了爆发性增长，所需的人力成本极高，且很容易出现场景上、激励上或者结果分析上的缺失导致功能验证完备性不够。

对于大规模复杂芯片，往往存在IO管脚上的多功能复用，可通过寄存器的不同配置，灵活的使IO管脚实现不同的接口功能。对于该复用技术的验证，如果采用传统的UVM验证方法，则需要搭建验证环境，针对每个管脚的每个功能，进行相关配置，提供IO管脚上或者芯片内部的不同激励，在芯片内部或者IO管脚进行观测，对结果进行判断，首先大规模芯片运行时间较长，SoC芯片仅仅CPU核的boot启动就有相当长的时间消耗，其次工作量极大，对于典型的mcu芯片，如果有40个管脚，平均每个管脚有5个功能复用，则该验证过程需要编写200次。

发明内容

本发明提出一种基于形式化验证的芯片IO复用验证方法，可大幅提升该类验证的效率。该形式化验证方法无需芯片的仿真运行，只需编译后，调用形式化验证工具（常见的如VC Formal或者Japer Gold），并结合提供的IO复用的关系表格，即可进行自动化的分析和验证，最终输出结果，首先能大幅提供工作效率，降低人力成本和时间成本消耗，其次将测试的完备型来源浓缩到根据芯片spec，编写IO复用关系文件上，降低了出现完备性下降的风险。

采取的技术方案如下：

一种基于形式化验证的芯片IO复用验证方法，包括如下步骤：

S1、根据芯片规定定义，提炼芯片IO复用关系文件；

S2、根据芯片IO复用关系文件，自动形成IO描述文件；

S3、开启形式验证，同时导入芯片文件和IO描述文件到验证工具；

S4、启动形式化验证，输出验证结果；

S5、分析结果，判断是否为设计BUG。

对本发明技术方案的优选，S1中，根据芯片设计文档，撰写一份芯片IO复用关系文件，芯片IO复用关系文件包括类型和信号名，类型为输入项input、输出型output或输入输出兼备inout；信号名包括功能复用项的信号名和每项复用后的信号名。

对本发明技术方案的优选，S2中，IO描述文件是根据芯片IO复用关系文件中的信息，撰写一份相应的脚本配置文件；IO描述文件内的每个管脚，将每个input型和每个output型的复用功能点均扩展为一个表项，将每个inout型的复用功能点均扩展为两个表项。

对本发明技术方案的优选，每个表项均包括管脚在芯片代码里的层次路径、芯片内部驱动该复用功能点或者受其驱动的信号、使能条件和测试名称。

对本发明技术方案的优选，S3中，验证工具为VC Formal。

对本发明技术方案的优选，S3中，开启形式化验证工具，进行相关功能配置，导入芯片源代码文件，并进行编译综合成网表, 再导入IO复用描述文件，获取待测试的每一个表项，设置初始化状态，时钟、复位信号。

对本发明技术方案的优选，S4中，启动验证，通过IO描述文件的每个表项的输入、输出和使能条件，进行连接性测试，判断IO复用的正确性，并输出结果，对结果进行分析。

对本发明技术方案的优选，S5中，IO复用方式与设计文档不匹配，打印出错误信息来进行结果分析；当打印出的信息表示某引脚出错，就表示在当前脚本设置的条件下，芯片文件中引脚的复用情况与脚本设置不一致；当出现了上述不一致，可能为两种情况，其一是芯片文件有错误，即设计BUG，其二是脚本写的有错误，即使能条件设置不准确。

对本发明技术方案的优选，当验证结果出现问题，则判断是芯片IO复用的设计BUG，还是表项的使能条件设置不准确；如果是后者，则修改迭代S2的表项，重新启动S3和S4，进行下一轮测试，直到所有设计Bug被发现为止。

本发明与现有技术相比的有益效果是：

1、本发明的验证方法，相比传统的Uvm验证,基于形式化验证的IO复用验证技术使用简单，步骤简洁，大幅降低了工作量。

2、本发明的验证方法，该方法无需芯片系统级仿真运行，因而运行时间短，大幅提升了验证效率。

附图说明

图1为本发明验证方法的流程框图。

图2为本实施例的IO复用关系文件的示意图。

具体实施方式

下面对本发明技术方案进行详细说明，但是本发明的保护范围不局限于所述实施例。

为使本发明的内容更加明显易懂，以下结合附图1-图2和具体实施方式做进一步的描述。

为了使本发明的目的、技术方案及优点更加清楚明白，以下结合附图及实施例，对本发明进行进一步详细说明。应当理解，此处所描述的具体实施例仅用以解释本发明，并不用于限定本发明。

本实施例的一种基于形式化验证的芯片IO复用验证方法，包括如下步骤：

S1、根据芯片规定定义，提炼芯片IO复用关系文件；

S2、根据芯片IO复用关系文件，自动形成IO描述文件；

S3、开启形式验证，同时导入芯片文件和IO描述文件到验证工具；

S4、启动形式化验证，输出验证结果；

S5、分析结果，判断是否为设计BUG。

本实施例中，S1中，根据芯片设计文档，撰写一份芯片IO复用关系文件，芯片IO复用关系文件包括类型和信号名，类型为输入项input、输出型output或输入输出兼备inout；信号名包括功能复用项的信号名和每项复用后的信号名。

如图2所示，例如第一项芯片管脚P0[6]可复用为以下4个功能，I2S_RX_SDA类型为输入，SSP1_SSEL输入输出型，T2_MAT0输出型以及U1_RTS输出型。

本实施例中，S2中，IO描述文件是根据芯片IO复用关系文件中的信息，撰写一份相应的脚本配置文件；IO描述文件内的每个管脚，将每个input型和每个output型的复用功能点均扩展为一个表项，将每个inout型的复用功能点均扩展为两个表项。

每个表项均包括管脚在芯片代码里的层次路径、芯片内部驱动该复用功能点或者受其驱动的信号、使能条件和测试名称。具体为：每个表项涵盖以下部分：

a）管脚在芯片代码里的层次路径，便于形式化工具在芯片中网表中分析定位到该管脚；

b）芯片内部驱动该复用功能点，或者受其驱动的信号（模块级输出）；

c）使能条件（一般配置管脚为该复用功能的寄存器配置，对于output信号需要添加输出使能信号）；

d）测试名称，便于显示成功或者失败时指示是哪项测试。

本实施例中，S3中，验证工具为VC Formal或Japer Gold。这两个验证工具均为本领域内的已知验证工具，本领域技术人员已知。

本实施例中，S3中，开启形式化验证工具，进行相关功能配置，导入芯片源代码文件，并进行编译综合成网表, 再导入IO复用描述文件，获取待测试的每一个表项，设置初始化状态，时钟、复位等信号。

本实施例中，S4中，启动验证，通过IO描述文件的每个表项的输入、输出和使能条件，进行连接性测试，判断IO复用的正确性，并输出结果，对结果进行分析。

S5中，IO复用方式与设计文档不匹配，打印出错误信息来进行结果分析；当打印出的信息表示某引脚出错，就表示在当前脚本设置的条件下，芯片文件中引脚的复用情况与脚本设置不一致；当出现了上述不一致，可能为两种情况，其一是芯片文件有错误，即设计BUG，其二是脚本写的有错误，即使能条件设置不准确。

当验证结果出现问题，则判断是芯片IO复用的设计BUG，还是表项的使能条件设置不准确；如果是后者，则修改迭代S2的表项，重新启动S3和S4，进行下一轮测试，直到所有设计Bug被发现为止。

本实施例的验证方法，是采用形式化验证进行IO复用的验证方法和思路，传统UVM验证方法需要搭建验证环境、构建测试场景、使能测试激励获取测试结果并比对，并针对所有IO管脚的每个功能复用项进行重复测试，工作量巨大，且由于IO复用属系统级功能，需要整个芯片仿真运行，整芯片的系统运行耗时很长，验证效率较低。本专利技术基于形式化验证，步骤简单，且无需芯片系统级运行，只需编译通过，以及根据芯片spec提取和整理可描述IO复用相关表项即可。

具体实施例：

如图2所示，控制P0[6]的IO复用寄存器为P0_6_IOCON，当这个寄存器等于0，1，2，3，4分别对应该四个数字功能。在IO描述文件中设定使能条件为，P0_6_IOCON=3，那么此时芯片内部的信号t2_mat就应该连接到P0[6]端口上。在芯片描述文件中，就把信号t2_mat作为源端，把P0[6]作为目标端。

把IO描述文件和芯片文件同时导入后，工具会自动对比芯片文件中在使能条件下，芯片的连接方式是否与描述文件一致，如果不一致，则会打印报错。

发现报错后，工程师就会检查是IO描述文件撰写有误，还是芯片设计本身存在的BUG，分别处理来排除。

重复上述调试过程，直到所有的IO描述都与芯片文件能全部对应。

以上实施例仅为说明本发明的技术思想，不能以此限定本发明的保护范围，凡是按照本发明提出的技术思想，在技术方案基础上所做的任何改动，均落入本发明保护范围之内。