高阶逻辑编译器：从递归函数到时钟同步硬件的自动翻译

理论计算机科学电子笔记145（2006）27-43www.elsevier.com/locate/entcs基于高阶逻辑Mike Gordona Juliano Iyodaa Scott Owensb Konrad Slindb剑桥大学计算机实验室，威廉·盖茨大楼，JJ Thomson Avenue，Cambridge CB3 0FD，英国b犹他大学计算机学院，50 South Central Campus Drive，Salt Lake City，Utah UT 84112，USA摘要本文描述了一种自动将高阶逻辑中的递归函数定义翻译成时钟同步硬件的编译器。编译是通过HOL4系统中的机械化证明，并为编译的每个函数生成正确性定理。代表电路的逻辑公式以适合直接翻译为Verilog HDL的形式进行合成，以进行仿真并输入到标准设计自动化工具。编译脚本是开放的，可以安全地修改：合成的电路是正确的结构。 可合成子集 高阶逻辑的定义可以使用额外的基于证明的工具来扩展，这些工具将定义转换为子集。关键词：定理证明，编译，硬件综合1引言我们的目标是直接从高阶逻辑（HOL [5]）中的数学规范合成正确的构造硬件。HOL的“可合成子集”并不是要固定的，而是随着我们的案例研究而增长。编译器当前生成硬件来实现尾递归函数定义。一个例子是迭代累加器式乘法：MultIter（m，n，acc）=ifm= 0 then（0，n，acc）else MultIter（m-1，n，n+acc）由于MultIter（m，n，acc）=（0，n，（m×n）+acc），乘数定义为：Mult（m，n）= SND（SND（MultIter（m，n，0）1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.00328M. Gordon等人/理论计算机科学电子笔记145（2006）27其中SND（SND（x，y，z））的计算结果为z，因此Mult（m，n）= m×n。使用这个乘数，可以通过以下方式定义阶乘函数FACT n =if n = 0 then 1 else Mult（n，FACT（n-1））这(see第4节）可以自动生成一个可合成的定义：FactIter（n，acc）=ifn = 0 then（n，acc）else FactIter（n-1，Mult（n，acc）Fact n = SND（FactIter（n，1））linRec自动证明FACT = Fact。编译器将HOL中定义的函数f转换为设备DEVf，该设备通过四相握手电路对信号load，inp，done和out计算f。这些信号分别是请求线、数据输入总线、确认线和数据输出总线。加载输入干出来的加载完成tt+1tJFig. 1. 握手协议这种握手设备的确切行为在附录中给出的同品种DEV的HOL定义中有详细说明这个规范粗略地说，如果当在load上发出请求时，在inp上输入值v，那么最终f（v）将在out上输出，并且当这种情况发生时，在done上发出信号（图1）。这里通过断言（在时间t+1）load上的值T来发起事务，即load在时间t+1具有正边沿。这使得设备读取输入到inp（在时间t+1）的值，比如v，并将done设置为F。然后，器件对输入变得不敏感，直到T下一次在done上断言，此时计算值f（v）将在out上输出。2将函数表示为回路如果同步电路保证高阶逻辑公式：vf（v）DEVfM. Gordon等人/理论计算机科学电子笔记145（2006）2729DEVf（负载在1000，输入在1000，完成在1000，输出在1000）是真的（附录中有DEV的正式定义）。 信号load、inp、done、out被建模为将时间映射到值的函数，并且at运算符将信号投射到在时钟脉冲的上升沿处出现的值的序列。更准确地说，σ在t处是这样的信号，即对于所有时间t，该信号在时间t处具有信号σ在信号t的第t个上升沿处具有的值。符号时间投射的形式理论在Melham的专著[9]中有详细的介绍（ 在 那 里 它 被 称为 “ 时 间 抽 象 ” ） 。一个实际的电路被表示为一个公式的连接，每个公式代表一个元件实例。内部电线是存在量化的。这是高阶逻辑中硬件的标准建模，并且在Melham的书（同上）中也有详细描述。编译前面给出的MultIter定义的结果是下面的定理：► InfRise==>v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22v23 v24 v25 v26 v27 v28 v29v30 v31 v32 v33 v34 v35 v36 v37 v38 v39 v40 v41 v42v43 v44 v45 v46 v47 v48v49 v50 v51 v52 v53 v54 v55 v56 v57.DtypeT（，load，v21）NOT（v21，v20）与（v20，load，v19）（，done，v18）AND（v19，v18，v17）（v17，v16，v11）Dtype（第15节，第23节）（v23，v22）（v22，v15，v16）多路复用器（v16，v14，inp1，v3）多路复用器（v16，v13，inp2，v2）多路复用器（v16，v12，inp3，v1）codeDtypeT（第11节，第26节）（v26，v25）（v25，v11，v24）多路复用器（v24，v3，v27，v10）CMDtype（，v10，v27）DtypeT（v11，v30）NOT（v30，v29）AND（v29，v11，v28）MUX（v28，v2，v31，v9）Dtype（，v9，v31）DtypeT（第11节，第34节）（v34，v33）（v33，v11，v32）多路复用器（v32，v1，v35，v8）CMDtype（V8，V35）Dtype T（第11节，第39节）（v39，v38）（v38，v11，v37）不要（v37，v7）常量0 v40等式32（v3，v40，v36）双D型（，v36，v6）DtypeT（第7节，第44节）（v44，v43）（v43，v7，v42）（v42，v6，v5）非（v6，v41）（v41，v42，v4）Dtype（V5，V48）NOT（v48，v47）（v47，v5，v46）不要（v46，v0）常量0 v45常量类型（v45，out1）（v2，v9，out2）（v8，out3）（第4版，第53版）（v53，v52）AND（v52，v4，v51）NOT（v51，v15）常量1 v54 SUB32（v10，v54，v50）ADD32（v9，v8，v49）ADDtype（ADD32，v50，v14）ADDtype（ADD32，v9，v13）ADDtype（ADD32，v49，v12）ADDtype（ADD32，v50，v14）D型（V15，V56）与（v15，v56，v55）与（v0，v7，v57）AND（v57，v55，done））==>DEV多线程(load在100，（inp1>inp2>inp3）在100，完成于100，（out1>out2>out3）在100）该定理具有以下形式：► InfRise接口==>电路==>器械规格逻辑公式InfRise断言信号具有无限数量的上升沿。这是时间投影的标准前提条件（同上），并且由于在设备规范中使用at-运算符而需要逻辑公式电路是高阶逻辑中综合电路的标准表示。组件描述见第2节。这种形式的电路是我们生成的最低级别的形式表示30M. Gordon等人/理论计算机科学电子笔记145（2006）27然而，它们很容易转换为HDL，然后模拟或输入到其他工具。我们已经编写了一个逻辑公式设备规范使用上面描述的HOL谓词DEV来指定使用四阶段握手计算MultIter我们的编译器默认使用32位字。因此，MultIter的输入和输出是32位字的三元组，由项inp1>inp2>inp3和out1>out2>out3表示，其中inp1、inp2、inp3、out1、out2、out3是32位字，<>表示字级联。编译器使用来自预定义逻辑的组件生成电路，该逻辑可以更改以对应于目标技术（默认目标是使用Quartus II合成的Altera FPGA）。用于实现MultIter的组件有NOT、AND、OR（逻辑门）、EQ32（32位相等性测试）、MUX（多路复用器）、DtypeT（布尔D型寄存器，上电进入存储值T的初始状态）、Dtype（未指定初始状态的D型寄存器）、CONSTANT（具有预定义值的只读寄存器）、ADD32（32位加法器）和32位SUB32（32位减法器）。这些组件中的每一个都在高阶逻辑中以标准样式定义。例如，NOT的定义为：NOT（inp，out）=0. out（t）=<$inp（t）NOT是所有组合组件的典型（即，可以直接用逻辑门实现而不使用寄存器的组件两个时序元件Dtype和DtypeT是在时钟的正（上升）沿触发的寄存器，它们的定义使用谓词Rise，定义如下：上升s t=<$s（t）<$s（t+1）然后Dtype和DtypeT定义为：Dtype（m，d，q）= mt. q（t +1）= ifRise= tthend telseq tDtype T（q，d，q）=（q0 =T）<$Dtype（q，d，q）这些模型是标准的，在Melham的书中有描述3编译器如何工作编译器在HOL4系统中实现，并且是在Standard ML中的程序，其生成由系统支持的高阶逻辑的版本中的证明编译器用高阶逻辑创建实现函数f的电路M. Gordon等人/理论计算机科学电子笔记145（2006）2731其中f：σ1×···×σm→τ1×···×τn和σ1，.，σm，τ1，.，τn是可以在总线上承载的值的类型（例如，n位字）。编译的起点是HOL中这样一个函数f的的形式：f（x1，.，xn）= e，其中f在e中的任何递归调用必须是尾递归的。在这样的定义上对我们的编译器进行验证（如果需要，使用用户提供的测量函数来帮助证明终止性）将首先在高阶逻辑中定义f（使用TFL [15]），然后证明定理：|- InfRise==>circuit==> DEVf（负载在1000，输入在1000，完成在1000，输出在1000）当输入s为inp 1<>· ··<>inpm时，输出p uts为out1<>· ··<>outn（其中inpi的类型与σi匹配，而out j的类型与τj匹配），并且电路是表示具有输入i、load、inp 1、. . ，inpm和输出完成，out1，.. . ，outn计算f。第一步（步骤1）编译f（x1，. ..定义如下：Seqf1f2=λx. f2（f1x）Parf1f2=λx. （f1x，f2x）itef1f2f3= λx. 如果f1x那么f2x否则f3xRecf1f2f3= λx。 if f1x then f2x else Rec f1f2f3（f3x）编码到由Seq、Par、Ite和Rec构建的应用表达式中是由证明脚本执行的，并且产生定理λ（λ（x1，. ，xn）。 e）= E，因此，f = E。使用的算法很简单，这里不做描述。作为一个例子，证明脚本推导自：► FactIter（n，acc）=ifn= 0then（n，acc）else FactIter（n−1，n×acc）定理：► FactIter=Rec（Seq（Par（λ（n，acc）. n）（λ（n，acc）. 0））（=））（Par（λ（n，acc）. n）（λ（n，acc）. （acc））（Par（Seq（Par（λ（n，acc）. n）（λ（n，acc）. 1））（−））（Seq（Par（λ（n，acc）. n）（λ（n，acc）. acc））（×））第二步（步骤2）用组成握手设备的相应电路构造器SEQ、PAR、ITE和REC替换组合子Seq、Par、Ite和Rec关键32M. Gordon等人/理论计算机科学电子笔记145（2006）27这些构造器的性质是以下定理，这些定理使我们能够组合地推导出形式为λImp= λDEVf的定理，其中Imp是使用电路构造器构造的公式，因此是握手设备。 长箭头符号=表示提升到函数的含义：f =g = load inp done out。 f（load，inp，done，out）f（load，inp，done，out）► DEVf=DEVf► （P1=DEVf1）（P2=DEVf2）SEQP1P2=SEQDEV（Seqf1f2）► （P1=DEVf1）（P2=DEVf2）（PARP1P2=► （P1=DEVf1）（P2=DEVf2）（P3=DEVf3）（ITEP1P2P3=► 共计（f1、f2、f3）（P1=（RECP1P2P3=谓词Total的定义是Total（f1，f2，f3）确保终止。如果E是使用Seq、Par、Ite和Rec建立的表达式，则通过设置谓词变量P1、P2和P3，这些定理使逻辑公式F能够从电路构造器SEQ、PAR、ITE和REC建立，即，Δ F=ΔDEVE 从步骤1中，我们有f=E，因此F=DEVf一个组合函数f可以使用构造器ATM打包成一个握手设备，它创建了一个简单的握手接口并满足精化定理：► ATMf=ΔDEVf电路构造器ATM与附录中的其他构造器一起定义为了避免内部握手的扩散，当从E构造F的证明脚本实现Seqf1f2时，它检查f1是否或f2是组合函数的组合，如果是，则引入PRECEDE或使用以下定理，使用FOLLOW代替SEQ► （P=P0DEVf2）P（PRECEDEf1P=P0DEV（Seqf1f2））► （P=DEVf1）（FOLLOWPf2=DEV（Seqf1f2））PRECEDEfd在将输入发送给d之前用f处理输入，FOLLOWd f用f处理d的输出。定义如下：M. Gordon等人/理论计算机科学电子笔记145（2006）2733PRECEDEfd（load，inp，done，out）=v.COMBf（inp，v）FOLLOWd f（加载，输入，完成，输出）=v. d（load，inp，done，v）COMBf（v1，v2）用f（v1）驱动v 2，即COMBf（v1，v2）=t。v2t=f（v1t）.SEQd1d2在d1和d2的执行之间引入了握手，但是PRECEDEfd和FOLLOWdf分别在d之前或之后“连接用PRECEDE或FOLLOW替换SEQ是“窥视孔”优化的一个示例第二步得到一个定理：F=第三步（步骤3）是用这些定义重写tors（参见附录中的定义），以获得由标准类型的门（AND，OR，NOT和MUX），通用组合组件COMBg（其中g将是表示为HOLλ表达式的函数）和Dtype寄存器构建的电路然后将形式为COMBg（inp，out）的公式转换为仅使用预定义电路库中的元件构建的电路 默认库当前包括布尔函数（例如， 多路复用器，以及对n位字的简单操作（例如+、-和各种移位的等）。 一种特殊用途的证明规则使用递归算法来合成组合电路 举例来说► COMB（λ（m，n）. （m< n， m +1））（输入1<>输入2，输出1<>输出2）=0.0000 COMB（）（inp1<>inp 2，out 1）输出常量1v0COMB（+）（输入1<>v 0，输出 2）其中<>是总线级联，CONSTANT1v 0连续驱动v0为高，并且假定COMB和COMB+是给定的组件（如果没有给定，则可以显式实现它们，但必须在某个地方停止<第3步结束时产生的电路使用非锁定抽象寄存器DEL、DELT和DFF，这些寄存器是为了方便定义ATM、SEQ、PAR、ITE和REC而选择的（见附录）。寄存器DFF很容易用DEL、DELT和一些组合逻辑来定义（细节省略）。第四步（步骤4）引入一个时钟（默认名称为“时钟”），并使用以下定理执行Melham的书[ 9 ]中描述的自动时间投影►InfRise电子邮件q. Dtype（m，d，q）mDEL（datm， q=0）34M. Gordon等人/理论计算机科学电子笔记145（2006）27►InfRise电子邮件q. DtypeT（n，d，q） DELT（dat q= 0）通过实例化步骤3中得到的定理中的load，inp，done和out，分别为loadatn，inpat n，doneat n和outat n，然后使用上述定理以及存在量化和合取关于蕴涵的单调性进行一些推导，我们得到一个定理：|- InfRise中文版==>实现f==>的电路DEVf（负载在1000，输入在1000，完成在1000，输出在1000）4其他工具：linRecHOL的目前这只包括尾部递归函数定义。我们期望通过使用转换为可合成子集的证明工具来编译更高级别的这些工具被设想为作为初步实验，我们正在实现一个工具linRec来将线性递归转换为尾递归。例如，这将使MultIter和FactIter能够从更自然的定义中自动生成Mult（m，n）=ifm= 0 then 0 else m+Mult（m-1，n）事实n =ifn = 0 then 1 else n* 事实（n-1）linRec的原型实现已经存在。它使用以下线性和尾递归递归方案的定义：linRec（x）=if a（x）then b（x）else c（linRec（d x））（e x）tailRec（x，u）=if a（x）then c（b x）u else tailRec（d x，c（ex）u）线性递归与linRec的定义相匹配，以找到a，b，c，d，e的值，然后通过实例化定理将其转换为尾递归A B C D E.WF R（<$（ax）==>R（dx）x）（pqr. cp（cqr）=c（cpq）r）==>你是 谁？c（linRec a b c d e x）u = tailRec a b c d e（x，u）其中WF R意味着R是有根据的。启发式算法用于为R选择合适的见证者。M. Gordon等人/理论计算机科学电子笔记145（2006）27355现状和未来工作这里描述的编译器已经经历了几个版本，现在可以在我们尝试过的所有示例上运行。我们已经编写了一个当我们第一次尝试Verilog模拟时，最初存在困难。我们的形式模型将位表示为布尔（T，F），但Verilog仿真模型是多值的（1，0，x，z等），所以我们的正式模型不能预测寄存器初始化为x的Verilog仿真行为。因此，Verilog仿真生成的是未定义的x值，而不是我们的证明所预测的输出。大多数真实硬件的行为与Verilog仿真不一致，因为在现实中寄存器初始化为一个确定值，对于我们使用的Altera FPGA，该值为0通过使我们的Dtype的Verilog模型将其状态初始化为0，我们能够成功地模拟我们所有的例子。由于我们的证明对任何初始值都是有效的，所以Dtype的Verilog模型是该模型在高阶逻辑中的有效实现。我们对这个问题的调查由于Verilog仿真测试工具中的一个错误而变得复杂：load在done变为T之前被断言，违反了握手协议的前提条件，所以即使在我们理解了初始化问题之后，仿真仍然给出了令人费解的结果。然而，一旦我们修复了测试台，一切都正常工作。我们的所有示例现在都可以在仿真和Altera Excalibur FPGA板上正确执行。如果我们使用标准Verilog模拟器（http://www.icarus.com）模拟输入为 （ 5 ， 7 ， 0 ） 的 MultIter 实 现 ， 并 使 用 波 形 查 看 器（http://home.nc.rr.com/gtkwave）查看结果，结果为：0 s 100 s 145 sMain.Main.完成Main.inp1[31：0]Main.inp2[31：0]Main.inp3[31：0]Main.loadMain.out1[31：0]Main.out2[31：0]Main.out3[31：0]load在时间15被断言;done是T，但是在时间15中立即下降到F。响应负载被断言。在负载被断言时，值5、7和0分别被置于线inp1、inp2和inp3上。在时间135，done再次上升到T，此时out1，out2和out3的值分别为0，7和35，因此Mult32Iter（5， 7， 0）=（ 0， 7， 35），这是正确的。 在不久的将来，我们计划完成一个实质性的例子，正在犹他大学完成，使用我们的编译器来实现广告，000570000771421283536M. Gordon等人/理论计算机科学电子笔记145（2006）27高级加密标准（AES）[12]用于私钥加密的算法这指定了一种基于有限场运算的原始计算的多轮算法从AES的现有形式化开始[16]，我们已经为加密（和解密）轮的主要组件生成了网表和电路。虽然AES的工作还不完整，但我们目前的进展证实了我们的合成方法的可行性AES的形式化包括算法的功能正确性证明：具体来说使用逻辑推理从已证明的规范中推导出硬件，可以向我们保证硬件解密器是硬件解密器的逆许多AES规范不是尾递归的，但形式上推导（和验证）尾递归版本是简单的。为了自动化这些证明，我们开发了linRec工具（第4节）。目前，所有数据细化（例如，从数字或枚举类型到单词）必须通过高阶逻辑中的证明手动完成HOL4系统有一些“布尔化”功能，可以自动将更高级别的数据类型转换为位串，我们希望开发基于这些功能的“第三方”工具，用于我们要研究使用编译器生成测试台监视器，可以运行在并行模拟与设计，不正确的建设。因此，我们的硬件可以作为测试其他实现的这里描述的工作是通过证明创建硬件/软件组合的项目的一部分我们希望研究为ARM处理器创建软件并将其链接到由我们的编译器创建的硬件（可能打包为ARM协处理器）的选项。我们的重点可能是加密硬件和软件，因为在这个领域中，显然需要6相关工作以前的方法相结合的定理证明和正式的合成建立了一个目标导向的证明技术和交互式设计过程之间的类比。在LAMBDA中，用户从行为规范开始，通过添加原始硬件组件逐步构建电路，这些硬件组件会自动简化目标[4]。Hanna等 [6]介绍几种将当前目标简化为更简单的子目标的技术（函数）。技术是对低成本战术硬件设计的适应。替代方法通过将语义保持变换应用于它们的规范来合成电路。例如，数字设计衍生-M. Gordon等人/理论计算机科学电子笔记145（2006）2737DDD（DDD）将尾递归lambda抽象中指定的有限状态机转换为分层布尔系统[7]。Lava和Hydra都是嵌入在Haskell中的硬件描述语言，其程序由门的定义及其连接（网表）组成[1，11]。虽然Lava与外部定理证明器接口以验证其电路，但Hydra设计者可以通过正式的等式推理（使用函数编程中的定义和引理）来合成它们。函数式语言µFP和Ruby在硬件设计中采用了类似的原则[8，14]。电路是根据布尔、数字和列表上的原始函数以及高阶函数（组合形式）来定义的，这些函数组成不同结构的硬件它们的数学性质为设计探索提供了一种这些方法只在抽象的门级或状态机级处理交互式综合.此外，合成和正确性证明需要大量的用户指导。Gropius和SAFL是解决这些问题的两个相关作品。Gropius是一种硬件描述语言，定义为HOL的子集[2，3]。它的算法层提供了控制结构，如if-then-else，顺序组合和while循环。原子命令是由lambda抽象表示的编译器最初在程序的最外层将每个while循环合并为一个：输出默认值（LOCVAR变量（WHILEc（PARTIALIZEb）WHILE循环的主体b是一个非循环DFG。listout默认为输出变量提供初始值。术语LOCVAR声明局部变量vars，PARTIALIZE将非递归（终止）DFG转换为潜在的非终止命令。然后编译器合成一个封装这个程序的握手接口这些硬件块中的每一个现在都被视为系统级的原始块或进程进程通过通信单元（k进程）连接，这些通信单元实现进程输出数据的延迟、同步、复制、拆分和连接（实际上有10个不同的k进程[2]）。虽然综合产生了每个进程和k-进程的正确性证明，但并没有产生顶层系统的正确性其原因主要是因为进程和k进程网络的顶层接口与握手接口模式不匹配。我们的编译方法部分受到SAFL（静态分配函数语言）[10]的启发，特别是Richard Sharp的PhD the- sis [ 13 ]中的思想SAFL是一种一阶函数式语言，其程序由一系列尾递归函数定义组成。它的抽象层次--38M. Gordon等人/理论计算机科学电子笔记145（2006）27它允许利用传统合成系统中不可用的强大程序分析和然而，合成不是基于正确的构造原则，编译器也没有得到验证。我们的方法的新颖之处是自动编译的HOL功能的硬件与自动生成的合成的正确性证明我们的方法为编译器验证提供了一种替代方法我们不需要证明编译器的正确性，只需要一次性地证明五个电路构造器的正确性一个验证编译器，然后可以很容易地编程的设施所提供的一个机械化的证明助理，如HOL。7确认David Greaves在握手协议的硬件实现方面给了我们一些建议，并帮助我们理解了编译器模拟电路的结果Simon Moore和Robert Mullins借给我们一块Excalibur FPGA板，我们在上面运行编译后的硬件，他们帮助我们使用Quartus II设计软件来驱动该板。Ken Larsen使用他的dynlib库为串行端口编写了原始C接口的ML版本（用于与Excalibur板通信）。引用[1] Per Bjesse，Koen Claessen，Mary Sheppard，and Satnam Singh. Lava：Haskell中的硬件设计。ACM SIGPLAN Notices，34（1）：174[2] Ch ristia n Blumenréohr. 一种形式的程序可以使系统更灵活，并使其大小与系统级别相同。IinGIWorkshop Modellierung und Veri fikation von Systemen，pages 11沙克尔出版社[3] Ch ristia n Blummenréohrand d DirkEisenbiegler.在一个定理证明器中实现高层次的程序变换。在Proceedings of the Digital System Design WorkshopatthEuromicro98Conference ， Va？steras，Sweden，pages34-37，UniversitéatKarlsruhe，Institutfu？rRechnerentwurfundFehlertoleranz，1998年。[4] Simon Finn，Michael P. Fourman，Michael Francis，and Robert Harris.形式系统设计-基于计算机辅助形式推理的交互式综合。Luc Claesen，编辑，IMEC-IFIP International Workshop onApplied Formal Methods for Correct VLSI Design，第1卷，第97-110页，Houthalen，比利时，1989年11月。Elsevier Science Publishers，B. V. North-Holland，阿姆斯特丹[5] 迈克尔·J·C Gordon和Thomas F.梅勒姆编辑们HOL简介：高阶逻辑的定理证明环境。剑桥大学出版社，1993年。HOL4网站：http://hol.sourceforge.net。[6] 法光Hanna，M. Longley和N. Daeche数字系统的形式综合。在洛Claesen，编辑，正确的VLSI设计的应用形式方法，第1531989年北荷兰M. Gordon等人/理论计算机科学电子笔记145（2006）2739[7] Steven D.约翰逊和巴斯卡·博斯。机械化数字化设计推导系统DDD。技术报告TR323，印第安纳大学，IU计算机科学系，1990年。[8] 杰兰特·琼斯和玛丽·谢蒂Ruby中的电路设计来自丹麦林比暑期学校的关于红宝石的讲义，1990年9月。[9] Thomas F.梅尔汉姆高阶逻辑和硬件验证。剑桥大学出版社，英国剑桥，1993年。剑桥理论计算机科学论文集31.[10] 艾伦·麦考夫和理查德·夏普 使用函数式语言的硬件/软件协同设计。在Proceedings of Tools andAlgorithms for the Construction and Analysis of Systems（TACAS史普林格出版社LNCS Vol.2031年[11] 约翰·奥唐纳Hydra：一种用于同步数字电路设计的并发语言。第16届国际并行与分布式处理研讨会论文集。IEEE Computer Society Press，2002.[12] 美国国家标准与技术研究所高级加密标准。2001.[13] 理查德·夏普高级硬件合成。剑桥大学计算机实验室博士论文，英国剑桥，2002年。[14] 玛 丽 · 谢 里 登 muFP 是 一 种 用 于 VLSI 设 计 的 语 言 。 1984 年 ACM Symposium on Lisp andFunctional Programming会议记录，第104-112页。ACM，ACM，1984年8月。[15] 康拉德·斯林高阶逻辑中的函数定义。在Theorem Proving in Higher Order Logics中，计算机科学讲义第1125号，第381-398页，芬兰图尔库，1996年8月。史普林格出版社[16] 康拉德·斯林 在HOL中验证Rijndael。 在V.A. Carreno，C. A. 穆尼奥斯，S. Tahar，编辑，TPHOLs 2002年补充会议记录，编号CP-2002-211736，美国宇航局会议记录，2002年8月。附录：高阶逻辑四阶段握手协议的规范由谓词DEV的定义表示，它使用辅助谓词Posedge和HoldF。信号的正沿被定义为其值从低到高的过渡，或者在我们的情况下，从F到T。公式HoldF（t1，t2）s表示信号s在从t1开始到t2之前的半开间隔期间保持低值F。正式定义如下：► Posedges t=ift=0then F else（<$s（t−1）<$s t）► HoldF（t1，t2）s= Δt。t1≤t< t2<$（s t）40M. Gordon等人/理论计算机科学电子笔记145（2006）27计算函数f的握手设备的行为由项DEVf（load，inp，done，out）描述，其中：► DEVf（负载，输入，完成，输出）=（不好意思。donetPosedgeload（t +1）⇒J.tJ> t +1 HoldF（t +1，tJ）donedone tj（out tJ=f（inp（t+1）（不好意思。done t<$（Posedgeload（t +1））done（t+1））done（不好意思。（done t）tJ>tdone tJ）右侧的第一个合取项说明，如果器件可用且负载上出现正沿，则未来存在时间tJ，此时done发出终止信号并产生输出。时间tJ的输出值是将f应用于时间t+1的输入值的结果。done信号在计算期间保持值F。第二个conjunction指定在加载时不进行呼叫且设备仅保持空闲的情况。最后，最后一个合取词指出，如果设备繁忙，它最终将完成计算并变得空闲。电路制造商电路构造器使用以下基本元件► AND（in1，in2，out） 不好。输出t =（输入1t等于输入2t）► OR（in1，in2，out）=0。输出t =（输入1t等于输入2t）► NOT（inp，out）=0.输出t=<$（输入t）► MUX（sw，in1，in2，out）= MUX（sw，in 1，in 2，out）out t = ifswtthenin1telsein2t► COMBf（inp，out）=Δt。输出t=f（输入t）► DEL（inp，out）= Δt。 out（t +1）= inp t► DELT（inp，out）=（out 0 = T）延迟。out（t +1）= inp t► DFF（d，sel，q）= DFFt. q（t +1）= if Posedge sel（t +1）then d（t +1）else q t► POSEDGE（inp，out）= 100c0c1。 DELT（inp，c0）NOT（c0，c1）AND（c1，inp，out）原子握手装置。► ATMf（加载，输入，完成，输出）=0c0c1. POSEDGE（load，c0）NOT（c0，done）COMB f（inp，c1）DEL（c1，out）M. Gordon等人/理论计算机科学电子笔记145（2006）2741握手设备的顺序组成。42M. Gordon等人/理论计算机科学电子笔记145（2006）27► SEQf g（加载，输入，完成，输出）=c2c0c1c2c3数据。NOT（c2，c3）函数（c3，load，c0）函数f（c0，inp，c1，data）函数g（c1，data，c2，out）与（c1，c2，done）握手设备的并行组成。► PARf g（负载，输入，完成，输出）=c0c1start done1done2data1data2out 1out2.POSEDGE（load，c0）DEL（done，c1）AND（c0，c1，start）f（start，inp，done1，data1）g（start，inp，done2，data2）DFF（data1，done1，out1）DFF（data2，done2，out2）AND（done1，done2，done）（out = λt. （输出1t，输出2t））握手设备的条件组合。► ITEe f g（加载、输入、完成、输出）=c0c1c2start startJdone e data e q not e data f data g sel done fdone g start f start gPOSEDGE（load，c0）DEL（done，c1）AND（c0，c1，start）e（start，inp，done e，data e）POSEDGE（donee，startJ）DFF（data e，done e，sel）DFF（inp，start，q）AND（startJ，data e，start f）NOT（data e，not e）AND（startJ，not e，start g）f（start f，q，done f，data f）g（start g，q，done g，data g）MUX（sel，data f，datag，out）AND（done e，done f，c2）AND（c2，done g，done）尾递归构造函数。M. Gordon等人/理论计算机科学电子笔记145（2006）2743梳f► RECe f g（加载，输入，完成，输出）=已完成g数据g开始e q完成e数据e开始f开始g输入e完成fc0c1c2c3c4start sel startJnot e.POSEDGE（load，c0）DEL（done，c1）AND（c0，c1，start）OR（start，sel，start e）POSEDGE（done g，sel）MUX（sel，data g，inp，inp e）取DFF（inp e，start e，q）取e（start e，inp e，done e，data e）取POSEDGE（done e，startJ）取AND（startJ，data e，start f）取NOT（data e，not e）取AND（not e，startJ，start g）f（start f，q，done f，out）g（开始g，q，完成g，数据g）DEL（完成g，c3）AND（done g，c3，c4）AND（done f，done e，c2）AND（c2，c