延迟不敏感设计的形式化建模及正式验证方法

理论计算机科学电子笔记146（2006）41-59www.elsevier.com/locate/entcs延迟不敏感设计JulienBoucaron1Jean-Vivien Millo2Robert De Simone3AOSTE团队INRIA2004，Route des Lucioles-BP93 Sophia Antipolis，法国摘要我们重新审视中继站的形式化建模，中继站是全局异步/局部同步系统的延迟不敏感设计理论中使用的特定连接元素。中继站负责在处理信令/数据传输的同时考虑物理强制性延迟，以避免本地IP同步计算块的饥饿、死锁和拥塞。自Carloni等人提出以来，这些中继站的结构和行为已经得到了充分的表征和分析。但以前的工作并没有提供这些机制的完全正式和周期准确的描述，例如，可以进行正式验证（相反，主要是开发仿真模型）。由于整个方案需要精确性，我们认为可能需要这样一个正式的描述。我们在这里描述这样的尝试。关键词：延迟不敏感，中继站，Shell，GALS，形式验证，标记图，同步，Esterel，SyncCharts1电子邮件：jboucaro@sophia.inria.fr2电子邮件：jvmillo@sophia.inria.fr3电子邮件：rs@sophia.inria.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.03542J. Boucaron等人/理论计算机科学电子笔记146（2006）411引言长导线互连延迟可能在现代SoC设计中引起时间闭合困难，其中信号在单个时 钟 周 期 中 跨 管 芯 的 传 播 变 得 有 问 题 。 对 L.Carloni ， K.McMillan 和A.Sangiovanni-Vincentelli [21，22]，对这个问题提出了解决方案该理论可以粗略地描述为：初始的完全同步参考规范首先被描述为同步块组件的异步网络（GALS系统）。然后引入适当的互连机制来重新同步全球系统，但允许在互连处的特定（整数时间）延迟，其形式为所谓的中继站的固定大小的线路。这些中继站与同步“珍珠”IP块周围的“外壳”包装器一起在它们的帮助下，在可能暂时无法运行的计算块之间执行适当的调节，这要么是因为输入数据不可用，要么是因为网络的其余部分无法存储它们的结果（如果它们被产生的话）。第二个问题来自硬件资源的有限性，以及互连（中继站的线路）的固定大小的缓冲容量自从中继站被发明以来，它一直是许多研究小组关注的对象在[12、15、14]中提供了广泛的建模、表征和尽管如此，建模级别还没有完全达到完全正式的阶段，因此正确性的证明仍然是非正式的，无论是基于文本证明提示，还是基于仿真模型执行。我们将以Casu et Macchiarulo [25]的一篇论文作为我们的出发点，该论文提供了这样一个（优秀的）模型但是，我们在许多特征上偏离了它们的描述（例如，它们不包括输出函数作为描述每个中继站的控制结构的FSM状态机的一部分每个中继站可以被看作是一个单元，是一条线路的一部分，然后组成一条具有n个时钟周期延迟的分段线路中继站实现给定的协议，该协议在某种意义上将通过它们的链接来保留每个站都可以从其前任站（IP块周围的外壳或另一个站）接收有效信号数据，并在下一个时钟周期将其向下传递到其继任站。中继站还可以在相反方向上接收实现“背压”特征的调节在这种情况下，该站应避免发送其值，并保留它。它还应该仍然能够接收该周期中的下一个（因为前一个节点没有被警告拥塞J. Boucaron等人/理论计算机科学电子笔记146（2006）4143然而），并且如果必要的话，应当在下一个时钟周期中将背压拥塞信号传播到前一个节点。需要“下一周期延迟”来遵守物理延迟假设。当然，也有一些时候，由于上游计算由于缺乏输入而暂时停止，因此没有有效的数据从前一个节点传输因此，应当注意，任何中继站都需要同时保持两个值的容量，以防在新的值同时到达时它不能传播当前值。如果有效数据的生成速度比消费速度慢，它也可以为空。目前，中继站的作用是双重的：它们通过背压机制实现适当处理拥塞风险所需的在线调度方案;它们还提供数据的临时存储第二个角色是有争议的：如果数据被允许继续他们的路由，他们可以被存储在目的地shell，如果它将提供一个专用的缓冲器，其大小与这条线上所有中继站的累积缓冲容量相同。更好的是，将所有存储移动到一个空间位置将减轻物理合成的负担。这一点在[25]中得到了证实 当然，运输调节和背压机制仍应以强制方式应用，因为否则最终目的地缓冲器可能会过度流动。但它们只会在外壳级延迟数据传输和计算，而不会在互连过程中延迟背压机制现在示出了关于“向下”报告的拥塞和交通堵塞的反向传播信息的净效应他们只在需要的时候才这样做，但要尽可能早，同时要尊重通过长电线所需的时间本文件的结构如下：在第2节中，我们简要回顾了同步电路（用于局部组件）和GALS系统（作为由无界缓冲器连接的局部同步计算组件的网络）的基本上下文定义我们提到了一些初始化问题，如[17]中通过将GALS模型的数据无值抽象为Petri网标记图来解决这里应该注意的是，围绕标记图（在文献中也称为事件图）开发的理论结果的主体可以为此类系统的表征提供许多有用的分析结果[16，5]。在容量有限的地方也是如此，它为以前关于LID系统的论文中提到的特别地，它为行中的数据的正确初始化提供了足够的条件，从而保证了没有死锁的活动性，但也完全拥塞另一方面，事件图（和所有Petri网子类一样）作为并发模型本质上是异步的，它们在调度和“最大”调度中的应用44J. Boucaron等人/理论计算机科学电子笔记146（2006）41“进展在这里，答案可能已经存在于文献中。在第3节中，我们提供了中继站模型要满足的抽象要求和形式约束。我们从[ 25 ]的模型开始，它本身在某种程度上总结了以前的工作。 我们以SyncChart的形式提供正式模型，具有常规功能和输出信号清晰的时序规范。我们的模型是服从描述在埃斯特雷尔[7]或SyncCharts [3，4]，从而允许形式化方法和模型检查技术[9]。当然，这也可以通过例如以blif格式提供直接网表描述来实现，但是我们获得了语法灵活性，以容易地描述例如将多个中继站组合成大延迟的线路在第3.2节中，我们正式指定了一些正确性的性质，可以建立在一条线的中继站。当然，暴力模型检查不允许对参数模型进行推理（这里的参数是线路的延迟长度n），因此我们需要实例化几个恒定长度值。我们将在第2.1节中描述shell包装器（这里非常接近[25]的版本四、 我们再次对它们进行模型检查，以建立正确性属性。在[11，24，13]中开始了使用静态调度来优化周期分配的相关工作，命名为回收，并受到软件流水周期分配技术的启发。它扩展并以某种方式引用了时序电路重定时的范例[20]。最后，我们提出几个开放性问题。吸引我们注意力的扩展的主要主题是以下一个：目前的设计方法学从单片同步规范开始。这需要保留来自商业EDA流程的几种重要合成技术。但是，如果人们能够认识到，这种看似同步的描述实际上包含指示定时不稳定性和潜在分解成更小的同步“珍珠”的信息这里我们指的是所谓的异步进程（这里的“异步”一词适用于计算模型），而不是缓冲连接（这里的“异步”一词适用于通信模型）这种额外信息的示例可以由用户提供（作为多速率/多锁建模扩展或独占控制模式）[1，8，27]。它也可以通过动态语义分析来提取，正如Benveniste等人 [23，6]的等时/内时理论所做的那样（据我们所知）。J. Boucaron等人/理论计算机科学电子笔记146（2006）4145J2个房间同步电路：同步电路与时钟相关联。它有一个由三组（布尔）输入、寄存器和输出信号组成的信号接口，以及一个由一组（布尔）寄存器（或布尔寄存器）组成的内部状态。在每个时钟周期，它根据输入和寄存器的当前值形式上，同步电路因此是结构I，O，R，Out，Next >，其中<• I是布尔输入变量的集合{I0，.，I n-1}。 我们称向量I = ∈B n是一个输入事件。它表示在给定时刻对所有输入变量的估值。• O是布尔输出变量{O0，.，O m−1}，我们称向量O = ∈B m是一个输出事件。它表示在给定时刻对所有输出变量的估值。• R是布尔寄存器变量的集合{R0，.，R p−1}，我们称R = ∈Bp当前状态。我们还使用下一状态RJ=，使用带撇号的名称。0p−1• Out是一个向量的布尔函数，Out j：（B n×B p）→B。因此，每个函数Outj从输入和寄存器变量的当前值定义输出变量Oj• Next是一个向量布尔函数，N ext j：（B n×B p）→B。因此，每个函数N extj定义寄存器变量RJ从输入和寄存器变量的当前值同步电路的同步或异步网络通过并行设置本地（IP）同步组件，建立不同块的输入到输出的所需点对点互连，可以构建更大的电路这显示在图1中，如果假设连接是简单的电线，并且所有组件都在同一时钟上运行其结果是一个复合网表，在本质上与本地组件同步电路同质另一方面，也可以假设本地同步组件不是全局同步的，并且连接是通过这构建了图1的另一种解释，即全球数据流网络。现在，每个组件只有在其所有输入数据值都存在时才能其运行的结果是，46J. Boucaron等人/理论计算机科学电子笔记146（2006）41图1.一、同步IP块网络（同步或异步）在每个输入通道上产生一个输入值，并在其输出通道上产生一个输出它可以被认为是一个完全不受限制的GALS系统。我们将把这个表示阶段仅仅作为概念建模的中间如[17]所述，当忽略所携带的值时，无限制GALS模型直接映射到事件/标记图（Petri网的一个众所周知的子类作为信号数据。这种关联有助于证明，在一些谨慎的初始化条件下，这个异步版本在功能上等同于以前的完全同步版本（参见下面关于初始化的讨论标记图在文献中也被称为事件图，它们形成了Petri网的一个特殊子类，其中位置只有一个输入转换和一个输出转换[16]。在我们的例子中，转换表示本地同步组件，它在每个输入通道上消耗一个数据，并在每个步骤中在每个输出通道上产生一个数据当数据被抽象为标记/事件图是不同的执行只是在个别转换的相对触发上有所不同，而这些触发是一致的：给定转换的触发不能禁止另一个转换的触发，如果它以前是允许的。此外，给定图循环中所有位置标记的总和在任何执行过程中都保持不变一个Petri网（PN）被称为活的，如果任何转移仍然可以执行（可能经过一些步骤）从任何可达标记。文[16]证明了一个有标记图是活的，如果图的每个圈在它的一个位置上至少包含一个标记。图2显示了与先前的GALS网络相关联的标记图（以其异步形式）。具有库所容量的在GALS理论（如延迟不敏感设计等）中，目的通常是在完全同步和同步之间建立一个模型。J. Boucaron等人/理论计算机科学电子笔记146（2006）4147图二. 与前一个GALS图片相关联的实时标记图异步的。特别地，在SoC设计中能够限制互连以便仅使用有界空间是重要的。因此，一般的哲学是：第一，对完全同步规范进行去同步化;第二，通过仔细的调度机制以尊重强制性物理延迟的方式重新同步它，同时只使用有限的通信资源。在抽象的PN层次上，这种有界性可以用位置容量来建模（调度问题将在后面的其他地方处理）。在Petri网中，通过要求给定的位置不能容纳超过n个令牌来引入容量，n是该位置的容量容量可以追溯到PN历史的基础，没有明确的开创性论文（定义见[5]，等价定理的证明见[2]事实上，通过为每个现有的PN添加新的位置，用另一个没有容量的等效PN替换有容量的PN是立即的，其标记与原始位置容量和其当前初始标记之间的差异一样。这个新的地方是连接到过渡在相反的方式作为原来的。图3显示了一个具有容量的PN网（为简单起见，这里为1），以及具有重复后向位置的等效PN当然，有限的容量带来了新的活跃性问题，这次是因为拥塞和过流，而不是饥饿和缺乏可用的数据令牌。幸运的是，我们可以使用重要的事实，即上述完成保留了标记图子类，并且在此上下文中将找到解决方案。如稍后将出现的，我们的GALS系统的延迟不敏感松弛同步版本将拥有在包括n个中继站的连接线上保持2n个数据令牌的容量LID理论中产生的最终模型是（第一次近似）具有容量的标记图的延迟有界的简化版本在下文中，我们将称它们为松弛同步系统，因为它们结合了同步特性（所有组件和互连在同一时钟上运行）和用户强加的互连最小延迟（线路传输其信号/数据值的恒定当数据仍在传输中时，计算部分被其周围的shell暂停，使用时钟门控机制。为了尊重固定大小的缓冲能力，跨中继站应用背压拥塞控制协议。48J. Boucaron等人/理论计算机科学电子笔记146（2006）41(a) a有容量Petri网（b）无容量图三.从一个有容量的Petri网（a）到另一个没有容量但具有相同行为的Petri网（b）初始条件和良构条件我们在这里考虑各种问题的适当初始化和结构良好的网络，确保每个语义，无论是同步或异步，饥饿自由（或PN活性），和拥塞自由（或PN安全）。我们还简要地考虑了生产率（或生产能力）的定量问题。我们回顾了一个众所周知的事实，即任何图都可以分解为强连通分量（SCC）的有向无环图（DAG），SCC可能包含单个节点。关于同步组件的同步网络，在时钟节拍时，有效信号/数据必须存在于每条导线上。为了实现这一点（同时假设它来自网络的主要输入），通常要求网络上没有组合回路换句网络图中每个循环的字必须穿过一个寄存器， 它的输出在下一个时钟周期比它收到它作为输入。这里的网络图由组件内部的局部依赖关系加上组件之间的互连这是一个严格的较弱的条件，以强制所有组件输出被锁存（如摩尔时尚），即使第二个假设通常是建议的复合设计风格，实际上是隐含地采用在一些GALS文献。请注意，将长组合导线分割为多个部分的程序只有在并非所有本地输出都被锁存时才能完成。然而，如果是这样的话，人们仍然能够把单位延迟变成任意选择的延迟。关于同步组件的异步网络，如果在每个网络循环回路中存在至少一个令牌（假设每个主输入提供无限的信号/数据流，则网络是活动的（使得所有本地组件无限频繁地被触发）。J. Boucaron等人/理论计算机科学电子笔记146（2006）4149课程）。这是一个直接的结果标记图的活性。这与同步网络上的相应假设密切匹配，前提是寄存器实际上是本地输出上的锁存器（但仍然不是所有输出都需要锁存，每个网络通信周期中只有一个然后，在某种意义上，锁存的输出可以从本地组件中提取，以成为互连FIFO队列的种子初始值当然，在队列中使用更多值进行初始化是可行的，同时保留活性但是，如果从一个完全同步的规范开始，以保持功能等效，那么如何获得这些种子值通常是有问题的考虑松弛同步版本，其中有界容量的通道取代FIFO队列的无界缓冲容量，提出了一种新的活性问题由于潜在的拥塞，本地计算块现在可能会被阻塞，因为它们的输出通道还没有准备好接受他们的结果，他们不能储存没有过度的。这个问题理论上可以通过要求完成的PN网络不允许任何空白周期来解决。在这里，PN完成包括添加后向位置以发挥容量的作用换句话说，完成的图中的每个图循环都应该在其一个位置中至少包含一个令牌标记。图3的网络是一个典型的反例：每个地方的容量为1，左边的网络被阻塞;这在右边的完整网络中被明确表示为空白循环正如我们将在后面看到的，n个中继站的信道具有2n个信号/数据值的缓冲在（常见的）情况下，假设该行仅用一个值初始化，则虚拟向后位置都至少包含一个标记，从而明确禁止空白循环。在GALS文献中经常提到，最终，（简单连接的）松弛同步网络的运行速度不会超过其最慢的简单循环回路的速度首先，任何SCC都被限制在其最慢周期的速度（可能在初始阶段之后，足够的内部令牌可以允许某些部件然后，每当位于SCC前面的部分开始向前运行时，令牌就会在此SCC的入口处累积，直到有界缓冲器被填满，之后别无选择，只能运行SCC行为部分。下游部件也是如此，需要从上游和SCC部件生成数据才能运行。已经确定，最慢循环的速率被计算为数据/令牌的数量与循环上的总体缓冲能力的比率50J. Boucaron等人/理论计算机科学电子笔记146（2006）413中继站我们现在进入这篇文章的主要部分。其目的是实现固定大小的通信信道，将长导线分成多个部分，使得信号/数据可以仅在下一个时钟周期中从一个部分传播到下一个类似地，实现拥塞控制背压所需的信号为此，中继站被引入[21]。它们是特定的硬件元件，在各部分（以及通道两端的外壳）之间提供适当的接口这些元件必须有一些缓冲活动，当然是为了在“路由”上存储数据3.1中继站建模尽管在文献中描述中继站的出版物的数量无论是他们的精确约束表示的物理时间要求（在时钟周期），也不是他们的正式模型和他们的适当的满意度是充分的描述。最接近这一点的论文是[25]。然而，他们没有使用一个纯粹的同步建模在他们的有限状态机（FSM我们现在将处理所有这些问题。见图4。 中继站-框图我们从[25]中借用输入/输出信号的接口如图4所示。数据接收由升高的输入信号val表示（其对应于关于LID的先前文章中的τ它是一个纯布尔值信号（我们可以抽象数据值）。然后，RS将数据与对应的val_out信号。关于背压，RS可以接收具有信号的停止命令中继站接收输入数据，并发出有效信号停止输出。然后，它将其与停止输入信号一起传输（因此停止输出是输入，停止输入是输出）。伪物理要求：重要的是要注意，信号/数据不能从一个部分组合传播到下一个• val in <$→nextval out。J. Boucaron等人/理论计算机科学电子笔记146（2006）4151• 停在外面<$→下一站在里面。另一方面，在stop in和val in（resp.在stop out和val out之间，因为它们属于同一部分。(a)（b）第（1）款图五、 （a）中继站结构（b）中继站同步图因此中继站需要寄存器（例如，IP-IP）来保留接收和传播之间的信号。事实上，如[21]所示，它们需要两个这样的时隙，以防新数据到达而当前数据无法传播。然后，拥塞机制应该保证没有更多的数据可以被接收（从而丢失），因为它们被保留在上游的其他地方。这就是抽象的图5（a）。3.1.1中继站-SyncChart我们在图5（b）中将中继站表示为SyncChart [3，4]，具有显式状态，因此处理输出和下一个状态函数。现在我们介绍这个同步图，它使用中继站内空闲寄存器的数量进行状态SSM（安全状态机）包含3个状态，对应于寄存器的占用：52J. Boucaron等人/理论计算机科学电子笔记146（2006）41当RS中当前没有数据时为空;在这种状态下，RS只是等待有效的输入数据，并将其存储在其主寄存器中（进入半状态）。停止信号被忽略，并且不向上游传播，因为该单元可以吸收TRANSFER。当其保持一个数据时为一半;然后，如果RS小区没有接收到停止停止信号，则RS小区仅发送其当前的、预先接收的信号数据（记住，该组合关系是正确的，在一个区段内）。如果停机，它将保留其数据，但也必须接受来自上游的潜在新数据（因为它尚未发送任何背压保持信号）。在第二种情况下，它变成了满的，第二个值占据了它的如果RS可以发送（停止为假），它要么返回到空状态，要么检索新的有效数据，然后保持相同的状态。另一方面，它仍然不准备传播背压（在下一个时钟周期中），因为由于其自身的缓冲能力，它仍然是不必要的。当它包含两个数据时为满;然后它在任何情况下都产生停止输入信号，将在前一个时钟周期中接收到的保持停止输出信号传播到上游部分如果它自己没有接收到新的停止，那么下游的线路被清除得足够多，以便它可以传输它的数据;否则它保持它并保持停止。注意：只有当为真时才发出信号（用/表示），否则为假。讨论利用这种精确的循环精确模型，例如，人们可以想知道是否可以改进设计，以便能够在充满时既传播其当前数据又接受新数据，保持充满。当然，这在实践中应该是无用的，因为不能接收到val in信号（因为前一个单元，当被警告其停止时，阻止其val out成为当前RS但是如果RS连接到另一个元件，例如，必须检查和保证外壳、约束止动件和/或约束止动件，或者至少必须检查适当的行为。这可以可以很容易地通过对我们的形式化描述进行简单的模型检查来完成3.2正确性性质和形式验证与前面讨论的评论保持一致，可以对中继站或中继站的线路（或稍后，包括贝壳和珍珠的网络）表达许多正确性属性。请记住，活动的正确性标准（被视为摆脱死锁和J. Boucaron等人/理论计算机科学电子笔记146（2006）4153拥塞）已经被建立为PN图标记条件，与第2节中的数据初始化相关联。其他属性包括：• 中继站不能超过100W或低于100W。• 保持数据顺序• 在任何时间点，从一行产生的有效数据的数量相对于输入的数量是有界的：#（val in）+Init line≤#（val out）≤#（val in）+Init line+2×length line其中Init line是最初驻留在RS行中的数据的数量，而length line是RS的数量。• 给定其初始内容，N个中继站的线路不能向其源通知拥塞，除非其接收到足够的类似背压信号• 相反，接收足够的背压保持信号和数据的线路最终将被填充并注意到拥塞。见图6。 塞尔维亚共和国观察员第一个属性可以由图6中的观察者检查。然后，检查将包括证明这样的状态在所有RS中都不可达。第二个属性可以在受限情况下通过用索引“标记”连续的数据信号来建模最简单的方案是交替0和1标签，提供交替位协议类型验证。我们通过模型检查来检查这些属性，用（低范围）常数代替整数参数，并从这些公式构建观察器54J. Boucaron等人/理论计算机科学电子笔记146（2006）414贝壳包装见图7。 外壳-电路4.1贝壳造型在这里，我们的模型非常接近Casu和Macchiarulo的模型[25]。如图7所示。壳方程• 停止i=停止0... Nflipflop out.• V AL INi=val iniflipflop out.• valout t0. N1=锁=锁停下来... N2VALIN0. N3.• flipflopin=（（valiniflipflopout t）stopout t0. N2）（valiniflipflopout<$stopout t0. N2）。如第2节所述，可以考虑贝壳和珍珠具有潜在的零延迟传播的情况（只要不存在仅涉及贝壳的shell需要能够存储已经到达的数据，等待其他仍然丢失的数据。Shell的工作原理如下：J. Boucaron等人/理论计算机科学电子笔记146（2006）4155• 内部pearl的时钟和所有val out i有效输出信号是在所有val in，而stop为false时生成的内部停止信号本身表示所有输入停止输出j信号与输出通道的分离• 只要不是所有其它输入数据都可用，就同时使用给定输入通道的缓冲寄存器• 因此，每当后向停止输出j出现为真，或者前向值输入i为假时，内部Pearl在这种情况下，已经忙碌的寄存器保持其真实值，而其他寄存器可能“刚刚”接收有效数据• 对于其相应寄存器已经被加载（之前接收到数据，但仍然没有被消耗）的所有通道，停止输入I信号被升高，以警告它们在该时钟周期中不要传播任何值。当然，如果数据是当前接收的，则不能发送这样的信号，因为这会引起因果关系悖论（和组合循环）。• 当pearl的时钟上升时，pip-pipop寄存器被重置只有当触发器i已经保持一个值并且停止输出被升高时，信号stop ini才被升高。我们应该记住中继站为了正常运行所要求的约束，即在生产者（在这种情况下是外壳）的每个输出通道上，都有停止j valoutj，它在这里成立。4.2正确性性质和形式验证考虑到中继站，我们想展示这个属性：• 在处理前一个数据之前不能接受数据：保留数据顺序可以简单地检查该属性，因为外壳同步地连接到中继站（或另一外壳），因此当外壳保持数据时，中继站不能向外壳发送任何数据。外壳只能有一个数据从每个通道，如前所述，然后它不能重写或松散的数据，直到所有需要的数据都存在的反应。由于假设互连网络是点对点的，不能丢失数据或改变数据顺序，外壳等待所有数据然后做出反应，因此数据顺序被保留，因此去串行化设计的部分顺序在这种情况下，我们也可以应用交替位协议验证。髋臼杯无死锁，因为我们已经将其确立为PN标记条件。该模型已使用Esterel构建，并使用模型检查器Xeve [9]和56J. Boucaron等人/理论计算机科学电子笔记146（2006）41[26]第二十六话Xeve是一个基于BDD的模型检查器，除了证明属性外，它还可以为组件提供一个规范的最小自动机Autograph允许用户以图形方式显示这个最小自动机（并在状态数保持可管理时识别其特征5其他专题到目前为止，这里开发的理论只考虑了本地同步器组件在每个计算步骤中都在所有输入和输出通道上消耗和产生数据的情况，并且它们都在同一时钟上运行在这种有利的情况下，保证了功能的确定性和连续性因此可以证明，松弛同步版本从与完全同步规范相同的输入流中产生相同的输出流（实际上，流中数据的秩对应于其在同步模型中的时间，从而重建连续时刻的结构有几篇论文在GALS系统的背景下考虑了扩展，但随后忽略了与初始时钟规范的函数对应问题，这是我们重要的正确性标准。这种强有力的假设可以通过多种方式削弱有些是与时钟周期率中组件的各种相对速度和节奏有关，有些是在异步设置中将标记/事件图扩展到Petri网中更一般的子类中，最重要的是将两者联系起来。这个问题在托勒密环境[19]的其他地方也有反映，其中所谓的SDF [18]域对应于事件图的轻微扩展，而在更一般的BDF和DDF域[10]中引入了潜在的冲突选择，其固有问题是静态有界FIFO调度变得不可判定。可以通过允许不同的节奏来扩展框架（以便各种处理块以不同的速度运行，表示为主时钟的整数倍）。更一般地，每个组件可以被分配其自己的时钟，假设所有时钟都是主时钟的子时钟，但不一定是周期性的。然后可以构建多速率/多时钟系统。但是，除非全局速率在每个环路周围完全均衡，否则这可能需要具有不同时钟的事实组件被馈送不相等长度的数据流通常，通过为每个互连信号引入特定的缺失值来尝试具有完全同步规范的链路，使得子时钟仅在以下时刻被定义为滴答作响：J. Boucaron等人/理论计算机科学电子笔记146（2006）4157给定的触发信号不是不存在的。在一般的PN理论中，可以从各种转换（这里是处理元件）向位置提供令牌（这里是因此，它合并了两个数据流（作为一个多路复用器）。 该位置还可以在另一端将其令牌分配给各种消费者，从而操作通过通道携带的数据流的分叉（或解复用器）。换句话说，道-肯是共享的。然后很难想象通道流中数据的秩会回忆起它在完全同步规范中交换的瞬间尽管如此，我们仍然可以设计一个当然，这两种扩展是链接的，因为信道共享要求多个生产或消费不冲突，因此可以确定它们是互斥的（通过在互斥子时钟上驱动成功的问题是保证全球系统中的活性和吞吐量。这应该通过设计适当的时钟脉冲来实现，它应该以适当的速率（延迟和节奏）生成时钟脉冲，以便数据在系统中平稳地传输。在这个方向上存在几个步骤，同步语言中的多锁系统和时钟演算的概念[1，8]。正确性标准是没有组件应该要求存在不存在的信号数据，并且信号数据不会不适当地丢失（有时忽略和丢弃它们是可以还进行了一些研究，以了解表面上的单片同步规范实际上表现出基于独立时钟的异步行为[27]。最后，我们的目标是定义一个通用的GALS建模框架，其中GALS组件可以放在GALS网络中（到目前为止，该框架不是组合的，因为本地组件需要同步）。一个系统将再次由计算和互连通信块组成，这次每个块都有适当的触发时钟，以及一个调度器，该调度器根据它们的外部主时钟和携带控制时钟流信息的几个信号我们的注意力被一位匿名的裁判带到了最近的一些工作中[28，29]，其中中继站被处理并被以循环方式交替携带数据的平行线所取代。需要更多的工作来比较我们的方法与那里提供的正式模型。最后，在以前的论文中经常建议延迟均衡可能是一个解决方案的方向;目的是增加额外的（非物理）潜在的，58J. Boucaron等人/理论计算机科学电子笔记146（2006）41以确保所有正确的输入数据同时提供给本地计算块。然后，在一些语义保持约束下，“非物理的”新的LABERRY可以在网络中上下移动，它们甚至可以用于允许在不太严格的约束下重新合成组分尽管如此，初步的调查表明，“均衡能力”的性质远不明显，而且有一些简单的网络例子，在这些网络中，延迟确实不能被均衡。关于这个有趣的标准的更多调查是有序的。引用[1] P. Amagbedon湖Besnard，and P. Le Guernic.数据流同步语言Signal的实现.在1995年PLDI'95会议记录[2] C. 还有。 Str u ct u raltransgivenB-Eq u ival entPT-Nets. 《应用与Petri网理论》，1981年。[3] C. 还有。 R eac t ina lysofReactiveBehavior s：ASyn ch r o u sAppr oach. 在系统应用中的计算工程，第19[4] C. 好的。 S.S. S.M. 陈文，张文，张文，等.[5] F. Baccelli，G. Cohen，G.J. Olsder和J.- P.样方。同步和线性。Wiley，1992年。[6] A. 本弗尼斯特湾Caillaud和P.勒盖尔尼克。从同步到同步。在Proceedings CONCUR[7] G. Berry 和 G. 贡 蒂 尔 Esterel 同 步 编 程 语 言 ： 设 计 ， 语 义 ， 实 现 。 Science of ComputerProgramming，19（2）：87[8] G. Berry和E.森托维奇多锁艾斯特瑞尔在Proceedings CHARMELNCS，2001年。[9] 阿马尔·布阿里Xeve，一个ESTEREL验证环境。CAV'98：第10届计算机辅助验证国际会议论文集，第500-504页，英国伦敦，1998年史普林格出版社[10] J.T. 巴克使用令牌流模型调度具有有限内存的动态数据流图。加州大学伯克利分校博士论文，1993年。[11] Luca P. Carloni和Alberto Sangiovanni-Vincentelli。结合重定时和回收优化同步电路性能第16届集成电路与系统设计研讨会论文集，2003年。[12] Luca P. Carloni和Alberto L. 桑吉瓦尼-文森泰利 延迟不敏感系统的性能分析和优化。设计自动化会议，第361- 367页[13] 马里奥河 卡苏和卢卡·马基亚鲁洛 一种新的延迟不敏感设计方法。在发援会[14] 作者声明：Agoda.com 格林斯特里特 一个极简的源同步接口。第15届IEEE ASIC/SOC会议论文集，第443-447页，2002年9月[15] Tiberiu Chelcea和Steven M.诺维克混合定时系统的鲁棒接口及其在延迟不敏感协议中的应用。设计自动化会议，第21-26页，2001年。J. Boucaron等人/理论计算机科学电子笔记146（2006）4159[16] F. Commoner，Anatol W.Holt，Shimon Even，and Amir Pnueli. 标记有向图。Journal of Computer and System Sciences，5：511[17] J. Cortadella，A.孔特拉季耶夫湖Lavagno和C. P. Sotiriou。一种去同步的并发模型。2003年第12届国际逻辑与综合研讨会[18] E.A. 李和丹吉 梅塞施米特 同步数据流。 IEEE，1987年。[19] Edward A.李你托勒密计划概述。技术报告，加州大学伯克利分校，2003年7月。[20] C.E. Leiserson和J.B. 萨克斯 重定时同步电路。 1991年，第6期[21] Luca P.Carloni，Kenneth L.McMillan，and Alberto L.Sangiovanni-Vincentelli.延迟不敏感设计理 论 。 IEEE Transactionson Computer-Aided Design of IntegratedCircuitsandSystems，2001。[22] Luca P.Carloni，Kenneth L.McMillan，Alexander Saldanha，and Alberto L.Sangiovanni-Vincentelli.一种基于构造的正确延迟不敏感设计方法。最佳ICAD，1999年。[23] Dumitr uPotop-B ut ucaru，BenobodyCaillau d， andAlbertBeveniste.同步系统中的互补性。在2004年ACSD'04会议记录中[24] 弗拉恩·科伊河。波耶，埃莫斯塔帕阿波耶哈米德，伊冯萨瓦里亚，和米切尔波耶。用软件流水进行同步电路的可编程设计1998年《ICCD会议记录》[25] Mario R.Casu和Luca Macchiarulo延迟不敏感协议的详细实现。FMGALS2003 Proceedings，2003.[26] 我的朋友们都很高兴见到你. A u too/autogra p h. InCAV史普林格出版社[27] 蒙特克·辛格和迈克尔·西奥博尔德。单时钟和多时钟结构的广义延迟不敏感系统。在2004年的时候[28] Syed Suhaib、David Berner、Deepak Mathaikutty、Jean-Pierre Talpin和Sandeep Shukla。介绍和形式化验证延迟不敏感设计的一系列协议。技术报告，弗吉尼亚理工大学，2005年2月。[29] Syed Suhaib、David Berner、Deepak Mathaikutty、Jean-Pierre Talpin和Sandeep Shukla。一个用于延迟不敏感协议验证的函数式编程框架。技术报告，弗吉尼亚理工大学，2005年3月。