用于存储器抽象以及用于使用该存储器抽象进行字级网表简化及其验证的方法和设备

摘要

一种包括存储器的电路设计的计算机实现的表示通过以下步骤被抽象成较小的网表：使用表示存储器中的所选槽的替代节点取代存储器，将网表中包括一个或多个替代节点的字级节点分割成分段节点，为分段节点寻找减小的安全尺寸，使用分段节点的减小的安全尺寸生成表示电路设计的更新数据结构。这种系统的正确性可能需要对比电路设计中存在的更少数量的存储器条目进行推理并且使用具有更小位宽的节点。作为结果，大大降低了验证问题的计算复杂性。

说明书

技术领域

本发明涉及集成电路设计，尤其涉及电子设计自动化工具以及对包含存储器的复杂设计进行验证和分析的工具。

背景技术

利用在比个体导线和基本门的级别高的级别上获取的设计信息来进行字级设计的分析是硬件验证中的一个新领域。在字级上，相对于一组不具有特殊语义的位级信号，数据路径单元和数据包本身被视为实体。

目前的模型检查技术针对检查面向控制的属性运转良好。然而，目前的模型检查技术针对具有宽数据路径和大型存储器的设计运转并不良好。以前的方法通过读取设计者注释或递增地计算设计的精确抽象来设法加速处理。然而，注释对于设计者来说是非常耗时的，而抽象的计算可以与解决原始问题一样困难。

最近围绕例如SMT求解器(S.Ranise和C.Tinelli.Satisfiabilitymodulo theories.Trends and Controversies-IEEE Intelligent SystemsMagazine，2006年12月)的字级公式判定过程，以及像UCLID(在2002年的Computer Aided Verification会议纪录中，R.Bryant，S.Lahiri，和S.Seshia的.Modeling and verifying systems using a logic of counter arithmeticwith lambda expressions and uninterpreted functions.)和BAT(在2007年的Computer Aided Verification会议纪录中，P.Manolios，S.Srinivasan和D.Vroon.BAT：The bit-level analysis tool.)的基于简化的过程已经有了许多研究。然而，随着此研究方向预期的兴起，使用这些过程来进行模型检查在本质上受到限制，因为这些过程对公式进行分析而不是对时序系统进行分析。这有两种结果：第一，时序属性仅能依靠诸如利用边界检查推断无界正确性的简化和插值之类的方法，来利用这些过程进行检查。第二，这些过程不适用于进行时序系统验证的基于变换的方法(在2006年的CAD会议中的Formal Methods的会议记录中，J.Baumgartner，T.Gloekler，D.Shanmugam，R.Seigler，G.V.Huben，H.Mony，P.Roessler，和B.Ramanandray的Enablinglarge-scale pervasive logic verification through multi-algorithmicformal reasoning.)，其中时序验证问题由后端模型检查器的大尺寸集合中的任何一个来迭代地简化并处理。

传统模型检查的最大障碍之一是混合了复杂控制逻辑的大型存储器的存在。这典型地导致了非常困难或难于控制的模型检查问题。因此，对包括大型存储器的硬件设计的有界及无界属性的实际字级模型检查需要有效地实现。

发明内容

提供了一种网表简化(netlist reduction)方法，其中将包含存储器的电路设计的网表抽象成较小的网表，该较小的网表可以通过标准验证工具和其它能够在网表上操作的工具进行分析。这种系统的正确性可能需要对比原来的电路设计中存在的更少数量的存储器条目进行推理。通过将这些存储器抽象成更少数量的条目，大大降低了验证问题的计算复杂性。

在一种方法中可以简化电路设计的计算机实现的表示，这种方法包含将电路设计表示为定义包括多个节点的网表的数据结构，例如以有向非循环图DAG的形式。例如，可以处理由高级描述语言表示的电路设计从而生成这种类型的输入数据结构。处理这种输入数据结构从而生成一种更新的网表，其具有较小的复杂度，需要较少的存储器槽和节点，减少了实现的位宽，同时又可以保持由网表表示的电路设计的预定属性。

输入网表的处理包括在电路设计中标识存储器，以及在所标识的存储器中标识一个或多个槽的地址，相应的一个或多个槽都需要满足所关注的指定属性。表示这些存储器的网表中的节点可以使用实现一个或多个槽的替代节点来取代。对网表中的字级节点进行分段并且为分段节点寻找减小的安全尺寸。然后使用这些分段节点和减小的安全尺寸来实现更新数据结构。实现验证条件，该验证条件使得能够使用更新数据结构来检查指定属性。应用这里描述的处理，通过去除表示不需要满足指定属性的槽的节点，在更新网表中表示的存储器的尺寸得以减小。

使用替代节点来取代网表中所标识存储器的一个或多个槽，该替代节点包括针对每个表示槽的、通过其位置来标识表示槽的节点(也就是下文实例中的“sel”)和相应的下一状态节点以及包含用于表示槽的数据的当前状态替代节点(也就是下文实例中的“cont”)和下一状态替代节点。表示向表示槽中进行写入的节点通过使用如下多路复用器实现，如果写数据与标识槽的节点的内容匹配，则该多路复用器用写数据来更新该槽的下一状态替代节点的内容，否则用当前状态替代节点的内容来更新表示槽的下一状态替代节点的内容。对于表示向表示槽进行读取的网表中的节点来说，替代节点包括如下多路复用器，如果读地址与标识该槽的节点的内容匹配，则该多路复用器返回表示槽的当前状态替代节点的内容，否则返回从外界中读取的非确定数据。

标识输入网表中存储器的处理包括：标识可重建模存储器(包括存储器阵列的一部分或者整个存储器阵列)，可重建模存储器的特征在于对存储器的当前状态节点和下一状态节点进行寻址的所有读和写节点可以读和写相同宽度的数据并且使用相同宽度的地址节点，以及存储器中的一个或多个槽以共同的方式初始化为一个确定值。

通过标识抽象对来选择在更新的网表中要表示的槽，其中抽象对包括在更新的网表中描述必须表示的存储器中的相应槽的节点和描述必须表示的周期期间的节点，以便满足例如电路设计中安全性定义这样的属性。因此，抽象对与更新的网表中表示的表示槽对应，并且包括标识表示槽的节点和表明如下周期的延迟参数，在这个周期中读取表示槽来满足属性。

组合输出形式的验证功能被重写以便当抽象对中指定的节点具有相应于适当的先前周期中相应槽的值时，可以检查输出。在实现更新网表时使用与关注的特定属性关联的抽象对，从而可以在更新网表中建立一组节点，该组节点针对每个抽象对指定所指示周期中的表示槽，将抽象节点与标识通过抽象对中的延迟参数所指示的周期中的表示槽的节点相比较。如果对于关联的抽象对表明相匹配，则就检查所关注的属性的输出。

在这里所描述的一种实现中，使用反例指导的精化处理来标识抽象对。例如，可以通过迭代地执行更新网表上的模型检查处理来标识抽象对，这种处理从最初的更新网表例如没有抽象对的实现开始。如果模型检查在特定状态中失败，捕获导致失败的迹线，然后使用原来的输入网表，基于特定状态的迹线确定的一组输入和初始状态变量赋值来运行仿真。如果仿真原网表没有指示失败，则处理更新网表来寻找导致失败的错误读取。选择抽象对以解决错误读取，将选择的抽象对添加到更新列表中。迭代返回模型检查步骤，并重复这个过程，直到更新列表通过模型检查，直到在仿真步骤中检测到真正的错误，或者直到更新网表大于目标尺寸为止。

在使用上述的有向非循环图数据结构的实现中，图表中的顶层节点包括表示电路输出和下一状态变量的字级节点，图表中的底层节点包括表示输入、状态变量和二进制常向量的所述字级节点，图表中的内部节点包括表示运算符的字级节点和存储器。

本申请介绍的技术处理字级网表来标识可重建模存储器，可重建模存储器仅仅使用专用读节点和写节点与外界交互，使用一致的方式初始化并且一致地存取。可重建模存储器可以以如下方式被抽象，即：当通过对与标准位级模型检查中所需数量相比少得多的存储器槽和时间实例进行推理来完成验证时，允许对属性的验证。

处理包括替代节点的字级节点从而提供上述减小的位宽。位宽减小处理在存储器抽象之后更有利，相比单独使用位宽减小处理来说，实现网表的更大简化。而且，通过在处理之前执行存储器抽象，为网表中的字级节点提供减小的位宽，位宽减小处理的复杂度大大降低。在这里描述的过程中，标识包含节点的网表中的第一组字级节点，这些节点包括具有一些被一致处理的数据路径分段的替代节点。第一组字级节点被分割成的段宽与一致处理的相应字的段一致。第二组节点不包括标识第一组节点时使用的一致处理的分段，第二组节点被转换成位级节点。通过应用计算机实现的功能，对分段的节点进行分析以确定减小的安全尺寸。然后使用分段节点的减小的安全尺寸生成代表电路设计的更新数据结构。然后可以分析更新数据结构以确定电路设计是否满足预定属性，例如安全性，并且在一种优选模式中，可以在数据处理系统的顺序系统验证中纳入一种基于变换的方法用于集成电路设计和制造。

在使用上述有向非循环图数据结构的实现中，图表中的顶层节点包括表示电路输出和下一状态变量的所述字级节点；图表中的底层节点包括表示输入、当前状态变量和二进制常向量的所述字级节点；图表中的内部节点包括表示运算符的所述字级节点。

对于特定电路设计的第一组节点包括表示存储器槽的一个或多个替代节点、表示比较运算符(等于)和(不等于)的字级节点、表示多路复用器运算符的字级节点、表示串接运算符的字级节点、表示提取运算符的字级节点、表示输入的字级节点、表示状态变量的字级节点和表示二进制常量的字级节点。对于特定设计的第二组节点包括表示算术运算符的字级节点、表示比较运算符(小于)、(小于或等于)、(大于)和(大于或等于)的字级节点、表示逻辑与运算符的字级节点以及表示逻辑非运算符的字级节点。

通过在数据结构中注册每一个节点以及对该节点构造一个分区列表，标识该节点的分段以及包括该节点的每个分段的依赖组，促进分段和转换处理。当注册所述节点时构造的分区列表和依赖组标识包括位(0...k-1)、其中节点宽度为k的节点的单个段。在该处理中保持依赖组以便它们标识依赖注册的特定节点的节点以及其依赖的节点。分段操作拆分在包含特定节点的特定依赖组内的节点，直到依赖组内的节点的分段匹配为止。转换操作将依赖组内的节点拆分成单个位段。

优选地，在为概率搜索所组织的数据结构例如跳表数据结构中保持节点的分区列表。

在使用依赖组的实施例中通过处理依赖组中的节点的分段来寻找分段的减小的安全尺寸，然后对每个节点的段进行求和，由此寻找减小的安全尺寸。寻找减小的安全尺寸的有用公式是：减小的安全尺寸是min(S，log₂(N_S+2))，其中依赖组包括段宽S、状态变量的数目N_S以及输入段的尺寸S和最多两个常量。

这里描述的技术可以实现为一种在数据处理机上执行的处理、一种适于执行所述过程的数据处理机以及一种可由数据处理机执行并且存储在计算机可读数据存储介质上的计算机程序。另外，这里的技术是用于制造集成电路的工艺的一部分，包括开发限定图案的数据，例如用于在集成电路制造中的光刻工艺中使用的一个掩膜或一组掩膜的布局数据。

这里描述的处理的特征包括，该实现可以在标准安全属性验证问题上操作、可以完全自动化而不需要抽象提示、可以与通常的位级模型检查器一起用作后端决策进程、并且可以无缝地嵌入标准变换验证范例。

本发明的其它方面和优势可以在下面的附图、详细描述和权利要求中得到更清楚地体现。

附图说明

图1示出了示意性集成电路设计流程的简化表示。

图2是计算机系统的简化方块图，该系统适用于该技术的实施例以及技术的电路实施例和电路设计。

图3是用于减小数据结构的尺寸并且使用减小的数据结构执行验证处理的过程的简化流程图，该数据结构表示包括存储器的电路设计。

图4是作为包括存储器和多个节点的有向非循环图实现的网表的代表性实例。

图5示出了对图4中示出的电路设计的抽象。

图6示出了使用图5的抽象对安全属性的实现。

图7-8示出了通过对存储器进行抽象来减小表示电路设计的数据结构的尺寸的过程的更详细流程图。

图9示出了读节点的多路复用器树的实现。

图10示出了使用包括多个抽象对的更新网表对安全属性的实现。

图11是计算机实现的、反例指导的抽象精化环的方块图。

图12是用于减小表示电路设计的数据结构的尺寸并使用减小的数据结构执行验证处理的过程的简化流程图。

图13是作为包括多个节点的有向非循环图实现的网表的代表性实例。

图14是示出了在图9-13的过程中使用的数据结构的简化图。

图15示出了拆分分区节点的操作。

图16示出了针对一组节点合并依赖组的操作。

图17示出了使一组节点可兼容的操作。

图18-22示出了用于减小表示电路设计的数据结构的尺寸的过程的更详细流程图。

图23示出了处理提取节点的操作。

具体实施方式

图1是示意性集成电路设计流程的简化表示。对于文中所有的流程图来说，应当理解图1中的很多步骤都是可以组合、可以并行执行或者以不同的顺序执行，而不影响所实现的功能。在一些情况中，只要也作出某些其它的改变，重新排列这些步骤会获得相同的结果，而在其它情况中，只要满足某些条件，重新排列这些步骤也将获得相同的结果。这些重新排列的可能性对于读者是显而易见的。

在高层中，图1的过程始于产品构想(方块100)并且在EDA(电子设计自动化)软件设计处理(方块110)中实现。当设计定稿时，进行制造处理(方块150)以及封装和组装处理(方块160)，最后得到成品集成电路芯片(结果170)。

EDA软件设计处理(方块110)实际上由多个步骤112-130组成，为了简化起见以线性方式示出。在实际的集成电路设计过程中，特定设计可能需要在多个步骤当中返回直到通过某些测试。类似地，在任一实际的设计过程中，这些步骤可以以不同的顺序和组合发生。因此该描述是通过上下文和一般性说明的方式而不是作为对特定集成电路的特定或者推荐的设计流程来提供的。

下面将提供EDA软件设计处理(方块110)的组成步骤的简要描述。

系统设计(方块112)：设计者描述他们想要实现的功能，他们可以执行假设规划以精化功能、检验成本等等。这个阶段可以出现硬件-软件架构。可以在这个步骤使用的来自Synopsys公司的示例性EDA软件产品包括ModelArchitect、Saber、System Studio以及产品。

逻辑设计和功能验证(方块114)：在这个阶段，编写用于系统中模块的高级描述语言(HDL)代码，例如VHDL或者verilog代码，并且针对功能准确性检查设计。更具体而言，检查设计以确保其生成响应于特定输入激励的正确输出。可以在这个步骤使用的来自Synopsys公司的示例性EDA软件产品包括VCS、VERA、Magellan、Formality、ESP以及LEDA产品。使用下文中详细描述的存储器抽象的字级网表简化技术可以作为例如用于Magellan产品的一部分或者附加工具来实现。

合成和可测性设计(方块116)：这里，将VHDL/Verilog转译成网表。该网表可以被优化用于目标技术。另外，设计并实现测试以允许检查成品芯片。可以在这个步骤使用的来自Synopsys公司的示例性EDA软件产品包括DesignPhysical Compiler、Test Compiler、Power Compiler、FPGACompiler、TetraMAX以及产品。

网表验证(方块118)：在这个步骤，检查网表与定时约束的符合性以及与VHDL/Verilog源代码的一致性。可以在这个步骤使用的来自Synopsys公司的示例性EDA软件产品包括Formality、PrimeTime以及VCS产品。

设计规划(方块120)：这里，针对定时和顶层布线构造并分析芯片的整个布局规划图。可以在这个步骤使用的来自Synopsys公司的示例性EDA软件产品包括Astro和IC Compiler产品。

物理实现(方块122)：在这个步骤进行布置(电路元件的定位)以及布线(电路元件的连接)。可以在这个步骤使用的来自Synopsys公司的示例性EDA软件产品包括AstroRail、Primetime以及Star RC/XT产品。

分析和提取(方块124)：在这个步骤，在晶体管级验证电路功能，这有允许假设精化。可以在这个步骤使用的来自Synopsys公司的示例性EDA软件产品包括AstroRail、PrimeRail、Primetime以及Star RC/XT产品。

物理验证(方块126)：在这个阶段执行各种检查功能以确保制造、电问题、光刻问题以及电路的正确性。可以在这个步骤使用的来自Synopsys公司的示例性EDA软件产品包括Hercules产品。

流片(方块127)：这个阶段提供“流片”数据以制造掩膜用于产生成品芯片的光刻。可以在这个步骤使用的来自Synopsys公司的示例性EDA软件产品包括CATS(R)系列产品。

分辨率增强(方块128)：这个阶段涉及布局的几何操纵以提高设计的可制造性。可以在这个步骤使用的来自Synopsys公司的示例性EDA软件产品包括Proteus/Progen、ProteusAF和PSMGen产品。

掩膜制备(方块130)：这个阶段包括掩膜数据制备和掩膜本身的写入。可以在这个阶段使用的来自Synopsys公司的示例性EDA软件产品包括CATS(R)系统产品。

这里描述的网表简化技术实施例可以在上述的一个或多个阶段中使用。例如，本发明的实施例可以在逻辑设计和功能验证(图1的块114)过程中使用。在这个阶段，编写用于系统中模块的VHDL或Verilog代码并且针对功能准确性检查设计。更具体而言，检查设计以确保它响应于特定的输入激励生成正确的输出。

图2是适用于该技术的实施例的计算机系统210的简化方块图。计算机系统210通常包括至少一个处理器214，该至少一个处理器214经由总线子系统212与多个外围设备通信。这些外围设备可以包括存储子系统224、用户接口输入设备222、用户接口输出设备220以及网络接口子系统216，该存储子系统224包括存储器子系统226和文件存储子系统228。输入和输出设备允许用户与计算机系统210的交互。网络接口子系统216提供至外部网络的接口，包括至通信网络218的接口，并且经由通信网络218耦合到其它计算机系统中的相应接口设备上。通信网络218可以包括多个互联的计算机系统和通信链路。这些通信链路可以是有线链路、光链路、无线链路或者任何其它用于信息通信的机制。在一个实施例中，通信网络218是因特网，而在其它实施例中，通信网络218可以是任意适当的计算机网络。

用户接口输入设备222可以包括键盘、指示装置(例如鼠标、轨迹球、触摸板或者图形输入板)、扫描仪、与显示器结合的触摸屏、音频输入设备(例如声音标识系统)、麦克风以及其它类型的输入设备。通常，使用术语“输入设备”旨在于包括用以向计算机系统210中或通信网络218上输入信息的所有可能类型的设备和方式。

用户接口输出设备220可以包括显示器子系统、打印机、传真机或者例如音频输出设备的非可视显示器。显示器子系统可以包括阴极射线管(CRT)、例如液晶显示器(LCD)的平板设备、投影设备或者一些其它用于生成可视图像的机制。显示器子系统还可以提供例如经由音频输出设备的非可视显示器。通常，使用术语“输出设备”旨在于包括用以从计算机系统210向用户或其它机器或者计算机系统输出信息的所有可能类型的设备和方式。

存储子系统224存储基本编程和数据构造，其提供文中描述的EDA工具的一部分或所有功能，包括应用于分析简化网表的存储器抽象以及字级网表简化技术和验证工具。这些软件模块通常由处理器214执行。

存储器子系统226通常包括多个存储器，所述存储器包括于在程序执行期间存储指令和数据的主随机存取存储器以及其中存储固定指令的只读存储器(ROM)232。文件存储子系统228为程序和数据文件提供永久性存储，并且可以包括硬盘驱动器、与关联的可移除介质一起的软盘驱动器、CD-ROM驱动器、光盘驱动器或者可移除介质磁带。实现某些实施例的功能的数据库和模块可以通过文件存储子系统228存储。

总线子系统212提供一种用于使计算机系统210的各种组件和子系统如所期望的那样彼此通信的机制。虽然总线子系统212示意性地以单个总线的形式示出，但是总线子系统的可替代实施例可以使用多个总线。

计算机可读介质240可以是与文件存储子系统228和/或网络接口子系统216相关联的介质。计算机可读介质可以是硬盘、软盘、CD-ROM以及光学介质、可移除介质磁带或者电磁波。计算机可读介质240示出为存储电路设计280，包括例如电路设计的HDL描述以及使用文中描述的技术创建的简化网表。还示出了使用文中描述的技术创建的电路290。

计算机系统210本身可以是多种形式，包括个人计算机、便携式计算机、工作站、计算机终端、网络计算机、电视、大型主机或者任意其它数据处理系统或者用户设备。由于计算机和网络的经常改变的特性，对图2示出的计算机系统210的描述目的仅仅是作为用于解释优选实施例的一个特定示例。还可以使用计算机系统210的很多其它配置，这些配置可以具有比图2示出的计算机系统更多或更少的组件。

图3是对电路设计执行验证步骤的过程的基本流程图，其中包括在简化网表上进行操作。在图3的过程中，包括多个节点的字级网表根据电路设计的高级描述语言的描述编译，优选以节点的有向非循环图形式(方块300)。存储器抽象技术的实施例在字级节点上操作。然而，可替代系统可以应用于位级实现。标准前端流程采用例如以硬件描述语言(HDL)表达的寄存器传输级(RTL)描述，该RTL描述补充有用户约束、属性和其它信息的定义，并且标准前端流程生成后文中将要详细描述的隐含钟控DAG表示。使用标准前端流程，通过将具有属性和约束的硬件设计处理成多个节点，从而将电路设计编译为网表，该多个节点表示基于一组不受约束的输入I、状态变量S和常量的组合逻辑。得到的多个节点的顶层包含下一状态变量S’和单个位输出O。使用这种技术进行验证的属性包括所有的安全属性，这些属性的失败通过假定值为“假”的一些输出来发信号通知。安全属性是电路设计属性的子类，其具有一些输出总是成立的形式(也就是，总能通过有限迹线示出其失败)。另外，在一些实施例中每个状态变量可以假定为具有未知的初始状态。

以这种方式编译的图中的内部节点包括：

node1＝not(node2)

node1＝and(node2，node3)

node1＝arithOp(node2，node3)，arithOp为{＝，-，...}中的一个

node1＝compOp(node2，node3)，compOp为{小于，小于或等于，等于，不等于，大于或等于，大于}中的一个

node1＝mux(selector，node2，node3)

node1＝extract(x，node2)

node1＝concat(node2，node3，...)

node1＝read(op1，addrj)

node1＝write(opk，addri，dataj)

从其中结果的位i通过将布尔运算符应用到输入节点的位i而得到这种意义上来说，“not”和“and”运算符是按位运算符。如果selector为真并且node3不为真，则“mux”节点返回node2。“extract”节点通过从其操作数的位置(x)到(x+k-1)投射出k位从而构造较小的位向量。最后，“concat”节点通过串接其操作数形成较大的位向量从而形成较大的信号。自变量表中的早期操作数拼接变成较高级位，因此concat(01，00)变成0100。

mux的选择信号以及比较运算符节点的输出被限制为具有位宽1。这些信号据称为位级信号。不是位级信号的信号称为字级信号。术语“分段”表示一组连续位，并且可以是指整个字或者字的一部分。

读节点和写节点用于对存储器进行建模。读节点的语义规定，对于宽度w的读节点，该节点返回投射出在来自其自变量中位向量op的位置addr*w...(addr+1)*(w-1)处的位的结果。对于具有宽度w的数据操作数的写节点，写节点返回的位向量将产生于利用其自变量中的数据对其自变量中位向量op的区域addr*w...(addr+1)*(w-1)的重写。读节点和写节点的地址空间不需要以任何特定形式进行限制。越界读取针对不存在的位返回非确定值。越界写入什么都不做。专用“存储器”寄存器节点，或者对读节点和写节点可以施加到什么信号的限制，都不是必须的。这样，RTL存储器设计可以象任意其它节点那样被建模为位向量寄存器。通过恰当使用控制逻辑，与多个读节点和写节点一起，该示例中的DAG支持具有大量读端口和写端口的任意复杂的存储器接口。而且，通过嵌套读节点、写节点和其它节点，可以在来自同周期读和写的更新和读区顺序上实现复杂的策略。

回到图3，遍历输入网表以标识可重建模存储器和存储器的读节点和写节点(方块301)。可重建模存储器是一种可以使用该技术进行提取的存储器。基本上，在一个实际实现中的可重建模存储器可以限定成用一致方式对所有槽进行寻址，仅以另一种实现可以被容易替代的方式与设计的其它部分进行通信，并且具有特定简单结构的下一状态函数。更加正式地，在一种给定寄存器变量mem的实现中，用于mem的标记为“纯存储器节点”的一组存储器节点可以递归地定义如下：

1)节点mem是用于mem的纯存储器节点；

2)如果op^k是用于mem的纯存储器节点，则write(op^k，addrⁱ，data^j)是用于mem的纯存储器节点

3)如果optrue^k和opfalse^k是用于mem的纯存储器节点，则mux(sel^l，optrue^k，opfalse^k)是用于mem的纯存储器节点。

用于状态变量mem的一组纯读节点包括所有的网表读节点read(opⁱ，addr^j)，其中opⁱ是用于mem的纯存储器节点。而且，用于mem的一组写节点包括所有的网表节点write(op^k，addrⁱ，data^j)，其中op^k是用于mem的纯存储器节点。

给定这一术语，可重建模存储器可以定义为满足下述要求的寄存器状态变量mem：

1)在它们的支持中具有mem的所有读节点和写节点使用相同宽度a的地址节点读取和写入相同宽度w的数据。而且，mem的位宽是w的整数m倍，并且2a≤m*w，以便在存储器内可以进行所有的存储器存取。

2)mem被初始化为布尔常量0000...0、1111...1或者其它确定的初始值。

3)用于mem的下一状态函数是用于mem的纯存储器节点，没有其它的下一状态函数是用于mem的纯存储器节点。

4)每个来自mem的扇出路径由一系列纯存储器节点组成，这一系列节点终止于(1)用于mem的下一状态节点，或者(2)纯读节点。

第一要求确保存储器被视为通过一致方式进行读和写的槽的位向量。第二要求确保所有槽具有相同的初始状态，这样保证了在更新网表中选择用于表示的槽都具有相同的初始状态。剩余的要求确保存储器寄存器仅仅出现在其它状态寄存器的扇入中并且通过读节点进行输出，以及确保存储器的下一状态函数是一个简单的多路复用器树，其在不同的对存储器进行更新的写节点之间进行选择。

在本文中使用的可重建模存储器的定义提供了在能够覆盖最关注的存储器实现同时足以简单地提供相对直接的存储器抽象算法之间的一种平衡。利用适当的处理考虑例外情况，也可以对其它类型的存储器进行重建模。

给定一种编码为字级DAG的网表，可以使用直接线性遍历算法来提取一组可重建模存储器，并且计算它们关联的一组读节点和写节点。

再回到图3，一旦标识了可重建模存储器连同它们的一组读节点和写节点，则就可以对存储器进行重建模，以将所表示的存储器槽的数量减少为需要满足所关注的指定属性例如一个安全属性或者一组安全属性的那些槽，如下文中更详细描述的那样(方块302)。

接下来，执行字级网表简化处理以减小网表中的数据路径的位宽(方块303)。这个处理将在下文中结合附图进行更详细的描述。

然后处理简化网表以确定电路设计是否满足指定属性，或者可以执行一个更加严格的模型检查(方块304)。如下文中所提到的，在特定简化网表上执行的模型检查可以作为代表性实施例中抽象精化环的一部分来实现。而且，简化网表可以在各种工具中处理，包括在顺序系统验证的基于变换的方法中进行操作的工具。

图4示出了以DAG形式实现的示例性网表，其包括含有存储器的电路设计。在DAG的底部，网表包括：mem¹⁶³⁸⁴，其为具有16384位宽的存储器的当前状态节点400；具有宽度为9的读地址节点raddr⁹401；具有宽度为9的写地址节点waddr⁹402；具有宽度32的数据节点data³²403；以及具有宽度32的常量节点0³²404。DAG的顶部包括宽度为1的输出节点safe^l418和存储器的下一状态节点mem’¹⁶³⁸⁴419。读节点405通过使用在节点401的地址读取存储器节点400而产生输出。比较器节点406将读节点405的输出和存储在节点407中的常量100³²进行比较。

＞运算符节点408将数据节点403的内容和节点409中常量200³²的内容进行比较。将节点408中运算符的结果施加为对多路复用器410的selector输入。当节点408的输出为真时，多路复用器410选择数据节点403的内容，或者当节点408的输出为假时选择来自节点404的常量0³²。写节点411使用多路复用器节点410的输出提供的数据在写地址节点402提供的地址处写入存储器节点400的下一状态寄存器406。

因此，在每一时钟周期，系统从mem读取地址raddr处的槽的内容。并且如果数据大于200，它向地址waddr处的槽写入输入数据，否则就写入0。实现的属性是安全属性，要求从mem读取的值永远不等于100。很明显在这种简单的系统中对于任意执行迹线都为真。并且，这个声明可以通过推理存储器中单个槽随时间的内容也就是最后的槽读取来验证。

从概念上来说，图4中建模的电路可以分成两部分。第一部分(虚线415所包围的)包括大存储器mem，并且通过如下两个输入和两个输出与设计的其余部分通信：节点402和411之间的9位宽写地址端口wa、节点410和411之间的32位宽写数据端口wd、节点401和405之间的9位宽读地址端口ra以及节点405和406之间的32位宽读数据端口rd。图4的电路的第二部分是电路的平衡部分。

图4中示出的存储器可以如图5所示那样进行抽象，通过使用如下两个寄存器的当前状态和下一状态的版本来取代16384位宽的当前状态和下一状态存储器节点：9位宽的sel节点500和sel’节点501，其例如通过包含所表示的存储器槽的地址来标识该槽；以及每个都是32位宽的cont节点502和cont’节点503，其起到容纳表示槽的内容的作用。电路初始化期间选择以这种方式表示的槽，并且在接下来的系统执行期间一直保持不变。该实现中的节点sel具有无约束初始状态和仅把当前状态值传递到下一状态节点501的下一状态函数。寄存器cont 502、503被初始化为存储器槽的指定初始值，例如所有都为0。

来自图4所示实现的写节点由多路复用器504取代，如果sel节点500的内容等于由比较器505的输出指示的写地址端口wa⁹上的地址，则多路复用器504使用写数据端口wd³²上的数据更新cont的下一状态值；否则，多路复用器504将cont的当前状态节点502传递到下一状态节点503。来自图4所示实现的读节点由多路复用器506取代，如果sel节点500的内容等于由比较器507的输出指示的读地址端口ra⁹上的地址，则多路复用器506向读端口rd³²提供来自cont的当前状态节点502的内容；否则，多路复用器506提供来自非确定读节点508的非确定数据。

另外，在如图6所示的示例中，更新网表以改变正确性的定义，使得只有当从当前时钟周期读取的地址是由sel节点500指示的所表示槽的地址时才检查所关注的属性。这样，节点408中的safe输出通过蕴含运算符601的输出馈送。如节点600的输出所指示的，如果馈送读地址端口ra的节点401与sel节点500的内容匹配，则蕴含运算符601只检查原来的安全定义电路safedef¹602的输出。这种实现防止了由存储器抽象引入的伪反例，该伪反例发生在如下情况中：(1)其中末循环中raddr的值不同于选择为sel的初始值的值以及(2)ndtrd 508的内容是100。在这个反例中，通过sel的初始化选择用于表示的槽不与反例中读取的地址同步。这样导致的错误读取会错误地触发安全定义的假输出。通过重新实现图6所示的验证条件，消除错误假指示的可能性。

在刚刚参考图4-6描述的示例中，基于由raddr节点401标识的槽的当前值对存储器进行抽象。这样做对于该示例来说运行良好。然而对于很多系统来说，必须正确地执行从多个时间实例或周期的存储器存取，以确保可以在当前周期内检查系统的正确性。例如，为了检查完整的多部件消息被一直正确转发，则安全性定义可能要求随时间进行正确的一系列读取的性能。为了控制这些类型的系统，可重建模存储器在这个进程内被基于一组抽象对(v_i，d_i)抽象，其中v_i是一个信号，例如raddr节点401，其包含表示槽的读地址，d_i是一个整数时间延迟，其指示在当前周期之前的多个周期。节点v_i和所有的抽象对必须与在存储器上的读和写操作的地址节点具有相同的宽度。在参考图4-6描述的示例中，存储器被基于单个抽象对{(raddr9，0)}而抽象。

在简化网表的特定实现中应用的该组抽象对由下文描述的处理来标识。假设已经标识出抽象对，图7和图8提供了用于引入表示槽、重新实现读节点以及修改验证条件来产生更新网表的流程图。

该处理包括遍历输入网表以标识可重建模存储器(块700，块701)。对于每个可重建模存储器来说，引入“n”个抽象对(块702)。如块703所示，通过利用未初始化的初始状态函数引入用于(v_i，d_i)的当前状态变量Sel_i和仅传递上述前一状态值到下一状态变量sel’_i的下一状态函数(块704)，处理每个抽象对(v_i，d_i)。Sel_i寄存器将包含在系统运行期间由该抽象对表示的具体的槽数量。另外，针对表示槽，还引入容器寄存器cont_i及其下一状态寄存器cont’_i。容器寄存器以对应于原始mem节点的初始化的方式被初始化。驱动下一状态寄存器cont’的函数被作为更新网表中用于所标识存储器中下一状态函数的节点。这种可能是存在的，因为该示例中的可重建模存储器的定义确保了用于mem的下一状态函数是用于mem的纯存储器节点。

接下来，由替代节点取代网表中用于所标识的可重建模存储器mem的纯存储器节点。如块705中所示，如果节点是所标识的存储器，则对应于当前抽象对的容器寄存器(contⁱ)和初始化向量用作存储器的替代节点(块706)。如果节点是形式为write(op^k，addr^l，data^m)的写节点(块707)，则用逻辑mux(sel^l＝addr^l，data^m，s0)取代它，其中s0表示对应于更新网表中op^k的节点，例如图5中的容器寄存器cont(块708)。

进行到图8，如果节点是形式为mux(selector，optrue，opfalse)的多路复用器(块709)，则用逻辑mux(selⁱ＝addr^l，s0，s1)来取代它，其中s0和s1是分别在更新网表中表示optrue和opfalse的节点(块710)。

接下来，替代节点连接到对应槽的下一状态容器寄存器cont’ⁱ，例如节点504连接到图5中的cont’503(块711)。该处理以这种方式遍历抽象对，直到它们都在更新网表中重新实现(块712，块713)。

接下来，对读节点进行重新实现。如果节点具有形式read(op^k，addr^l)，其中op^k由用于抽象对的所表示的存储器槽取代，则对读节点多路复用器树进行修改以包括该表示槽(块714)。该对于读节点的多路复用器树的实现在下文中参考图10进行描述。

在处理了对应于所标识的存储器的节点后，修改验证条件(块715)使得只有当由抽象节点标识的信号v_i具有在适当的前一时间实例d_i上的选择值时才检查属性。一种用于实现验证条件的技术在于定义时域公式prev^di(s)，在系统执行期间的时刻t，如果t≥d并且在时刻t-d时组合信号s估计为真，则上述公式为真。假设对于信号s存在n个抽象对(vi，di)，通过针对该时域公式合成检查器可以产生新的safe输出：

其中safedef是馈送旧safe输出的组合节点。在图4描述的示例中，safedef是节点406，当读数据端口rd上的数据不等于100时该节点为真。可以使用延迟一些网表节点比较的先前值的多个寄存器链，以一种简单的方式实现这种检测器。下面参考图10描述一个示例。注意，所标识的存储器mem是可重建模存储器。因此只会发生在其它状态变量通过读节点的扇入中。更新网表重新实现满足安全条件所需的所有读节点。因此，可以通过移除原来的存储器mem和所有以上述方式依赖于它的逻辑来简化网表。

块716-718示出了针对该处理的一些实施例重新实现网表中所涉及的另外的步骤。将这些节点插入到流程图中以反映出它们是可以使用的一部分处理示例，而不是指示处理执行的顺序。首先，如上所述，在一种方法中针对所有读节点引入寄存器ndtrd。替代实现可以应用双轨编码，将附加位添加到信号路径内的寄存器，该附加位作为一个标志用于指示内容是否是非确定的。可以评估网表，以确定对于给定的电路设计实现哪种方法更加有效，并且选择这种技术(块716)。这可以通过一次使用双轨编码和一次使用非确定数据节点执行重新实现环(例如节点702-715)并且比较结果来完成。而且，初始化函数可以针对各种节点而建立，包括不是全部为0或不是全部为1的用于存储器的容器节点，释放可重建模存储器的定义以允许不一致的初始化(块717)。最终，可重建模存储器的定义可以放宽到允许无约束地址宽度，在这样的情况下更新网表可以通过增加用于读节点和写节点的越界地址检查来进一步更新(块718)。

一旦生成了更新网表，该处理会继续进行到执行反例指导的抽象精化处理以确定是否需要增加额外的抽象对(块719)。下面将参考图11描述代表性的反例指导的抽象精化处理的细节。

如上面参考块714所述的，在更新网表中由图9中所示的多路复用器树表示纯读节点。图9中示出的多路复用器树返回第一所选槽的内容，其具有匹配读地址端口ra地址的地址。如果该地址不匹配任一所选槽，则在输入节点ndtrd 901处从外界读取非确定值。多路复用器树包括多路复用器905-0至905-n，并且接收标识表示槽sel0至seln的节点作为输入，在比较器节点902-0至902-n，将这些节点与读地址端口上的地址相比较。比较器节点902-0至902-n的输出用作相应多路复用器905-0至905-n上的selector输入。而且，多路复用器树接收所表示槽cont0至contn的替代节点作为输入。如果比较器节点902-0的输出为真，则多路复用器905-0选择cont0的内容，否则选择多路复用器905-1的输出(未示出)。如果比较器节点902-n的输出为真，则树中的最后一个多路复用器905-n选择contn的内容，否则选择ndtrd节点901的值。

图10示出了参考块713在上面提到的验证条件的重新实现。在这个示例中，“safe”输出920由蕴含运算符921驱动。当AND节点922的输出为真时，蕴含运算符操作为仅检查安全性定义safedef¹的输出。AND节点922由基于抽象对的一组比较器驱动，该组比较器的输出延迟在抽象对中指示的适当延迟时间。这样，来自抽象对(v₀，d₀)910-0的值v₀与标识由抽象对表示的槽的sel0节点比较。由于延迟值d₀为0，指示抽象对对应于当前周期内的槽读取，比较器911-0的输出没有延迟地施加在AND节点922。来自抽象对(v₀，d₀)910-1的值v₁与标识由抽象对表示的槽的sel1节点比较。由于延迟值d1为1，指示抽象对对应于当前周期之前的一个周期内的槽读取，比较器911-1的输出以通过寄存器912的一个周期延迟施加在AND节点922上。来自抽象对(v₂，d₂)910-2的值v₂与标识由抽象对表示的槽的sel2节点比较。由于延迟值d₂是2，指示抽象对对应于当前周期之前的两个周期内的槽读取，比较器911-2的输出以通过寄存器913和914的两个周期延迟施加在AND节点922上。在图10中简化了延迟寄存器以避免使图显得拥挤。在代表性系统中，延迟912通过建立具有下一状态节点d1’的节点d1实现。比较器911-1的输出提供当前周期中的节点d1’。提供寄存器d1的内容作为AND节点922的输入。同样，通过创建寄存器d1和d2实现延迟913和914，其中下一状态节点d1’由比较器911-2的输出驱动，当前状态节点寄存器d1驱动下一状态寄存器d2’，提供d2作为AND节点922的输入。

图11示出了针对特定设计问题寻找抽象对的处理。一种替代方法是依靠用户提供对一组抽象对的标识作为该处理的输入。然而，优选图11中示出的自动方法。因而，对于图11的处理，为设计中的每个可重建模存储器保持当前的一组抽象对。用于每个可重建模存储器的该组抽象对在图11示出的迭代处理中单调增加。该处理提供其中没有可重建模存储器的存储器槽被表示的初始抽象，其具有0个抽象对(块948)。在这个初始抽象中，在所表示的系统中，每个来自存储器的读取都返回一个非确定结果。给定该初始抽象，计算抽象的系统，通过使用例如上面关于图7和图8描述的进程提供更新网表(块949)。BIT WIDTH RED(块950)。将更新网表应用于位级模型检查例程，例如通常在本领域中用来检查设计的正确性(块951)。如果检查的属性保持在更新网表上，抽象处理继续进行到对原系统的有界检查(块953)。在这个步骤中，使用标准基于SAT的有界模型检查程序，通过对应于更新网表中该组抽象对中的最大延迟值的周期数量确定边界，检查原系统的边界正确性。如果检查通过，则宣布系统是正确的(块960)。如果对原系统的有界检查失败，则原系统就是有错误的并且会报告一个错误(块955)。

如果块951的模型检查检测到由更新网表表示的抽象系统上的一个反例，则进程会试图精化该抽象。抽象系统的输入是原系统输入的父集。因此可以使用更新网表中指示失败的迹线确定的输入和状态变量在原系统上进行仿真来重放该反例。这样，将网表中的失败迹线转译回原位宽(块952)，并且仿真原机器(块954)。如果在仿真中检测到错误，则向用户报告一个错误(块955)。如果仿真中没有出现错误，则有必要精化抽象组来消除错误迹线。

由于原系统和会引入伪反例的抽象系统之间唯一的不同是存储器编码，所以在一些时间实例中的一些抽象读节点必须返回未表示的槽的内容。通过检查运行在原系统上的仿真和比较抽象前后的读节点的值，在抽象系统的执行中可以标识出随着时间的错误读取(块956)。

并不是所有的错误读取对所检查的属性都有影响。该进程通过最初强制在抽象系统仿真中对于所有错误读取都提供正确值，并且以贪心方式反复缩减该校正组直到确定仿真中仍可以消除错误的局部最小强制读取，由此确定最小的一组读取和关联的时间点。

给定一组待校正的错误读取和与发生错误读取的错误周期的时间距离，对于每个时间点必须标识出抽象信号。可以使用启发法选择抽象信号，如下：如果与存储器槽数量相关的存储器的一部分读节点小于一些经验选择值，例如20％，则使用与末周期的相应时间距离处的失败读取的地址信号来创建新的抽象对。然而，如果与存储器槽数量相关的存储器的一部分读节点大于这些选择值，则该进程搜索一种如下寄存器：(1)该寄存器的尺寸与存储器地址宽度相同，(2)该寄存器位于存储器的影响锥内，并且(3)该寄存器包含由错误读节点在执行读取的时间实例读取的地址值。一旦发现满足这些标准的寄存器，就使用所标识的寄存器节点创建一个新的抽象对。在具有大量读节点的电路设计中，为了成功地抽象存储器，包含所标识槽的寄存器入口应当能够在设计中的任何地方存在。这种假设对于处理某些类型的存储器来说很重要，例如内容可寻址存储器，其中存储器中的每个入口在每个周期都被读取，但是只有小量的读取会在给定的时间内进行。

例如，对于具有含32个槽和2个读节点的单个可重建模存储器的设计的抽象版本，假设长度为15个周期的反例。如果形式为read(mem，raddri)的读节点需要在周期13(其是失败周期之前的一个时间步长)具有正确值，则为了移除错误迹线，向当前抽象组添加抽象对(raddri，1)。然而如果存储器具有28个读节点，则该进程将搜索寄存器reg，该寄存器reg在周期13包含读取失败的具体地址，并且所发现的寄存器将形成新的抽象组(reg，1)的基础。如果不存在这样的寄存器，则该进程将转向对存储器的原始的未抽象建模。

在块957选择新的一组抽象对后，所述处理执行评估是否有进展的步骤(块959)。当然这个步骤与图11示出的其它步骤一起都可以以任何适当的顺序发生。例如，如果块951之后确定的抽象尺寸例如大于原网表尺寸的75％，则该进程会分支到使用原网表(块958)。在一种替代方案中，在块959处系统可以进行检查，以确定处理是否超过了时限或者超过了预定循环数量，从而指示是否实现改进。

在任何情况中，向抽象系统添加新的一组抽象对，并且完成提供该新的一组抽象对所需要的这种修改(块951)。该进程围绕图11示出的循环迭代，直到模型检查成功(块960)，报告错误(块955)，或者作出使用原网表的决定(块958)。

图12是用于执行电路设计的验证步骤的处理的基本流程图，该验证步骤包括在简化网表上进行操作。在图3的处理中，包括多个节点的字级网表由电路设计的高级描述语言编译，优选以节点的有向非循环图的形式(块1200)。标准前端流程采用例如以硬件描述语言(HDL)表达的寄存器传输级(RTL)描述，该RTL描述补充有用户约束、属性和其它信息的定义，并且标准前端流程产生下文中描述的隐含钟控DAG表示。使用标准前端流程，通过将具有属性和约束的硬件设计处理成多个节点，从而将电路设计编译为网表，该多个节点表示基于一组无约束输入I、状态变量S和常量的组合逻辑。得到的多个节点的顶部包含下一状态变量S’和单个位输出O。可以使用这种技术进行验证的属性包括所有其失败通过假定值为“false”的一些输出来发信号通知的属性，其中包括安全属性。安全属性是电路设计属性的子集，其具有总能保持一些输出的形式(也就是，总能通过有限迹线示出其失败)。另外，在一些实施例中每个状态变量都可以假设具有完全或部分未知的初始状态。

以这种方式(如上所述)编译的图表中的内部节点包括：

node1＝not(node2)node1＝and(node2，node3)

node1＝arithOp(node2，node3)，其中arithOp是{+，-，...}中的一个

node1＝compOp(node2，node3)，其中compOp是{小于，小于或等于，等于，不等于，大于或等于，大于}中的一个

node1＝mux(selector，node2，node3)

node1＝extract(x，node2)

node1＝concat(node2，node3)

从其中结果的位i通过将布尔运算符应用到输入节点的位i上而得到这种意义上来说，“not”和“and”运算符是按位运算符。如果selector为真而node3不为真，则“mux”节点返回node2。“extract”节点通过从其操作数的位置(x)至(x+k-1)投射出k位从而构造较小的位向量。最后，“concat”节点通过串接其操作数形成较大的位向量从而形成较大的信号。自变量表中的较早操作数串接变为较高级位，所以concat(01，00)就变成0100。

mux的选择信号和比较运算符节点的输出被限制为具有位宽1。这种信号据称为位级信号。不是位级信号的信号称为字级信号。术语“分段”指的是一组连续位，并且可以是指一个完整的字或者字的一部分。

返回图12中的流程图，块1201表示存储器抽象可以在字级简化之前执行，如上所述。在文中描述的示例中，没有讨论读节点和写节点。然而，这种处理对于它们的扩展是直接的，下面将要描述。

接下来，分析多个节点，以从控制逻辑分离数据路径节点，并将数据路径节点分割成一致处理的分段尺寸(块1202)。分析电路的分段后的数据路径部分，以寻找用于所有字级节点和分段节点的减小的安全尺寸(块1203)。使用减小的安全尺寸产生更小的最终网表，该减小的安全尺寸可以在模型检查算法中通过标准门级简化进行分析(块1204)。分析最终的网表以确定例如电路设计是否满足由电路验证工具指定的安全属性(块1205)。

图13示出了作为有向非循环图实现的网表，其中顶层节点包括表示电路输出(o0)的字级(和/或位级)节点和下一状态变量(s0’)，其中底层节点包括表示输入(i0，i1，i2)的字级(和/或位级)节点、初始状态变量(s0)和二进制常向量(111111111，111，000)，其中内部节点包括表示运算符(n1-n9)的字级(和/或位级)节点。在图13中，示出的与节点指示符相邻的上标表示节点的宽度，其中所述宽度对应于位的数量。在初始化期间使用初始化向量000000000⁹来设定s0⁹的初始状态，并且所关注的属性是输出o0¹总为真。电路通过连接三个部分生成状态变量s0的下一状态s0’。最低部分是新的输入值i0，但是只有当其不等于111时(否则它切换为000)。另外两个分段是保持s0的当前2个较低级分段(0..2)和(3..5)，或者利用s 0的较高级分段(6..9)在s0的较低级分段(0..2)中交换的结果，取决于两个外部控制的输入i1和i2的值。因此，由于输出从不为假，所以系统是安全的。图表中的每个节点具有关联信号宽度k。在本描述中，节点注释有上标以表示信号宽度。

可以看到，通过将所有的变量拆分成单个位段，并且根据布尔的单个位逻辑实现内部节点，可以将图13示出的结构或者类似的数据结构中表示的电路设计“按位拆分(bitblasted)”成等效的位级网表。这将产生如下网表，其中所有的信号都具有宽度1，并且内部节点为布尔运算符。为了提供文中所述的简化的字级网表，通过以深度优先方式遍历图表，标识一致处理的数据路径节点的分段，并且相应地对这些节点分段，由此执行选择性的按位拆分。所有其它的运算符被转译成位级构造。这样，标识了分段节点的减小的安全尺寸，并且使用分段节点的减小的安全尺寸以及位级构造生成了更新网表。

执行这种分析的技术包括利用如下信息注释图表中的每个节点，该信息是关于该节点的哪些分段被视为字级包，也就是，一致性处理的数据单元。这种类型的分析用以简化公式，而不是这里描述的顺序系统，如在2002年的zu Kiel上的Christian-Albrechts-Universit中作者为P.Johannesen的“Speedingup hardware verification by automated datapath scaling”的博士论文所述，其全部内容并入本文作为参考。

图14示出了在执行所述处理的数据处理机中使用的简化的数据组织，其包括：输入数据结构1400，其中电路设计由布置为有向非循环图的多个节点表示；分区表1401，包括标识节点中的分区的分段信息；用于分区表1401中分段的依赖组的表1402；以及简化的数据结构1403，提供为所述处理的输出。分区表1401保持每个节点上分成位分段的分区。对于每个节点的每个位分段，在表1402中保持依赖级别，包括依赖于分段或者分段依赖的节点的分段，并且处理简化的数据结构1403作为文中描述的进程的结果。

使用依赖组和间隔上的操作处理数据结构，包括registerNode(n)、split(n，j)、mkCompatible(n1，n2，...)、bitblast(n)和MergeDepGps(n1，n1，...)。

创建运算符registerNode(n)添加在分区表中具有分段(0，...k-1)的节点n，并且构造包含分段(0...k-1)的单个依赖组，假设该节点具有k位。

精化运算符split(n，j)、mkCompatible(n1，n2，...)和bitblast(n)执行以下功能：

1.split(n，j)：这个运算符用于为包括位j的节点n寻找分段依赖组。如果位j落在分段间隔i...k内，其中i＜j＜k，则依赖组被拆分成两个新组，其中第一组包含每个分段的前j-i位，另一组包含每个分段的剩余位。

图15示出了在位置1上组1500的拆分操作的结果。因此，依赖组1500包括三个具有3位宽度的分段：Sig0(0..2)，Sig1(0..2)，Sig2(12..14)。在拆分(Sig0，1)之后，依赖组1501和1502产生，其中依赖组1501包括三个具有2位宽度的分段：Sig0(0..1)，Sig1(0..1)，Sig2(12..13)；依赖组1502包括三个具有1位宽度的分段：Sig0(2..2)，Sig1(2..2)，Sig2(14..14)。通过使用拆分来在目标节点中所有在第一节点有切割的位置上引入切割，由此可以将第一节点的分段传递到目标节点。

2.mkCompatible(n1，n2，...)：该运算符将拆分运算符应用到其操作数，直到它们的分割匹配。图16示出了mkCompatible(s1，s2)的结果，其中在操作节点s1包括两个分段(包括一个单个位的分段0..0和一个31位的分段1..31)之前，同时节点s2包括两个分段(包括一个两位的分段32..33和一个30位的分段34..63)。为了分割匹配，节点s1中的31位分段必须在位置1处被拆分，节点s2中的两位分段必须在位置1处被拆分，从而形成图中示出的匹配分割，包括节点s1和s2中的三个分段，包括两个单个位的分段和一个30位的分段。在一组节点上完成制造可兼容操作mkCompatible(n1，n2，...)之后，在该组中的节点的分割与该组中所有其它节点的分割一致，因为一个节点中所有的切割也将存在于所有其它节点中。

3.bitblast(n)：该运算符将拆分运算符应用到节点n，直到其被分割成单个位的片段。

合并运算符MergeDepGps(n1，n1，...)采用分割匹配的多个节点，这些节点具有相同数量的分段。合并运算符通过针对其操作数的所有第一分段合并依赖组，针对其操作数的所有第二分段合并依赖组，等等，直到形成k个新的依赖组，由此生成k个新的依赖组。图17示出了节点Sig0和Sig1的合并依赖组操作，其中每个节点具有一个3位的分段(1700，1701)和一个29位的分段(1702，1703)。作为运算符的结果，创建了两个新的依赖级别(1704，1705)，其包含来自节点Sig0和Sig1的分段。

图18-22示出了用于遍历输入数据结构以生成文中所述的简化网表的处理。通过以深度优先递归方式遍历数据结构中的节点执行数据流分析，该数据结构优选具有上文提到的有向非循环图的形式，其中在该深度优先递归方式中，使用registerNode运算符注册遇到的每个节点并且然后进行处理(块1800)。

如果节点是一个常量(块1801)，则拆分运算符用于将节点划分成其形式为00...0和11...1连续位的最大分段(块1802)。因此，具有六个位置0-5的常量000100将会被拆分成分段(0，1)，(2，2)和(3，5)。也可以将其它技术应用于常量，只要不将常量的数量通过依赖组限制为2，包括对于每个依赖组的特定处理，或者对于依赖组的选择类型。文中描述的将常量限制为2的技术是简单且快速的，但是不会产生最佳分段。

如果节点是变量(块1803)，则什么也不做(块1804)。

如果节点是形式为node1等于NOT node2的“not”运算符(块1805)，则在node1和node2上应用bit blast运算符，并且然后应用合并依赖组运算符(块1806)。

如果节点是形式为node1等于AND(node2，node3)的“and”运算符(块1807)，则在node1，node2，node3上应用bit blast运算符，并且然后应用合并依赖组运算符(块1808)。

如果节点是形式为node1等于ARITHOP(node2，node3)的算术运算符(块1809)，则在node1，node2，node3上应用bit blast运算符，并且然后应用合并依赖组运算符(块1810)。

进行到图19，如果节点是形式为node1等于compOp(node2 and node 3)的比较器运算符，则操作依赖于运算符的类型(块1811)。如果运算符是“等于”或“不等于”运算符中的一个(块1812)，则在node1和node2上应用制造可兼容运算符(make compatible operator)，并且然后应用合并依赖组运算符(块1813)。如果运算符是“小于”、“小于或等于”、“大于或等于”和“大于”运算符中的一个(块1814)，则在node1和node2上应用bit blast运算符，并且然后应用合并依赖组运算符(块1815)。

如果运算符是形式为node1等于MUX(selector，node2，node3)的多路复用器运算符(块1816)，则在node1，node2和node3上应用制造可兼容运算符，并且然后应用合并依赖组运算符(块1817)。

如果运算符是形式为node1^k等于EXTRACT(x，node2^m)的提取运算符(块1818)，如果x+k小于node2的宽度m，则使用拆分运算符在位位置x以及位位置x+k上引入切割，其中k是node1的宽度。然后将位位置x和位位置x+k以及node2之间的区域中的所有分段切割传递到node1。然后对node1和node2应用合并依赖组运算符(块1819)。

进行到图20，如果运算符是形式为node1等于concat(node2ⁱ，node3^j...)的串接运算符(块1820)，则对node1进行分段以匹配操作数边界(也就是位置i，位置i+j等等)，并且将操作数中的所有内部分段切割传递到node1中的相应点。然后对node1和node2应用合并依赖组运算符(块1821)。

例如，考虑图13中的验证问题。假设通过首先访问s0遍历网表。这就产生了在单个依赖组中的分区信息s0：(0..8)。在访问节点n3，n4，n5，i1，n2，i2和n1之后，具有新的分段s0：(0..2)，(3..5)，(6..8)。s0：(0..2)的依赖组现在包含其它元件n1：(0..2)，n2：(0..2)，n3：(0..2)，n4：(0..2)，n5：(0..2)，s0：(3..5)和s0：(6..8)。

接下来，确定输入数据结构中所有节点是否已被处理(块1822)。如果没有，该进程对于新的节点返回到块1801(块1823)。如果它们已被全部处理过，则遍历所有的当前状态和下一状态变量对(node1，node1’)(块1824)。首先，对于每个对应用制造可兼容运算符，并且对于每个对应用合并依赖组运算符(块1825)。最后，使用拆分运算符以确保每个当前状态节点的分段与其初始状态向量的分段一致，当开始仿真时使用该初始状态向量设定当前状态节点的值，并且该初始状态向量作为如常量的约束进行分段，参考块1801所描述的(块1826)。

在执行了数据流分析后，将产生对于每个节点的分段信息，确保：(1)当前和下一状态变量的分段一致，(2)当前状态变量和初始状态变量的分段一致，并且(3)大于网表DAG之一的尺寸的分段源将只通过多路复用器网络传送或者使用运算符{等于，不等于}比较。

进行到图21，在该处理中的这个阶段，算法访问每个依赖组，并通过应用调整尺寸的公式对组中的分段计算新的减小的尺寸，这确保了保存节点的所有属性。节点被调整尺寸为节点的调整尺寸的分段之和(块1827)。在步骤1827中使用的调整尺寸的公式可以解释如下。选择性按位拆分的网表现在具有两个组件：(1)字级组件，其从输入和字级寄存器读取包，使用多路复用器将它们四处移动，并且执行包比较，以及(2)位级组件，其从输入读取位级信号，控制多路复用器(可能基于来自比较运算符的输出)，并计算位级输出。由于字级变量仅仅被针对等式和不等式进行比较并且四处移动，所以它们可以被抽象以提供减小的宽度。

在1995年的论文中，Hojati和Brayton引入了他们称为“DataComparison Controller(DCC)”的对设计的简化(R.Hojati和R.Brayton.Automatic datapath abstraction in hardware systems，1995年，Computer Aided Verification会议纪录)。这些设计被划分成布尔部分和数据路径部分，通过将它们四处移动和比较它们来操作被建模为整数的无限包，如文中描述的处理的选择性按位拆分设计。在Hojati和Brayton的论文中示出对于每个DCC，总是存在可以保存设计属性状态的有限的最小包的尺寸。实际上，如果系统具有N个无限的整数变量以及M个整数常量节点，则可以使用长度S_min＝[log₂(N+M)]位向量来安全地对这些整数建模。

这个结果在这里不能直接应用，有两个不同的原因：(1)选择性按位拆分的包不具有无限初始尺寸；以及(2)存在多于一个的包尺寸。然而，只要特定节点的初始包尺寸大于某些确定的最小包尺寸，只要调整尺寸的节点至少与初始包尺寸和最小包尺寸中的最小值一样大，节点的属性就将保持。对于每个依赖组都确定一个减小的安全尺寸，其具有大于1的初始宽度。如果依赖组包括n个常量以及m个输入和变量片段，则减小的安全尺寸定义为：min(w_i，log₂(n+m))。而且应注意到，由于在上述示例性进程中对常量的划分，每个依赖组都可以具有最多一个“全0”常量和一个“全1”常量，如上所述。所以在这个示例中，M(特定长度的常量的数量)总是小于或等于2。当然，可以使用处理常量的其它技术，其中存在多于两个的如上所述的可能常量。

在选择性按位拆分之后，得到的网表没有能力将尺寸为N的字级分段转换成一些其它尺寸的分段。不同宽度的分段因此不能比较或者在相同的字级寄存器片段中注册。转换的设计因此是通用的DCC，具有一个位级组件和有限数量的独立的字级组件，该字级组件仅仅使用位级信号彼此通信。通过在Hojati和Brayton中迭代变元，可以看到，这些字级组件中的每一个都可以单独抽象。因此，可以如下计算减小的安全尺寸：

对于特定依赖组中的节点中尺寸为S的每个分段，在依赖组中存在数量为N_S的状态变量和尺寸为S的输入分段。如果尺寸S被调整为具有新的尺寸min(S，log₂(N_S+2)，则就保持选择性按位拆分的网表的所有属性。这样会产生一个减小的安全宽度。而且，可以应用其它公式或处理来寻找最小安全尺寸，包括对由每个依赖组表示的电路的更严格评估以寻找最小安全尺寸，该最小安全尺寸可以小于上述技术所寻找的尺寸。

当所有字级状态变量和常量被定义尺寸后，通过重写选择性按位拆分设计的字级组件以使用新的正确尺寸的变量和常量，并调整内部运算符的宽度，来计算抽象的网表。所以，回到图21，该进程进到生成一个修改的字级网表(块1850)，通过将原网表中的每个节点转换到新节点列表中，包括每个分段一个节点。

通过遍历节点，确定节点类型，然后执行下面所述的适当的操作，就可以生成修改的网表。如果节点是具有n个分段的变量或常量节点(块1828)，则生成具有相同节点类型的n个节点的列表，其尺寸与为分段的依赖组指定的尺寸相应(块1829)。

如果节点是“not”和“and”算术运算符以及比较运算符“小于”、“小于或等于”、“大于”、“大于或等于”中的一个(块1830)，则之前的处理将产生单个位的分割(按位拆分)。因此就其输入而言，对应于运算符的位级实现返回得到的信号列表(块1831)。

如果节点是形式为node1等于CompOp(node2，node3)的比较器运算符(块1832)，并且该运算符是“等于”或者“不等于”类型中的一个，则node1作为基于相应分段的等式的布尔网络实现(块1833)。

如果节点是形式为node1等于MUX(selector，node2，node3)的多路复用器运算符(块1834)，则多路复用器列表由形式mux(selector，x，y)产生，其中每个多路复用器采用node2和node3的相应分段x，y(块1835)。例如，假设形式为mux³²(n1¹，n2³²，n3³²)的32位宽的多路复用器节点被分割成一个8位宽的分段以及一个16位宽的分段(0...7)，(8...31)，重新实现n1¹的结果是[m1¹]，重新实现n2³²和n3³²的结果分别是[m2²⁴，m3⁸]和[m4²⁴，m5⁸]。然后返回一个24位宽的多路复用器和一个8位宽的多路复用器如下：[mux²⁴(m1¹，m2²⁴，m4²⁴)，mux⁸(m1¹，m3⁸，m5⁸)]。

继续到图22，如果节点是形式为node1等于extract(x，node2)的提取运算符(块1836)，则针对node2的分段生成新的节点表(块1837)。图23示出了形式为Sig2³＝extract(x，Sig1)的提取操作的示例，其中Sig1是一个8位节点，其是具有节点Sig0的依赖组2300的成员。提取运算符是一个三位宽的操作，其可以通过在Sig1中的位置x处开始提取三位来生成一个三位宽节点Sig22301。节点Sig1和Sig0被分成在位置x处开始的第一组3位分段，其成为依赖组2302的成员，而输出节点Sig2被分成在位位置0上的单个位分段，其成为依赖组2303的成员，并且被分成在位位置4上开始的第二组3位分段，其成为依赖组2304的成员。

如果节点是形式为node1等于concat(node2，node3，...)的串接运算符(块1838)，则针对操作数生成新节点列表的串接(也就是，从对(node2，node3...)的处理得到的节点)(块1839)。

下面，确定是否数据结构中所有节点都被处理过(块1840)。如果没有，则该进程针对新的节点返回到块1828(块1841)。

如果它们都被处理过，则为了生成最后的分段数据结构，在有向非循环图的顶部，在馈送图表顶部的每个新的简化节点，提供一个新的下一状态变量或者输出(块1842)。作为这个处理的结果，生成选择性按位拆分的网表(块1843)。选择性按位拆分的网表包括在具有位宽为1的信号上操作的节点，其中该信号是使用标准布尔逻辑处理的位级信号。另外，选择性按位拆分的网表包括在具有位宽大于1的信号上操作的字级节点。字级信号通过多路复用器网络中的网表移动，使用比较运算符生成位级信号。而且，设计中的原输出或者状态变量被分为几个部分，其中一些是位级的，一些是字级的。

在针对特定网表的上述技术实现中，在逻辑锥(logic cone)中不共享常量，因为共享常量将不必要地强制从一个锥体到另一个椎体的分段传递。这样，对于常量的每个引用引入新的变量节点。在分析的最后，这些引入的变量节点转换回常量节点。

另外，可以预处理从HDL前端接收的电路表示以提供改善的分析开始点。尤其是，扫描输入网表以检测子图表，其中字被拆分成位级信号，以一致的方式被路由，并且被重新组合成字级信号。这些子图表可以在字级上自动重新实现。

另外，表示为抽象读节点和写节点的符号存储器也可被处理。在这样的情况中，向存储器写入，将数值数据的分段传递到存储器中的所有槽，并且该数值数据成为存储器中所有槽的依赖级的成员。对于读取来说，来自存储器的分段将传递到读节点的输出，并且读节点输出的依赖级将包括所有槽。在向具有特定分段的数据的阵列中写入时，将分段引入到通过写入可存取的每个存储器位置。在读取中，将存储器中槽的分段应用到读节点。

描述旨在于对工业性网表进行无界属性检查的字级模型检查方法。该方法基于两步法，其中快速分析将网表重写入设计中，其中将操作包的字级节点分段与逻辑的其余部分完全分离。然后使用静态计算的安全低边界对所有的包调整尺寸，该安全低边界确保保存检查的属性。可以使用任意标准位级模型检查技术分析得到的系统，或者使用转换验证简化进一步处理所得到的系统。

介绍了一种使用字级网表信息标识可重建模存储器的技术。这种存储器仅使用专用读节点和写节点与它的外界交互，以一种特定方式被初始化，并被一致存取。应用了对包含这种存储器的网表的抽象，其允许验证某一类型的属性，这种验证可以通过推理比标准位级模型检查中需要的数量要小得多的存储器槽和时间实例完成。为了避免不得不依赖来自用户的抽象信息，可以使用驱动抽象精化框架的反例，其分析伪反例来逐渐地精化抽象。

该技术的特征包括：(1)其适合用于安全属性验证的标准的基于变换的验证系统，(2)算法是完全自动的，(3)不需要用户对于抽象输入，(4)可以使用任意位级模型检查器作为抽象精化框架中的决策进程。

尽管通过参考上述优选实施例和详细示例公开了本发明，但应当理解这些示例都是示意性的而非限制性的。可以预期，本领域技术人员可以很容易的对其进行修改和组合，这些修改和组合将在本发明的精神实质内和所附权利要求的范围内。