构造性循环的安全性验证方法

理论计算机科学电子札记88（2004）55-69www.elsevier.com/locate/entcs循环同步电路Koen Claessen1查尔姆斯理工瑞典哥德堡摘要今天最常见的硬件形式验证工具无法处理包含组合回路的电路。然而，在硬件编译、电路综合和电路优化领域，很自然会出现这些循环的子类，即所谓的构造性循环。这些是物理上存在于电路中的回路，但在逻辑上从未被采用。 本文基于命题定理证明和时间归纳法，提出了一种含构造性组合回路的电路安全性验证方法.它既可以用来证明电路的构造性，也可以直接证明电路的安全性。与以前提出的方法不同，不需要固定点迭代，我们不必计算可达状态，也不必计算电路的无环表示1介绍在硬件编译、电路综合和电路优化等领域中，经常会出现含有组合回路的同步电路。一个例子是同步语言Esterel，它可以直接编译成可能包含循环逻辑的硬件电路[10]。在没有循环逻辑的情况下实现相同的功能通常意味着电路大小的爆炸。然而，今天最常见的电路分析和验证工具拒绝在同步硬件中使用组合循环。这使得1电子邮件：koen@cs.chalmers.se1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.05.00456K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-1010）F）））1 ）y））0）S sFig. 1. 一种构造性循环回路很难使用标准工具来正式验证所生成的循环电路的属性。然而，通常所产生的循环是所谓的假循环，在这个意义上，它们在电气地实现和运行电路时并不真正引起问题[7]中的一个例子（如图1所示）由一个循环电路和两个组合子电路F和G组成。电路根据选择信号计算y=G（F（x））或y=F（G（xS.该电路仅使用F和G的一个副本，因此包含一个组合循环。然而，在输出y总是定义良好的意义上，循环是假的。对于一个给定的循环回路，需要对回路进行单独的分析，以证明所有存在的循环都是假的，或者用[10]的术语来说，回路是构造性的。1994年，Malik提出了一种组合电路的分析方法[7]，Shiple等人对此进行了扩展能够处理时序电路[10]。他们的分析产生了一个新的电路，它在功能上等同于原始电路，但不包含任何循环。这个新电路可以通过其他形式验证工具进行分析，以检查电路的形式属性。上述分析均基于BDD [3]。这具有的缺点是，难以使用BDD来表示的电路难以使用该方法来处理，因为该方法固有地依赖于计算表示电路实现的功能的BDD。此外，分析涉及BDD的固定点计算，这可能会引入额外的成本。1999年，Namjoshi等人提出了一种不需要固定点迭代的电路分析方法[8]。然而，他们的方法只适用于组合电路，为了使该方法适用于时序电路，他们采用了与[10]中类似的方法;使用）GXK. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-57来计算系统中的可达状态本文的主要贡献如下。我们提出了一个健全的和完整的自动分析方法，电路包含组合回路，不涉及不动点迭代，计算可达状态，或计算一个新的无环电路，证明了电路的构造性我们使用[8]中的基本思想，但我们使用命题定理证明器（有时称为SAT求解器）而不是决策图。然后，我们使用时间归纳[9]将该方法扩展到时序电路。如上所述，该方法不计算非循环等效电路。相反，人们可以直接使用该方法来证明电路的可能安全特性。本文的其余部分组织如下。前三节可以看作是关于这个主题的教程，介绍背景材料，其中大部分在其他地方也有介绍;在第2节中，我们介绍了电路的定义，以及它们的朴素经典语义是什么;在第3节中，我们展示了如何使用命题定理证明器在经典语义下验证这些电路的安全属性;在第4节中，我们介绍了电路的构造性语义，它更接近于电路中发生的事情我们的主要结果在第5节中给出，在那里我们展示了如何在构造性语义下证明循环电路的安全性。最后，在第6节中，我们讨论了相关的工作，并得出结论。2电路的经典语义在本节中，我们将介绍本文中使用的组合电路和时序电路模型我们严格遵循[1]中的术语。组合电路 布尔公式由变量x、y、z和运算符0、1（空值）、<$（一元值）和、（二进制值）组成。定义写为x=f，由布尔变量x和公式F.组合电路是一个有限的定义集C，使得对于每个变量x，C中至多有一个形式为x=f的定义。对多个定义的限制被添加，因为我们不想谈论包含由多个信号驱动的点的电路电路C的变量x称为输入，如果没有定义58K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-C中的x=f形式。组合电路的解是一个赋值，即将所有变量赋值为布尔值0或1，从而满足所有定义，使用布尔运算符的通常解释时序电路延迟定义写为x：=y，由两个变量x和y组成。时序电路（C，D）是一对组合电路C和一组有限的延迟定义D。同样，我们应用这样的限制：对于每个变量x，C中至多有一个形式x=f的定义，或者D中至多有一个形式x：=y的延迟定义。 一个变量x被称为（C，D）的输入，如果在C中没有x=f形式的定义，在D中没有x：=y形式的延迟定义。为了帮助定义时序电路的语义，我们定义了以下重命名操作。设i≥1为自然数。对于一个组合电路C，我们写C[i]作为C的拷贝，每个变量x都被一个新的变量xi替换。对于一组延迟定义D，我们写D [i]对于组合电路{x i= y i−1|x：= y∈D}。 电路的初始状态通过定义D0为组合电路{y0= 0|x：= y∈D}。最后，对于变量x上的赋值s，我们将标号变量xi上的赋值写成s[i]，其中，s[i]（xi）=s（x）。对于一个给定的时序电路（C，D），我们定义组合展开式（C，D）[k]为组合电路：Ki=1C[i]D[i]一系列估值（s1，.，sk）称为时序电路（C，D）的解路，若（s1 [1]<$s2[2]<$··<$sk [k]）是组合电路D0<$（C，D）[k]的解.3证明安全属性在本节中，我们将展示如何自动证明组合和时序电路的安全属性安全属性。在本文中，安全属性是电路中的一个特定变量p，它应该在电路的所有可能场景中始终为真。我们说，对于给定的组合电路，K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-59C的所有解s，若s（p）=1，则安全性p成立.如果我们希望安全性是一个更复杂的性质，而不仅仅是一个变量，即公式f，我们可以简单地将p=f作为定义添加到C。在本文的其余部分，我们有时会含蓄地这样做对于一个时序电路（C，D），我们说一个安全性质p是有效的，如果对所有k，对所有解路径（s1，.，sk），且对所有的1 ≤i≤k，si（p）= 1.证明组合性质。为了检查给定的属性p对于给定的组合电路C是否有效，我们可以使用命题逻辑定理证明器，通常称为SAT求解器。有许多这样的定理证明器可用。我们对定理证明器的选择将在第6节中讨论。为了检验安全属性p的有效性，我们只需证明：.x=f∈CΣx=fp众所周知，证明组合安全性质的有效性是一个共NP完全问题。因此，只有已知的最坏情况的指数时间算法可以做到这一点。证明序列属性。接下来，我们展示如何检查安全属性p对于给定的时序电路（C，D）是否有效。在这里，我们使用时间归纳的方法，如[9]所述。我们的想法是证明的性质在两个步骤：基本情况下，和归纳步骤。在基本情况下，我们证明了该性质在初始状态下成立。这相当于证明p是组合电路D0<$（C，D）的有效性质[1]。我们可以使用上面的方法来做到这一点。在步骤的情况下，我们证明，如果属性在某个状态下成立，它也将在下一个状态下成立。这对应于证明p1<$p2在组合电路（C，D）中有效[2]。这也可以用上述方法来完成。完成归纳。上 述 的时间归纳法是合理的，但并不完备。这意味着存在有效但不能通过所提出的方法证明的安全属性。特别地，当安全性p非常弱时，将其假设为归纳假设不足以使归纳步骤成为有效公式。为了使时间归纳完备，我们增加了归纳深度的概念，它是一个自然数d。我们修改基本情况，使其60K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-证明了前d个时间步的性质，因此我们可以假设该性质在归纳步骤中对d个步骤成立因此，新的基本情况是证 明 p1···pd 对 电 路 D0 （ C ， D ） [d] 有 效 。 阶 跃 情 形 变 为 证 明p1<$···<$pd<$pd+1对电路（C，D）[d+1]有效。如果某个属性对基本情况有效，但对阶跃情况无效，我们只需增加归纳深度d，然后再试一次。如果基本情况不成立，我们从定理证明器得到一个显示错误的跟踪然而，这个过程可能永远不会终止。当不可达状态空间包含循环时，可能会发生这种情况。为了排除循环并使方法完整，我们可以在步骤情况下添加一个额外的假设，即其中使用的所有状态都是唯一的。 假设这一点是合理的，因为如果存在一条通向p不为真的状态的解路径，那么也存在一条通向由唯一状态组成的状态的解路径因此，我们定义Di（D，i，j）意味着时间实例i和j中的状态是差异：Di（D，i，j）=<$.x：=y∈DΣx i= x j 。然后，新的归纳步骤相当于证明以下公式对电路（C，D）[d+1]有效：.1≤i j≤d+1ΣDi（D，i，j）p1时间归纳的更详细的描述可以在[9，2]中找到，感兴趣的读者可以找到一个合理性和完整性证明，以及几种使时间归纳更强的方法4电路的构造语义在本节中，我们将讨论电路在电气实现时的意义有趣的情况是，电路的组合部分包含一个所谓的循环。周期性。对于给定的组合电路C，以及变量x和y，我们说x直接依赖于y，如果y包含在x的定义的右侧。通过取这个关系的传递闭包，我们得到关系x依赖于y。现在，组合电路C称为循环的，如果存在变量x，K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-61x= x xx=<$xx= x xx=0 x（一）（b）第（1）款（c）第（1）款（d）其他事项图二. 四循环电路x取决于它自己。 一个时序电路（C，D）是循环的，如果C是循环的。电路。我们在数学上定义的电路对应于一个明显的电气实现：逻辑连接符可以实现为相应的逻辑门，具有相同变量名的点对于组合无环电路，我们知道每个输入向量存在唯一解。这也是相应电路计算的解。对于循环电路，经典的语义学过于幼稚。为了说明这一点，在图2中，我们给出了四个循环组合电路的例子。他们都没有任何输入。电路（a）有两个解（x=0和x=1），(b)没有解，并且电路（c）和（d）都恰好有一个解（分别为x=1）。x=0）。然而，对于大多数现有的电路技术，例如使用CMOS晶体管的门的标准实现，只有电路（d）电计算该解决方案。电路（a）、（b）和（c）都导致未驱动的输出。电气语义学为了知道循环回路在几何学上意味着什么，我们必须能够推理出未被驱动的导线。我们通过将迄今为止使用的布尔域{0，1}扩展到三元域来{00，0，1}。 我们称这个值为未定义值，0和1是定义值。为了讨论使用这个新域的电路的解决方案，我们必须将布尔运算符扩展到这些域。事实证明，大多数技术中的电子门的行为如图3所示。我们可以例如，一个与门（ANDGATE）只要它的一个输入为0，即使另一个输入未被定义，它也会产生输出0。还要注意，异或门（XOR）是一个所谓的严格运算符;只要它的一个参数是如果是，则输出也为0如果我们将新的三重域解释为Scott域，并将其最小元素设为n，则图3中的运算符称为相应布尔运算符的并行扩展在本文的剩余部分中，我们使用Scott域的自反序;此外，但是0和1是不可比较的。我们可以很容易地看到，使用都是关于这个排序的单调的排序自然62K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-x<$x0 11 0⊥ ⊥XyX射线X射线X射线X射线000010010111100101111110⊥00⊥⊥⊥0⊥0⊥1⊥⊥1⊥11⊥1⊥⊥1⊥⊥⊥⊥⊥⊥⊥⊥图三. 算子的并行扩张扩展到向量和值序列：（x1，.，xn）≤（y1，.，yn）当且仅当对所有i，xi≤yi。构造性组合电路。 将布尔域扩展到三值域可能会增加组合电路的解的数目。然而，由于我们的操作是单调的，总是存在一个最小的解决方案。这是由塔斯基不动点定理得出的在这篇论文中，还认为，给定一个组合电路，并为电路的所有输入给出定义值，它的电气对应物总是计算斯科特域中的最小解但是，我们不希望电路计算未驱动的值。因此，我们做出如下定义。一个组合电路C被称为构造性的，当且仅当对于所有定义的输入，对应的最小解中的所有值都被定义[10]。我们现在已经确定了以下内容。如果一个电路是构造性的，那么我们知道它的经典语义对应于构造性语义，即电路的电学行为。建设性的顺序电路。同样，我们可以定义什么是构造性时序电路。一个时序电路（C，D）是构造性的，如果对于所有的k和所有长度为k的定义输入序列，长度为k的最小解路径中的所有值都被定义。注意，对于非构造性时序电路，最小解路径构成K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-63泰宁可能不能忠实地反映电路中发生的电学情况。事实上，由于延迟元件得到一个DAC输入时会发生什么是非常不明确的，因此很难对非构造性时序电路中发生的电气情况进行建模。但对于构造性时序电路，我们的模型是准确的。越来越弱这里可以做一个额外的评论：为了使电路产生有意义的结果，我们可能希望削弱构造性的定义 在本文的其余部分，我们假设了构造性的最强定义，但我们也可以很容易地调整方法来处理较弱的定义独特的解决方案。构造性语义是根据最小解来定义的。然而，由于我们使用的域具有特定的形状，我们可以导出一个有用的引理：组合电路C是构造性的，当且仅当对于所有定义的输入，所有解中的所有值都被定义[8]。这个证明来自于这样一个事实：如果所有的解都被定义，那么最小解也被定义。如果定义了最小解，则只能有一个解（因为任何其他定义解的存在将意味着存在包含k的最小解），因此所有解都被定义。我们对时序电路也有类似的引理。一个时序电路（C，D）是构造性的，当且仅当，对于所有的k和所有长度为k的定义输入序列，所有长度为k的解路径中的所有值都被定义。这些引理是有用的，因为它们消除了定点迭代的需要，从而允许我们将构造性条件公式化为电路的安全属性。5循环电路在本节中，我们将展示如何使用构造性语义来检查包含循环的电路的安全属性。安全性和建设性。为了检验一个循环回路的安全性，我们首先要检验这个回路是否是有构造的。例如，由于图2中的电路（b）包含使用经典语义的矛盾，因此可以证明任何安全属性。因此，我们做出如下定义。给定一个电路和一个安全属性p，p是建设性有效的，如果电路是建设性的，并且性质p是a64K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-X01⊥？（x0，x1）（1，0）（0，1）见图4。 域的双轨编码x=y→x0=y0x1= y1x=<$ y→x0= y1x1= y0x= y z→x0=y0<$z0x1= y1<$ z1x= y z→x0= y0<$ z0x1= y1<$ z1x= y z→x0=y1<$z0x= y z→x0=y0<$ z0<$ y1<$ z1x1= y0<$ z1x1= y0<$ z1<$y1<$ z0图五. 组合定义电路的有效安全特性。因此，为了检查安全属性是否有效，我们需要检查电路是否具有构造性。双轨编码。时序电路和组合电路的构造性都可以用公式表示为电路变换版本的经典意义上的安全属性。根据上一节末尾提到的引理，构造性条件几乎已经是一个安全性质。唯一的区别是它是在三元域而不是布尔域上制定的。因此，我们通过为每个三进制变量x引入两个新的布尔变量x0和x1来编码三进制域。这被称为双轨编码。在图4中，我们展示了新变量的值如何对应于x的值。 当x可证明为1时，变量x1为1;当x可证明为0时，变量x0为1。 请注意，我们必须引入一个额外的在域中，它不对应于任何实际值。我们将忽略包含此ghost值的解决方案，因为它不对应于我们模型中的任何内容。K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-65x：=y→x0：=y0x1=<$x0见图6。 延迟定义定义编码。当将每个三进制变量变为两个二进制变量时，我们必须相应地改变电路中的定义。为了做到这一点，我们假设所有的定义只包含浅公式，即。最多包含一个运算符的公式。这总是可以通过引入额外的变量来实现。图5和图6显示了如何将这些定义转换为使用双轨变量。这些定义对应于图3中的表格。运算符的双轨编码的性质是，根据双轨域编码，三元域中定义的解对应于变换后定义的经典请注意，每一个延迟定义都变成了一个延迟定义和一个正常定义。这意味着变换不会增加电路中状态变量的数量。这是正确的，因为我们可以假设电路中延迟元件的输出总是被定义的。然而，这个假设只有在我们真正证明延迟元件的输入总是有定义的情况下才有效。所得电路的经典解对应于原电路的构造解。建设性作为一种安全属性。现在，我们将构造性条件表述为经典的安全属性：对于所有定义的输入，所有解都被定义。这与表明以下属性是变换电路的有效安全属性相同。(We设I是所有输入变量的集合，V是电路中所有变量的集合.- 是的我0我1Σx0x1i∈I x ∈V我们假设输入是定义的，使用xor（i）来确保（i0，i1）是（0，1）或（1，0）。然后，我们检查是否所有的变量都被定义了，使用or（0），检查它们是否不是（0，0）。 我们对其他变量也不使用xor（xor）的原因是，弱性质出现在蕴涵的右侧，而强性质出现在蕴涵的左侧。请注意，此安全属性可用于组合电路和时序电路。因此，为了检查给定的电路是否是建设性的，我们将66K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-电路，并验证上述安全特性适用于转换后的电路。我们可以使用任何形式验证方法，只要它为组合循环提供经典语义就我们的目的而言，第3节中提出的时间归纳方法已经很好地发挥了作用。循环电路的安全性质。作为奖励，我们可以同时做到这两点，而不是首先展示电路的构造性，然后证明所需的安全属性。假设我们对循环回路的安全性p感兴趣，我们可以如上所述变换回路并证明：.i∈IΣ我0我1.x∈VΣx0x1第1章这有一个优点，特别是在做时间归纳证明的时候。归纳证明的成功取决于归纳假设的强度。一般来说，同时归纳证明多个属性实际上可以减少所需的归纳深度。我们已经观察到许多情况下，当同时证明强安全性时，构造性证明所需的6讨论相关工作。正 如 在引言中提到的，与我们的工作最接近的是[ 8 ]中提出的工作。他们的工作和我们的工作之间有两个主要的区别：（1）我们使用命题定理证明器，他们使用决策图;（2）他们计算系统的可达状态，而我们使用时间归纳法。我们在时间归纳方面的经验是，对于足够强的属性，所需的归纳深度非常低，因此该属性变得相对容易证明。构造性是一个非常强的属性，因为它表达了电路中所有在实践中，我们发现我们通常不需要超过1或2的归纳深度，从而导致简单的命题公式。注意，感应深度仅取决于状态的可达性对电路的构造性的影响程度。如果电路在所有状态下都是构造性的，甚至是不可达的状态（或者如果电路是组合的），那么深度为0的归纳总是足够的。BDDs与命题定理证明。B D D 和propo- sitional定理证明方法都有自己的小生境，他们工作得很好。BDD已被用于合理地显示电路的构造性-K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-67过去，我们的工作很成功，但我们相信命题方法更适合这项工作。 我们认为，这是因为许多现代...现代命题定理证明器基于能够以廉价的方式全局传播局部信息的算法这种算法的示例是Stemal-Marck的方法[ 12 ]和使用学习的算法[ 11 ]。在许多情况下，信息的传播是显示构造性所需的全部，因为构造性通常仅取决于电路的控制逻辑的一小部分，并且点的定义很容易传播以解决问题。相比之下，当使用BDD时，通常也必须表示电路中逻辑上不相关的部分。让我们看一下Malik现在，如果x是一个宽的数据路径，相应地F和G是具有大数据路径的复杂函数，任何BDD计算都将有困难，甚至表示F和G。然而，关于电路的构造性的推理根本不受F和G实际实现的内容的影响;只有电路中的循环数取决于F和G的数据路径的大小。在处理这种电路时，例如当F和G是类似乘法器的电路时，使用BDD是根本不可能的。相比之下，尽管大多数SAT求解器在乘数的推理方面也存在问题，但构造性分析仍然只需要通过F和G传播定义性信息，因此理论上可能需要线性时间。然而，在实践中，我们的实验表明，时间复杂度接近二次时间。另一个例子，在我们的一个实验中遇到的，包含一个FIFO缓冲器，它以通常的方式在硬件中实现：一个连接在一个周期中的寄存器序列，以及头部和尾部索引机制。现在，实现查找功能，即在一个时钟周期内查找FIFO中满足某些属性的第一个元素，以最有效的方式，需要组合逻辑中的周期。(This是因为搜索从头部开始，在尾部结束，这是循环结构中的动态索引。）使用BDD表示FIFO对于大型数据路径实际上是不可行的，因为众所周知，BDD在这种情况下会爆炸。然而，组合循环的构造性根本不依赖于数据路径。将数据路径增加到232，我们的分析仍然可以在短短几秒钟内证明建设性。我们自己基于BDD的分析无法构建BDD。总之，我们的主要观点是，基于传播的定理证明方法非常适合解决这类问题。实施.我们在Lava [6]中实现了所提出的分析，68K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-同步硬件描述和验证工作台。将构造性条件公式化为安全属性的优点是，我们可以独立于底层验证方法来实现分析在Lava中，我们刚刚实现了一个电路转换，它执行第5节中描述的转换。 然后，可以使用任何内置的验证方法使用经典语义来执行分析，例如第3节中描述的方法。如前所述，我们最常用的方法是深度递增的归纳法。从那以后，我们在硬件编译框架中广泛使用了该分析[5]。可能的改进。我们没有追求的一种改进的可能性是从结构上研究电路，并且只对强连接的组件进行分析，即。一个循环中所涉及的电路部分在实践中，这将相当于不适用双轨encod，在从输入到电路包含周期的部分导致的路径上，而不是在从周期到寄存器的路径效率改进的另一种可能性是使用在内部使用3值逻辑的SAT求解器。许多SAT算法在内部使用一种结构，这使得它们很容易适应3值世界。局限性和其他未来的工作。所提出的方法的一个局限性是，当使用- 第四个元素T，表示短路，即电路中由0和1驱动的点。 据我们所知，计算构造性的这样的电路需要定点迭代，因为第4节末尾提到的引理对相应的域不成立。[7，10]中基于BDD的方法在这种情况下仍然有效，因为它们能够计算最小不动点。处理T仍然是我们未来工作的一部分。引用[1] G'er a rdBerry. PureE ste re l的核心tru ct ive m an ic。Unfinnissheddraft，availableefromhttp://www.synalp.org，1999年。[2] Per Bjesse和Koen Claessen。基于SAT的验证，无需状态空间遍历。计算机辅助设计，2000年。[3] R. E.布莱恩特基于图的布尔函数操作算法。IEEE Transactions on Computers，35（8），1986.[4] R. E.布莱恩特论布尔函数的VLSI实现和图形表示的复杂性及其在整数乘法中的应用。IEEETransactions on Computers，40（2），1991.K. Claessen / Electronic Notes in Theoretical Computer Science 88（2004）55-69[5] K. Claessen和G. 步伐 一种用于硬件编译的嵌入式语言框架。在设计正确的电路，2002年。[6] K.Claessen 和 M. 谢 利 Lava 教 程 ： 硬 件 描 述 和 验 证 系 统 。 可 查 阅http://www.cs.chalmers.se/，2000年。[7] S.马利克循环组合电路分析。IEEE Transactions on Computer Aided Design of IntegratedCircuits and Systems，13（7），1994年7月。[8] K. S. Namjoshi和R. P. Kurshan循环定义的有效分析。计算机辅助验证。Springer，1999年。[9] 玛丽·舍埃兰，S·塔那姆·辛格，和G·纳·S·塔那阿尔马克。使用感应和SAT解算器，确保安全性。在FMCAD，LNCS 1954中。斯普林格，2000年。[10] T.希普尔湾Berry和H. Touati。循环回路的构造性分析。1996年欧洲设计与测试会议[11] 若昂·马克斯·席尔瓦。GRASP主页。购自http://sat.inesc.pt/http：//www.example.com两千[12] GunnarStAlmarck.ASystemtemforDeteterminingPropositionalLogicTheoremsbyApplyingValues and Rules to Triplets that are Generated from a Formula，1989. 瑞典专利号467 076（1992年批准）、美国专利号5 276 897（1994年）、欧洲专利号0403 454（1995年）。