用于生成形式验证环境的方法、电子设备及存储介质

摘要

本申请提供了一种用于生成形式验证环境的方法、电子设备及存储介质。该方法包括：接收用于描述逻辑系统设计的功能的配置文件，其中，配置文件指示逻辑系统设计的设计类型以及与设计类型对应的参数；根据配置文件确定与逻辑系统设计对应的数据库文件；在数据库文件中获取与逻辑系统设计对应的多个形式验证环境参数；以及根据形式验证环境参数生成形式验证环境。

权利要求

1.一种用于生成形式验证环境的方法，其中，所述方法包括：接收用于描述逻辑系统设计的功能的配置文件，其中，所述配置文件指示所述逻辑系统设计的设计类型以及与所述设计类型对应的参数；

根据所述配置文件确定与所述逻辑系统设计对应的数据库文件；

在所述数据库文件中获取与所述逻辑系统设计对应的多个形式验证环境参数；以及根据所述形式验证环境参数生成形式验证环境，其中，所述数据库文件包括信号说明列表，并且根据所述配置文件确定与所述逻辑系统设计对应的数据库文件进一步包括：根据所述配置文件获取所述逻辑系统设计的输入信号；

在所述信号说明列表中检测所述输入信号的匹配信号；以及响应于在所述信号说明列表中检测到所述输入信号的匹配信号，唯一绑定所述输入信号和所述匹配信号；

在所述数据库文件中获取与所述逻辑系统设计对应的多个形式验证环境参数进一步包括：根据所述配置文件按修改优先级对所述多个形式验证环境参数进行排序，以生成配置参数修改表；

所述形式验证环境包括行为模型和断言语句，所述形式验证环境参数包括所述逻辑系统设计的验证规则，并且根据所述形式验证环境参数生成形式验证环境进一步包括：根据所述配置文件确定所述逻辑系统设计的设计类型；

根据所述设计类型配置所述行为模型；以及

根据所述配置参数修改表选择所述逻辑系统设计的验证规则以生成所述断言语句；

所述形式验证环境还包括：约束语句和反馈延迟，并且所述根据所述形式验证环境参数生成形式验证环境进一步包括：根据所述配置文件确定验证请求；

定义所述验证请求的行为以生成所述约束语句；以及确定所述验证请求被响应的所述反馈延迟。

2.如权利要求1所述的方法，其中，所述设计类型包括调度程序类型、流量管理器类型、内存控制器类型或状态机模块类型。

3.如权利要求1所述的方法，其中，所述设计类型是所述调度程序类型中的仲裁器，并且所述根据所述设计类型配置所述行为模型进一步包括：获取所述仲裁器的配置参数；以及

将所述仲裁器的配置参数赋予所述行为模型。

4.如权利要求1所述的方法，其中，所述方法进一步包括：加载与所述数据库文件对应的数据库模型；以及连接待测设备的接口和所述数据库模型的接口。

5.一种电子设备，包括存储器、处理器及存储在存储器上并可在处理器上运行的计算机程序，所述处理器执行所述程序时实现如权利要求1至4任意一项所述的方法。

6.一种非暂态计算机可读存储介质，所述非暂态计算机可读存储介质存储电子装置的一组指令，该组指令用于使所述电子装置执行权利要求1至4任一项所述的方法。

说明书

用于生成形式验证环境的方法、电子设备及存储介质

技术领域

[0001] 本申请涉及计算机软件技术领域，尤其涉及一种用于生成形式验证环境的方法、电子设备及存储介质。

背景技术

[0002] 所谓形式验证(Formal Verification)是指从数学上完备地证明或验证电路的实现方案是否确实实现了电路设计所描述的功能。然而，在形式验证中，选择合适的属性进行验证以及创建属性的过程十分复杂。

发明内容

[0003] 有鉴于此，本申请提出了一种用于生成形式验证环境的方法、电子设备及存储介质。

[0004] 本公开的第一方面，提供了一种用于生成形式验证环境的方法，包括：接收用于描述逻辑系统设计的功能的配置文件，其中，所述配置文件指示所述逻辑系统设计的设计类型以及与所述设计类型对应的参数；根据所述配置文件确定与所述逻辑系统设计对应的数据库文件；在所述数据库文件中获取与所述逻辑系统设计对应的多个形式验证环境参数；以及根据所述形式验证环境参数生成形式验证环境。

[0005] 本公开的第二方面，提供了一种电子设备，包括存储器、处理器及存储在存储器上并可在处理器上运行的计算机程序，所述处理器执行所述程序时实现第一方面所述的方法。

[0006] 本公开的第三方面，提供了一种非暂态计算机可读存储介质，所述非暂态计算机可读存储介质存储电子装置的一组指令，该组指令用于使所述电子装置执行第一方面所述的方法。

[0007] 本申请提供的用于生成形式验证环境的方法、电子设备及存储介质，通过根据接收的用于描述逻辑系统设计的功能的配置文件，确定与该逻辑系统设计对应的数据库文件，进而从数据库文件中获取用于构建形式验证环境的形式验证环境参数，根据形式验证环境参数生成形式验证环境。从而降低了形式验证的使用门槛，快速简便地搭建形式验证环境，提高了形式验证的证明效率和收敛比例。

附图说明

[0008] 为了更清楚地说明本申请或现有技术中的技术方案，下面将对实施例或现有技术描述中所需要使用的附图作简单地介绍，显而易见地，下面描述中的附图仅仅是本申请，对于本领域普通技术人员来讲，在不付出创造性劳动的前提下，还可以根据这些附图获得其他的附图。

[0009] 图1示出了本申请实施例所提供的示例性电子设备的结构示意图。

[0010] 图2示出了根据本申请实施例的示例性形式验证工具的示意图。

[0011] 图3示出了根据本公开实施例的形式验证过程的示例性流程图。

[0012] 图4示出了根据本公开实施例的待测设备DUT的示例性交互示意图。

[0013] 图5示出了本公开实施例所提供的一种用于生成形式验证环境的示例性方法的流程示意图。

具体实施方式

[0014] 为使本申请的目的、技术方案和优点更加清楚明白，以下结合具体实施例，并参照附图，对本申请进一步详细说明。

[0015] 需要说明的是，除非另外定义，本申请使用的技术术语或者科学术语应当为本申请所属领域内具有一般技能的人士所理解的通常意义。本申请中使用的“第一”、“第二”以及类似的词语并不表示任何顺序、数量或者重要性，而只是用来区分不同的组成部分。“包括”或者“包含”等类似的词语意指出现该词前面的元件或者物件涵盖出现在该词后面列举的元件或者物件及其等同，而不排除其他元件或者物件。“连接”或者“相连”等类似的词语并非限定于物理的或者机械的连接，而是可以包括电性的连接，不管是直接的还是间接的。

[0016] 图1示出了本实施例所提供的一种电子设备100的结构示意图。电子设备100例如可以是计算机主机。该电子设备100可以包括：处理器102、存储器104、网络接口106、外围接口108和总线110。其中处理器102、存储器104、网络接口106和外围接口108通过总线110实现彼此之间在设备内部的通信连接。

[0017] 处理器102可以是中央处理器(Central Processing Unit，CPU)、图像处理器、神经网络处理器(NPU)、微控制器(MCU)、可编程逻辑器件、数字信号处理器(DSP)、应用专用集成电路(Application Specific Integrated Circuit，ASIC)、或者一个或多个集成电路。处理器102可以用于执行与本申请描述的技术相关的功能。在一些实施例中，处理器102还可以包括集成为单一逻辑组件的多个处理器。如图1所示，处理器102可以包括多个处理器
102a、102b和102c。

[0018] 存储器104可以配置为存储数据(例如，指令集、计算机代码、中间数据等)。例如，如图1所示，存储的数据可以包括程序指令(例如，用于实现本申请的技术方案的程序指令)以及要处理的数据(例如，存储器104可以存储在编译过程产生的临时代码)。处理器102也可以访问存储的程序指令和数据，并且执行程序指令以对要处理的数据进行操作。存储器104可以包括易失性存储装置或非易失性存储装置。在一些实施例中，存储器104可以包括随机访问存储器(RAM)、只读存储器(ROM)、光盘、磁盘、硬盘、固态硬盘(SSD)、闪存、存储棒等。

[0019] 网络接口106可以配置为经由网络向电子设备100提供与其他外部设备的通信。该网络可以是能够传输和接收数据的任何有线或无线的网络。例如，该网络可以是有线网络、本地无线网络(例如，蓝牙、Wi‑Fi、近场通信(NFC)等)、蜂窝网络、因特网、或上述的组合。可以理解的是，网络的类型不限于上述具体示例。在一些实施例中，网络接口106可以包括任意数量的网络接口控制器(NIC)、射频模块、接收发器、调制解调器、路由器、网关、适配器、蜂窝网络芯片等的任意组合。

[0020] 外围接口108可以配置为将电子设备100与一个或多个外围装置连接，以实现信息输入及输出。例如，外围装置可以包括键盘、鼠标、触摸板、触摸屏、麦克风、各类传感器等输入设备以及显示器、扬声器、振动器、指示灯等输出设备。

[0021] 总线110可以被配置为在电子设备100的各个组件(例如处理器102、存储器104、网络接口106和外围接口108)之间传输信息，诸如内部总线(例如，处理器‑存储器总线)、外部总线(USB端口、PCI‑E总线)等。

[0022] 需要说明的是，尽管上述设备仅示出了处理器102、存储器104、网络接口106、外围接口108和总线110，但是在具体实施过程中，该设备还可以包括实现正常运行所必需的其他组件。此外，本领域的技术人员可以理解的是，上述设备中也可以仅包含实现本申请实施例方案所必需的组件，而不必包含图中所示的全部组件。

[0023] 图2示出了根据本申请实施例的示例性形式验证工具200的示意图。在芯片设计领域，形式验证工具200可以是芯华章科技股份有限公司出品的GalaxFV形式验证工具。形式验证工具200可以是运行在电子设备100上的计算机程序。在一些实施例中，形式验证工具200可以包括仿真器等组件。

[0024] 基于待验证的系统设计和用于形式验证该系统设计的断言(Assertion)，形式验证工具200可以对该系统设计进行形式验证。形式验证工具200的输入可以包括系统设计208和断言210。

[0025] 系统设计208可以是硬件的或软件的设计。例如，系统设计208可以由C、C++、Java等软件语言、由VHDL、Verilog、SystemVerilog等硬件描述语言、或寄存器传输级(RTL)代码等描述的设计。在本申请的描述中，以集成电路设计作为系统设计208的示例进行说明。

[0026] 在一些实施例中，系统设计208可以是RTL设计。在集成电路设计中，RTL(register‑transfer‑level)是用于描述同步数字电路操作的抽象级。在RTL级，芯片是由一组寄存器以及寄存器之间的逻辑操作构成。之所以如此，是因为绝大多数的电路可以被看成由寄存器来存储二进制数据、由寄存器之间的逻辑操作来完成数据的处理，数据处理的流程由时序状态机来控制，这些处理和控制可以用硬件描述语言来描述。

[0027] 断言210则可以例如是由SystemVerilog描述的SystemVerilog Assertion(SVA)。断言210可以用于描述系统设计208的期望行为。通过证明或证伪断言210可以用来验证系统设计208是否正确。因此，断言210是与系统设计208的正确性关联的行为描述。

[0028] 如图2所示，形式验证工具200可以包括前端202、中端204和后端206。系统设计208和断言210在经由前端202、中端204和后端206的处理后，最终输出验证结果。

[0029] 前端202可以包括语义分析单元2022和综合单元2024。

[0030] 语义分析单元2022可以用于对系统设计208进行语义分析以将特定语言描述的系统设计208转换为适宜于进一步综合的表达形式。语义分析可以包括词法分析(lexical analysis)和语法分析(syntax analysis)。词法分析可以将字符序列转换为单词(Token)序列，而语法分析则可以对系统设计208的描述进行语法检查，构建由输入的单词组成的数据结构(一般是语法分析树、抽象语法树等层次化的数据结构)。

[0031] 系统设计208(例如，RTL设计)在经由语义分析单元2022处理之后可以被转换为抽象语法树(abstract syntax tree，AST)。

[0032] 综合单元2024可以基于抽象语法树对系统设计208进行逻辑综合。例如，综合单元2024可以将模块实例化，识别真实电路的机构并转换为电路单元(例如，寄存器、加法器、比较器、多路选择器(MUX)等)。

[0033] 综合单元2024还可以进一步将上述电路单元转换为门(例如，AND门，OR门，XOR门等)和触发器(例如，flip‑flop)，优化电路逻辑，并最终生成电路网表(netlist)。电路网表通常是门级的，因此电路网表也通常被称为门级电路网表。

[0034] 在一些实施例中，综合单元2024可以生成字级别(word‑level)、全展开(full‑view)并且具有层次结构的(hierarchical structure)的通用网表模型。这样的通用网表模型可以方便地使用遍历工具(例如，遍历函数)进行遍历操作。

[0035] 中端204可以包括建模单元2042，用于根据断言210和电路网表生成形式验证数据模型。

[0036] 在一些实施例中，建模单元2042可以将输入的断言210转换为验证目标(verification target)。如上所述，断言210描述了系统设计208所期望的行为，而这种行为通常可以对应于一种或多种形式验证属性。换而言之，断言210可以等价地转换为希望证明或证伪的形式验证属性，即，转换为验证目标。验证目标可以包括断言验证(assert)、空泛性验证(vacuity)、目击验证(witness)等。

[0037] 在一些实施例中，建模单元2042可以基于验证目标和由前端202提供的电路网表来生成形式验证数据模型，然后后端206基于该形式验证数据模型进行形式验证。在一些实施例中，建模单元2042可以将验证目标或电路网表用表达式(例如，正则表达式、时序表达式等)来表示，因此，形式验证数据模型可以是基于表达式的数据模型。

[0038] 在又一些实施例中，中端204还可以根据断言210和电路网表生成形式验证所需的状态数据(例如，要验证的功能模块的初始状态)。

[0039] 后端206可以将形式验证数据模型分发给对应的验证引擎进行形式验证。

[0040] 在逻辑系统设计的过程中，形式验证是一种重要的验证手段。形式验证可以避免穷举式的验证，提高验证的速度和准确性。通常，形式验证通过证明或证伪逻辑系统设计的某一种属性来验证逻辑系统设计的某种功能的正确性。

[0041] 如背景技术部分所述，形式验证对于验证工程师来讲是一个门槛较高的验证方法，常出现验证工程师由于缺乏足够的经验，而无法选择合适的属性进行验证，并且创建属性的过程也很复杂。

[0042] 在一些实施例中，逻辑系统设计的各个模块根据其功能特点可以包括几个主要的大类，即逻辑系统设计的设计类型，例如，调度器(scheduler)类型、流量管理器(flow manager)类型、内存控制器(memory controller)类型以及状态机模块(FSM‑like module)类型。

[0043] 调度器类型的模块通常用于根据指令将包(packet)发送到指定的地址。流量管理器类型的模块通常用于控制逻辑系统内总线对于存储器的访问。内存控制器类型的模块通常用于对内存进行控制。状态机模块类型的模块则通常用于对不同的状态进行控制和切换。

[0044] 在一些实施例中，调度器类型例如可以是仲裁器(arbiter)，流量管理器类型例如可以是直接存储器访问(DMA)控制器，状态机模块类型可以例如是电源管理器。可以理解的是，每种类型都可以包括多种类型的模块，而不限于上述示例。

[0045] 正由于每一种类型的模块通常具有自身的一些设计特点，使得一些属性可以共性地应用于该类型的模块。而针对于这种共性的特点，可以根据配置文件来获取生成形式验证环境所需要的属性。

[0046] 接收到的配置文件可以由用户配置，其中配置文件指示出逻辑系统设计的设计类型以及与设计类型对应的参数。

[0047] 在一些实施例中，与设计类型对应的参数可以根据不同的设计类型进行分类，例如，对于调度程序类型，其对应的参数可以包括：“调度程序规则(例如rr/priority/rr with priority…)”、“主客户机的数量”、“从客户机的数量”、“启用/禁用信号”等。对于流量管理器类型，其对应的参数可以包括：“如果操作冲突，pkt是否可以丢弃？”、“每个通道的数据包检查？”、“是否基于身份去检查？”、“数据包是否可以检查出故障？”、“数据包是否能按顺序检查？”等。对于内存控制器类型，其对应的参数可以包括：“地址范围”、“读/写端口的数量”、“读/写是否存在冲突”、“是否必须先执行写操作”等。对于状态机模块类型，其对应的参数可以包括：“初始状态？”、“死锁检查”、“活锁检查”等。

[0048] 图3示出了根据本公开实施例的形式验证过程300的示例性流程图。

[0049] 如图3所示，电子设备100将配置文件302输入形式验证工具200。形式验证工具200可以根据配置文件302确定与逻辑系统设计对应的数据库文件304，确定该逻辑系统设计的设计类型以及设计类型对应的参数。

[0050] 在一些实施例中，数据库文件304可以包括信号说明列表。形式验证工具200根据配置文件302可以获取逻辑系统设计的输入信号，在数据库文件中的信号说明列表中检测输入信号的匹配信号。响应于能够在信号说明列表中检测到输入信号的匹配信号，则说明在信号说明列表中存在用户需要的信号，可以唯一绑定输入信号和匹配信号。

[0051] 在一些实施例中，形式验证工具200可以加载与数据库文件304对应的数据库模型，并连接待测设备的接口以及数据库模型的接口，从而进行输入信号的匹配与绑定。

[0052] 能够唯一绑定输入信号和匹配信号，则根据匹配信号确定了该逻辑系统设计的类型，例如调度程序类型、流量管理器类型、内存控制器类型或状态机模块类型。进一步地，可以在数据库文件中获取与逻辑系统设计对应的形式验证环境参数。参考以下的表1，形式验证工具200可以根据配置文件302按照修改优先级对多个形式验证环境参数进行排序，从而得到配置参数修改表。以调度程序类型中的循环优先级仲裁器为例，形式验证环境参数可以包括仲裁器外挂的发起请求对象数目、仲裁器的仲裁规则、仲裁器的优先级和仲裁器等级制度。其中，多个形式验证环境参数的修改优先级可以根据创建形式验证环境的历史数据进行经验分析，确定不同形式验证环境参数与形式验证环境生成过程中的相关性，相关性越高，则该形式验证环境参数的修改优先级越高。

[0053] 表1配置参数修改表

[0054]

[0055] 参考图3，形式验证环境可以包括行为模型306(Behavior model)、断言语句308(Assertion)、约束语句310(Assumption)和计分板312(Scoreboard)。在形式验证环境参数中可以确定逻辑系统设计的验证规则。进一步地，形式验证工具200可以根据形式验证环境参数配置形式验证环境。其中，计分板可以视为行为模型的一种，针对流量管理器类型的逻辑系统设计产生。

[0056] 在一些实施例中，形式验证工具200可以根据逻辑系统设计的设计类型配置行为模型，根据配置参数修改表选择逻辑系统设计的验证规则从而生成断言语句。例如，对于循环优先级仲裁器，形式验证工具200根据配置文件302中指示出的设计类型，获取仲裁器的配置参数，并将行为模型配置为rr arbiter，实现将仲裁器的配置参数赋予行为模型。进一步在配置参数修改表中选择逻辑系统设计需要的验证规则，生成对应的断言语句。

[0057] 需要说明的是，行为模型可以根据相关技术获取，在配置文件302中指示出的逻辑系统设计的设计类型的不同，采用与设计类型对应的参数对行为模型进行配置。其中，每个不同的模块、元件或是实例，都可以对应于不同的行为模型。

[0058] 在一些实施例中，根据行为模型的参数变化，由于不同设计类型之间的各个属性存在一定的共性，因此可以仅改变少数配置参数，例如新增或排除部分属性。

[0059] 对于循环优先级仲裁器而言，仲裁模块的核心功能就是针对不同对象发起的操作请求，按照一定的规则进行仲裁，按照一定的先后顺序返回给各个对象仲裁的结果。验证规则可以包括：对于任何一个对象发起的仲裁请求，不论间隔多久，都应该有仲裁反馈，以及不同对象同时发起的仲裁请求，优先级判断应该严格遵照仲裁规则，例如循环型，此类型的调度程序就要求对不同客户发起的请求要同等概率进行仲裁。

[0060] 图4示出了根据本公开实施例的示例性调度过程400的示意图。

[0061] 形式验证环境还可以包括反馈延迟。如图4所示，多个客户机402‑406与调度器408之间进行交互，调度器408能够接收不同客户机发送的验证请求(例如，req1、req 2或req 3)，并在对应的反馈延迟后给出对应的反馈(例如，rsp1、rsp 2或rsp 3)。形式验证工具200可以根据配置文件确定不同客户机发送的验证请求，定义验证请求的行为，从而生成约束语句，并能够确定验证请求被响应的反馈延迟。

[0062] 在一些实施例中，约束语句可以用来约束生成合法激励的假定特性(assume property)。例如，约束语句可以为“assume property@(posedge clock)disable iff(reset)(req&！grant|＝>req)”，解释为当某一个客户机发起验证请求以后，在仲裁结果返回前，这个请求应该一直保持，不应该跳转。约束语句还可以用来描述待测试功能的断言特性(assertion property)。例如，约束语句可以为“assert property@(posedge clock)disable iff(reset)(req|‑>s_eventually(grant))”，解释为每一个客户机发起的验证请求，总会有一个仲裁作为这个验证请求被允许的反馈。

[0063] 需要说明的是，利用根据逻辑系统设计的设计类型配置的行为模型、根据验证规则生成的断言语句以及约束语句生成形式验证环境，各个参数仅需要根据配置文件中指示的参数进行配置和修改，针对不同设计类型的逻辑系统设计选择不同的参数，利用生成的形式验证环境对待测设备的功能进行形式验证，降低了形式验证环境创建的难度。

[0064] 图5示出了本公开实施例所提供的一种用于生成形式验证环境的示例性方法500的流程示意图。

[0065] 本公开实施例所提供的一种用于生成形式验证环境的方法500。该方法500可以由图1所示的电子设备100执行。例如，方法500可以由电子设备100上运行的仿真工具200执行。该方法500可以包括以下步骤。

[0066] 在步骤502，形式验证工具200可以接收用于描述逻辑系统设计的功能的配置文件(例如，图3的配置文件302)，其中，所述配置文件指示所述逻辑系统设计的设计类型以及与所述设计类型对应的参数。

[0067] 在一些实施例中，所述设计类型可以包括调度器类型(例如，仲裁器)、流量管理器类型(例如，DMA控制器)、内存控制器类型(例如，内存控制器)或状态机模块类型(例如，电源管理器)。

[0068] 在步骤504，形式验证工具200可以根据所述配置文件确定与所述逻辑系统设计对应的数据库文件(例如，图3的数据库文件304)。

[0069] 在一些实施例中，所述数据库文件可以包括信号说明列表，并且形式验证工具200根据所述配置文件确定与所述逻辑系统设计对应的数据库文件进一步可以包括：形式验证工具200可以根据所述配置文件获取所述逻辑系统设计的输入信号；在所述信号说明列表中检测所述输入信号的匹配信号；以及响应于在所述信号说明列表中检测到所述输入信号的匹配信号，唯一绑定所述输入信号和所述匹配信号。

[0070] 在一些实施例中，所述方法500可以进一步包括：形式验证工具200可以加载与所述数据库文件对应的数据库模型；以及连接所述待测设备的接口和所述数据库模型的接口。

[0071] 在步骤506，形式验证工具200可以在所述数据库文件中获取与所述逻辑系统设计对应的多个形式验证环境参数。

[0072] 在一些实施例中，形式验证工具200在所述数据库文件中获取与所述逻辑系统设计对应的形式验证环境参数进一步可以包括：形式验证工具200可以根据所述配置文件按修改优先级对所述多个形式验证环境参数进行排序，以生成配置参数修改表(例如，表1的配置参数修改表)。

[0073] 在步骤508，形式验证工具200可以根据所述形式验证环境参数生成形式验证环境。

[0074] 在一些实施例中，所述形式验证环境可以包括：行为模型和断言语句，所述形式验证环境参数可以包括所述逻辑系统设计的验证规则，并且形式验证工具200根据所述形式验证环境参数生成形式验证环境进一步可以包括：形式验证工具200可以根据所述配置文件确定所述逻辑系统设计的设计类型；根据所述设计类型配置所述行为模型；以及根据所述配置参数修改表选择所述逻辑系统设计的验证规则以生成所述断言语句。

[0075] 在一些实施例中，所述形式验证环境还可以包括：约束语句(例如，“assume property@(posedge clock)disable iff(reset)(req&！grant|＝>req)”或“assert property@(posedge clock)disable iff(reset)(req|‑>s_eventually(grant))”)和反馈延迟，并且形式验证工具200根据所述形式验证环境参数生成形式验证环境进一步可以包括：形式验证工具200可以根据所述配置文件确定验证请求；定义所述验证请求的行为以生成所述约束语句；以及确定所述验证请求被响应的所述反馈延迟。

[0076] 在一些实施例中，当所述设计类型是所述调度程序类型中的仲裁器时，形式验证工具200根据所述设计类型配置所述行为模型进一步可以包括：形式验证工具200可以获取所述仲裁器的配置参数；以及将所述仲裁器的配置参数赋予所述行为模型。

[0077] 本申请提供的用于生成形式验证环境的方法、电子设备及存储介质，通过根据接收的用于描述逻辑系统设计的功能的配置文件，确定与该逻辑系统设计对应的数据库文件，进而从数据库文件中获取用于构建形式验证环境的形式验证环境参数，根据形式验证环境参数生成形式验证环境。从而降低了形式验证的使用门槛，快速简便地搭建形式验证环境，提高了形式验证的证明效率和收敛比例。

[0078] 上述对本申请特定实施例进行了描述。其他实施例在所附权利要求书的范围内。在一些情况下，在权利要求书中记载的动作或步骤可以按照不同于实施例中的顺序来执行并且仍然可以实现期望的结果。另外，在附图中描绘的过程不一定要求示出的特定顺序或者连续顺序才能实现期望的结果。在某些实施方式中，多任务处理和并行处理也是可以的或者可能是有利的。

[0079] 所属领域的普通技术人员应当理解：以上任何实施例的讨论仅为示例性的，并非旨在暗示本申请的范围(包括权利要求)被限于这些例子；在本申请的思路下，以上实施例或者不同实施例中的技术特征之间也可以进行组合，步骤可以以任意顺序实现，并存在如上所述的本申请的不同方面的许多其它变化，为了简明它们没有在细节中提供。

[0080] 另外，为简化说明和讨论，并且为了不会使本申请难以理解，在所提供的附图中可以示出或可以不示出与集成电路(IC)芯片和其它部件的公知的电源/接地连接。此外，可以以框图的形式示出装置，以便避免使本申请难以理解，并且这也考虑了以下事实，即关于这些框图装置的实施方式的细节是高度取决于将要实施本申请的平台的(即，这些细节应当完全处于本领域技术人员的理解范围内)。在阐述了具体细节(例如，电路)以描述本申请的示例性实施例的情况下，对本领域技术人员来说显而易见的是，可以在没有这些具体细节的情况下或者这些具体细节有变化的情况下实施本申请。因此，这些描述应被认为是说明性的而不是限制性的。

[0081] 尽管已经结合了本申请的具体实施例对本申请进行了描述，但是根据前面的描述，这些实施例的很多替换、修改和变型对本领域普通技术人员来说将是显而易见的。例如，其它存储器架构(例如，动态RAM(DRAM))可以使用所讨论的实施例。

[0082] 本申请旨在涵盖落入所附权利要求的宽泛范围之内的所有这样的替换、修改和变型。因此，凡在本申请的精神和原则之内，所做的任何省略、修改、等同替换、改进等，均应包含在本申请的保护范围之内。