CN117435483A - 基于Formal工具的仿真验证激励生成方法、装置、介质及终端 - Google Patents

Abstract

本申请提供一种基于Formal工具的仿真验证激励生成方法、装置、介质及终端，包括：利用Formal工具对属性数据进行覆盖验证；若验证结果为属性数据能被覆盖，则基于属性数据被覆盖的事件发生时所对应的目标输入信号值生成输入接口信号时序数据；基于UVM环境采集所述输入接口信号时序数据，以还原生成属性数据对应的输入接口信号激励序列；将输入接口信号激励序列进行封装以获取输入接口信号激励序列库，以供在UVM测试用例中进行仿真调用；基于UVM环境对输入接口信号激励序列库和属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。本申请提升了生成对应命中待测试设计相应场景的验证激励的效率、节省时间。

Description

基于Formal工具的仿真验证激励生成方法、装置、介质及终端

技术领域

本申请涉及芯片验证领域，特别是涉及一种基于Formal工具的仿真验证激励生成方法、装置、介质及终端。

背景技术

在当前超大规模集成电路芯片项目的工作中，验证工作占据了相当大的比例，使用UVM验证方法学进行仿真验证是“前端验证”工作(有别于物理验证，FPGA验证，EMU验证等其他验证阶段)的主流手段，验证工程师在搭建好验证平台之后，相当长的一段时间，工作的主要内容是构造测试用例，测试用例本质上是通过写DUT输入接口的激励序列，来让DUT工作起来并且采集DUT的输出信号，以期望发现DUT的行为与验证平台的参考模型行为不一致的地方，从而发现错误，反馈给设计人员进行修正；该事项在项目进行过程中不断重复迭代前进，直到验证计划中的所有验证项都已构建好测试用例(激励)，且全部通过比对之后，可以认为仿真验证工作结束。

然而，基于UVM验证环境的验证激励大多数是基于CRT随机生成激励数据，来期望命中意料之外的错误，激励生成的随机规则基本上只依赖于DUT的输入接口协议，所以偶然性很高，并且往往需要通过大量时间的回归测试，才可能命中错误。另外，对于些更深层级的错误，验证激励不容易生成，而随机激励中的测试用例可能无法命中相应的场景。

发明内容

鉴于以上所述现有技术的缺点，本申请的目的在于提供一种基于Formal工具的仿真验证激励生成方法、装置、介质及终端，用于解决现有技术中构造达成待测试设计内部场景的定向验证激励时，需要分析待测试设计的代码结构，并且不好生成验证激励、验证激励生成效率低、耗费时间长的问题。

为实现上述目的及其他相关目的，本申请的第一方面提供一种基于Formal工具的仿真验证激励生成方法，包括：

获取基于UVM环境进行仿真测试中出现错误的目标RTL代码，并确定目标RTL代码所对应的待测试设计；

根据目标RTL代码中所包含的目标输出信号及信号值生成属性数据；

利用Formal工具对所述属性数据进行覆盖验证；若验证结果为所述属性数据能被覆盖，则基于所述属性数据被覆盖的事件发生时所对应的目标输入信号值生成输入接口信号时序数据；

基于UVM环境采集所述输入接口信号时序数据，以还原生成所述属性数据对应的输入接口信号激励序列；

将所述输入接口信号激励序列进行封装以获取输入接口信号激励序列库，以供在UVM测试用例中进行仿真调用；

基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

于本申请的第一方面的一些实施例中，基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景的方式包括：

将所述输入接口信号激励序列库和所述属性数据保存至仿真数据文件中，并在UVM测试用例中添加驱动脚本；

令所述UVM环境从所述UVM测试用例中读取所述驱动脚本，并利用所述驱动脚本从所述仿真数据文件中提取所述输入接口信号激励序列库和所述属性数据；

利用所述驱动脚本、所述输入接口信号激励序列库和所述属性数据驱动所述待测试设计，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

于本申请的第一方面的一些实施例中，通过如下任一种方式来确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景：

若所述UVM测试用例中的属性数据被UVM仿真结果覆盖到了，则确定仿真的输入接口信号激励序列命中所述属性数据的事件发生时所对应的场景；

若所述UVM测试用例中的属性数据没有被仿真结果覆盖到，则确定仿真的输入接口信号激励序列没有命中所述属性数据的事件发生时所对应的场景。

于本申请的第一方面的一些实施例中，所述利用Formal工具对所述属性数据进行覆盖验证；若验证结果为所述属性数据能被覆盖，则基于所述属性数据被覆盖的事件发生时所对应的目标输入信号值生成输入接口信号时序数据的方式包括：

将所述Formal工具与所述待测试设计的输入端和输出端建立信号连接并启动Formal验证流程，以使所述Formal工具按照穷举方式向所述输入端发送输入信号值；

基于所述输入信号值与输出信号值生成对应的波形文件；

从所述波形文件中提取所述目标输入信号值，并基于所述目标输入信号值生成输入接口信号时序数据。

于本申请的第一方面的一些实施例中，获取基于UVM环境进行仿真测试中出现错误的目标RTL代码之前，还包括：获取预设配置信息，并利用所述预设配置信息对所述Formal工具进行初始化配置。

于本申请的第一方面的一些实施例中，所述预设配置信息包括所述Formal工具所使用的时钟信号、复位信号、FPV工具、工作模式、实例化文件目录及顶层模块名中的任一种或多种的组合。

为实现上述目的及其他相关目的，本申请的第二方面提供一种基于Formal工具的仿真验证激励生成装置，包括：

获取模块，用于获取基于UVM环境进行仿真测试中出现错误的目标RTL代码，并确定目标RTL代码所对应的待测试设计；

属性数据生成模块，用于根据目标RTL代码中所包含的目标输出信号及信号值生成属性数据；

时序数据生成模块，用于利用Formal工具对所述属性数据进行覆盖验证；若验证结果为所述属性数据能被覆盖，则基于所述属性数据被覆盖的事件发生时所对应的目标输入信号值生成输入接口信号时序数据；

激励序列生成模块，用于基于UVM环境采集所述输入接口信号时序数据，以还原生成所述属性数据对应的输入接口信号激励序列；

激励序列库生成模块，用于将所述输入接口信号激励序列进行封装以获取输入接口信号激励序列库，以供在UVM测试用例中进行仿真调用；

验证模块，用于基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

于本申请的第二方面的一些实施例中，所述验证模块基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景的方式包括：

将所述输入接口信号激励序列库和所述属性数据保存至仿真数据文件中，并在UVM测试用例中添加驱动脚本；

令所述UVM环境从所述UVM测试用例中读取所述驱动脚本，并利用所述驱动脚本从所述仿真数据文件中提取所述输入接口信号激励序列库和所述属性数据；

利用所述驱动脚本、所述输入接口信号激励序列库和所述属性数据驱动所述待测试设计，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

为实现上述目的及其他相关目的，本申请的第三方面提供一种计算机可读存储介质，其上存储有计算机程序，所述计算机程序被处理器执行时实现如上所述的基于Formal工具的仿真验证激励生成方法。

为实现上述目的及其他相关目的，本申请的第四方面提供一种电子终端，包括：处理器及存储器；所述存储器用于存储计算机程序；所述处理器用于执行所述存储器存储的计算机程序，以使所述终端执行如上所述的基于Formal工具的仿真验证激励生成方法。

如上所述，本申请的基于Formal工具的仿真验证激励生成方法、装置、介质及终端，具有以下有益效果：利用Formal工具对所述属性数据进行覆盖验证，当所述属性数据能被覆盖时，通过UVM环境中的采集组件采集待测试设计的输入接口信号时序数据并进行分析，以还原出所述属性数据被覆盖时所对应的输入接口信号激励序列；将所述输入接口信号激励序列进行封装以获取输入接口信号激励序列库，以供在UVM测试用例中进行仿真调用；基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景，并自动将UVM测试用例添加到回归测试列表中，如果后续回归测试确定仿真的输入接口信号激励序列没有命中所述属性数据的事件发生时所对应的场景，说明待测试设计的RTL代码可能发生了更新，重新获取基于UVM环境进行仿真测试中出现错误的目标RTL代码，以生成新的输入接口信号激励序列库进行仿真测试，从而能够保证待测试设计的属性数据随着项目的进行一直有被验证激励命中到相应场景，由于本申请通过Formal工具分析获得对应的属性数据被覆盖时所对应的输入接口信号时序数据，可被UVM环境中的采集组件采集到，并还原成对应的输入接口信号激励序列库，以方便在UVM环境测试用例中进行调用，用来命中所述属性数据的事件发生时所对应的场景，大大提升了生成对应命中待测试设计相应场景的验证激励的效率。

附图说明

图1A显示为本申请一实施例中基于Formal工具的仿真验证激励生成方法的流程示意图。

图1B显示为本申请一实施例中生成输入接口信号时序数据的流程示意图。

图1C显示为本申请一实施例中对UVM测试用例进行验证的流程示意图。

图2显示为本申请一实施例中基于Formal工具的仿真验证激励生成装置的结构示意图。

图3显示为本申请一实施例中电子终端的结构示意图。

具体实施方式

以下通过特定的具体实例说明本申请的实施方式，本领域技术人员可由本说明书所揭露的内容轻易地了解本申请的其他优点与功效。本申请还可以通过另外不同的具体实施方式加以实施或应用，本说明书中的各项细节也可以基于不同观点与应用，在没有背离本申请的精神下进行各种修饰或改变。需说明的是，在不冲突的情况下，以下实施例及实施例中的特征可以相互组合。

需要说明的是，在下述描述中，参考附图，附图描述了本申请的若干实施例。应当理解，还可使用其他实施例，并且可以在不背离本申请的精神和范围的情况下进行机械组成、结构、电气以及操作上的改变。下面的详细描述不应该被认为是限制性的，并且本申请的实施例的范围仅由公布的专利的权利要求书所限定。这里使用的术语仅是为了描述特定实施例，而并非旨在限制本申请。空间相关的术语，例如“上”、“下”、“左”、“右”、“下面”、“下方”、“下部”、“上方”、“上部”等，可在文中使用以便于说明图中所示的一个元件或特征与另一元件或特征的关系。

在本申请中，除非另有明确的规定和限定，术语“安装”、“相连”、“连接”、“固定”、“固持”等术语应做广义理解，例如，可以是固定连接，也可以是可拆卸连接，或一体地连接；可以是机械连接，也可以是电连接；可以是直接相连，也可以通过中间媒介间接相连，可以是两个元件内部的连通。对于本领域的普通技术人员而言，可以根据具体情况理解上述术语在本申请中的具体含义。

再者，如同在本文中所使用的，单数形式“一”、“一个”和“该”旨在也包括复数形式，除非上下文中有相反的指示。应当进一步理解，术语“包含”、“包括”表明存在所述的特征、操作、元件、组件、项目、种类、和/或组，但不排除一个或多个其他特征、操作、元件、组件、项目、种类、和/或组的存在、出现或添加。此处使用的术语“或”和“和/或”被解释为包括性的，或意味着任一个或任何组合。因此，“A、B或C”或者“A、B和/或C”意味着“以下任一个：A；B；C；A和B；A和C；B和C；A、B和C”。仅当元件、功能或操作的组合在某些方式下内在地互相排斥时，才会出现该定义的例外。

现有的超大规模集成电路芯片仿真验证通常是基于UVM验证环境进行，验证激励大多数是基于CRT随机生成激励数据，来期望命中意料之外的错误，激励生成的随机规则基本上只依赖于DUT的输入接口协议，所以偶然性很高，并且往往需要通过大量时间的回归测试，才可能命中错误，耗费时间长。但是在实际的项目中，设计人员的一些更深层级的错误，往往通过随机激励很难命中或者命中效率极低，但是对于设计人员而言，设计工程师在编写RTL代码时，其实是比较清楚当发生什么场景时(或附近时刻)，DUT更容易出现错误，所以设计人员期望验证工程师的激励能够明确命中这些场景，希望回归测试中有定向用例(而不是靠随机激励命中)保证激励覆盖过这些场景；超大规模集成电路芯片仿真验证对待DUT更希望是个黑盒子，这样不需要与设计实现耦合和绑定，验证人员只是针对接口生成激励序列；另外，如果DUT内部发生场景的信号的深度较深时，设计人员也很难清楚的告知给验证工程师，如何生成激励序列，可以命中这些场景；甚至有可能，因为中间逻辑的原因，设计人员期望命中的这种场景其实根本不可能发生。比如从输入激励到该处逻辑的中间逻辑已经过滤了这种情况，或者中间的逻辑是另一个设计人员的代码，这种情况下往往会白白耗费相当多的人力资源才会认识到该场景不会发生。尤其对于多层级的超大规模集成电路仿真验证而言，上述问题更为严重，因为对于DUT的错误，BT/IT/ST层面的输入接口到达内部DUT的逻辑深度更深，要想随机生成命中该处错误的概率更低，需要耗费大量的回归资源；或者要想确定该场景不会发生，分析非常费劲并且耗费人力资源。

为解决现有技术中构造达成DUT(待测试设计)内部场景的定向验证激励时，需要分析DUT(待测试设计)的代码结构，并且不好生成验证激励、验证激励生成效率低、耗费时间长、命中率低的问题，本发明提供一种基于Formal工具的仿真验证激励生成方法、装置、介质及终端，旨在如何快速生成验证激励、提高生成对应命中待测试设计相应场景的验证激励的效率。

在对本发明进行进一步详细说明之前，对本发明实施例中涉及的名词和术语进行说明，本发明实施例中涉及的名词和术语适用于如下的解释：

<1>UVM(Universal Verification Methodology)验证：通用验证方法学，主要目标是通过使用可重用的验证组件来提高设计验证的效率。

<2>EMU(Emulator)验证：是通过软件运算模拟其他硬件环境的软件，可以借助电脑或者其他多媒体平台能够运行其他平台上的程序。

<3>FPGA(Field Programmable GateArray)验证：是对FPGA芯片设计的正确性进行验证的过程。

<4>DUT(Design Under test)：待测试设计，也就是设计好的RTL代码。

<5>EDA(Electronic design automation)：电子设计自动化，是指利用计算机辅助设计软件，来完成超大规模集成电路芯片的功能设计、综合、验证、物理设计(包括布局、布线、版图、设计规则检查等)等流程的设计方式。

<6>CRT(constraint random test)：约束随机试验，测试集的随机化。

<7>RTL代码：一种硬件描述语言，用于描述同步数字电路操作的抽象级。

<8>BT/IT/ST：芯片应用场景的逐级分解。

<9>Formal工具：利用数学分析的方法，通过算法引擎建立模型，对待测试设计的状态空间进行穷尽分析的形式验证。

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

如图1A所示，展示了本发明实施例中的基于Formal工具的仿真验证激励生成方法的流程示意图。本实施例中的基于Formal工具的仿真验证激励生成方法主要包括如下各步骤：

S101：获取基于UVM环境进行仿真测试中出现错误的目标RTL代码，并确定目标RTL代码所对应的待测试设计。

于本实施例中，在提取目标RTL代码之前，应当确定所述目标RTL代码对应的待测试设计，并对Formal工具进行配置。示例性地，可对Formal工具所使用的时钟信号、复位信号、FPV工具、工作模式、实例化文件目录及顶层模块名进行配置，其中FPV(FormalProperty Verification)工具为形式验证工具。以上示例仅作参考，本发明实施例对于Formal工具的具体配置方式及过程并不做限定。

于本实施例中，在获取基于UVM环境进行仿真测试中出现错误的目标RTL代码之前，所述方法还执行如下：获取预设配置信息，并利用所述预设配置信息对所述Formal工具进行初始化配置。所述预设配置信息包括但不限于所述Formal工具所使用的时钟信号、复位信号、FPV工具、工作模式、实例化文件目录及顶层模块名中的任一种或多种的组合。

S102：根据目标RTL代码中所包含的目标输出信号及信号值生成属性数据。

于本实施例中，RTL代码可利用待测试设计的输出信号来实现对应的逻辑功能，即当RTL代码对应的目标输出信号输出了目标信号值时，该段代码对应的逻辑功能被触发。同样可以理解的是，在向待测试设计输入不同的激励信号之后，待测试设计可产生不同的输出信号。因此，只要能够找到使出现错误的目标RTL代码对应的目标输出信号的激励信号值，便够确定可使出现错误的目标RTL代码被覆盖的激励条件，进而可根据该激励条件对UVM仿真测试进行验证。

于本实施例中，所述属性数据(Property数据)由多个逻辑事件的组合表示，在数字电路中，逻辑事件的组合可以使用布尔代数来表示，把布尔表达式封装成序列，序列是一个涉及一个或者多个周期的布尔表达式，其好处是可以提高重用性，如此在调用逻辑表达式时，可以使用序列替代，多个序列可以组成一个更复杂的序列，将序列再封装一层就是属性数据(Property数据)。

S103：利用Formal工具对所述属性数据进行覆盖验证；若验证结果为所述属性数据能被覆盖，则基于所述属性数据被覆盖的事件发生时所对应的目标输入信号值生成输入接口信号时序数据。

于本实施例中，通过利用Formal工具的覆盖功能，Formal工具遍历所有可能的状态空间，在这些状态空间中分析出所述属性数据被覆盖时的目标输入信号值，此时对应的目标输入信号值即为所述出现错误的目标RTL代码被覆盖的外部激励条件，基于所述属性数据被覆盖的事件发生时所对应的目标输入信号值生成输入接口信号时序数据。可以理解的是，若所述属性数据没有被覆盖，则确定出现错误的场景实际上不会发生，从而更新出现错误的目标RTL代码。

如图1B所示，展示了本发明实施例中的生成输入接口信号时序数据的流程示意图，所述利用Formal工具对所述属性数据进行覆盖验证；若验证结果为所述属性数据能被覆盖，则基于所述属性数据被覆盖的事件发生时所对应的目标输入信号值生成输入接口信号时序数据的方式包括：

S1031：将所述Formal工具与所述待测试设计的输入端和输出端建立信号连接并启动Formal验证流程，以使所述Formal工具按照穷举方式向所述输入端发送输入信号值。

于本实施例中，为了与所述待测试设计的输入端与输出端建立信号连接，Formal工具应当依照该输入端和输出端所包含的信号(如时钟信号、复位信号、输入信号及输出信号)生成对应的对接信号，进而利用对接信号与所述待测试设计连接。本发明实施例并不限定时钟信号、复位信号、输入信号及输出信号的具体形式，也不限定上述信号的具体数量，可根据具体的待测试设计进行设置。

于本实施例中，所述Formal工具根据预设的输入信号约束范围，按照穷举方式向输入端发送输入信号值，在接收到输出端的输出信号值时，Formal工具便可利用该输出信号值确定所述属性数据能否被覆盖，若所述属性数据能被覆盖，则确定所述所述属性数据被覆盖的事件是存在的。

S1032：基于所述输入信号值与输出信号值生成对应的波形文件。

于本实施例中，若所述属性数据能被覆盖，Formal工具便利用输出信号值与输入信号值生成对应的波形文件。

于本实施例中，对应的输入信号值为可能使出现错误的目标RTL代码被覆盖的一或者多个外部激励条件。

S1033：从所述波形文件中提取所述目标输入信号值，并基于所述目标输入信号值生成输入接口信号时序数据。

于本实施例中，若所述属性数据能被覆盖，Formal工具从所述波形文件中提取出现错误的目标RTL代码所对应的目标输入信号值，并基于所述目标输入信号值生成输入接口信号时序数据，以供获取出现错误的目标RTL代码对应场景的验证激励。

于本实施例中，目标输入信号值为出现错误的目标RTL代码被覆盖时所对应的外部激励条件，基于所述对应的外部激励条件生成输入接口信号时序数据。

S104：基于UVM环境采集所述输入接口信号时序数据，以还原生成所述属性数据对应的输入接口信号激励序列。

于本实施例中，若所述属性数据能被覆盖，UVM环境中的采集组件通过采集待测试设计的输入接口信号时序数据并进行分析，以还原出所述属性数据被覆盖时所对应的输入接口信号激励序列。

S105：将所述输入接口信号激励序列进行封装以获取输入接口信号激励序列库，以供在UVM测试用例中进行仿真调用。

于本实施例中，每个输入接口信号激励序列对应一个验证激励，输入接口信号激励序列库包括一或多组验证激励，在UVM测试用例中加入输入接口信号激励序列库，以供在UVM环境中进行仿真测试时复用，使用输入接口信号激励序列来验证是否能够命中待测试设计中会出现错误的不同场景，从而大大提升生成对应命中待测试设计相应场景的验证激励的效率。

S106：基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

如图1C所示，展示了本发明实施例中对UVM测试用例进行验证的流程示意图。基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景的方式包括：

S1061：将所述输入接口信号激励序列库和所述属性数据保存至仿真数据文件中，并在UVM测试用例中添加驱动脚本。

S1062：令所述UVM环境从所述UVM测试用例中读取所述驱动脚本，并利用所述驱动脚本从所述仿真数据文件中提取所述输入接口信号激励序列库和所述属性数据。

S1063：利用所述驱动脚本、所述输入接口信号激励序列库和所述属性数据驱动所述待测试设计，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

于本实施例中，通过如下任一种方式来确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景：

若所述UVM测试用例中的属性数据被UVM仿真结果覆盖到了，则确定仿真的输入接口信号激励序列命中所述属性数据的事件发生时所对应的场景。

若所述UVM测试用例中的属性数据没有被仿真结果覆盖到，则确定仿真的输入接口信号激励序列没有命中所述属性数据的事件发生时所对应的场景，说明待测试设计的RTL代码可能发生了变动，重新回到步骤S101，以生成新的输入接口信号激励序列库进行仿真测试。

值得说明的是，本发明利用Formal工具对所述属性数据进行覆盖验证，当所述属性数据能被覆盖时，通过UVM环境中的采集组件采集待测试设计的输入接口信号时序数据并进行分析，以还原出所述属性数据被覆盖时所对应的输入接口信号激励序列；将所述输入接口信号激励序列进行封装以获取输入接口信号激励序列库，以供在UVM测试用例中进行仿真调用；基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景，并自动将UVM测试用例添加到回归测试列表中，如果后续回归测试确定仿真的输入接口信号激励序列没有命中所述属性数据的事件发生时所对应的场景，说明待测试设计的RTL代码可能发生了更新，重新回到步骤S101，以生成新的输入接口信号激励序列库进行仿真测试，能够保证待测试设计的属性数据随着项目的进行一直有被验证激励命中到相应场景，大大提升了生成对应命中待测试设计相应场景的验证激励的效率、节省时间、命中率高。

如图2所示，展示了本发明实施例中的基于Formal工具的仿真验证激励生成装置的结构示意图，该装置200包括：

获取模块201，用于获取基于UVM环境进行仿真测试中出现错误的目标RTL代码，并确定目标RTL代码所对应的待测试设计。

属性数据生成模块202，用于根据目标RTL代码中所包含的目标输出信号及信号值生成属性数据。

时序数据生成模块203，用于利用Formal工具对所述属性数据进行覆盖验证；若验证结果为所述属性数据能被覆盖，则基于所述属性数据被覆盖的事件发生时所对应的目标输入信号值生成输入接口信号时序数据。

于本实施例中，时序数据生成模块203还用于执行如下步骤：

将所述Formal工具与所述待测试设计的输入端和输出端建立信号连接并启动Formal验证流程，以使所述Formal工具按照穷举方式向所述输入端发送输入信号值；

基于所述输入信号值与输出信号值生成对应的波形文件；

从所述波形文件中提取所述目标输入信号值，并基于所述目标输入信号值生成输入接口信号时序数据。

激励序列生成模块204，用于基于UVM环境采集所述输入接口信号时序数据，以还原生成所述属性数据对应的输入接口信号激励序列。

激励序列库生成模块205，用于将所述输入接口信号激励序列进行封装以获取输入接口信号激励序列库，以供在UVM测试用例中进行仿真调用。

验证模块206，用于基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

于本实施例中，验证模块206还用于执行如下步骤：

将所述输入接口信号激励序列库和所述属性数据保存至仿真数据文件中，并在UVM测试用例中添加驱动脚本；

令所述UVM环境从所述UVM测试用例中读取所述驱动脚本，并利用所述驱动脚本从所述仿真数据文件中提取所述输入接口信号激励序列库和所述属性数据；

利用所述驱动脚本、所述输入接口信号激励序列库和所述属性数据驱动所述待测试设计，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

于本申请的一实施例中，本申请提供一种计算机可读存储介质，其上存储有计算机程序，所述计算机程序被处理器执行时实现如上所述的基于Formal工具的仿真验证激励生成方法。

本领域普通技术人员可以理解：实现上述各方法实施例的全部或部分步骤可以通过计算机程序相关的硬件来完成。前述的计算机程序可以存储于一计算机可读存储介质中。该程序在执行时，执行包括上述各方法实施例的步骤；而前述的存储介质包括：ROM、RAM、磁碟或者光盘等各种可以存储程序代码的介质。

于本申请提供的实施例中，所述计算机可读写存储介质可以包括只读存储器、随机存取存储器、EEPROM、CD-ROM或其它光盘存储装置、磁盘存储装置或其它磁存储设备、闪存、U盘、移动硬盘、或者能够用于存储具有指令或数据结构形式的期望的程序代码并能够由计算机进行存取的任何其它介质。另外，任何连接都可以适当地称为计算机可读介质。例如，如果指令是使用同轴电缆、光纤光缆、双绞线、数字订户线(DSL)或者诸如红外线、无线电和微波之类的无线技术，从网站、服务器或其它远程源发送的，则所述同轴电缆、光纤光缆、双绞线、DSL或者诸如红外线、无线电和微波之类的无线技术包括在所述介质的定义中。然而，应当理解的是，计算机可读写存储介质和数据存储介质不包括连接、载波、信号或者其它暂时性介质，而是旨在针对于非暂时性、有形的存储介质。如申请中所使用的磁盘和光盘包括压缩光盘(CD)、激光光盘、光盘、数字多功能光盘(DVD)、软盘和蓝光光盘，其中，磁盘通常磁性地复制数据，而光盘则用激光来光学地复制数据。

如图3所示，展示为本申请于一实施例中的电子终端的结构示意图，本实例提供的电子终端300，包括：处理器301和存储器302；存储器302通过系统总线与处理器301连接并完成相互间的通信，存储器302用于存储计算机程序，处理器301用于运行存储器302存储的计算机程序，使电子终端300执行如上所述的基于Formal工具的仿真验证激励生成方法。

本发明实施例提供的基于Formal工具的仿真验证激励生成方法可以采用终端侧或服务器侧实施，就电子终端的硬件结构而言，请参阅图3，为本发明实施例提供的电子终端300的一个可选的硬件结构示意图，该终端300可以是移动电话、计算机设备、平板设备、个人数字处理设备、工厂后台处理设备等。电子终端300包括：至少一个处理器301、存储器302、至少一个网络接口304和用户接口306。装置中的各个组件通过总线系统305耦合在一起。可以理解的是，总线系统305用于实现这些组件之间的连接通信。总线系统305除包括数据总线之外，还包括电源总线、控制总线和状态信号总线。但是为了清楚说明起见，在图3中将各种总线都标为总线系统。

其中，用户接口306可以包括显示器、键盘、鼠标、轨迹球、点击枪、按键、按钮、触感板或者触摸屏等。

可以理解，存储器302可以是易失性存储器或非易失性存储器，也可包括易失性和非易失性存储器两者。其中，非易失性存储器可以是只读存储器(ROM，Read Only Memory)、可编程只读存储器(PROM，Programmable Read-Only Memory)，其用作外部高速缓存。通过示例性但不是限制性说明，许多形式的RAM可用，例如静态随机存取存储器(SRAM，StaticRandom Access Memory)、同步静态随机存取存储器(SSRAM，Synchronous StaticRandomAccess Memory)。本发明实施例描述的存储器旨在包括但不限于这些和任意其它适合类别的存储器。

本发明实施例中的存储器302用于存储各种类别的数据以支持电子终端300的操作。这些数据的示例包括：用于在电子终端300上操作的任何可执行程序，如操作系统3021和应用程序3022；操作系统3021包含各种系统程序，例如框架层、核心库层、驱动层等，用于实现各种基础业务以及处理基于硬件的任务。应用程序3022可以包含各种应用程序，例如媒体播放器(MediaPlayer)、浏览器(Browser)等，用于实现各种应用业务。实现本发明实施例提供的基于Formal工具的仿真验证激励生成方法可以包含在应用程序3022中。

上述本发明实施例揭示的方法可以应用于处理器301中，或者由处理器301实现。处理器301可能是一种集成电路芯片，具有信号的处理能力。在实现过程中，上述方法的各步骤可以通过处理器301中的硬件的集成逻辑电路或者软件形式的指令完成。上述的处理器301可以是通用处理器、数字信号处理器(DSP，Digital Signal Processor)，或者其他可编程逻辑器件、分立门或者晶体管逻辑器件、分立硬件组件等。处理器301可以实现或者执行本发明实施例中的公开的各方法、步骤及逻辑框图。通用处理器301可以是微处理器或者任何常规的处理器等。结合本发明实施例所提供的配件优化方法的步骤，可以直接体现为硬件译码处理器执行完成，或者用译码处理器中的硬件及软件模块组合执行完成。软件模块可以位于存储介质中，该存储介质位于存储器，处理器读取存储器中的信息，结合其硬件完成前述方法的步骤。

在示例性实施例中，电子终端300可以被一个或多个应用专用集成电路(ASIC，Application Specific Integrated Circuit)、DSP、可编程逻辑器件(PLD，ProgrammableLogic Device)、复杂可编程逻辑器件(CPLD，Complex Programmable LogicDevice)，用于执行前述方法。

综上所述，本申请提供的基于Formal工具的仿真验证激励生成方法、装置、介质及终端，利用Formal工具对所述属性数据进行覆盖验证，当所述属性数据能被覆盖时，通过UVM环境中的采集组件采集待测试设计的输入接口信号时序数据并进行分析，以还原出所述属性数据被覆盖时所对应的输入接口信号激励序列；将所述输入接口信号激励序列进行封装以获取输入接口信号激励序列库，以供在UVM测试用例中进行仿真调用；基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景，并自动将UVM测试用例添加到回归测试列表中，如果后续回归测试确定仿真的输入接口信号激励序列没有命中所述属性数据的事件发生时所对应的场景，说明待测试设计的RTL代码可能发生了更新，重新获取基于UVM环境进行仿真测试中出现错误的目标RTL代码，以生成新的输入接口信号激励序列库进行仿真测试，从而能够保证待测试设计的属性数据随着项目的进行一直有被验证激励命中到相应场景，大大提升了生成对应命中待测试设计相应场景的验证激励的效率、节省时间、命中率高。所以，本申请有效克服了现有技术中的种种缺点而具高度产业利用价值。

上述实施例仅例示性说明本申请的原理及其功效，而非用于限制本申请。任何熟悉此技术的人士皆可在不违背本申请的精神及范畴下，对上述实施例进行修饰或改变。因此，举凡所属技术领域中具有通常知识者在未脱离本申请所揭示的精神与技术思想下所完成的一切等效修饰或改变，仍应由本申请的权利要求所涵盖。

Claims (10)

1.一种基于Formal工具的仿真验证激励生成方法，其特征在于，包括：

获取基于UVM环境进行仿真测试中出现错误的目标RTL代码，并确定目标RTL代码所对应的待测试设计；

根据目标RTL代码中所包含的目标输出信号及信号值生成属性数据；

利用Formal工具对所述属性数据进行覆盖验证；若验证结果为所述属性数据能被覆盖，则基于所述属性数据被覆盖的事件发生时所对应的目标输入信号值生成输入接口信号时序数据；

基于UVM环境采集所述输入接口信号时序数据，以还原生成所述属性数据对应的输入接口信号激励序列；

将所述输入接口信号激励序列进行封装以获取输入接口信号激励序列库，以供在UVM测试用例中进行仿真调用；

基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

2.根据权利要求1所述的基于Formal工具的仿真验证激励生成方法，其特征在于，基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景的方式包括：

将所述输入接口信号激励序列库和所述属性数据保存至仿真数据文件中，并在UVM测试用例中添加驱动脚本；

令所述UVM环境从所述UVM测试用例中读取所述驱动脚本，并利用所述驱动脚本从所述仿真数据文件中提取所述输入接口信号激励序列库和所述属性数据；

利用所述驱动脚本、所述输入接口信号激励序列库和所述属性数据驱动所述待测试设计，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

3.根据权利要求1或2所述的基于Formal工具的仿真验证激励生成方法，其特征在于，通过如下任一种方式来确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景：

若所述UVM测试用例中的属性数据被UVM仿真结果覆盖到了，则确定仿真的输入接口信号激励序列命中所述属性数据的事件发生时所对应的场景；

若所述UVM测试用例中的属性数据没有被仿真结果覆盖到，则确定仿真的输入接口信号激励序列没有命中所述属性数据的事件发生时所对应的场景。

4.根据权利要求1所述的基于Formal工具的仿真验证激励生成方法，其特征在于，所述利用Formal工具对所述属性数据进行覆盖验证；若验证结果为所述属性数据能被覆盖，则基于所述属性数据被覆盖的事件发生时所对应的目标输入信号值生成输入接口信号时序数据的方式包括：

将所述Formal工具与所述待测试设计的输入端和输出端建立信号连接并启动Formal验证流程，以使所述Formal工具按照穷举方式向所述输入端发送输入信号值；

基于所述输入信号值与输出信号值生成对应的波形文件；

从所述波形文件中提取所述目标输入信号值，并基于所述目标输入信号值生成输入接口信号时序数据。

5.根据权利要求1所述的基于Formal工具的仿真验证激励生成方法，其特征在于，获取基于UVM环境进行仿真测试中出现错误的目标RTL代码之前，还包括：获取预设配置信息，并利用所述预设配置信息对所述Formal工具进行初始化配置。

6.根据权利要求5所述的基于Formal工具的仿真验证激励生成方法，其特征在于，所述预设配置信息包括所述Formal工具所使用的时钟信号、复位信号、FPV工具、工作模式、实例化文件目录及顶层模块名中的任一种或多种的组合。

7.一种基于Formal工具的仿真验证激励生成装置，其特征在于，包括：

获取模块，用于获取基于UVM环境进行仿真测试中出现错误的目标RTL代码，并确定目标RTL代码所对应的待测试设计；

属性数据生成模块，用于根据目标RTL代码中所包含的目标输出信号及信号值生成属性数据；

时序数据生成模块，用于利用Formal工具对所述属性数据进行覆盖验证；若验证结果为所述属性数据能被覆盖，则基于所述属性数据被覆盖的事件发生时所对应的目标输入信号值生成输入接口信号时序数据；

激励序列生成模块，用于基于UVM环境采集所述输入接口信号时序数据，以还原生成所述属性数据对应的输入接口信号激励序列；

激励序列库生成模块，用于将所述输入接口信号激励序列进行封装以获取输入接口信号激励序列库，以供在UVM测试用例中进行仿真调用；

验证模块，用于基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行

验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

8.根据权利要求7所述的基于Formal工具的仿真验证激励生成装置，其特征在于，所述验证模块基于UVM环境对所述输入接口信号激励序列库和所述属性数据进行验证测试，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景的方式包括：

将所述输入接口信号激励序列库和所述属性数据保存至仿真数据文件中，并在UVM测试用例中添加驱动脚本；

令所述UVM环境从所述UVM测试用例中读取所述驱动脚本，并利用所述驱动脚本从所述仿真数据文件中提取所述输入接口信号激励序列库和所述属性数据；

利用所述驱动脚本、所述输入接口信号激励序列库和所述属性数据驱动所述待测试设计，以确定所述UVM测试用例是否覆盖所述属性数据的事件发生时所对应的场景。

9.一种计算机可读存储介质，其上存储有计算机程序，其特征在于，所述计算机程序被处理器执行时实现权利要求1至6中任一项所述的基于Formal工具的仿真验证激励生成方法。

10.一种电子终端，其特征在于，包括：处理器及存储器；

所述存储器用于存储计算机程序；

所述处理器用于执行所述存储器存储的计算机程序，以使所述终端执行如权利要求1至6中任一项所述的基于Formal工具的仿真验证激励生成方法。