高级综合：PSL规范自动合成数字电路设计的可行性和优势

理论计算机科学电子笔记190（2007）3-16www.elsevier.com/locate/entcs指定、编译、运行：来自PSL的Roderick Bloem1Stefan Galler1BarbaraJobsmann1Nir Piterman2Amir Pnueli3MartinWeiglhofer11格拉茨理工大学2洛桑联邦理工学院3魏茨曼研究所{rb loe m，bj ob st，mweig lh}@ist. 您可以登录z.atnir.piterman@ep.chamir@wisdom.weizmann.ac.il摘要我们建议使用形式化的规范语言作为高级硬件描述语言。形式语言允许紧凑的，明确的表示和产量的设计是正确的，通过验证。从规格自动合成的想法是古老的，但过去是完全不切实际的。最近，从规范到高效的合成已经取得了很大的进步。在本文中，我们扩展这些最新的方法，以产生紧凑的电路，我们通过综合一个通用的缓冲器和仲裁器的ARM这些是这是第一个根据其规格自动合成的工业实例。保留字：时序逻辑，综合，博弈，二元决策图1引言在标准的硬件设计流程中，首先编写实现，然后验证，通常使用正式的规范。在本文中，我们考虑一种替代方案：我们应用自动高级综合过程，直接从属性规范语言（PSL）中编写的规范生成正确的构造门级实现。为了简单起见，我们将这种形式的高级综合称为在本文中，我们证明了从PSL规范中导出正确代码的合成方法的可行性。合成最明显的好处是它消除了手工编码电路的需要。不那么雄心勃勃的好处包括从规范构建快速原型的可能性，以及综合是调试规范的一种非常好的方式，随着正式规范开始用作手动实现的基础，这一点将变得越来越重要从（时间）逻辑规范自动合成数字设计一直吸引着设计师的想象力，并被认为是1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.09.0044R. Bloem等人/理论计算机科学电子笔记190（2007）3电路设计中最具挑战性的问题。首先确定为教会这个问题在[17]中再次被考虑，在从线性时序逻辑（LTL）中给出的规范合成反应模块的上下文中，PSL的子集。对于给定的LTL规范，[17]中提出的方法首先构造一个Bu？chiatomaton，其中，该构造是一个自动机，用于确定Rabin自动机。这种转换可能达到一个双指数的复杂度在大小的100。在[17]中建立的高度复杂性导致合成被认为是毫无希望的棘手，并阻止了许多从业者试图将其用于系统开发。然而，有几个有趣的情况下，如果要合成的设计的规范被限制为更简单的自动机或LTL的部分片段，则合成问题可以更有效地解决[14，21，1，8，11]。在[16]中已经取得了重大进展，这表明设计可以从属于Gen-LTL类的LTL秩为1的广义反应性（GR（1）），时间为N3，其中N是状态设计的空间。GR（1）类涵盖了电路规范中出现的绝大多数性质。我们已经在一个名为Anzu1的工具中实现了[16]的方法，并将其扩展为不仅产生代表一组可能实现的BDD，而且还产生实际电路。我们通过两个例子说明了综合方法的应用第一个是来自IBM的通用缓冲器，这是一个教程设计，有一个很好的规范。第二个是AMBA总线之一的仲裁器[2]，这是一种不太大的特色工业设计。以前的合成工作只考虑了玩具的例子，如简单的互斥协议，电梯控制器，或交通灯控制器[8，16，10]。这是第一次处理现实的工业实例。本文是[4]的姊妹篇。 当前的论文展示了GenBuf案例研究的细节，而[4]则侧重于AMBA示例。本文详细描述了我们开发的从BDD构造电路的算法，描述了[4]中未包括的一些扩展，并在AMBA示例中显示了重大改进本文继续如下：在2中，我们描述了如何从规格合成电路。在第三节中，我们描述了广义Bucher，给出了它的形式化说明，并给出了综合结果。在第4节中，我们对AMBA AHB仲裁器进行了相同的操作。我们在第5节讨论了经验教训，并在第6节提出了我们的结论。2合成在本节中，我们将讨论如何从PSL规格自动获得电路。对PSL的全面介绍可以在[7]中找到。本文中显示的规范对于熟悉1www.ist.tugraz.at/staff/jobstmann/anzu/包含Anzu和此处描述的规格。R. Bloem等人/理论计算机科学电子笔记190（2007）35我不G关于LTL特别是，总是，最终！下一个！ 分别对应于G、F和X;对于一个原子命题p，prev（p）成立，如果p在前一个循环中成立，rose（p）= p，fell（p）=prev（p）p。 最后，下一个事件！（p）（n）=（<$p）U（pn）。2.1GR（1）性质本文简要回顾了文献[16]中关于GR（1）性质综合的结果。我们对PSL规格的可实现性问题感兴趣（参见：[17]）。假设有两组布尔变量X和Y。直观地说，X是由环境控制的输入变量的集合，Y是系统变量的集合意识到-能力相当于检查是否存在满足以下条件的开放控制器：规格。这样的控制器是一个Mealy机，它在任何一步都读取X变量的值并输出Y变量的值在这里，我们集中在一个子集的PSL的可实现性和综合可以有效地解决。我们所考虑的规范是形式=e→s。我们要求对于α∈{e，s}的<$α可以重写为以下部分的合取。• ϕ站。•α-一个公式，形式如下：i总是Bi，其中每个Bi都是布尔组合，从X到Y的变量和表达式的形式下！ 其中v∈X如果α=e，否则v∈X <$Y。•α-的形式为公式i∈I 总是最后！B我其中，每个B是一个布尔为了允许其他形式的公式（例如， 总是（p→（q直到r）），其中p、q和r是布尔值）， 我们通过 添加确定 性变量来扩 充变量集 。 根据输 入和输出 的选择，DetermisticmonitorsareBu？chiautomatahosebehavisdetermi-istic这些监视器遵循嵌套在always运算符中的表达式的真值确定性自动机在PSL中很容易用三组公式表示：（1）自动机的每条边都有一个公式，形式总是（si→next！（sJ）），其中s和sJ标识状态，并且i是输入，（2）表示初始状态的布尔公式，以及（3）总是最终！（B）表示公平性条件，其中B是表示一组状态的布尔公式。(An示例见第3.3节。）应该注意的是，即使有这些限制，所有可能的（有限状态）设计都可以表示为一组属性。我们把PSL公式的可实现性问题简化为在系统和环境之间进行的无限两人游戏中系统的目标是满足规范，而不管系统的行为如何。环境一个博弈结构是一个多重图，它的节点都是X和Y的真值赋值。 节点v通过边连接到所有节点vJ使得对X和Y的真值赋值满足V e，其中v提供t t赋值给当前值，vJ赋值给下一个值。然后，我们将所有同意将vJ中的X分配给一个多边的边分组。一出戏的开头是6R. Bloem等人/理论计算机科学电子笔记190（2007）3X′X′|X|XFFSComb.Y′|Y|FFSY逻辑Y′Fig. 1. 发电电路环境选择对X的赋值，系统选择一个状态，我我同意这个任务的人一出戏是由环境选择一个多边缘，并且系统选择连接到该多边缘的节点之一。如果这种相互作用产生了一个满足“e→s”的无限游戏，系统就赢了。G g我们解决这个博弈，试图决定这个博弈是环境赢还是系统赢。如果环境正在获胜，则规范是不可实现的。如果系统赢了，我们就合成一个获胜策略。这个策略，BDD，是一个工作实现的非确定性表示从形式上讲，我们有以下几点。定理2.1 [16]给定变量X和Y的集合以及上面给出的具有m和n个合取的形式的PSL公式，我们可以使用符号算法来确定是否可以在时间上与（mn 2d+1）成比例地实现。|X|+ |Y|其中d是由监视器添加的变量的数量。2.2从BDD在本节中，我们将介绍如何从该策略构建电路。该策略是变量X，Y，XJ和YJ上的BDD，其中X是输入变量，Y是输出变量，并且启动版本表示下一个状态变量。相应的电路包括：|X|+的|Y|存储最后一个时钟周期中输入和输出的值。(See图1.）在每一步中，电路读取下一个输入值XJ，并使用具有输入I=X <$Y <$XJ和输出O=YJ的组合逻辑来确定下一个输出值。注意，该策略并没有为每个组合输入规定唯一的组合输出在大多数在一些情况下，多个输出是可能的，在不可到达的状态下（假设系统遵守策略），不允许输出。我们尝试了两种方法来构建组合逻辑，一种是基于[12]一个是基于计算余因子的。[12]的方法产生了一个电路，对于给定的输入，该电路可以生成该策略允许的任何输出。为此，它使用一组额外的输入到组合逻辑。请注意，这比我们需要的更一般：一个电路总是在给定输入的情况下产生一个有效输出。我们将在后面看到，这种普遍性是以沉重的代价来的，R. Bloem等人/理论计算机科学电子笔记190（2007）37为了所有的人S ' =存在O\o. Sp = S'中 o的正余因子//（*）careset= p*！n+！p*nf[o]= p最小化 wrt。caresetS =S[用f[o]代替o]od图二. 从BDDp = p *！nn = n *！p对于所有输入i，p ' =存在i。p n ' =存在i.n如果p菲恩德图三. 算法扩展逻辑的大小构建组合逻辑的第二种方法使用图2所示的伪代码。对于组合输出，我们写o ∈O，对于组合输入，写i ∈ I。该策略用S表示，O\o是不包括输出o的组合输出的集合。 对于每一个组合输出o，我们构造一个函数f，它与给定的策略BDD相容。 该算法通过一个接一个的组合输出o进行：首先，我们构建S '以得到一个BDD，该BDD仅根据I限制o。 然后，我们建立S'相对于o的正和负余因子（p，n），也就是说，我们找到o可以被1（分别为0）对于出现在正余因子和负余因子中的输入，两个值都是允许的。既不在正余因子中也不在负余因子中的组合输入在获胜区域之外，因此表示不可能发生的情况（只要环境满足假设）。 因此，f必须在pn中为1，在pn中为0，这给了我们一组护理状态。我们用护理集最小化正余因子以获得函数f。最后，我们将S中的变量o替换为f，并继续处理下一个变量。因为组合输出可能是相关的，所以替换是必要的通过使用CUDD的DumpBlif命令[ 19 ]写入函数的BDD来然后，我们使用ABC[3]优化结果，并将其映射到标准单元库。我们还使用ABC来估计所需的门的数量。下面我们将描述两个简单有效的扩展（参见第3.3节和第4节）优化辅助因子图2所示的算法根据每个组合输出的组合输入生成一个函数。有些输出可能不依赖于所有输入，我们希望从函数中删除不必要的输入给定变量o的正和负余因子，如果当我们存在性量化变量i时，余因子不重叠，则不需要变量i来区分o必须为1和o必须为0的状态，我们可以简单地忽略它。我们通过在标有（*）的位置插入图3所示的代码来调整图2中的算法。8R. Bloem等人/理论计算机科学电子笔记190（2007）3删除因变量在计算组合逻辑之后，我们对可达状态集进行因变量分析[9]以简化生成的电路 。 给 定 一 个 布 尔 函 数 f 在 x0 ， . xn ， 变 量 xi 函 数 依 赖 于 f ， 如 果anndonlyif∈xi。f=0。不是fx是函数，而是由f的其余变量统一确定，并且可以由函数g（x0，. xi−1，xi+1. xn）。假设我们生成的电路具有可达状态集R（X <$Y）。如果一个状态变量s在R中函数依赖，我们可以去掉相应的在电路中，将其值计算为其他IPv6操作的值的函数。3广义布尔运算器案例研究3.1广义Bucher通用缓冲器（generalized buffer，以下简称GenBuf）是由IBM开发的一种设计，作为Rulebase验证工具2的教程。GenBuf在PSL中有相对完整的规范。见图4。 GenBuf的框图，有四个接口图4包含设计及其接口的框图。虚线框表示环境。GenBuf是由数字参数化的缓冲器族n. 它将数据从n个接收器传输到两个接收器。 数据由数据中心2参见http：//www.haifa.ibm.com/projects/verification/RBHomepage/tutorial3/。GenBufStoB（0）DI（0..BtoR_（0）StoB_（1）StoB（2）BtoR_（0）StoB_（3）FIFODI（96..BtoS_ACK（3）发送者3DO（0..（第三十一条）DI（64..RtoB_ACK（1）BtoS_ACK（2）发送者2接收器1DI（32..BtoS_ACK（1）发送者1RtoB_ACK（0）接收器0BtoS_ACK（0）控制器发送者0充分空DEQENQSLC（0..R. Bloem等人/理论计算机科学电子笔记190（2007）39并由接收机以循环顺序接收。缓冲器具有与每个发送器和每个接收器的握手协议。对于每个发送者i，GenBuf具有输入StoB ACK（i）（发送者到缓冲器请求），其用信号通知发送请求，以及输出BtoS ACK（i）（缓冲器到发送者确认）。此外，每个发送器都有一个32位的数据总线，用于将数据发送到缓冲器。的缓冲器包含一个四槽FIFO来保存数据。在接收端，存在类似的接口。它使用输出BtoB ACK（j）（总线器到接收器请求）和输入RtoB ACK（j）（接收器到总线器确认）将总线器连接到每个接收器。接收器共享一条32位数据总线。Genbuf由控制器、FIFO和多路复用器组成。我们从它的规格合成控制器，同时假设FIFO和多路复用器的实现已经给出。FIFO和多路复用器是标准的逻辑部件，从规范中合成它们会使任务变得不必要的复杂，特别是因为它们涉及32位数据总线。控制逻辑通过两个输出和两个输入与FIFO通信。输出ENQ（入队数据）和DEQ（出队最旧的数据）用于填充和清空FIFO。输入FULL和EMPTY告诉控制器FIFO是否准备好接收或发送数据。控制器使用称为SLC的多位输出与多路复用器通信，确定当ENQ被断言时加载来自客户端的发送方和GenBuf之间的接口是一个四阶段握手：(i) 通过提升StoB（i），Rtti启动转移。一个周期后，它将数据放到总线上。(ii) 在StoB ACK（i）被引发之后至少一个tick，GenBuf引发BtoS ACK（i）并读取数据。(iii) 在BtoS ACK（i）被提升之后的一个滴答，发送方降低StoB ACK（i）。从这时起，不再需要将数据保存在总线上(iv) GenBuf最终降低BtoS ACK（i）。可能需要几个周期才能做到这一点。直到BtoS ACK（i）降低后的一个周期，发送方iGenBuf和接收器之间的握手是类似的，除了在这种情况下GenBuf发起传输，并且除了在步骤4中应答信号在请求降低后一个周期降低。3.2正式规格现在，我们将介绍我们为GenBuf开发的规范。这与IBM由于我们不会自动合成FIFO和多路复用器，因此我们删除了说明它们正确工作的规范，并添加了指定FIFO和多路复用器相互作用的公式。规范的PSL公式见表1。在表中，我们使用i ∈ {0，. ，n}来表示发送者的号码。我们用j∈ {0，1}表示10R. Bloem等人/理论计算机科学电子笔记190（2007）3接收器。与发送者保证1来自发送方的请求总是得到确认。此外，确认最终被降低。保证2禁止立即确认，因为发送方的数据直到请求断言后的一个步骤才有效。保证3没有请求就没有确认。保证4除非发送方首先取消其请求，否则不会取消确认。假设1请求在被送达之前不会降低。 信号StoB_ACK（i）在BtoS_ACK（i）被升高之后的一个周期被降低，并且它不能被升高直到BtoS_ACK（i）被降低之后的一个周期。保证5任何时候只有一个发送方发送数据。与接收方的通信假设2来自业务员的请求总是得到确认。 此外，确认在请求降低后一个滴答降低假设3除非缓冲器首先撤销其请求，否则不会撤销确认。假设4没有请求就没有确认。保证6在送达请求之前不会降低请求。该请求在确认被引发后的一个周期被降低，并且直到确认被降低后的一个周期才能被引发保证7 GenBuf不会同时请求两个接收器。GenBuf不会向任何接收方发出两个连续的请求（这保证了循环调度.）保证8GenBuf将在接收器j之后一个周期J确认了请求。FIFO和多路复用器保证9选择和入队信号跟随着对队列的应答。保证10数据在传输到接收方完成时出队。保证11当FIFO满时不入队，我们不出队数据，当它为空时不出队。保证12如果FIFO不为空，最终将发生出队。R. Bloem等人/理论计算机科学电子笔记190（2007）311假设5 FIFO的行为正确。如果我们入队和出队的simul-simplex或根本没有，FIFO的状态不会改变。如果数据仅被入队（分别被出队），FIFO在下一个周期中不能为空（满）最初，我们根据上述规范合成的缓冲器忽略了FIFO。相反，它会等待，直到它可以发送数据到接收方之前，接受来自发送方的数据。因此，我们添加了以下属性，以确保使用FIFO。保证13如果FIFO未满并且发送方请求发送数据，则数据在此步骤或下一步骤中排队。表1PSL规范always（StoB）→eventually！ BtoS ACK（i））G1i：always（<$StoB BtoS ACK（i））G2i：始终（rose（StoB（i））→ <$BtoS ACK（i））G3i：always（rose（BtoS ACK（i））→prev（StoB（i）G4i：always（（BtoS ACK（i）StoB（i））→next！ BtoS ACK（i））i：always（StoBStoB（i））的1i：always（BtoS ACK（i）→next！ （i）G5=i=i：总是<$（BtoS ACK（i））j：always（BtoRRtoB ACK（j））一个2j：总是（<$BtoR RtoB ACK（j））A3j：always（BtoR（j）RtoB ACK（j）→next！A4. RtoB ACK（j）：总是（RtoB ACK（j）-prev（BtoB ACK（j）j：总是（BtoR BtoR（j））G6RtoBACK（j）→下一个！ BtoR（j））总是<$（BtoR <$（0）<$BtoR<$（1））。G7j：always（rose（BtoR（j）→下一个！下一个活动！ （rose（BtoR（0））rose（BtoR（1））（<$BtoR（j）。G8ACK（j）：always（RtoB ACK（j）→next！（<$BtoR（j）always（参与者：rose（BtoS ACK（i）九国集团S1：总是（rose（BtoS ACK（i））→SLC =i）G10始终（DEQ参与（失败（RtoB ACK（0））失败（RtoB ACK（1）））always（（FULL<$ DEQ）→ <$ENQ）十一国集团总是（EMPTY→ <$ DEQ）G12总是（<$EMPTY→最终！DEQ）always（（DEQ ParticipENQ）→（EMPTY Participnext！空）always（（DEQParticipENQ）→（FULLParticipnext！Full））一个5always（（ENQDEQ）→next！空）always（（DEQENQ）→下一个！€FULL）A13always（（<$FULLi：StoB（i））→（ENQnext！ENQ））3.3合成如第2.1节所述，并非所有PSL规格都可以直接合成。我们首先要把保证1、2、7、12和假设2翻译成适当的形式。12R. Bloem等人/理论计算机科学电子笔记190（2007）3考虑到保证4、6和假设4，我们可以结合R. Bloem等人/理论计算机科学电子笔记190（2007）313空的<$EMPTY<$ DEQsSDEQ图五. 监控保证12保证1和2到最后，总是！（StoB_ACK（i）），我们可以将假设2重写为最后总是！ （BtoRRE Q（i）ParticipRtoBACK（i））。对于保证12和保证7的第二部分，我们必须构建确定性监视器。虽然有些公式不存在确定性监控器，而且构造这样的监控器通常很难[13]，但构造本文考虑的公式非常简单。例如，图5示出了保证12的确定性自动机，其声明总是（<$EMPTY →最终！DEQ）。我们使用标准应用程 序 从 LT L 为 多 个 应 用 程 序 （ 例如，，[20]），其中标 准 扩 展 规 则 的 修 改 形 式 特 别 是 ， 我 们 最终使 用 了 扩 展 规 则 ！q 等 于q<$（<$q <$）下一个！ 最终！ q）以及以下事实：<$EMPTY→等于EMPTY（<$EMPTY）。在规格已被带到适当的形式，它是使用第2节中描述的算法合成。在图6中，我们显示了针对不同数量的时钟合成GenBuf所需的时间，不包括ABC优化电路所需的时间，通常为几秒钟。我们绘制了使用基于[12]的方法生成电路所需的时间，我们的算法所需的时间(See第2.2节）合成时间保持在一分钟以下，并且对于所有方法都是类似的。(We不能解释为什么当我们有9个时合成要快得多。我们能够合成高达60 μ g的GenBuf规格。我们的实施大约需要13个小时，60个小时。合成一个含有70个碱基的规范似乎是一个时间问题，而不是记忆问题。图7我们显示了ABC优化后所得电路的门数。基于[12]的方法产生的电路比我们的电路大约大一个数量级（对于超过6 μ s的情况，此方法产生的电路太大，ABC无法处理。）优化辅因子产生约16%。删除的因变量减少了5- 12%的锁存器的数量很难预测发现哪些（这些信号可以从BtoS ACK信号推断。通过ABC的优化产生约20%的门的数量的改进。14R. Bloem等人/理论计算机科学电子笔记190（2007）3504540353025201510501 2 3 4 5 6 7 8 910人数1000080006000400020000【KS00】未优化的优化余因子选择cof，无depvars手写1 2 3 4 5 6 7 8 9 10人数见图6。 合成GenBuf的时间图7。 GenBuf电路的大小应该指出的是，电路的增长是良好的行为，但电路的5000个门仍然很大。4AMBA AHB案例研究在本节中，我们总结了一个在高级高性能总线（AHB）上执行的案例研究我们提出的新结果明显优于[4]中的结果。AHB是一种片上通信标准，用于连接处理器内核、高速缓存和DMA控制器等设备。总线允许多达16个主机与多达16个客户端进行通信（读或写）。 巴士由 数据总线和地址总线。在任何时候，只有一个主机被允许访问每个总线。对地址总线的访问由仲裁器控制，这是本节的主题。对总线的访问可以被锁定或解锁，可以是单次传输或突发传输，其中包括指定或未指定的传输次数。锁定的访问不能被中断，因此仲裁器必须考虑不同的访问模式。为了访问总线，主机驱动地址和控制信号以指示它想要的传输类型。奴隶是被动的，只能响应请求。仲裁器决定总线的下一个所有者以及其访问是否将被锁定。然后，它断言相应的控制信号以指示其决定，并且当电流传输完成时，总线被切换。我们从AMBA AHB标准中推导出了仲裁器的正式规范。该标准允许各种仲裁方案，包括基于优先级的和公平总线.我们写了一个公平总线的规范，合成了它，并构建了一个电路。随后，我们构建了一个如第2.2节所述的电路。在我们最初的实验[4]中，我们只能为最多四个主节点合成仲裁器，对于更大的仲裁器，合成算法在构建策略时会耗尽内存。(2GB内存可用）。在重写规范之后，在不改变其含义的情况下，我们可以处理多达10个master。的时间【KS00】未优化的优化辅因子opt cof，w/o depvars合成时间（s）门数R. Bloem等人/理论计算机科学电子笔记190（2007）3152500020000150001000050000合成+重排序BDD重排序1 2 3 4 5 6 7 8 910人数50000450004000035000300002500020000150001000050000未优化的优化余因子手写1 2 3 4 5 6 7 8 9 10船长人数见图8。 合成AMBA总线的时间图9。 AMBA电路的大小用于合成的时间在图8中示出，并且范围从几秒到6.5小时。大部分时间都花在重新排序BDD上。(We我不知道为什么九个大师的合成比八个大师的合成快在图9中，我们使用我们的算法和手动实现示出了仲裁器的门的数量作为主机的数量的函数对于一个master，手动和自动生成的实现具有大致相同的大小。自动生成的实现随着主机的数量迅速增长，而手动实现几乎与主机的数量无关自动生成的十个master的实现比手动实现大大约一百倍。自动生成的仲裁器实现循环仲裁方案。这可以从综合算法中策略的构造来解释，但它也是公平仲裁器的最简单实现。我们通过将最终的仲裁器与手动编写的主程序和客户端相结合来验证我们的规范，它可以毫无问题地进行合作。5讨论在本节中，我们将讨论自动合成的最重要的优点和缺点。为广义缓冲器编写正式规范是很简单的。这可能部分归因于块的简单性，部分归因于IBM提供的明确规范（尽管规范既不完整，也没有错误）。另一方面，为AMBA仲裁器编写一个完整的正式规范并非易事。首先，仲裁器的许多方面在ARM这种模糊性将导致长时间的讨论，关于如何实现总线设备的人可以阅读标准，以及仲裁器应该允许哪些行为请注意，在为仲裁器编写手动实现时也会出现同样的问题。构造一个完整的规范是一个迭代的过程。特别是对于仲裁员来说，这个过程很麻烦，我们遇到了问题合成时间（s）门数16R. Bloem等人/理论计算机科学电子笔记190（2007）3提出了一定的要求。这些问题最好通过引入额外的信号来解决（就像编写手动实现时所做的那样）。在这个过程中，我们写了几个无法实现的规格，以及一些规格产生的电路不符合我们的预期。 （GenBuf意外行为的一个简单示例在第3.2节中描述并解决。该工具抱怨无法实现的规格，但在查明问题方面没有任何帮助。同样，意外行为通常很容易发现，但并不总是容易补救。一些关于调试规范的工具的工作已经完成[15]，但需要进一步的研究，特别是与可实现性有关的研究。手动实现参数化电路的任务通常并不强烈依赖于参数。 (The在GenBuf的情况下，参数是主机的数量，在仲裁器的情况下，参数是主机的数量）。对于自动合成来说，情况并非如此：合成时间和生成的电路的大小随着参数的增加而增加。不幸的是，生成的门级输出很复杂，并且无法轻松手动更改。为给定的规范找到一个小的实现是很困难的。一个规范对应于一组（可能是无限的）实现它的开放控制器。首先，[16]的算法规定了一组开放式控制器，并构造了一个策略，该策略对应于实现正确开放式控制器的有限（但通常很大）组合块集。其次，我们必须从这个集合中选择一个具有小表示的控制器。并不是每个规范允许的小实现都能在第一步中存活下来。即使这样做，也很难从第二步中的策略所允许的回路中找到一个小回路。我们正在研究改进每一步的方法，我们希望我们能够显著减小所产生电路的大小从好的方面来说，所得到的PSL规范简短、可读、易于修改，比VERSARG中的手动实现要好得多。合成算法也是一个很好的工具，以获得规范一致和完整。虽然规范的构建有时很麻烦，但我们怀疑如果没有综合工具，我们是否能够编写出完整和一致的规范。自动综合首先适用于控制电路。我们正在研究的方法，结合手动编码的数据路径与自动合成的控制电路，这需要一个控制器的合成问题的形式6结论当规范在早期可用时，自动合成可以用于获得第一个实现，当关键块被手动实现取代时，产生一个功能测试环境此外，这些实现可以作为规范的有价值的健全性检查，这在手动实现基于正式规范时非常重要。虽然自动合成一直在追求，只有最近的发展，R. Bloem等人/理论计算机科学电子笔记190（2007）317使它适用于现实的例子。本文及其对比[4]首次提出了从其规范合成真实块的方法我们得到的电路是相当大的，但这种方法仍然是年轻的，只有几个途径进行了优化。我们尝试使用[12]的方法生成电路。第二次尝试使用辅因子产生的电路要小一个数量级，对这种方法的优化产生了显着的改进。我们预计，未来的研究将产生进一步的大的改进，使自动合成的一个真正的替代手动编码的某些类型的电路。确认这项工作得到了欧洲联盟委员会的部分支持，合同号为507219（PROSYD）。我们感谢卡琳·格雷梅尔和米兰·米林科维奇在执行方面提供的帮助引用[1] R. Alzheimer和S.拉托雷。LTL片段的确定性生成器和游戏。ACM Transactions on ComputationalLogic，5（1）：1-25，Jan. 2004年[2] ARM有限公司AMBA规范（修订版2）。 可查阅www.arm.com，1999年。[3] 伯 克 利 逻 辑 综 合 与 验 证 组 。 ABC ： 序 列 合 成 和 验 证 系 统 ， 版 本 61208 。http://www.eecs.berkeley.edu/alanmi/abc/.[4] R. Bloem，S.加勒湾Jobstmann，N. Piterman，A. Pnueli和M.魏格尔霍夫从规格自动硬件综合：案例研究。在欧洲设计，自动化和测试会议论文集，2007年。[5] J. 布希河和湖。 L和WEBER。Solvinge ntialconditin s byite-s tates trategie s.Tran s。 Amer. 数学协会，138：295 -311，1969.[6] A. 教堂逻辑、算术和自动机。 在proc 小行星1962恭喜数学，第23[7] C. Weinner和D.菲斯曼PSL的实用介绍。Springer-Verlag，2006.[8] A. Harding，M. Ryan和P. Schobbens LTL对策中策略综合的一种新算法。在工具和算法的建设和系统的分析，第477-492页[9] A. J.Hu和D.迪尔通过利用函数依赖性减少BDD大小。设计自动化会议论文集，第266-271页[10] B. Jobstmann和R.布罗姆LTL合成的优化。计算机辅助设计中的形式方法会议，第117-124页，2006年[11]B. Jobsmann，A. Griesmayer和R.布罗姆修复程序作为一个游戏。第17届计算机辅助验证会议（CAV[12] J. H. Kukula和T. R.船从关系中建立电路。计算机辅助验证会议，第113-123页，2000年[13] O. Kupferman和M. Y.瓦迪自由、软弱与决定论：从线性时间到分支时间。IEEESymposium on Logic inComputer Science，1998。[14] M.梅德尔CTL和LTL的共同片段。在Proc. Foundations of Computer Science，第643-652页[15] I. Pill，S.森普里尼河卡瓦达湾罗韦里河Bloem和A. Cimatti.硬件需求的形式化分析。在设计自动化会议，2006年。[16] N. Piterman，A. Pnueli和Y.萨尔反应性⑴设计的合成。在Conference on Verification，ModelChecking，and Abstract Interpretation，第364-380页[17]A. Pnueli和R.罗斯纳关于反应模的合成。在Proc. 16th ACM Symp.的Prog。浪第179-190页[18] M.拉宾《无限对象自动机和丘奇美国数学学会，1972年。[19] F.索门齐CUDD：CU决策图包。科罗拉多大学博尔德分校，ftp://vlsi.colorado.edu/pub/。[20] F.所 以 我 和 R 。Bloem.EcienBuhiafromLTLformul ae.InC onFe re nceon C omputerAidedVerification（CAV'00），pages 248-263，2000.[21] N. 我是P. 胡滕和W. 你好。系统策略是根据要求的响应规范来确定特定的系统结构。在自动机的实现和应用国际会议上的会议记录。Springer-Verlag，2003.