本发明涉及芯片设计领域，特别是涉及一种形式验证方法、电子设备及存储介质。
背景技术：
1、在芯片设计领域，芯片系统的架构是芯片系统的核心行为、数据流和控制逻辑的高级描述。寄存器传输级(rtl)代码是架构的具体硬件实现，用于制造实际的集成电路。rtl代码的实现是通过硬件描述语言，如verilog或vhdl，描述架构的核心行为、数据流和控制逻辑。快速模型是一种软件实现，通常使用c/c++等高级语言编写，用于快速验证架构的概念和算法的有效性，其侧重于模拟架构的行为，而忽略底层硬件细节。
2、形式验证的目的是确保rtl代码和快速模型在功能上等价，形式验证的过程包括：模型对齐，确保rtl代码和快速模型在接口和行为上一致；测试用例验证，通过运行测试用例收集快速模型和rtl模型的输出结果；结果对比，将两者的输出结果进行比较，确保两者的行为一致。由于rtl代码和快速模型为不同类型的语言实现，将两类不同的语言进行对齐的难度很大，不仅容易出错而且增加了验证周期。因此，亟需一种更加容易对齐的形式验证方法。
技术实现思路
1、针对上述技术问题，本发明采用的技术方案为：一种形式验证方法，所述方法包括如下步骤：
2、s100，获取快速模型，所述快速模型采用第一种编程语言。
3、s200，获取寄存器传输级模型，所述寄存器传输级模型与所述快速模型用于描述同一个系统架构中的同一个或多个功能模块。
4、s300，将所述寄存器传输级模型转换为采用所述第一种编程语言的全真模型。
5、s400，将所述全真模型与所述快速模型进行对齐，得到对齐后的全真模型和对齐后的快速模型。
6、s500，通过经过验证的目标测试用例验证对齐后的快速模型的正确性，得到第一测试结果。
7、s600，通过所述目标测试用例验证所述对齐后的全真模型的正确性，得到第二测试结果。
8、s700，当所述第一测试结果和第二测试结果完全相同时，得到在功能上一致的快速模型和寄存器传输级模型。
9、此外，本发明还提供了一种非瞬时性计算机可读存储介质，所述存储介质中存储有至少一条指令或至少一段程序，所述至少一条指令或所述至少一段程序由处理器加载并执行以实现上述方法。
10、此外，本发明还提供了一种电子设备，包括处理器和上述非瞬时性计算机可读存储介质。
11、本发明至少具有以下有益效果：
12、本发明实施例提供了一种形式验证方法，其通过将寄存器传输级模型转换为采用所述第一种编程语言的全真模型，将全真模型与采用第一种编程语言的快速模型进行对齐，得到对齐后的全真模型和对齐后的快速模型；比较将目标测试用例分别输入对齐后的全真模型和对齐后的快速模型之后的测试结果，两测试结果相同时，得到在功能上一致的快速模型和寄存器传输级模型。其中，由于全真模型和快速模型均采用第一种编程语言，不仅对齐容易，而且两者的目标测试用例不需要任何调整可以直接复用，提高了形式验证的效率且缩短了形式验证的周期。
1.一种形式验证方法，其特征在于，所述方法包括如下步骤：
2.根据权利要求1所述的方法，其特征在于，s300还包括转换步骤：
3.根据权利要求1所述的方法，其特征在于，s400还包括对齐步骤：
4.根据权利要求1所述的方法，其特征在于，s200中的寄存器传输级模型为已经经过设计验证的模型。
5.根据权利要求1所述的方法，其特征在于，s200中还包括获取用户指定的验证数量阈值n；当已经经过设计验证的寄存器传输级模型的数量为n时，执行s300-700。
6.根据权利要求1所述的方法，其特征在于，s200中还包括获取用户指定的目标时间，根据所述目标时间范围内已经经过设计验证的多个寄存器传输级模型，执行s300-700。
7.根据权利要求1所述的方法，其特征在于，所述快速模型为行为模型。
8.根据权利要求1所述的方法，其特征在于，所述第一种编程语言为c语言、c++语言或者systemc语言。
9.一种非瞬时性计算机可读存储介质，所述存储介质中存储有至少一条指令或至少一段程序，其特征在于，所述至少一条指令或所述至少一段程序由处理器加载并执行以实现如权利要求1-8中任意一项的所述方法。
10.一种电子设备，其特征在于，包括处理器和权利要求9中所述的非瞬时性计算机可读存储介质。
