使用形式技术的设计验证转让专利
申请号 : CN200410097618.0
文献号 : CN1667622B
文献日 : 2010-10-06
发明人 : 卢远
申请人 : 美国博通公司
摘要 :
形式技术可应用于工业设计问题中，例如用于验证一个电路设计。其初始决定包括定义一些属性以验证设计的步骤。其中会生成一个设计的抽象，然后对该抽象进行模型检查。通过性能分析及对顺序操作的验证，使用这些技术所得的结果可以得到扩展。
权利要求 :
1.一种验证电路设计的方法，其特征在于，包括以下步骤：
通过抽象为设计电路生成一个简化模型；
对所述简化模型进行模型检查，并且在所述电路设计不满足至少一个属性时生成一个跟踪记录，根据所述跟踪记录修改设计电路的至少一个属性，将所述被修改的所述至少一个属性应用到所述简化模型；通过使用归纳法将设计的初始状态的属性定义成初始状态的一个超集，将所述超集以矩阵表示以验证所需的属性，以及对所述简化模型进行性能分析，其中包括识别至少一个性能界限，以验证所述电路设计。
2.根据权利要求1所述的验证电路设计的方法，其特征在于，所进行的性能分析中包括修改至少一个属性的步骤。
3.根据权利要求1所述的验证电路设计的方法，其特征在于，所进行的性能分析中包括识别一个最坏案例情况的步骤。
4.根据权利要求1所述的验证电路设计的方法，其特征在于，还包括产生至少一个性能分析结果，并将所述至少一个性能分析结果应用到所述电路设计以验证该电路设计的步骤。
5.一种验证电路设计的方法，其特征在于，包括以下步骤：
通过抽象生成一个电路设计的简化模型；
对所述简化模型进行模型检查，其中包括与设计电路相关的属性，每一个属性用来验证一个独立的寄存器传输滞后函数，并且在所述设计电路不满足至少一个属性时生成一个跟踪记录，根据所述跟踪记录修改设计电路的至少一个属性，并重新验证一个独立的寄存器传输滞后函数，将所述重新验证一个独立的寄存器传输滞后函数应用到所述简化模型；通过使用归纳法将设计的初始状态的属性定义成初始状态的一个超集，将所述超集以矩阵表示以验证所需的属性，以及为电路设计的一个顺序操作产生至少一个模型；以及
将所述至少一个模型应用到所述简化模型，以验证所述电路设计。
6.根据权利要求5所述的验证电路设计的方法，其特征在于，所述产生至少一个模型步骤中，包括定义一套内部状态的步骤，所述内部状态包括定义在一个在先操作之后可能会产生的初始状态及剩余状态。
说明书 :
技术领域
本发明涉及设计验证，更确切地说，涉及形式分析验证技术。
背景技术
电路设计的验证，包括在物理实现该设计(如制成一个集成电路)之前对该电路设计进行测试。通过这种方式，设计错误(即bugs)才可被识别出来，从而可让设计者避免在制作时的损失。
随着电路设计的日趋复杂，要创制一个有效的验证工具也越来越困难。例如，传统的芯片系统中包括相对较大、快速且复杂的集成存储器、芯片内的总线、以及复杂的仲裁器。而且，这些设计通常还包括一些可能相互依存的并行进程。
传统上是用基于仿真的工具来验证设计。这些工具通常是通过对设计的某些一部分随机地施加测试，以验证整个设计。然而，基于仿真的验证理论经常不能发现那些死角(corner-case)错误。所述死角错误的一个例子中包括当一些特定的情况同时出现时才会发生的错误，而这些情况的发生频率相对较低。
为验证电路设计，目前已有多种可用的形式分析技术(形式技术)。形式技术背后的概念就是要彻底地找出设计中的错误。例如，所述形式技术中可包括模型检查、定理证明及符号模拟。
形式技术的应用，包括使用符号模型检查器验证高速缓存相干协议，以及验证普遍使用的设计结构，例如运算电路、流水线、总线仲裁器、以及Tomasulo算法等。最近，形式技术已被用于更广的设计范围。例如，B.Bentley的“验证英特尔奔腾4微处理器”(发表于2001年的设计自动化会议(DesignAutomation Conference)第244-248页)中，讨论了使用形式技术在奔腾4微处理器中发现的100多个“高质量”的逻辑错误。
然而，大多的形式技术不能被有效用于相对较大的工业设计。某些技术被提出来解决这一问题，包括符号算法、SAT程序、以及抽象技术，但是解决这些问题仍存在一个持续的要求。
随着电路设计的日趋复杂，要创制一个有效的验证工具也越来越困难。例如，传统的芯片系统中包括相对较大、快速且复杂的集成存储器、芯片内的总线、以及复杂的仲裁器。而且，这些设计通常还包括一些可能相互依存的并行进程。
传统上是用基于仿真的工具来验证设计。这些工具通常是通过对设计的某些一部分随机地施加测试，以验证整个设计。然而，基于仿真的验证理论经常不能发现那些死角(corner-case)错误。所述死角错误的一个例子中包括当一些特定的情况同时出现时才会发生的错误，而这些情况的发生频率相对较低。
为验证电路设计，目前已有多种可用的形式分析技术(形式技术)。形式技术背后的概念就是要彻底地找出设计中的错误。例如，所述形式技术中可包括模型检查、定理证明及符号模拟。
形式技术的应用，包括使用符号模型检查器验证高速缓存相干协议，以及验证普遍使用的设计结构，例如运算电路、流水线、总线仲裁器、以及Tomasulo算法等。最近，形式技术已被用于更广的设计范围。例如，B.Bentley的“验证英特尔奔腾4微处理器”(发表于2001年的设计自动化会议(DesignAutomation Conference)第244-248页)中，讨论了使用形式技术在奔腾4微处理器中发现的100多个“高质量”的逻辑错误。
然而，大多的形式技术不能被有效用于相对较大的工业设计。某些技术被提出来解决这一问题，包括符号算法、SAT程序、以及抽象技术，但是解决这些问题仍存在一个持续的要求。
发明内容
形式技术被用于验证电路设计等工业设计问题中。这些技术可包括作出验证决定，定义属性以验证一个设计，为所述设计创建一个抽象体和一个模型检查。在一些实施方式中，所述验证还可延伸至性能分析和/或验证顺序操作。
在一些实施方式中，会生成一个设计的抽象体(即简化模型)，并将该抽象体应用于模型检查过程中。例如，基于典型的模型检查，可利用归纳技术避免当环境模型变得更复杂时而产生的状态爆炸。因此，可以更加有效地执行模型检查。
在一些实施方式中，会针对“高质量”的错误提出一个定义，并基于该定义得出分析结果。这样，就可将形式技术的结果与其它验证技术的结果进行比较。
在一些实施方式中，所述验证还涉及到识别性能界限。所述识别性能界限可包括修改属性并将修改后的属性应用到提象体以识别时间界限。单独地通过传统形式技术或仿真方法，是不太可能实现的这种性能分析的。
在一些实施方式中，所述验证还涉及分析顺序操作的设计性能。这种分析包括识别在模型检查过程中会使用的内部寄存器的初始状态及剩余状态。
在一些实施方式中，会用一个符号模型检查器来验证集成电路(即“芯片”)中的电路。符号模型检查器，例如一个Candence SMV，可用来验证一个具有动态属性及较大并行量的电路设计，如千兆以太网芯片中的以太网开关逻辑块。这里，可以对开关块的某些部分进行提象，以减小被验证模型的复杂度。另外，也可用这个方法来验证开关延迟等性能。与现有技术相比，本发明所述的验证技术可用来验证可能具有基本不同的验证问题的网络芯片，如缺少准确规格的网络芯片。
这样，本发明所述的验证技术能提供传统验证技术所得不到的验证结果。例如，本发明教导的方法可实施于一个初始决定，这个初始决定的首要目标是检索设计错误而不是完全地验证整个设计。通过这种方法，相对现有的验证技术而言，可以更快地识别出错误。而且，使用这些技术还可发现传统技术所不能发现的一此错误。
本发明一方面提供一种验证电路设计的方法，包括以下步骤：
为设计电路生成一个简化模型；
对所述简化模型进行模型检查；以及
对所述简化模型进行性能分析，以验证所述电路设计。
优选地，所进行的性能分析中包括修改至少一个属性的步骤。
优选地，所进行的性能分析中包括将所述被修改的至少一个属性应用到所述简化模型的步骤。
优选地，所进行的性能分析中包括识别至少一个性能界限的步骤。
优选地，所进行的性能分析中包括识别至少一个最坏案例情况的步骤。
优选地，本方法包括产生至少一个性能分析结果，并将所述至少一个性能分析结果应用到电路设计中以验证电路设计的步骤。
优选地，本方法还包括识别至少一个与学习操作相关联的界限的步骤。
优选地，本方法还包括识别至少一个与查找操作相关联的界限的步骤。
优选地，本方法还包括识别至少一个与时效操作相关联的界限的步骤。
优选地，所述生成一个简化模型的步骤中包括对电路设计应用归纳法的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减表格尺寸的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减地址长度的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减端口数量的步骤。
优选地，所述生成一个简化模型的步骤中包括忽略顺序操作的步骤。
优选地，所述模型检查步骤中包括生成与设计电路相关的属性的步骤。
优选地，每一个属性用来验证一个独立的RTL函数。
另一方面，本发明还提供一种验证电路设计的方法，包括以下步骤：
生成一个电路设计的简化模型；
对所述简化模型进行模型检查；以及
为电路设计的一个顺序操作产生至少一个模型；以及
将所述至少一个模型应用到所述简化模型，以验证所述电路设计。
优选地，所述生成至少一个模型的步骤中包括定义一套内部状态的步骤其中包括初始状态及剩余状态。
优选地，所述生成至少一个模型的步骤中包括为所述内部状态定义一个子集的步骤。
优选地，所述生成至少一个模型的步骤中包括在内部寄存器中定义所述子集的映射的步骤。
优选地，所述生成至少一个模型的步骤中包括将所述子集应用到所述简化模型的步骤。
优选地，所述顺序操作包括一个请求。
优选地，所述生成一个简化模型的步骤中包括将归纳法应用于电路设计的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减表格尺寸的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减地址长度的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减端口数量的步骤。
优选地，所述生成一个简化模型的步骤中包括忽略顺序操作的步骤。
优选地，所述模型检查步骤中包括生成与设计电路相关的属性的步骤。
优选地，每一个属性用来验证一个独立的RTL函数。
在一些实施方式中，会生成一个设计的抽象体(即简化模型)，并将该抽象体应用于模型检查过程中。例如，基于典型的模型检查，可利用归纳技术避免当环境模型变得更复杂时而产生的状态爆炸。因此，可以更加有效地执行模型检查。
在一些实施方式中，会针对“高质量”的错误提出一个定义，并基于该定义得出分析结果。这样，就可将形式技术的结果与其它验证技术的结果进行比较。
在一些实施方式中，所述验证还涉及到识别性能界限。所述识别性能界限可包括修改属性并将修改后的属性应用到提象体以识别时间界限。单独地通过传统形式技术或仿真方法，是不太可能实现的这种性能分析的。
在一些实施方式中，所述验证还涉及分析顺序操作的设计性能。这种分析包括识别在模型检查过程中会使用的内部寄存器的初始状态及剩余状态。
在一些实施方式中，会用一个符号模型检查器来验证集成电路(即“芯片”)中的电路。符号模型检查器，例如一个Candence SMV，可用来验证一个具有动态属性及较大并行量的电路设计，如千兆以太网芯片中的以太网开关逻辑块。这里，可以对开关块的某些部分进行提象，以减小被验证模型的复杂度。另外，也可用这个方法来验证开关延迟等性能。与现有技术相比，本发明所述的验证技术可用来验证可能具有基本不同的验证问题的网络芯片，如缺少准确规格的网络芯片。
这样，本发明所述的验证技术能提供传统验证技术所得不到的验证结果。例如，本发明教导的方法可实施于一个初始决定，这个初始决定的首要目标是检索设计错误而不是完全地验证整个设计。通过这种方法，相对现有的验证技术而言，可以更快地识别出错误。而且，使用这些技术还可发现传统技术所不能发现的一此错误。
本发明一方面提供一种验证电路设计的方法，包括以下步骤：
为设计电路生成一个简化模型；
对所述简化模型进行模型检查；以及
对所述简化模型进行性能分析，以验证所述电路设计。
优选地，所进行的性能分析中包括修改至少一个属性的步骤。
优选地，所进行的性能分析中包括将所述被修改的至少一个属性应用到所述简化模型的步骤。
优选地，所进行的性能分析中包括识别至少一个性能界限的步骤。
优选地，所进行的性能分析中包括识别至少一个最坏案例情况的步骤。
优选地，本方法包括产生至少一个性能分析结果，并将所述至少一个性能分析结果应用到电路设计中以验证电路设计的步骤。
优选地，本方法还包括识别至少一个与学习操作相关联的界限的步骤。
优选地，本方法还包括识别至少一个与查找操作相关联的界限的步骤。
优选地，本方法还包括识别至少一个与时效操作相关联的界限的步骤。
优选地，所述生成一个简化模型的步骤中包括对电路设计应用归纳法的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减表格尺寸的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减地址长度的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减端口数量的步骤。
优选地，所述生成一个简化模型的步骤中包括忽略顺序操作的步骤。
优选地，所述模型检查步骤中包括生成与设计电路相关的属性的步骤。
优选地，每一个属性用来验证一个独立的RTL函数。
另一方面，本发明还提供一种验证电路设计的方法，包括以下步骤：
生成一个电路设计的简化模型；
对所述简化模型进行模型检查；以及
为电路设计的一个顺序操作产生至少一个模型；以及
将所述至少一个模型应用到所述简化模型，以验证所述电路设计。
优选地，所述生成至少一个模型的步骤中包括定义一套内部状态的步骤其中包括初始状态及剩余状态。
优选地，所述生成至少一个模型的步骤中包括为所述内部状态定义一个子集的步骤。
优选地，所述生成至少一个模型的步骤中包括在内部寄存器中定义所述子集的映射的步骤。
优选地，所述生成至少一个模型的步骤中包括将所述子集应用到所述简化模型的步骤。
优选地，所述顺序操作包括一个请求。
优选地，所述生成一个简化模型的步骤中包括将归纳法应用于电路设计的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减表格尺寸的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减地址长度的步骤。
优选地，所述生成一个简化模型的步骤中包括缩减端口数量的步骤。
优选地，所述生成一个简化模型的步骤中包括忽略顺序操作的步骤。
优选地，所述模型检查步骤中包括生成与设计电路相关的属性的步骤。
优选地，每一个属性用来验证一个独立的RTL函数。
附图说明
下面将结合附图和具体实施例对本发明作进一步说明，附图中：
图1是本发明验证操作的一种实施方式的流程图；
图2是本发明性能分析操作的一种实施方式的流程图；
图3是本发明顺序操作分析的一种实施方式的流程图；
图4是一个电路结构的简化框图；
图5是本发明中所激起的错误示意图；
图6是本发明中的错误可见度示意图；
图7是本发明性能分析的简化示意图。
图1是本发明验证操作的一种实施方式的流程图；
图2是本发明性能分析操作的一种实施方式的流程图；
图3是本发明顺序操作分析的一种实施方式的流程图；
图4是一个电路结构的简化框图；
图5是本发明中所激起的错误示意图；
图6是本发明中的错误可见度示意图；
图7是本发明性能分析的简化示意图。
具体实施方式
下次参考示例性实施例对本发明进行详细描述。显然，本发明的实施形式是多种多样的，不能以所揭示的实施方式来限定本发明。因此，以下所描述的特定结构和功能仅作参考，而不能用来限定本发明的范围。
图1为本发明一个实施例中设计验证操作的流程图。该图1所示的实施例中，这些操作被实施于一个电路设计。例如，可用一个寄存器传输滞后(“RTL”)来定义一个电路设计。当然，所述的操作也可用于其它类型的电路设计中。
如图1所示，在步骤102会为电路设计定义一个模型。其中可能包括识别设计的特性及识别会影响验证结论的问题。例如，一个给定设计中可能包括各种需将其特征化以验证该设计的寄存器、表格及逻辑操作。另外，会作出与环境模型有关的决定，以增加验证过程的效率。例如，可能会作出一个只验证并行操作而不验证顺序操作的决定。
在步骤104中，会定义各种属性以验证设计。该过程中包括基于一个广泛的设计知识，定义各种条件下的内部寄存器状态。例如，如果一个电路按需要运行，该电路的设计应可使得在执行了一个给定操作后，寄存器中的值被限定到一个特定范围。如果寄存器内没有所述期望数值，则会在模型检查时产生一个错误条件(及一个相应的“轨迹”)。
在某些实施方式中，可以利用计算树逻辑(“CTL”)规范语言来书写设计规格，从而定义所述属性。在某些实施方式中，会用每一个属性来验证设计的一个不同属性。例如，在一个以RTL定义的设计中，可用每一个属性来验证不同的RTL函数。
某些应用中，要求将属性定义到一个相对较高的等级。这样，这些属性不会完全基于设计而定义。因此，这些属性中不会含有与设计相同的那些错误。
在某些情况下，可能没有一个完整的设计规格。这时，就要求定义尽可能多的属性，以最大可能地验证所述设计。
在步骤106中，会将提象技术应用于模型，以减小模型的尺寸。例如，可以对表格使用归纳法，如果一个验证的属性与表格的子集不符，则这个属性必定与整个表格不符。这样，由于模型检查可在表格的子集中执行而不是在整个表格上执行，因此，在模型检查阶段所要求的操作次数会大大地减少。
通过使用提象而可以减少的设计方面包括：表格的大小，表格中的入口数量，地址的长度，端口数量。可以理解的是，本发明抽象技术不仅局限于上述例子，还可应用于设计不同方面。
这种简化模型可以通过例如对RTL设计重新编码来生成，可使用如ePERL或VPP这样的工具来对RTL设计重新编码。
在步骤108中，对简化模型执行模型检查。所述模型检查中，可执行一个状态横断以验证该设计。通常，不同操作是在不同的时间运行，并顺序按不同的重复度运行，以测试设计的不同方面。
如果该设计不满足某一属性，则模型检查器会生成一个跟踪记录。通过分析这个跟踪记录，可以确认该设计为什么不满足这个属性。
模型检查器的一个例子是Cadence符号模型检查器(“SMV”)。传统的模型检查器中可使用二进制决策图表(“BDD”)或/和可满足性解算器(“SAT”)。
与现有的验证方法相比，使用本发明的简化模型可更快地发现错误。在某些情况下，最好在设计过程中就用本发明的验证技术快速地发现错误，而不是等到最后再完完整地验证整个设计。
如步骤110所示，模型检查的结果被应用于设计电路。例如，一旦发现一个错误，就可修改设计中相应的错误。然后再执行该验证过程。
为进一步提高对设计的验证，还可执行其他步骤。如步骤112所示，还可执行性能分析操作，以确定设计的性能界限。如步骤114所示，还可验证顺序操作。后面将结合附图2和3对步骤112及步骤114作详细的描述。
图2是本发明一个实施例中性能分析操作的流程图。所述性能分析可包括为操作确定一个最坏案例情况。这样，性能分析可以确定某一给定操作必须在其间完成的一个最大的时钟周期。这样的性能分析在设计中有关键性的作用，一个后续操作是否为正确操作取决于前一个操作在后一操作开始前是否完全结束。
如步骤202所示，其中为性能分析定义一个或多个属性。例如，可设计一个属性以在给定的操作完成之前发生一个特定数量的周期。
在下一步(即步骤204)中，将这些属性施加于简化模型。例如，利用一个模型检查器来完成这一操作。
如步骤206所示，该模型检查器会产生一个结果，该结果会表明设计是否满足所述属性。例如，这个结果可以表明设计是否在设计范围内操作。
步骤208，如果没有达到设计范围(如最坏案例情况)，则会修改这些属性，以进一步测试设计范围。例如，参考步骤202中所举的例子，可增加操作能在其间能完成的时钟周期数量。修改完这些属性之后，再次回到步骤204，将其应用到简化模型中，以确定是否达到设计范围。
如果在步骤206确认已达到了设计范围，则模型检查器会产生一个记录，这个记录会被分析以确定是否已到达设计范围。所述信息可用来定义一个设计在一方面或多方面的性能界限。
而且，所述记录可用来确定能达到设计范围的具体条件(如寄存器及变量的状态，被执行的特别操作，等等)。在重新设计电路以提高其性能时，这些信息将会有用。
如步骤210所示，可将这些结果应用于设计中。例如，如果性能界限需要增加，则需要修改设计。
综上所述，当性能分析被施加于简化模型中时，该性能分析会更有效。如果所述简化模型与本发明所讨论的那样正好是一个适当的选择，则其获得的结果可用于整个设计。
图3为本发明一个实施中的顺序操作验证的流程图。如前所述，在某些实施例中，可能会设计这样一个模型，其中不会发生这种顺序操作。图3中所描述的操作可用来改进由该模型所提供的验证。
当验证顺序操作时可能会遇到一个问题，即该顺序操作的初始状态不容易确定。当在先的操作没有将过程中会使用的所有状态设置到一个或多个预先定义的状态时，这个问题就会发生。因此，要有效地测试这种顺序操作，需要模拟出完成在先操作之后的结果中可能的剩余状态。通过这种方法，顺序操作中的操作可以被有效地验证。
通过使用归纳法，设计的初始状态的属性可以被定义成初始状态的一个超集。然后将所述超集以矩阵表示，以验证所需的属性。因此，如步骤302所示，其中为一个顺序操作定义了一套初始状态(设计的内部状态，例如寄存器及变量的值)。其中包括定义在一个在先操作之后可能会产生的初始状态(如复位状态)和剩余状态(如逻辑操作趋于“平静”后的状态)。
如步骤304所示，所述超集是由一系列的子集所定义的。在某些实施方式中，不会去费力搜索具体的超集，而是针对所述子集在多套内部状态(如剩余状态)上的投射作出一个预测。所述的内部状态可能与寄存器的状态有关。
如步骤306所示，用于检查顺序操作的那些属性被应用于所述设计(如使用一个模型检查器)。可以利用前述步骤中确定的初始状态的子集来验证这些属性。
在图4至图7中，描述了将前述技术应用于验证千兆以太网开关的一个例子。本实施例中，在图4示出了这个设计的功能性和微结构。然后会识别影响验证决定的属性特征及直觉观测。然后会定义基本的抽象技术。如图5和图6所示，通过引用两个规格来分析错误质量，可归纳出实验性结果。图7示出了如何提高包括性能分析的模型检查功能。最后，基于以上描述，即可得出验证结论。
图4示出了一个千兆以太网开关400，其中包括一个独立芯片，含有12个千兆以太网(GE)端口402，一个10千兆高速互连(“10G”)404，以及一个CPU界面406。开关400执行开关功能，如以太网开关(第二层，或L2)，IP开关(第三层，或L3)，以在地址分辨逻辑(“ARL”)块中的更高层的开关，其中的一部分被划分为图4中的块408。
在结构层中，每一个接收到数据包的端口(如与GE 402或10G 404相连的端口)会向ARL发送一个请求。ARL逻辑会返回一个基于L2或L3的目的地址的出口端口。L2及L3的功能均使用哈稀表，分别为L2表及L3表。下面举例说明对L2表的验证。
L2表将MAC地址映射至端口。基于它们的目标MAC地址，从千兆端口来的数据包被传至合适的出口端口。以一个MAC地址的形式与一个端口映射的开关信息在硬件中被动态地训练及更新。10千兆端口是一个互连。CPU通过插入或删除入口来修改表格，这此入口可从动态的更新中除去。基于长时间使用、或CPU的请求，可将入口动态地从表格中老化删除(aged out)。
对于每个数据包，ARL最多可执行三个可能的动作：源MAC地址检查、目的MAC地址检查、以及动态训练。如果芯片的运行频率为125MHz，则L2表逻辑应在84个周期为每个千兆端口、或在8个周期内为每个10千兆端口完成这些动作。
L2表的结构为一个如图1中所描述的哈稀表(hash table)410。使用哈稀函数将16K逻辑入口映射至2K存储段，每个存储段有8个入口。这些存储段之间没有先后顺序。同样，在每一个存储段中的各个入口之间也没有先后顺序。在一个存储段内复制入口是严格禁止的。动态修改采用要求一致性的读-改-写(read-modify-write)操作。读及写被退耦。其中，时效的优先权低于查找，因此证明该设计是饥饿案件(starvation cases).
由于其动态特征，L2表逻辑通常比较难验证。首先，其中可能没有高等级的训练规范。训练可能因多种原因而被取消。不知道周期精确级的逻辑状态，就不可能预知训练何时会发生。时效及CPU操作同样有助于动态行为，结果是产生一些使用现有仿真技术很难进行仿真的死角错误。
第二，在仿真时很难识别性能问题。所述设计必须公平、有效地同时处理多个进程，以满足整体及潜在的考虑。与单个数据包关联的多重操作可能在多个周期后被退耦。错误的行为会在其发生了数千个周期之后产生可观察到的效果，或者没有什么效果，这依赖于具体的测试或应用。这些问题导致验证性能的仿真更加困难。
第三，对这个块写入一个检查器可能不太合适。由于其动态特征，检查器可能与RTL一样容易被写入。然而，如果检查器与RTL相似，则很难确保检查器的正确性。
因此，对于这样一个设计，本发明提供了比现有的仿真技术更有效的验证。
为有效地发现设计错误，这里举两个验证决定的例子。第一，在没有完整可得的规格的情况下，可能需定义尽可能多的属性。在这个例子中，每个属性能验证一个不同的RTL函数。
如前所述，所述定义的属性可验证设计的各个方面。例如，为测试L2表中的堆栈位操作，当有效位＝0且训练正在进行时，会验证一个属性，而不应设置堆栈位。如果当前CPU没有运行，则会验证另一个属性，而不应设置堆栈位。
第二，可通过抽象来减小设计尺寸。在这个例子中，L2表逻辑包括大约3000个寄存器及一个16K入口(1M bit)查找表。要用目前工艺水平的模型检查器，去验证这样一个具有复杂属性的大型设计是不太现实的。因此，最好采用更强的抽象技术，即使这会导致一些重要的属性不能被验证。
假设以Kripke结构M＝(S，I，R，L，h)来模拟L2表逻辑，其中，S表示状态的集合，IS表示初始状态的集合，RSXS表示转换关系。L是表格在S上的集合，h：N48→N11是映象函数，其中Ni＝{1…2i}。换句话说，h是将MAC地址映射至L2表索引的哈稀函数。同样，假设L不包括与哈稀函数相关的表。最后，设M↓t为模型M的简化表示，其中函数t是无效的。例如，M↓aging表示简化的L2表模型，其中aging是无效的。
引理1 设i及j为哈希表的两个索引(index)，也就是说，有两个MAC地址a和b，其中，h(a)＝i，h(b)＝j。假设M’↓aging为修改后的L2表模型，这个L2表模型是通过分别交换i及j的两个入口索引得到的。那么，M↓aging与M’↓aging相似。
引理1表明，当aging无效时，L2表中的存储段是完全对称的。这样，只需模拟2个存储段，而不是所有的2048个存储段。此时，各个存储段是相互独立且完全相同的。因此，一个存储段的操作与另一个存储段的操作是相同的。
当aging有效时，因原始的L2表太大而不能有效地进行验证，所以会使用简化的L2表。因此，需修改aging行为使其与简化表格相匹配。然而，这种方法会引入错误积极表现或错误消极表现。这些不需要的表现可通过对设计的正确分析及调试而得以避免。
相似的对称性也可存在于存储段。例如，存储段中的任意两个入口可能是对称的。所以，对于每个存储段只需要模拟两个入口，而不是模拟八个入口。
除了减小表格的尺寸，还可应用两个抽象方法来对简化模型的复杂性作进一步的简化。首先，由于简化的L2表中只有四个入口，所以可以只用2个比特位来表示MAC地址，而不是用48个比特位来表示。这是形式验证的现有技术。其次，即使12千兆网端口不是对称的，其端口的行为仍是相互独立的。这种对称性的缺陷可能是仲裁的一个结果，其中，一个端口的优先权被分配得高于另一个端口。
引理2用M↓porti表示L2表模型，它没有从端口i发送请求，而p为M↓porti的一个ACCTL属性，那么：
根据引理2，如果简化模型M↓porti的一个普通属性在是不正确的，则该属性在原始模型M上会是一个错误。因此，简化模型最多可以合并两千兆网端口而不是12千兆网端口。此时，可准确模拟10千兆网端口及CPU界面。通过采用这个抽象技术，L2表的尺寸可减少到少于150个寄存器。如表1所示。 原始模型 简化模型 #寄存器 2878 ＜150 #存储段 2048 2
原始模型 简化模型 #入口/存储段 8 2 #位/MAC地址 48 2 #千兆网端口 12 2
表1
除了抽象，环境模型同样可被简化。从千兆网端口到L2表的请求每84个周期到达一次。如果对每个端口准确地模拟，则SMV很难完成一个定点运算。在某些应用中，多端口单请求比单端口多请求更能使设计验证的观点被引起注意。因此，每个端口仅有一个单请求被模拟，从而可有效地减少验证时间。
可以使用ePerl来重编码RTL从而完成所述抽象。所述重写的编码可能是可配置的。例如，为验证带有一个千兆网端口、一个10千兆网端口以及老化功能的逻辑，会用ePerl来生成所述模型，同时生成与之相关的属性。如果SMV认为某一属性不正确，这个工具会举出一个相应例子来解释该属性为什么是错误的。
总的来说，验证设计所需定义的属性数量由设计的复杂度所决定。在某些应用中，可能有150-300个属性。每个属性的运行时间通常为15秒至2小时。例如，要对35个不同配置的验证，并使所有的设计变化还原回这35种配置，则需要8个月的时间来完成这一形式验证过程。
本发明所述的验证比现有的仿真技术更为有效。比如，可用一个仿真器在ARL块的界面观察信号。因此，不仅要仿真L2表逻辑的错误行为，还应使这些行为在ARL界面上可被观察到。这会降低仿真器的效率。
要量化被发现的错误的质量，需定义两个规格：错误激励及错误可见度。
第一个规格，错误激励函数(“ES”)，它是输入错误激励的可能性，用于发现在初始状态时开始的错误。例如，假设一个有效的MAC地址A被存储于L2表中的一个特定存储段。MAC地址B的查找ES函数h(B)＝h(A)为1/2048。ES值越低，通过随机仿真而出现该种错误的机会越小。在计算ES时，仅需使用最有可能的已知情形来仿真相应的错误。这样会得到较保守的ES近似值。
一个错误的错误可见度(“EV”)是时间及输入激励的函数。Evtime是将错误行为扩展至测试工作台所需的周期数。Evstim估量将错误由原因扩展至外部可发现的征兆所需的输入激励的可能性。EV＝Evstim/Evtime提供了一种比较错误的相对可发现度的方式。Evstim的计算与ES相似，都是基于一个保守的近似值。比如，假设将错误扩展至ARL界面的周期的最小值为84个周期。同时假设所需的激励包括：
两个相邻的10千兆网端口在存储段i的查找请求，
一个特定千兆网端口在存储段i的查找请求，然后有：
Evstim＝(1/13)2*1/2048*1/13*1/2048＝2.5e-7
及
EV＝Evstim/Evtime＝3.0e-9
这样，由于Evtime为使用最短的记录估算出来的，而Evstim为扩展错误所需激励的上界，就可以适当地估算出EV值。
在图5和图6中，描述了错误激励ES和错误可见度EV的两个例子。在图5和图6中，X轴表示错误的累计数量，而Y轴分别表示ES及EV。Y轴以对数为单位。比如，在图6中，-6表示EV＝10-6。在图5和图6中，Y轴的值越低，错误可被仿真器发现的可能性越小。在图5中，第16个错误比第15个错误更难仿真。而对于仿真器来说，发现第15个错误相对容易些。相反地，如果没有形式方法，要通过随机仿真来发现第16个错误是相当困难的。在图6中，第4个及第5个错误的EV值由于没有直接被扩展至ARL界面，所以没有计算出来。然而，这些错误会降低系统性能。累积的低效性最终会导致一个可发现的错误。要发现这种错误所需的仿真周期数量会大到不允许的范围。因此，具有较低ES及EV的错误被定义为“高质量”的错误。
当使用更积极的抽象时，某些重要的性能问题可能不会被强调。例如，在上面所述的例子中，所有的千兆网端口查找请求及训练应该在84个周期范围内。相应地，可建立一个初始分析，所述设计分别具有47％和21％的查找和训练界限。
对于抽象模型，这些性能要求不会被完全验证。然而，在一个抽象结构中，当逻辑从老化模式转换到正常开关模式时，SMV被用来决定使一个训练被服务得比预期晚很久。如果在这个转换前正好有一个查找请求，则它的训练会发生得更晚些。通过对所有端口人工建构一个相似的方案，可用性能分析来确定训练的性能要求仅满足界限。比如，训练的实际界限可能是3％而不是21％(如图7所示)。
由于在RTL设计中的假定，可能会导致一些潜在的问题。由于要求按特定的顺序及在特定的时间内发生20个以上的行为，用仿真来探测记录可能会存在困难。相反地，以一个SMV记录开始，可利用性能分析来建构一个非正式分析，以提供出独立地通过仿真或形式验证不能得到的验证结果。
如前所述，所述性能分析包括建构一些属性以测试设计范围，执行模型检查及修改属性以确定实际的设计范围。
比如，可能需要定义一些属性以测试查找及训练操作。从SMV记录开始，对界限的初始信息进行分析。查找及训练会在请求周期内被不断推回(如通过修改属性)，直到SMV产生一个记录。
在前述的抽象模型中，仅考虑每个端口的一个请求。也就是不考虑顺序请求。这们，相同端口的相邻请求间的相互作用就不会被模拟或验证。
理论上，如果一个请求已被满足，则相关的状态寄存器会返回复位值。实际上，由于前一个请求的剩余状态可能未被清除，这个理论就有可能不成立。这种情况会对后来的请求产生一些不可预料的行为。在某些实施例中，通过使用初始状态的集合Q来模拟结构的请求以记录所述问题，集合Q包含集合I，即IQ，Q-I建构剩余状态集合模型。L2表可能已经被不精确地模拟。这样，只需考虑L2表外部的寄存器的初始值。这个结果在下面的论点中。
引理1 设M↓req＝(S，I，R↓req，L)为L2表模型，其中每个端口只有一个请求，P为M↓req的ACTL属性。设IQ，QS，且M’↓req＝(S，I，R↓req，L)为使用初始状态集合Q修改后的KRIPKE结构，那么
其中，
理由描述：由一个千兆网端口发出的每两个请求之间，至少有84个周期。这个理论很容易通过每个端口的每一个84周期的归纳性推论而证明。
延伸这个结论的关键是找到状态Q的集合。这是个相对困难的任务。代替于搜索具体的集合Q，可以推算其在寄存器子集上的投射。假设V为寄存器于M↓req的子集。将V分成m个等级：Vi，即且Vi∩Vj＝Φ。设Qi为Q在Vi上的投射。那么，使用有以下请求的模型检查器可推算出Q，
如果不能推算出Qi，或Qi太大，那么使用I在Vi上的映射，表示为Ii。最后，Q’＝Qil x…x Qij x Ikl x…x Ikp可被用作模型检查的初始状态集。用这个近似值，不会总能完全地验证M上的想要的属性。然而，这个扩展可增加验证的可信度。
由上述可知，形式技术可用来验证如复杂的以太网开关表这样的电路。总之，这个处理过程包括，应用积极抽象排除基本逻辑错误。这个技术的有效性可通过一些“高质量”RTL错误证明。然后，基于典型的模型检查，这个技术可正式或非正式地扩展以分析属性。与ad hoc属性仿真相比，这种精确的分析可能超出仿真或形式技术的能力。下一步，当环境模型更复杂时，可以使用一个新的归纳对典型的模型检查进行扩展，以避免状态爆炸。这些技术能以较小的困难应用于许多表格控制的设计。
本发明的不同实施方式可以用各种硬件及软件处理单元来执行。在本发明的某些实施方式中，如控制器、状态机和/或逻辑电路等硬件可使用于本发明的系统架构中。在本发明的某些实施方式中，可在一个或几个处理设备上执行的软件或固件的编码可用来完成一个或多个所述的操作。
另外，本发明所述的技术可应用在各种设计问题中，并不局限于本发明所述的实施方式中。
总之，本发明本涉及一种改进的验证技术。虽然其中对某些示例性的实施方式进行了详细的描述，并画出了相应的附图，但可以理解的是，这些实施例仅起到示例的作用，而不能作为对本发明范围的限制。特别地，应承认本发明所教导的方法可应用到更广泛的系统及处理过程。因此，可对本发明所述的例子及其它实施方式进行各种修改，而不会脱离本发明的范围。根据上述的理解，本发明不仅限于所描述的实施方式，而可延伸至由权利要求所限定的精神及范围内的任何修改。
图1为本发明一个实施例中设计验证操作的流程图。该图1所示的实施例中，这些操作被实施于一个电路设计。例如，可用一个寄存器传输滞后(“RTL”)来定义一个电路设计。当然，所述的操作也可用于其它类型的电路设计中。
如图1所示，在步骤102会为电路设计定义一个模型。其中可能包括识别设计的特性及识别会影响验证结论的问题。例如，一个给定设计中可能包括各种需将其特征化以验证该设计的寄存器、表格及逻辑操作。另外，会作出与环境模型有关的决定，以增加验证过程的效率。例如，可能会作出一个只验证并行操作而不验证顺序操作的决定。
在步骤104中，会定义各种属性以验证设计。该过程中包括基于一个广泛的设计知识，定义各种条件下的内部寄存器状态。例如，如果一个电路按需要运行，该电路的设计应可使得在执行了一个给定操作后，寄存器中的值被限定到一个特定范围。如果寄存器内没有所述期望数值，则会在模型检查时产生一个错误条件(及一个相应的“轨迹”)。
在某些实施方式中，可以利用计算树逻辑(“CTL”)规范语言来书写设计规格，从而定义所述属性。在某些实施方式中，会用每一个属性来验证设计的一个不同属性。例如，在一个以RTL定义的设计中，可用每一个属性来验证不同的RTL函数。
某些应用中，要求将属性定义到一个相对较高的等级。这样，这些属性不会完全基于设计而定义。因此，这些属性中不会含有与设计相同的那些错误。
在某些情况下，可能没有一个完整的设计规格。这时，就要求定义尽可能多的属性，以最大可能地验证所述设计。
在步骤106中，会将提象技术应用于模型，以减小模型的尺寸。例如，可以对表格使用归纳法，如果一个验证的属性与表格的子集不符，则这个属性必定与整个表格不符。这样，由于模型检查可在表格的子集中执行而不是在整个表格上执行，因此，在模型检查阶段所要求的操作次数会大大地减少。
通过使用提象而可以减少的设计方面包括：表格的大小，表格中的入口数量，地址的长度，端口数量。可以理解的是，本发明抽象技术不仅局限于上述例子，还可应用于设计不同方面。
这种简化模型可以通过例如对RTL设计重新编码来生成，可使用如ePERL或VPP这样的工具来对RTL设计重新编码。
在步骤108中，对简化模型执行模型检查。所述模型检查中，可执行一个状态横断以验证该设计。通常，不同操作是在不同的时间运行，并顺序按不同的重复度运行，以测试设计的不同方面。
如果该设计不满足某一属性，则模型检查器会生成一个跟踪记录。通过分析这个跟踪记录，可以确认该设计为什么不满足这个属性。
模型检查器的一个例子是Cadence符号模型检查器(“SMV”)。传统的模型检查器中可使用二进制决策图表(“BDD”)或/和可满足性解算器(“SAT”)。
与现有的验证方法相比，使用本发明的简化模型可更快地发现错误。在某些情况下，最好在设计过程中就用本发明的验证技术快速地发现错误，而不是等到最后再完完整地验证整个设计。
如步骤110所示，模型检查的结果被应用于设计电路。例如，一旦发现一个错误，就可修改设计中相应的错误。然后再执行该验证过程。
为进一步提高对设计的验证，还可执行其他步骤。如步骤112所示，还可执行性能分析操作，以确定设计的性能界限。如步骤114所示，还可验证顺序操作。后面将结合附图2和3对步骤112及步骤114作详细的描述。
图2是本发明一个实施例中性能分析操作的流程图。所述性能分析可包括为操作确定一个最坏案例情况。这样，性能分析可以确定某一给定操作必须在其间完成的一个最大的时钟周期。这样的性能分析在设计中有关键性的作用，一个后续操作是否为正确操作取决于前一个操作在后一操作开始前是否完全结束。
如步骤202所示，其中为性能分析定义一个或多个属性。例如，可设计一个属性以在给定的操作完成之前发生一个特定数量的周期。
在下一步(即步骤204)中，将这些属性施加于简化模型。例如，利用一个模型检查器来完成这一操作。
如步骤206所示，该模型检查器会产生一个结果，该结果会表明设计是否满足所述属性。例如，这个结果可以表明设计是否在设计范围内操作。
步骤208，如果没有达到设计范围(如最坏案例情况)，则会修改这些属性，以进一步测试设计范围。例如，参考步骤202中所举的例子，可增加操作能在其间能完成的时钟周期数量。修改完这些属性之后，再次回到步骤204，将其应用到简化模型中，以确定是否达到设计范围。
如果在步骤206确认已达到了设计范围，则模型检查器会产生一个记录，这个记录会被分析以确定是否已到达设计范围。所述信息可用来定义一个设计在一方面或多方面的性能界限。
而且，所述记录可用来确定能达到设计范围的具体条件(如寄存器及变量的状态，被执行的特别操作，等等)。在重新设计电路以提高其性能时，这些信息将会有用。
如步骤210所示，可将这些结果应用于设计中。例如，如果性能界限需要增加，则需要修改设计。
综上所述，当性能分析被施加于简化模型中时，该性能分析会更有效。如果所述简化模型与本发明所讨论的那样正好是一个适当的选择，则其获得的结果可用于整个设计。
图3为本发明一个实施中的顺序操作验证的流程图。如前所述，在某些实施例中，可能会设计这样一个模型，其中不会发生这种顺序操作。图3中所描述的操作可用来改进由该模型所提供的验证。
当验证顺序操作时可能会遇到一个问题，即该顺序操作的初始状态不容易确定。当在先的操作没有将过程中会使用的所有状态设置到一个或多个预先定义的状态时，这个问题就会发生。因此，要有效地测试这种顺序操作，需要模拟出完成在先操作之后的结果中可能的剩余状态。通过这种方法，顺序操作中的操作可以被有效地验证。
通过使用归纳法，设计的初始状态的属性可以被定义成初始状态的一个超集。然后将所述超集以矩阵表示，以验证所需的属性。因此，如步骤302所示，其中为一个顺序操作定义了一套初始状态(设计的内部状态，例如寄存器及变量的值)。其中包括定义在一个在先操作之后可能会产生的初始状态(如复位状态)和剩余状态(如逻辑操作趋于“平静”后的状态)。
如步骤304所示，所述超集是由一系列的子集所定义的。在某些实施方式中，不会去费力搜索具体的超集，而是针对所述子集在多套内部状态(如剩余状态)上的投射作出一个预测。所述的内部状态可能与寄存器的状态有关。
如步骤306所示，用于检查顺序操作的那些属性被应用于所述设计(如使用一个模型检查器)。可以利用前述步骤中确定的初始状态的子集来验证这些属性。
在图4至图7中，描述了将前述技术应用于验证千兆以太网开关的一个例子。本实施例中，在图4示出了这个设计的功能性和微结构。然后会识别影响验证决定的属性特征及直觉观测。然后会定义基本的抽象技术。如图5和图6所示，通过引用两个规格来分析错误质量，可归纳出实验性结果。图7示出了如何提高包括性能分析的模型检查功能。最后，基于以上描述，即可得出验证结论。
图4示出了一个千兆以太网开关400，其中包括一个独立芯片，含有12个千兆以太网(GE)端口402，一个10千兆高速互连(“10G”)404，以及一个CPU界面406。开关400执行开关功能，如以太网开关(第二层，或L2)，IP开关(第三层，或L3)，以在地址分辨逻辑(“ARL”)块中的更高层的开关，其中的一部分被划分为图4中的块408。
在结构层中，每一个接收到数据包的端口(如与GE 402或10G 404相连的端口)会向ARL发送一个请求。ARL逻辑会返回一个基于L2或L3的目的地址的出口端口。L2及L3的功能均使用哈稀表，分别为L2表及L3表。下面举例说明对L2表的验证。
L2表将MAC地址映射至端口。基于它们的目标MAC地址，从千兆端口来的数据包被传至合适的出口端口。以一个MAC地址的形式与一个端口映射的开关信息在硬件中被动态地训练及更新。10千兆端口是一个互连。CPU通过插入或删除入口来修改表格，这此入口可从动态的更新中除去。基于长时间使用、或CPU的请求，可将入口动态地从表格中老化删除(aged out)。
对于每个数据包，ARL最多可执行三个可能的动作：源MAC地址检查、目的MAC地址检查、以及动态训练。如果芯片的运行频率为125MHz，则L2表逻辑应在84个周期为每个千兆端口、或在8个周期内为每个10千兆端口完成这些动作。
L2表的结构为一个如图1中所描述的哈稀表(hash table)410。使用哈稀函数将16K逻辑入口映射至2K存储段，每个存储段有8个入口。这些存储段之间没有先后顺序。同样，在每一个存储段中的各个入口之间也没有先后顺序。在一个存储段内复制入口是严格禁止的。动态修改采用要求一致性的读-改-写(read-modify-write)操作。读及写被退耦。其中，时效的优先权低于查找，因此证明该设计是饥饿案件(starvation cases).
由于其动态特征，L2表逻辑通常比较难验证。首先，其中可能没有高等级的训练规范。训练可能因多种原因而被取消。不知道周期精确级的逻辑状态，就不可能预知训练何时会发生。时效及CPU操作同样有助于动态行为，结果是产生一些使用现有仿真技术很难进行仿真的死角错误。
第二，在仿真时很难识别性能问题。所述设计必须公平、有效地同时处理多个进程，以满足整体及潜在的考虑。与单个数据包关联的多重操作可能在多个周期后被退耦。错误的行为会在其发生了数千个周期之后产生可观察到的效果，或者没有什么效果，这依赖于具体的测试或应用。这些问题导致验证性能的仿真更加困难。
第三，对这个块写入一个检查器可能不太合适。由于其动态特征，检查器可能与RTL一样容易被写入。然而，如果检查器与RTL相似，则很难确保检查器的正确性。
因此，对于这样一个设计，本发明提供了比现有的仿真技术更有效的验证。
为有效地发现设计错误，这里举两个验证决定的例子。第一，在没有完整可得的规格的情况下，可能需定义尽可能多的属性。在这个例子中，每个属性能验证一个不同的RTL函数。
如前所述，所述定义的属性可验证设计的各个方面。例如，为测试L2表中的堆栈位操作，当有效位＝0且训练正在进行时，会验证一个属性，而不应设置堆栈位。如果当前CPU没有运行，则会验证另一个属性，而不应设置堆栈位。
第二，可通过抽象来减小设计尺寸。在这个例子中，L2表逻辑包括大约3000个寄存器及一个16K入口(1M bit)查找表。要用目前工艺水平的模型检查器，去验证这样一个具有复杂属性的大型设计是不太现实的。因此，最好采用更强的抽象技术，即使这会导致一些重要的属性不能被验证。
假设以Kripke结构M＝(S，I，R，L，h)来模拟L2表逻辑，其中，S表示状态的集合，IS表示初始状态的集合，RSXS表示转换关系。L是表格在S上的集合，h：N48→N11是映象函数，其中Ni＝{1…2i}。换句话说，h是将MAC地址映射至L2表索引的哈稀函数。同样，假设L不包括与哈稀函数相关的表。最后，设M↓t为模型M的简化表示，其中函数t是无效的。例如，M↓aging表示简化的L2表模型，其中aging是无效的。
引理1 设i及j为哈希表的两个索引(index)，也就是说，有两个MAC地址a和b，其中，h(a)＝i，h(b)＝j。假设M’↓aging为修改后的L2表模型，这个L2表模型是通过分别交换i及j的两个入口索引得到的。那么，M↓aging与M’↓aging相似。
引理1表明，当aging无效时，L2表中的存储段是完全对称的。这样，只需模拟2个存储段，而不是所有的2048个存储段。此时，各个存储段是相互独立且完全相同的。因此，一个存储段的操作与另一个存储段的操作是相同的。
当aging有效时，因原始的L2表太大而不能有效地进行验证，所以会使用简化的L2表。因此，需修改aging行为使其与简化表格相匹配。然而，这种方法会引入错误积极表现或错误消极表现。这些不需要的表现可通过对设计的正确分析及调试而得以避免。
相似的对称性也可存在于存储段。例如，存储段中的任意两个入口可能是对称的。所以，对于每个存储段只需要模拟两个入口，而不是模拟八个入口。
除了减小表格的尺寸，还可应用两个抽象方法来对简化模型的复杂性作进一步的简化。首先，由于简化的L2表中只有四个入口，所以可以只用2个比特位来表示MAC地址，而不是用48个比特位来表示。这是形式验证的现有技术。其次，即使12千兆网端口不是对称的，其端口的行为仍是相互独立的。这种对称性的缺陷可能是仲裁的一个结果，其中，一个端口的优先权被分配得高于另一个端口。
引理2用M↓porti表示L2表模型，它没有从端口i发送请求，而p为M↓porti的一个ACCTL属性，那么：
根据引理2，如果简化模型M↓porti的一个普通属性在是不正确的，则该属性在原始模型M上会是一个错误。因此，简化模型最多可以合并两千兆网端口而不是12千兆网端口。此时，可准确模拟10千兆网端口及CPU界面。通过采用这个抽象技术，L2表的尺寸可减少到少于150个寄存器。如表1所示。 原始模型 简化模型 #寄存器 2878 ＜150 #存储段 2048 2
原始模型 简化模型 #入口/存储段 8 2 #位/MAC地址 48 2 #千兆网端口 12 2
表1
除了抽象，环境模型同样可被简化。从千兆网端口到L2表的请求每84个周期到达一次。如果对每个端口准确地模拟，则SMV很难完成一个定点运算。在某些应用中，多端口单请求比单端口多请求更能使设计验证的观点被引起注意。因此，每个端口仅有一个单请求被模拟，从而可有效地减少验证时间。
可以使用ePerl来重编码RTL从而完成所述抽象。所述重写的编码可能是可配置的。例如，为验证带有一个千兆网端口、一个10千兆网端口以及老化功能的逻辑，会用ePerl来生成所述模型，同时生成与之相关的属性。如果SMV认为某一属性不正确，这个工具会举出一个相应例子来解释该属性为什么是错误的。
总的来说，验证设计所需定义的属性数量由设计的复杂度所决定。在某些应用中，可能有150-300个属性。每个属性的运行时间通常为15秒至2小时。例如，要对35个不同配置的验证，并使所有的设计变化还原回这35种配置，则需要8个月的时间来完成这一形式验证过程。
本发明所述的验证比现有的仿真技术更为有效。比如，可用一个仿真器在ARL块的界面观察信号。因此，不仅要仿真L2表逻辑的错误行为，还应使这些行为在ARL界面上可被观察到。这会降低仿真器的效率。
要量化被发现的错误的质量，需定义两个规格：错误激励及错误可见度。
第一个规格，错误激励函数(“ES”)，它是输入错误激励的可能性，用于发现在初始状态时开始的错误。例如，假设一个有效的MAC地址A被存储于L2表中的一个特定存储段。MAC地址B的查找ES函数h(B)＝h(A)为1/2048。ES值越低，通过随机仿真而出现该种错误的机会越小。在计算ES时，仅需使用最有可能的已知情形来仿真相应的错误。这样会得到较保守的ES近似值。
一个错误的错误可见度(“EV”)是时间及输入激励的函数。Evtime是将错误行为扩展至测试工作台所需的周期数。Evstim估量将错误由原因扩展至外部可发现的征兆所需的输入激励的可能性。EV＝Evstim/Evtime提供了一种比较错误的相对可发现度的方式。Evstim的计算与ES相似，都是基于一个保守的近似值。比如，假设将错误扩展至ARL界面的周期的最小值为84个周期。同时假设所需的激励包括：
两个相邻的10千兆网端口在存储段i的查找请求，
一个特定千兆网端口在存储段i的查找请求，然后有：
Evstim＝(1/13)2*1/2048*1/13*1/2048＝2.5e-7
及
EV＝Evstim/Evtime＝3.0e-9
这样，由于Evtime为使用最短的记录估算出来的，而Evstim为扩展错误所需激励的上界，就可以适当地估算出EV值。
在图5和图6中，描述了错误激励ES和错误可见度EV的两个例子。在图5和图6中，X轴表示错误的累计数量，而Y轴分别表示ES及EV。Y轴以对数为单位。比如，在图6中，-6表示EV＝10-6。在图5和图6中，Y轴的值越低，错误可被仿真器发现的可能性越小。在图5中，第16个错误比第15个错误更难仿真。而对于仿真器来说，发现第15个错误相对容易些。相反地，如果没有形式方法，要通过随机仿真来发现第16个错误是相当困难的。在图6中，第4个及第5个错误的EV值由于没有直接被扩展至ARL界面，所以没有计算出来。然而，这些错误会降低系统性能。累积的低效性最终会导致一个可发现的错误。要发现这种错误所需的仿真周期数量会大到不允许的范围。因此，具有较低ES及EV的错误被定义为“高质量”的错误。
当使用更积极的抽象时，某些重要的性能问题可能不会被强调。例如，在上面所述的例子中，所有的千兆网端口查找请求及训练应该在84个周期范围内。相应地，可建立一个初始分析，所述设计分别具有47％和21％的查找和训练界限。
对于抽象模型，这些性能要求不会被完全验证。然而，在一个抽象结构中，当逻辑从老化模式转换到正常开关模式时，SMV被用来决定使一个训练被服务得比预期晚很久。如果在这个转换前正好有一个查找请求，则它的训练会发生得更晚些。通过对所有端口人工建构一个相似的方案，可用性能分析来确定训练的性能要求仅满足界限。比如，训练的实际界限可能是3％而不是21％(如图7所示)。
由于在RTL设计中的假定，可能会导致一些潜在的问题。由于要求按特定的顺序及在特定的时间内发生20个以上的行为，用仿真来探测记录可能会存在困难。相反地，以一个SMV记录开始，可利用性能分析来建构一个非正式分析，以提供出独立地通过仿真或形式验证不能得到的验证结果。
如前所述，所述性能分析包括建构一些属性以测试设计范围，执行模型检查及修改属性以确定实际的设计范围。
比如，可能需要定义一些属性以测试查找及训练操作。从SMV记录开始，对界限的初始信息进行分析。查找及训练会在请求周期内被不断推回(如通过修改属性)，直到SMV产生一个记录。
在前述的抽象模型中，仅考虑每个端口的一个请求。也就是不考虑顺序请求。这们，相同端口的相邻请求间的相互作用就不会被模拟或验证。
理论上，如果一个请求已被满足，则相关的状态寄存器会返回复位值。实际上，由于前一个请求的剩余状态可能未被清除，这个理论就有可能不成立。这种情况会对后来的请求产生一些不可预料的行为。在某些实施例中，通过使用初始状态的集合Q来模拟结构的请求以记录所述问题，集合Q包含集合I，即IQ，Q-I建构剩余状态集合模型。L2表可能已经被不精确地模拟。这样，只需考虑L2表外部的寄存器的初始值。这个结果在下面的论点中。
引理1 设M↓req＝(S，I，R↓req，L)为L2表模型，其中每个端口只有一个请求，P为M↓req的ACTL属性。设IQ，QS，且M’↓req＝(S，I，R↓req，L)为使用初始状态集合Q修改后的KRIPKE结构，那么
其中，
理由描述：由一个千兆网端口发出的每两个请求之间，至少有84个周期。这个理论很容易通过每个端口的每一个84周期的归纳性推论而证明。
延伸这个结论的关键是找到状态Q的集合。这是个相对困难的任务。代替于搜索具体的集合Q，可以推算其在寄存器子集上的投射。假设V为寄存器于M↓req的子集。将V分成m个等级：Vi，即且Vi∩Vj＝Φ。设Qi为Q在Vi上的投射。那么，使用有以下请求的模型检查器可推算出Q，
如果不能推算出Qi，或Qi太大，那么使用I在Vi上的映射，表示为Ii。最后，Q’＝Qil x…x Qij x Ikl x…x Ikp可被用作模型检查的初始状态集。用这个近似值，不会总能完全地验证M上的想要的属性。然而，这个扩展可增加验证的可信度。
由上述可知，形式技术可用来验证如复杂的以太网开关表这样的电路。总之，这个处理过程包括，应用积极抽象排除基本逻辑错误。这个技术的有效性可通过一些“高质量”RTL错误证明。然后，基于典型的模型检查，这个技术可正式或非正式地扩展以分析属性。与ad hoc属性仿真相比，这种精确的分析可能超出仿真或形式技术的能力。下一步，当环境模型更复杂时，可以使用一个新的归纳对典型的模型检查进行扩展，以避免状态爆炸。这些技术能以较小的困难应用于许多表格控制的设计。
本发明的不同实施方式可以用各种硬件及软件处理单元来执行。在本发明的某些实施方式中，如控制器、状态机和/或逻辑电路等硬件可使用于本发明的系统架构中。在本发明的某些实施方式中，可在一个或几个处理设备上执行的软件或固件的编码可用来完成一个或多个所述的操作。
另外，本发明所述的技术可应用在各种设计问题中，并不局限于本发明所述的实施方式中。
总之，本发明本涉及一种改进的验证技术。虽然其中对某些示例性的实施方式进行了详细的描述，并画出了相应的附图，但可以理解的是，这些实施例仅起到示例的作用，而不能作为对本发明范围的限制。特别地，应承认本发明所教导的方法可应用到更广泛的系统及处理过程。因此，可对本发明所述的例子及其它实施方式进行各种修改，而不会脱离本发明的范围。根据上述的理解，本发明不仅限于所描述的实施方式，而可延伸至由权利要求所限定的精神及范围内的任何修改。