异步电路设计：Balsa环境经验及验证方法优势和局限性分析

理论计算机科学电子笔记146（2006）189-206www.elsevier.com/locate/entcs异步电路设计X. 王明夸特科夫斯卡湾狄奥多罗普洛斯张1伯明翰大学计算机科学学院Edgbaston，Birmingham B152TT，UK摘要本文报告了我们的经验，应用过程代数和相关的工具（特别是CSP/FDR 2），以验证异步电路设计开发的Balsa环境。Balsa是一种异步逻辑合成系统，其使用语法指导编译来从并行编程语言（也称为Balsa）中的高级描述生成门级实现。在此之前，我们已经提出了一个统一的方法，在几个抽象层次上对Balsa设计进行组合验证。本文通过在几个大规模的实际案例研究中应用和测试我们的方法来继续我们的工作。 我们描述了案例研究的验证结果，并分析了我们的方法的优势和局限性。关键词：异步硬件，层次验证，CSP，模型检测，抽象层次。1引言异步和GALS（全局异步局部同步）[17，8]设计技术是同步的重要替代方案，基于全局时钟的设计技术，通过通信子系统之间的局部握手同步协议实现同步。移除全局时钟可能导致高度并发、不确定的系统，这使得单独的模拟不足以作为测试方法。1 {X.Wang，M.Z.Kwiatkowska，G.K.Theodoropoulos，Q.Zhang}@ cs.bham.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.042190X. Wang等人/理论计算机科学电子笔记146（2006）189在之前的论文[19]中，我们提出了一种使用Balsa作为背景的异步硬件系统的形式化验证方法，该方法是由曼彻斯特大学AMULET小组开发的基于CSP的[ 9 ]规范和综合系统[17，7]。Balsa采用语法指导编译，通过称为握手网络的中间层，从并行编程语言（也称为Balsa）的高级描述中生成门级实现[2]。Balsa被赋予了模拟工具，但没有验证工具。使用进程代数CSP的统一形式[15]，我们提出的方法可以在所有抽象级别上对Balsa设计进行组合验证（图1）。基于一些小的案例研究，我们展示了Balsa程序，握手网络（又名。握手电路）和异步门电路可以转换为CSP，这反过来又使FDR2 [15]（CSP的成熟模型检查器）能够用作后端验证工具。本文通过在几个大规模的实际案例研究中应用和测试我们的方法来继续我们的工作。我们描述了案例研究的验证结果，如果天真地编码和检查，将立即导致状态空间爆炸。我们展示了如何解决过程代数理论内的问题。特别地，我们将应用CSP/FDR 2框架的组合推理、数据独立理论和压缩功能总的来说，我们总结我们的经验，并分析我们的过程代数方法的优势和局限性。本文其余部分的结构如下。在简要总结了我们的分层（组合）验证方法之后，我们详细研究了两个不同抽象层次上的大规模验证问题高层通信是基于同步通信的，而低层通信是基于异步通信的。他们需要两种不同的技术来验证。这两种情况都遇到了状态空间爆炸.一个是更多地与击中FDR的我们解决了一个问题，使用本地压缩功能实现FDR，而其他使用一些组合推理和数据独立性理论。2统一的分层验证方法在这个异步逻辑综合框架，如Balsa，基于CSP的并行编程语言通常被用来给出一个高层次的算法描述的设计。 根据这样的描述，语法导向编译创建了握手组件的网络（组合），其中程序中的每个语言构造都映射到相应的握手实现。握手组件通常是预先设计和存储的X. Wang等人/理论计算机科学电子笔记146（2006）189191Balsa程序及其行为规范翻译CSP计划CSP规格语法制导翻译Rai握手网络及其协议翻译CSP网络&CSP协议异步逻辑综合Rai门级电路及其协议翻译电路CSP协议Fig. 1. 抽象的层次以门级电路片段的形式存在于库中基于硅编译框架，我们设计了一个分层的方法来验证异步硬件设计。该方法围绕着硅编译中的两个层次结构：抽象层次结构对于抽象层次，CSP适合于描述所有三个级别的系统描述。顶层描述了一个类似于标准CSP的同步系统;它使用了细粒度并行（顺序组合中的并行运算符），这很少被其他模型检查器支持两个较低的层次描述异步系统，这对标准CSP的表达能力提出了挑战。基于我们新颖的调度器思想，我们发现异步系统不仅可以直接直观地在CSP中建模，而且可以简化为仅使用跟踪模型。由于我们在抽象的所有层次上都使用CSP，因此我们可以基于各种技术（如行为细化，动作细化，抽象解释（RAI）等）在层次之间建立正式的语义链接对于组件层次结构，在所有三个级别上，都可以减少跨组件组成层次结构的验证问题。在同步的情况下，众所周知CSP精化支持组合验证。也就是说，将组件的规范与其实现分开;在检查了细化之后，在组成组件时可以使用规范而不是实现。在本文中，我们称之为基于规范的细化检查。 第一个案例研究，分布式着色算法的验证，将基于它。192X. Wang等人/理论计算机科学电子笔记146（2006）189在较低级别的异步情况下，它们是由通道连接的异步组件集合组成的输入/输出系统。每个组件都与一个协议相关联，该协议规定了连接通道上输入和输出事件的所有合法序列通道与延迟相关联。组件通过发送/接收具有非阻塞语义的信号进行通信。虽然CSP通常将同一通道上的输入和输出同步到单个事件中，但我们选择分别对这两个操作进行建模，并使用调度程序来显式地调度输入和输出的延迟调度程序首先会非确定性地选择发送组件的已启用输出（CSP进程的初始化），然后将其强制到接收组件的相应输入调度器的这种不确定性可以模拟系统的所有可能的延迟如果系统使用调度程序正确运行，这意味着系统在所有延迟场景中都正确运行也就是说，系统是延迟不敏感的。异步输入/输出系统可以是开路系统或闭路系统。开路系统模拟复合组件，通常与协议相关联。在验证闭路系统时，我们将系统与调度器并行运行。如果调度程序将输出强制到输入时它死锁（也称为扼流），我们说系统是不正确的，在这个意义上，系统没有构成一个良好的环境，其中所有的子组件的协议都得到遵守。由于调度程序参与每个事件的发生，因此调度程序的任何死锁都是全局的，因此很容易在FDR中检查。在验证一个开路系统之前，我们需要使用它的协议作为系统的环境来闭合它。新系统的无死锁性意味着开放电路系统与其协议的一致性，因此提出了基于名称协议的一致性检查。该方法的详细理论基础及其与其他异步电路验证理论的形式关系已在我们的另一篇论文中描述[20]。在本文的其余部分，我们将集中在两个大规模的研究，测试我们的方法的可扩展性，一个在顶层使用基于规范的细化检查，另一个在底层使用基于协议的一致性检查。3异步流水线与传统的同步流水线系统在锁定步骤中操作不同，控制危险（例如，分支或跳转）是非常重要的X. Wang等人/理论计算机科学电子笔记146（2006）189193更难处理，因为预取的深度，即已经进入处理器并因此必须被丢弃的指令的数量，由于不同阶段的自主和解耦操作而通常是不可预测的。因此，需要设计一些特殊的算法来解决这个问题，例如曼彻斯特大学AMULET小组为AMULET1处理器设计的算法。他们的技术使用一个比特来“着色”处理器在任何特定时刻的状态。每个指令，灰地址发出的内存，携带当前的操作颜色的处理器，这将被用来标记相应的提取指令。当控制冒险发生时，处理器的颜色改变，导致随后从新目标地址获取的指令的颜色改变到达数据路径执行的指令的颜色位与处理器的当前颜色进行比较如果找到匹配，则指令属于当前有效指令流并因此被执行，否则它被丢弃。然而，上述机制的一个重要限制是，控制危险不允许以分布式、非确定性的方式在多个阶段发生。这排除了它在MIPS系统中的应用，在MIPS系统中，控制风险可能会在多个阶段发生（例如，在EXE阶段可能会采取条件分支，而在ID阶段执行无条件跳转）[13]。为了克服这个问题，两位作者在[18]中提出了一种通用的该算法基于两个基本观察：• 系统的状态是分布式的。• 管道中较深的阶段比它们前面的阶段具有更高的优先级换句话说，在流水线阶段发生的控制转移事件使得可能在流水线中较早的流水线阶段中发生的其他事件不相关且无效，如果后者在时间上先于前者的话。基于上述两个观察，在所提出的方案中，处理器在任何特定时刻的颜色状态被定义为向量c =（c1，c2...，其中C是颜色集合C={ 0， 1}，n是流水线中的级数，并且ci是级i的颜色。ci的优先级>cj的优先级，i>j。详细的原始算法在Balsa [18]中描述，即在最高抽象级别。为了简洁起见，下面我们将仅使用其CSP翻译（即CSPm，FDR2 [15]使用的脚本语言）进行解释。对于Balsa语言及其翻译到CSP的介绍，读者可以参考[19]。194X. Wang等人/理论计算机科学电子笔记146（2006）189（C 1C2C3C4）（C1C2C3C4）（C1C2C3C 4）（C1C2C3C4）图二. 管道stg= 4--级数 sz= 5--内存大小名称类型STG ={1.. stg}名称类型COL ={0，1}CV（0）={<>}--<>是空序列CV（i）={^cv |c1<-COL，cv<-CV（i-1）}--operator ^是序列连接。nametypeCOLVEC= CV（stg） --颜色矢量数据类型零值（0）=>>最大值zeroseq（i）= 0>^zeroseq（i-1）zeroCV = zeroseq（stg）--所有元素都 为0的颜色向量。eq（cv，=if i== 1则head（cv）== head（else eq（tail（cv），tail（change（cv，i）--改变向量第i位的值=if i== 1则1-头（cv）>^尾（cv）else head（cv）>^change（tail（cv），i-1）将基于以下微架构来描述该算法。PCAddPC+InsAddNTAdd1NTAdd2NTAdd3NTAdd4Ins0S2S3Ins1 Ins2Ins3Ins4S1S4存储器AAUX. Wang等人/理论计算机科学电子笔记146（2006）189195指令集被抽象为stg+ 1类型的指令。它们中的任何一种都会在管道的各个阶段造成危害。最后一个模型的非危险指令。一条指令将包含两个字段，一个是类型信息，另一个是地址。nametypeINSCODE = {0.. stg}--1..在该阶段引起危险指令的stg--0表示非危险指令。名称类型ADDR ={0.. sz-1}名称类型INS =（INSCODE，ADDR）haz（（0，y））=false--如果指令是危险的haz（（x，y））=trueaddr（z）=let（x，y）=z withiny--获取指令的地址字段。icode（z）=let（x，y）=z within x--获取类型代码字段。通道Ins： {0..stg}.INS.COLVEC--通道，有3个数据字段;第一个字段用作索引。通道NTAdd：STG.ADDR.COLVEC通道InsAdd：ADDR.COLVEC通道 PCAdd： ADDR其中可能发生控制危险的每个流水线级SGi维持颜色状态的向量的副本通道读，写：COLVECccell（cv）=读取！cv -> ccell（cv）[]写？cv-- operator []是外部选择-- operator ->是前缀SG ⑴ =（SGCtr ⑴ [|{|读写|}|] ccell（zeroCV））|读写|}--operator '[|{|读写|}|]'是接口并行的--在读和写通道上。--operator'\{|读写|}"隐藏了两个通道。但它只负责管理与之对应的元素（图196X. Wang等人/理论计算机科学电子笔记146（2006）1892）的情况。对于到达级SGi以供执行的每个新指令，将其颜色状态向量与该级的状态向量进行比较。如果指令中任何较高优先级的颜色位（cj，其中j>i）与该级的相应颜色位不同，则意味着该指令是由于在流水线中更深处发生的控制冒险而导致的第一个传输地址。--比较i以上的两个向量的颜色位cmpr（cv，cv'，i）=if i== 0如果cv==>则为真else head（cv）== head（因此，该级允许指令通过，并且现在指令的状态向量变成其自身的状态向量。如果该级否则，执行该指令，并且该指令的状态向量变为其自身的状态向量。SGCtr（i）=Ins.i-1？移民局？公司简介--输入指令读书？cv_r->--读取局部颜色向量if（not cmpr（cv_r，cv，i））或eq（cv_r，cv，i）则如果icode（ins）==i --危险指令然后让cvcv' -> NTAdd.i！addr（ins）！cv-> Ins.i！移民局！CV'-> SGCtr（i）-- 通过否则写！cv -> Ins.i！移民局！cv -> SGCtr（i）--通过else SGCtr（i）--丢弃由于目标地址（NTAdd）可以在任何时间由任何流水线级生成，因此该方案假设存在仲裁单元，在图中称为地址仲裁单元（AAU）。地址仲裁单元向存储器发出所有指令地址信息，即，当它们从PC（正常操作）或从流水线级（在发生控制冒险的情况下）到达时，顺序指令地址PC将需要监控AAU发布的地址，并更新自己，以跟上最新的控制危险。next（x）=（x + 1）%szPC（x）= PCAdd！x -> InsAdd？x '？cv -> Ins.0？y.cv-> PC（next（[] InsAdd？x '？cv-> Ins.0？y.cv-> PC（next（在控制危险的情况下，AAU的作用是让记忆通过X. Wang等人/理论计算机科学电子笔记146（2006）189197指令地址是高优先级控制冒险的结果，同时阻止任何后续的较低优先级目标地址到达存储器，从而中断高优先级指令流。为了实现这一点，AAU保持处理器的颜色状态的记录，它根据到达它的指令地址的颜色向量更新。危害=（ NTAdd？我？x？cv -> Read？cv_r->--如果 cmpr（cv_r，cv，i），则接收到危险然后（InsAdd！x的！cv ->写！CV-> AAUCtr）--高优先级通过[]NTAdd？j？x '？cv ' - >--如果j>i，则接收到并发危险--高优先级获胜然后是InsAdd！x '！写！cvx的！cv ->写！cv ->AAUCtrelseAAUCtr）--低优先级丢弃AAUCtr =危害[]PCAdd？x->读取？cv_r->--下一条指令（（InsAdd！x的！cv_r ->AAUCtr）[]危害）AAU =（AAUCtr [|{|读写|}|] ccell（zeroCV））|读写|}这就完成了分布式着色算法的CSP描述3.1FDR2中的验证为了使用FDR2验证上述算法，系统的其他组件例如存储器（存储程序）和参考处理器（正确性标准）也需要在CSP中建模mcell（x，i）=InsAdd.x？k -> Ins.0！我！k -> mcell（x，i）- 存储一条指令的存储serializer = InsAdd？x？cv -> Ins.0？我？cv ->serializer--串行化对内存的访问。'=（|||x：地址@ |~| i：INS @ mcell（x，i））[|{|InsAdd，Ins.0|}|串行化程序--非确定性初始化单元的数组。--operator'|||x:ADDR@’isindexedinterleavingoverADDR.--operator'|~|i：INS"i s indexe d interna l choic e overt r IN S.seq（x）=InsAdd？y？cv -> Ins.0？ins.cv->if y== x然后是Ins.stg！移民局？CV'->if haz（ins）then seq（addr（ins））198X. Wang等人/理论计算机科学电子笔记146（2006）189seq（next（x））else seq（x）系统=（中文）|{|InsAdd，Ins.0|}|]（AAU [|{|NTAdd、PCAdd、InsAdd|}|]（PC（0）[|{|Ins.0|}|]（||i：STG @[{|Ins.i、Ins.i-1、NTAdd. i| SG（i））））的[|{|Ins.stg、Ins.0、InsAdd|}|] seq（0）--operator '||i：STG @[{|Ins.i、Ins.i-1、NTAdd. i|}]'--在STG上并行索引化。assert sys：[死锁释放[F]]参考处理器监视流水线的输入（即来自存储器的Ins.0），顺序地执行指令流，并通过在公共输出通道（即Ins.stg）上同步来将其输出与流水线的输出进行比较。如果发生不匹配，整个系统将死锁。因此，死锁自由意味着参考处理器由流水线处理器正确实现，从而意味着分布式着色算法的正确性在为参数（如级数（stg）和内存大小（sz））提供特定值后，我们启动FDR2来检查系统2。在stg= 4和（sz = 4的情况下，我们使用合理的时间和空间成功地验证了死锁自由。然而，当sz达到5时，状态空间爆炸立即发生。经过几天的运行，内存和硬盘消耗近15G，最终不得不中止检查。显然，记忆是国家爆炸的罪魁祸首为了解决这个问题，我们需要在CSP中进行一些组合推理将用其抽象之一“”代替“”，即CSP术语中的“”±“”。'= InsAdd？x？cv->|~|i：INS@INS. 0分！我！cv->mem在“ADDR由sz参数化，后两者由stg参数化。有趣的是，虽然COLVEC和INSCODE在[15]和[16]中独立于数据使用（定理15.2.1），但ADDR可以2CSPm中的详细信息和完整脚本可以在[22]中找到。X. Wang等人/理论计算机科学电子笔记146（2006）189199也可以通过简单的数据独立归纳法进行简化[5]。因此，对于所有可能的stg和sz，一般的问题都可以简化为stg和sz具有小的固定值时的问题，可以使用FDR 2进行简单的由于“”±因此，新系统是无死锁的意味着sys是无死锁的，反之可能不成立。由于“A”更有趣的是，在新系统中，ADDR类型变得弱数据无关[11]。根据[ 11 ]中的定理5.1.2，它可以简化为大小为1的数据类型。对于与stg相关的类型，一些非平凡的操作被定义在它们上面。这超出了数据独立性的范围因此，使用在sz上简化的模型，我们已经验证了FDR2中多达10个阶段对于大多数应用程序来说，分布式着色算法4树仲裁器电路在上述案例研究中，关键组件之一是地址仲裁单元（AAU），它需要在PC单元和流水线的stg级为了实现它，Balsa系统利用编译成门级电路的双向仲裁器树树仲裁器是一个异步电路验证中的经典例子，并且已知如果不应用高级状态空间缩减技术，则会出现状态爆炸问题：例如，BDD单独无法解决它。许多人使用不同的技术来解决这个问题，从BDD + PN（Petri网）[14]，BDD + POR（偏序约简）[1]到PN展开[12]。因此，它可以为我们的验证方法（即协议一致性和调度器）和FDR2工具进行良好的可扩展性测试。树仲裁器是以类仲裁器元素作为其根的仲裁器单元的二叉树名称类型TXS ={up， down}--导线通道r，a上的向上和向下转换：TXSBuf = r.up -> a.up -> r.down -> a.down -> Buf仲裁单元在它的两个子单元之间进行仲裁一旦一个孩子200X. Wang等人/理论计算机科学电子笔记146（2006）189一RR1a1 r2A2r.upr1.upr2.upa.upa1.upa2.upr1.downr2.downr.downa1.downa2.downa.down图三. STG中的仲裁单元及其协议请求（例如，r 1. up），则单元将把请求传播到其父单元（r. up）。与此同时，另一个孩子可以提出请求。在父单元格给予授予（a. up），单元格将查看有多少个孩子提出了请求。如果两者都已作出，则它将非确定性地选择一个并将授权传播给它（例如，1. up）。在孩子完成工作后，它会将补助金返还给单元格（r 1。而其父母，则是其父母。向下）。 在父母同意收回补助金后（a）。down），细胞可以这样回复孩子（a 1. 向下）。然而，请注意，如果另一个孩子同时在等待授予，则单元格可以回复第一个孩子（1。down）并代表第二孩子（r. 上）同时。STG（信号转换图）[4]可能是对仲裁单元它可以翻译成CSP（稍微复杂一点），如下所示：通道r1、a1、r2、a2：TXSArbL = r1.up -> a1.up -> r1.down -> r.down-> a.down-> a1.down-> ArbLArbR = r2.up -> a2.up -> r2.down -> r.down-> a.down -> a2.down -> ArbRSEQ= r.up -> a.up ->（a1.down -> SEQ[]a2.down-> SEQ）X. Wang等人/理论计算机科学电子笔记146（2006）189201ME1 = r1.up -> r.up -> a.up ->（a1.up ->ME1[]a2.up -> ME2）ME2=r2.up -> r.up -> a.up ->（a1.up ->ME1[]a2.up -> ME2）ME =（ME1 |||ME2）[|{|r，a|}|SEQArbcell =（ArbL |||ArbR）[|{|r1.up，r2.up，a1，a2|}|我使用仲裁器单元，（k级的）（平衡的）二进制仲裁器树可以如下逐级构建：k = 8--层数power（0）= 1幂（n）=2 * 幂（n-1）名称类型K= {0.. k+1}名称类型X={1..power（k）{通道ur，ua，sr，sa： K.X.TXSArbNode（v，s）= Arbcell[[r1<- ur.v.（2*s-1），a1- ua.v.（2*s-1），r2- ur.v.（2*s），a2-ua.v.（2*s），r-sr.v.s，a-sa.v.s]]--在二维空间Kx X中，树中的每个节点都有一个位置（v，s）。-- operator（2*s-1），.]]"--正在重命名，例如r1重命名为ur. v。（2*s-1）。ArbTree（0）= Buf[[r-ur.0.1，a-ua.0.1]]--0级树 只 包含Buf元素。ArbTree（n）=let l= power（n-1）within（|||x：{1..（n，x））|||ArbTree（n-1）--n层树由n-1层树组成--以及在级别n处的仲裁器单元的2^（n-1）阵列。k层的仲裁器树实现2k路仲裁器，其协议应该是：信道请求，确认： X.TXS202X. Wang等人/理论计算机科学电子笔记146（2006）189Arb（z）= req.z.up-> ack.z.up-> req.z.down-> ack.z.down -> Arb（z）--单向行为Mex = ack？x.向上->要求x.向下->墨西哥--确保一次只能有一条路通过ArbSpec =（|||x：X @ Arb（x））[|{ack.x.up，req.x.down |x-X<}|墨西哥人4.1FDR2验证我们使用我们的调度方法来验证异步电路。基本上，我们有：= sr？x：{1.. k+1}？y？z -> ur！x-1！y！z ->[] ua？x：{0.. k}？y？z -> sa！x+1！y！z ->--将级别n的sr上的事件传播到级别n-1的--并将级别n的ua上的事件传播到级别n+1的Sys=（ArbSpec[[req<-sr.k+1，ack<-sa.k+1]] |||ArbTree（k））[|{|sr，sa，ur，ua|}|] []]--ArbSpec处于k+1assert Sys：[死锁释放[F]]但是，这种幼稚的实现将立即导致状态爆炸，这是众所周知的文献。要解决这个问题，关键是要认识到Sys是确定性的，除了ua和sa上的上行传输之外，所有的事件都可以隐藏，而不会引入任何非确定性。外槽--非语义保留的FDR 2压缩函数透明法线--语义保留FDR 2压缩函数Arbcell =正态（（ArbL||| ArbR）[|{|r1.up，r2.up，a1，a2|}|] ME）Sys =（（ArbSpec[[req<-sr.k+1，ack<-sa.k+1]]|||ArbTree（k））[|{|sr，sa，ur，ua|}|] []]）|苏尔|\{ua.x.y. down，sa.x.y. down|x：K，y：X}X. Wang等人/理论计算机科学电子笔记146（2006）18920310710610510410310210110016 32 64 128 256 512 1024n路二叉仲裁树见图4。 验证时间assert chase（Sys）：[deadlock free[F]]新系统是一个确定性过程的事实可以从下面的命题中推导出来。对于确定性过程，可以安全地应用chase函数来缩减状态空间。追逐功能本质上迫使FDR2在深度优先风格的探索中优先考虑τ转换，而不[15]他们的归途命题4.1在Sys的LTS中，对于任何两条路径（从初始状态开始），分别在稳定状态s1和s2结束，如果p1和p2具有相同的迹，则s1和s2具有相同的使能事件集。将其加载到FDR23后，我们成功地检查了树仲裁器，k =10级，即2 ×10路。所用时间如下图所示。它几乎是线性的，超过了我们迄今为止从文献[1，12，14]中所知道的所有结果考虑到FDR2使用显式状态检查并利用偏序语义，这是令人惊讶的。更有趣的是，使用的内存是微不足道的（低于100 M）。我们认为，这在很大程度上是由于这样一个事实，即对于一个由小型并行过程组成的大型网络，FDR2不会构建整个产品状态空间，而是仅为单个过程构建显式状态空间，然后使用超级组合子将它们绑定在一起[15]。异步电路就是这种类型的系统，3CSPm中的详细信息和完整脚本可以在[22]中找到。（个）编译时间检查时间验证时间204X. Wang等人/理论计算机科学电子笔记146（2006）189大量的小部件并行运行[16]。5结论和今后的工作我们希望上述案例研究表明：• CSP形式主义和验证理论是通用的。同步和异步系统都可以很好地处理。• CSP表示法是表达性的，自然的，特别擅长描述大型系统。• 组合理论和数据独立性理论在大型参数化系统的验证中起着• 有了上述理论和人类的指导，FDR2可以很好地解决许多异步电路问题。类 似 的 工 作 也 可 以 在 其 他 进 程 代 数 中 实 现 ， 如 CCS/CWB 和LOTOS/CADP [3]。总的来说，我们相信进程代数提供了一个实际可行的方法来验证大规模的并行电路，即使有时它可能是具有挑战性的，需要理论和工具的专业知识相关工作的不完整调查已在[20]中给出总之，进程代数的优越性在于，• 与Petri网和图形符号不同，进程代数是组合的和可扩展的。• 很少有其他工作像标准进程代数理论那样拥有全边缘工具。• 进程代数可以为扩展现有的验证理论（如[6，10]）提供一些新的思路然而，我们的工作仍处于初步阶段。在未来，我们希望验证中涉及的一些专业知识可以自动化。例如，我们最近的研究结果表明，对于一个只由确定性异步组件组成的系统，可以在隐藏所有事件后直接应用chase[4]当然，还有改进的余地，如仲裁单元的协议。[5]请注意，异步系统和同步系统中的决定论定义是不同的。X. Wang等人/理论计算机科学电子笔记146（2006）189205确认我们要感谢Doug Edwards、Andrew Bardsley和Luis Plana的宝贵建议和帮助。该研究由EPSRC项目GR/S11091/01 GR/S11084/01资助。引用[1] R.巴尔河K. Brayton，T. A. Henzinger，S. Qadeer和S. K.拉贾马尼符号状态空间探索中的偏序约简。CAV 1997：340-351。[2] K.范·伯克尔。握手电路-一种用于超大规模集成电路编程的异步结构。剑桥大学出版社，1993年。[3] G.伯特威斯尔异步微流水线中的控制状态。AINT 2000，第45-55页，代尔夫特理工大学，2000年。[4] T. A.楚从图论规范综合自定时VLSI电路。麻省理工学院博士论文，1987年。[5] S. Creese和A. W.罗斯科同时使用数据独立性和FDR的无限系列归纳。FORTE/PSTV[6] D. L.迪尔速度无关电路自动分级验证的迹理论。ACM杰出论文。MIT Press，1993.[7] D. Edwards和A.巴兹利Balsa：一种异步硬件综合语言。计算机杂志，第45卷，第1期，第12-18页，2002年1月。[8] S. Hassoun和D.马库列斯库面向GALS设计方法。在FMGALS2003年。[9] C. A. R.霍尔通信顺序进程。Communications of ACM 21（8）：666- 677（1978）[10] M. B.约瑟夫和J. T.乌丁延迟不敏感电路的代数。 在CAVSpringer-Verlag，1990.[11] R. Lazi'c. 一个简单的研究数据与应用程序相结合的方法，以实现对数据的管理。博士论文，牛津大学计算实验室，1999年。[12] K. L.麦克米兰使用展开的异步电路迹理论验证。CAV 1995：180-195。[13] 帕特森地方检察官Hennessy，J.L.，计算机组织设计，第二版，摩根·考夫曼，1997年[14] O. Roig，J. Cortadella和E.牧基于BDD的Petri网模型检测在异步电路验证中的应用Petri网的应用与理论1995：374-391.[15] A.罗斯科 并发的理论与实践。 Prentice-Hall，1998年。[16] A. 罗 斯 科 将 共 享 变 量 程 序 编 译 成 CSP 。 PROGRESS2001 研 讨 会 论 文 集 。http://web.comlab.ox.ac.uk/oucl/research/areas/concurrency，2000年。[17] J. Sparso和S.费伯异步电路设计原理：系统观点。Kluwer Academic Publishers，2001.[18] G. Theodoropoulos和Q.张某异步流水线中控制冒险的分布式着色算法。Proceedings of I-SPAN206X. Wang等人/理论计算机科学电子笔记146（2006）189[19] X. Wang，M.夸特科夫斯卡湾Theodoropoulos和Q.张某面向异步硬件分层验证的统一CSP方法。出现在理论计算机科学中的电子笔记，AVOCS 2004年9月。2004年[20] X. Wang和M.奎亚特科夫斯卡异步电路的进程代数验证。2005年的MEMOCODE[21] Q. Zhang和G.狄奥多罗普洛斯异步MIPS R3000处理器ACSAC'03会议记录[22] Balsa验证示例页面。 http://www.cs.bham.ac.uk/research/parlard/examples网站。