局部序时序电路模块综合算法及其性能改进

180《理论计算机科学电子札记》65卷第6期（2002）URL：http://www.elsevie r.n l/l oc ate/en tcs/vol um e 65. ht ml22页基于局部序的时序电路模块综合Eric G Mercer和Chris J. Myers1，2，3犹他大学电气与计算机工程系美国盐湖城米田智宏4东京工业大学工学日本东京郑浩5IBMMicroelectronicsEssexJunction，美国摘要本文提出了一种通过部分降阶加速的定时电路模块综合算法。每个定时电路模块都使用层次规则Petri网（LPN）来指定，这是一种新型的Petri网，允许在每个位置和转换之间注释时序约束和布尔层次表达式。该算法综合了分层设计中的每个模块。它利用偏序约简来减少状态空间探索的其他模块通过考虑一个独立的启用转换的顺序。这种方法可以更好地管理状态爆炸问题，从而使合成时间减少一个数量级以上。改进的合成时间使得能够合成比以前可能的更大类别的定时电路1本研究得到NSF CAREER award MIP-9625014，NSF Japan Program的支持授予INT-0087281、SRC合同97-DJ-487和99-TJ-694、英特尔公司的资助和JSPS联合研究项目。2电子邮件：eemercer@ece.utah.edu3电子邮件：myers@ece.utah.edu4电子邮件地址：yoneda@cs.titech.ac.jp5电子邮件：haoz@us.ibm.com·c2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。美世1811介绍为了实现高性能，设计人员正在试验集成定时电路[26，27，24，12]。然而，以完全手工的方式设计这些电路开发此类CAD工具的一个重要问题是避免状态爆炸。本文提出了两种方法来管理状态爆炸：第一，在定时电路规范的语法抽象;第二，一个精确的模块化综合方法，使用偏序约简。先前的工作已经利用定时自动机来提供电路的低级别模型。它是一种基于状态的规范语言，状态之间的转换不仅由输入定义的布尔函数控制，而且也由时钟赋值控制。他的故事，是一部经典，是一部经典。然而，表达性并不总是综合所必需的;因此，它不必要地基于Petri网的表示是时间自动机的替代电路模型。 它是一种基于转换的规范语言，其中转换由时间和网络的标记状态控制。虽然它比时间自动机表达能力差，但它不仅适用于综合，而且适用于验证[5，13，25，29，30，23]。然而，它的结构在建模时变得非常复杂，即使是简单的逻辑函数[30]。这增加了可达状态空间的大小，并使具体化变得困难[2]。本文使用层次规则Petri网（LPNs），这是一个混合的Petri网和时间自动机。它们是基于转换的，但使用布尔函数。与时间自动机不同，这些函数只定义在输入上，而不是输入和时钟估值。布尔函数是模型结构中的语法抽象。连接性不再在边中显式，而是通过输入的布尔状态暗示。这减少了可达状态空间并简化了规范。LPN是[2，3]中描述的TEL结构的改进。LPN限制了对Petri网形式主义的约束，并促进了可达状态空间上的偏序约简偏序约简是缓解验证中状态爆炸的重要工具[9，28，15，17，4，19]。在[25，31]中，将偏序约简应用于综合。 [25]中的方法是一种展开技术，到不定时的规格。不仅不清楚该技术是否可以有效地应用于定时模型，而且该技术忽略了规范中的层次结构;因此，它在可应用于的系统大小方面受到限制。 [31]中的方法通过对不在目标子电路接口上的信号应用偏序约简来利用规范中的层次结构。 它修改了[28，30]中的部分降阶方法，使其始终包含接口上和目标支路中所有允许的信号顺序。然后使用[21]中的基于状态空间的合成方法来产生精确的电路。这项工作证明了一个显着减少运行时间的状态空间探索的综合问题，并大大增加了大小美世182可以分析的系统。然而，这种方法是绑在时间Petri网。由于模型的结构复杂性，这对缩减状态空间的大小产生了负面影响。本文中的工作将[31]中的模块化合成方法扩展到LPN，以通过语法抽象进一步减少可达状态空间的大小。它首先提出了一种新的时序分析算法的LPNs，可以应用到系统的能力，超出了现有的算法。需要新算法，因为[22，3]中的现有算法仅支持时序信息中的偏序，而不是状态空间探索中的偏序。[22，3]中的定时信息中的部分顺序与[4，19]中的类似，并且与[19]中的方法一样，不需要额外的参考时钟用于同步。新算法的基础实际上是在[19]中提出的，并且仅仅基于变迁的时间分离，但是在[18]中的时间Petri网上的初始实现表明它对于布尔表达式是不正确的，并且对于偏序约简是不完整的;因此，这项工作纠正了算法并完全导出了在约简中保持正确性所必需的条件。偏序约简仅限于安全网，适用于任何类型的选择结构。偏序约简使用来自[28]的不定时方法和定时方法[30，4，19]来确定转换之间的独立性。它扩充了这些定义，在布尔函数存在的情况下纳入了独立性的概念。这些定义不仅与网络的结构有关，还考虑了过渡的时间。本文证明了当网络没有时间依赖的选择时，在线性规划网络上的模块综合方法可以产生精确的电路。该方法的结果在一个数量级减少的时间成本的合成，并使合成更大的一类定时电路比以前可能的。接口抽象是一种常见的方法，通过利用规范中的层次结构来降低基于状态的合成的成本。由于手工执行抽象容易出错，[32]中的工作使抽象过程自动化。它通过从实际系统模型中删除不在目标子电路接口上的转换来改变实际系统模型。尽管简化的模型结构减少了可达状态空间，但该方法在其可以移除的转换方面受到限制，对于布尔函数的指定不高效，并且由于从抽象中获得的保守时序，可能产生不精确的电路[32]。本文中描述的工作不会改变规范。它通过探索不在目标子电路中的独立转换上的单个触发顺序来减少状态空间。本文的组织结构如下。第2节介绍了LPN。第三节提出了一种新的时间状态空间探索算法。第4节形式化了模块综合。第五节给出了一种综合的偏序约简，并证明了它的精确性。在第6节中使用几个示例（包括IBM的实验管道）评估了所提出方法的性能。美世183−∈··¬ ∧¬−→ → {∞}我的天·{∈|{∈ }·{∈|∈ }2层次规则Petri网每个定时电路模块都使用层次规则Petri网（LPN）进行指定。一个LPN是一个对M=（N，E），其中N是一个普通的Petri网，E是水平规则扩展。Petri网是一个四元组N=（T，P，F，μo）。T是一组转换。P是一组位置。F<$（T×P）<$（P×T）是一个幂级数关系。标记是位置的任何子集N的初始标记由μo指定。对于任意变迁t，t=p P（p，t）F 和t=p P（t，p）F分别表示t的源位置和目的地位置源转换和目的地转换的定义类似。水平规则的扩展是一个七元组E=（I，O，νo，wire，Eft，Lft，Lsat）。I和O分别是输入和输出线的有限集合。νo是O中连线的初始布尔状态。 请注意，I中某条连线的初始值必须由在该连线上产生转换的其他模块定义。函数wire：T→（O×{+，−}）<$T是从N到O中的导线上的过渡。 导线u∈O上的跃迁可以是上升的（u+）或下降（u）来改变其布尔状态。如果转型不是上升或下降过渡，则函数返回过渡本身。虽然这样的转换不会改变输出线的状态，但它会改变网络的状态。同样，I中的连接没有映射到转换，因为输入行为必须由其他模块定义有时，可以使用函数wirename（t）来代替，其返回与事件t相关联的连线的名称，或者其返回转换本身（即，如果wire（t）=u+，则wirename（t）=u;如果wire（t）=t，则wirename（t）=t）。 R=F（P×T）是一套规则 对于任何规则r=（p，t）R，r=p和r=t分别是r的源库所和目的地变迁。设Q+是非负有理数的集合。Eft：RQ+和Lft：RQ +是返回规则的最早和最晚触发时间的函数，使得对于所有r∈R，Eft（r）≤Lft（r）。Lsat：R→（{0，1}|我是|→{true，false}）为每个规则分配一个布尔函数。本文将布尔函数限定为信号值的简单合取或析取。图1（a）示出了一个LPN，其描述了具有输入a和b以及输出c的或门的行为。该LPN包括输出信号c上的两个跃迁，即tc+和tc−。在初始状态下，信号c为10w。有在这个LPN中有两个规则从pc−到tc+的规则用最早的触发时间为6，最晚触发时间为9，级别表达式为a/b。类似地，从pc+到tc的规则被注释为最早触发时间为6，最晚触发时间为9，并且表达式一B. 图1（b）和（c）示出了描述两个反相门行为的LPN，这两个反相门将c作为输入并产生输出a和b。定时电路规范由模块M= M1，M2，，M n的集合定义，其中每个模块M k由LPN，（N k，E k）定义。模的集合M必须是不相交的，这意味着对于任何i和j，如果i=j，Ti<$Tj=，Pi<$Pj=，Oi<$Oj=。一个分离美世184pa−−[4、6]ta+cC[4、6]pa+¬ ∧ ¬∨∅∈≤{∈|{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}∈∈pc−tc−a B[6、9]tc+ta tb一aB[6、 9]pc+(a)（b）（c）（d）其他事项Fig. 1. (a)一种或门，输入端为a和b，输出端为c。(b)一个反相器，输入端为c，输出端为a。(c)具有输入端c和输出端b的反相器。(d)电路合成了（a）、（b）和（c）。可以使用以下单个LPN表示模块集合形式：（n Nk，EJ）其中EJ的每个元素只是所有i=1Jn n除了I，它等于i=1Ik−i=1O k. 换句话说，一个信号如果它是组成模块中的输出，则不再被视为输入当IJ=时，模的集合是闭的。 每条线的行为由一组封闭的模块中的某个LPN定义。 而其余本文假设所有感兴趣的电路都是由一个不相交的封闭模块集合定义的。这是本文分析程序的要求。封闭系统的含义是，模块中每个信号的输出到输入因果关系是已知的。图1（a）、（b）和（c）中所示的模块形成了一个不相交且封闭的LPN集合。从这个模块集合的合成电路如图所示1（d）.LPN的定时状态σ是一个三元组（µ，ν，clock），其中µ是一个标记，ν是一个布尔状态，clock：R→Q+是记录时间已启用规则。初始状态σo是（µo，νo，clocko），其中初始标记中的µo，νo是初始布尔状态，对于所有r∈R，clocko（r）=0。 如果Lsat（r）（ν）=真，则称规则r∈R在定义于O上的状态ν中是水平满足的。如果规则r的源位置在标记中（·r∈μ），并且在布尔状态下是水平满足的（Lsat（r）（v）=true），则称规则r是使能的。令Ren（μ，ν）返回给定μ和ν的启用规则的集合，并且R（t）=R r r= t返回转换t的规则集。 如果所有的规则都被使能（R（t）<$Ren（μ，ν）），则称在布尔状态ν的标记μ中的转换被使能。设使能（μ，ν）为给定μ和ν的使能跃迁的有序集合。对于图1所示的初始状态，其中a和b初始为高，c为低，唯一使能的转变是tc+。转换tb−和ta-不被使能，因为c为低电平。如果时间流逝或转换触发，则LPN的状态可能会更改。 时间τQ+可以通过σ=（μ，ν，clock），如果对于所有的tenabled（μ，ν）存在规则r R（t）使得clock（r）+ τ左（右）请注意，如果一个规则超过了它的最后触发时间，它就被称为过期。这种形式主义允许使能转换的规则到期，只要每个转换存在一个可以接受τ而不到期的规则。新的定时状态从σ导出为σJ=（μ，ν，时钟J），其中μ和ν是来自σ的标记和布尔状态;pb−c−[4、6]tb+C[4、6]pb+CB美世185∈- 你好对于所有r Ren（μ，ν），时钟J（r）=时钟（r）+τ。在该示例的初始定时状态中，时间可以被允许前进多达9个时间单位。在9个时间单位之后，启用tc+的规则到期;t hus，tc+被强制触发。如果两个条件成立，则转移tf∈T可以在σ=（μ，ν，clock）中触发：第一，tf∈enabled（μ，ν）;第二，满足每个r∈R（tf）（即，clock（r）≥Eft（r））。新状态由σ导出为σJ=（μJ，νJ，clockJ）其中μJ=（μ−·tf）<$t f·，对于所有u∈O，如果wire（tf）=u+，则为1如果wire（tf）=u−，则νJ（u）=update（t f，ν）（u）=其他方面。对于所有r∈R，Jclock（r）ifr∈（Ren（μ，ν）<$Ren（μJ，νJ））时钟（r）= 000元，否则在这种形式主义中，转换的触发不消耗时间。它只更新标记、布尔状态和时钟函数。 在从上面的σ触发tf的情况下，更新μ以移除源并添加tf的目的地位置以获得μJ;νJ是触发tf，如果wire（tf）=tf，则不改变;以及新状态保持它们相同的时钟值，而所有其它规则被重置。一个Petri网是安全的，如果对于从初始状态开始的每个可达标记，以及对于每个可达标记中启用的每个转移t，以下条件成立：（µ t）t=。安全网在其可达标记集中不具有启用转换的标记，该转换在被触发时，标记更新将在当前标记中已经存在的位置添加到新标记。在实践中，这种限制并没有影响到可以使用的系统类型。使用该方法分析。 从图1所示的初始标记开始射击t c +。1，创建新的定时状态，其中标记为{pc+，pa+，pb+}，布尔状态为（1，1，1），时钟函数保持不变，除了clock（（pc−，tc+））=0。3时间状态类构造定时状态类（TSC）是无限数量的定时状态的有限表示。它用于捕获LPN的无限行为。LPNM =（N，E）的TSC是一个三元组s=（µ，ν，Z），其中µ是标记，ν是线路的当前布尔状态，Z是一组称为区域的关系，表示一组时钟函数[8]。 Z中的关系具有以下形式ta−tb≤c其中ta和tb是从N的转移，c是有理数。该关系被理解为意味着t被发射的时间减去tb被触发的时间小于或等于c;因此，它表示ta和tb之间的时间间隔。定时状态类转换是三元组美世186→→→→我不不∈ ∈ ∈·- ≤ −≤t1 S−（s，t，sJ）表示为s→tsJ，这意味着从TSCs开始，转换t开始燃烧将系统移动到TSCsJ。TSC被构造成使得对于M的定时状态σ，如果在经过某个时间τ后，转换t可以从σ触发为了获得新的状态σJ，则存在TSC转换s→tsJsuch，σ∈s和σJ∈SJ。定时状态类序列（TSCS）是一个连接的TSC转换从系统的初始TSC开始。 这是写如ρ=so1···我不是i−1si···→ s n.符号s i1不si∈ρ平均在TSCSρ中发现定时状态转换si−1→si，如图所示以上 这个符号也用于一组TSCS。令（M）表示M=（N，E）所允许的所有TSCS的集合，一个封闭的、不相交的LPN。该集合从M的初始TSC开始构造。回想一下，N=（T，P，F，μo），E=（I，O，νo，wire，Eft，Lft，Lsat）。M的初始TSC为so=（μo，νo，Zo）。μo和νo直接取自M。初始区域Zo是一组不等式，这些不等式与必须发射以创建初始标记的所有过渡相关。设T（μo）为这些跃迁的集合，使得t T（μo），如果存在p μo，使得t p。如果此集合包含多个变换，则随机选择一个来创建初始区域。假设T（μo）中的跃迁同时触发以创建初始标记;因此，对于所有的ta和tb对，其中ta∈T（μo）和tb∈T（μo），Zo包含一个关系ta−tb≤0。算法1中的函数find（M，s，T）使用bourne again POSET（BAP）定时分析来创建T（M）BAP实现了一个偏序约简，每个TSC的区域。这减少了捕获LPN的所有行为所需的TSC数量[4，19，22，3]。然而，BAP算法仅支持简单的合取或析取表达式。这意味着任何级别表达式都可以是任何大小的单个合取表达式，也可以是每个合取成员中有一条连线的析取表达式。如果一个LPN包含一个析取表达式，在该表达式的一个合取成员中有多条连线，那么下面的BAP分析是不精确的。它可能会错过可到达的TSC。本文仅限于具有此属性的LPN。find（M，s，T）函数是用一个LPNM，s=so，T=0来调用的，从初始TSC开始，它返回所有可能的状态转换的集合，从中可以构造T（M）。函数find（M，s，T）及其各种支持函数通过示例最好地理解。再次考虑图1中的系统。假设函数find（M，s，T）从图1中系统的初始TSC开始;因此，s0=（μ0，ν0，Z0），其中μ0={pa+，pb+，pc−}，ν0=（1，1，0）其中阶数为（a，b，c）;Z0={0≤ta+−tb+≤0，0 ≤tc−−ta+≤0，0 ≤tc−−tb+≤0}; 6且T=0。函数find（M，s，）首先调用算法2中的函数fireable（M，s）。这个函数返回可以从s并发触发的转换集。 这意味着每个转移tf∈fireable（M，s）都可以触发，6两个不等式tatbc1和tbtac2可以表示为c1tbtac2其中C1和C2是有理数。此转换用于所有区域。tnt2我不是美世187∈∈不F算法1find（M，s，T）对于所有tf 可击发（M，s），对于所有的SJ 后继者（M，tf，s），sJ=移除非因果（M，sJ）tfif（s→ sJ）∈/T），则T=T <${（s→sJ）}T=find（M，sJ，T）end if端对端返回T算法2可击发（M，s）Ten=enabled（µ（s），ν（s））如果（|田恩|= 1）然后返回Tenend ifTf=0对于所有的Cg∈因果群（Ten），对于所有的Ca∈因果指派（Cg，Z（s）），Z=设置顺序（Cg，因果分组（Ten），Z（s））Z=设置最小间隔（Cg，Ten，Z）Z=设置最大分离（Ca，Ten，Z）如果（valid（Z）=true），则Tf=Tf可先发射（Ten，Z）如果（Tf=Ten），则返回Tf结束如果结束如果endforendforreturnTf在所有其他可击发转换之前（M，s）。该函数首先导出s中的启用转换集。辅助函数µ（s）和ν（s）分别从参数列表中传入的TSCs=（µ，ν，Z）返回标记和布尔状态。7由于fireable（M，s）被称为s=so，在这个例子中，Ten={tc+}。 此时，该函数返回启用的集合Ten来找到（M，s，T），因为它包含单个使能的转换tc+。然后，函数find（M，s，T）通过调用算法中所示的函数successor（M，tc+，s）来计算由触发tc+美世1887这种表示法是一种类型，用于在只呈现符号时如何在元组中引用成员，并在本演示文稿的其余部分中使用。美世189S联系我们∈S S{}算法3后继（M，tf，s）S=µ=（µ（s）−·tf）tf·ν=update（tf，ν（s））;对于所有的cg∈因果群（tf），对所有tc∈因果指派（cg，Z（s）），Z=集合顺序（cg，因果分组（tf），Z（s））Z=设置最小分色（cg，tf，Z）Z=设置最大分色（tc，tf，Z）如果（valid（Z）=true）则=（μ，ν，Z）如果结束，则结束端返回SRithm 3.该函数首先创建一个空集来保存s的后继TSC，并更新标记和布尔状态以反映tc+的触发。然后，该函数通过查看其每个因果分组中对t c+的因果分配，开始考虑来自s的后继TSC。每个因果分组中的每个因果分配都可能创建一个s的唯一后继TSC。转换t的因果分组是一组转换，必须已触发才能使能t。 对于一个转换tc，t，它必须是t的位置或水平因果关系。一个变迁tc被称为与t位置因果的，如果tc直接连接到t，这意味着存在一个地方p∈·t使得tc∈·p。如果转变tc是导致规则的转变，则转变tc被称为是t的电平因果关系，对于要满足电平的t，这意味着存在规则r R（t）和转换tJT，使得wirename（tJ）=wirename（tc），wire（tJ）=wire（tc），Lsat（r）（v（s））=true，并且Lsat（r）（vJ）=false，其中vJ=update（tJ，v（s））。令因果分组（t）是转换t的所有因果分组的集合。一个跨-如果一个位置连接到具有两个源转换的任何位置，或者如果它在以下任何一个上具有析取电平表达式，则该位置可以具有多个它的规则本例中的函数causal grouping（tc+）返回tc+的两个因果分组：{tc−，ta+}和{tc−，tb+}。在其规则上的选言级别表达式a/b创建了两个分组。 因果分组意味着tc−和ta+或tc−和tb+需要激发tc+。对于转换t的因果分组的因果分配是选择因果分组中的转换，其用于确定t与因果分组中的其他转换之间的间隔。在LPN语义中，启用的转换t可以在满足其每个规则后立即触发，这意味着每个规则r∈R（t）至少已启用Eft（r）时间单位 当满足此条件时，则转换t美世190∈--关于我们can fire是在其规则之一的最晚触发时间，因为它必须在所有规则到期之前触发。这意味着对于任何规则r∈R（t），转换t可以从启用到启动Lft（r）时间单位;因此，因果分配tc到t意味着：(i) tc的触发导致r R（t）中的规则通过一个级别或一个位置被启用;(ii) t的触发发生在tc之后的Lft（r）个时间单位。令因果赋值（cg，Z）是从cg开始的转移的集合，使得每个转移存在于区域Z中的关系中。如果在任何关系Z中都没有找到潜在因果分配的转移，则假定它在Z中不是因果的;因此，它不被考虑。假定初始区域Z包含所有转换的关系，则每个分组tc−，ta+和tc−，tb+。所有这些因果分配都必须考虑，因为每个有效的因果分配都可以从s创建一个唯一的后继状态。因果分组和指定确定分区中过渡的顺序和间隔，以及添加到分区的过渡。 设cg是使能的转变t的因果分组，并且设Z是一个区域集合顺序（cg，causal groupings（tf），Z）函数改变Z中的关系，以使cg的水平因果转换在tf的其他因果分组中的水平因果转换之前发生。这种排序确保每个分组在Z中实际上是因果的。这种排序对于位置因果转换是不需要的，因为LPN的一个安全属性。如果LPN中的某个位置具有多个源转换（创建多个因果分组），则区域中仅存在这些源转换中的一个，使LPN成为单安全的。对于tc+从初始状态触发的例子，设因果分组c g为{tc−，ta+}。在这种情况下，集合顺序函数不需要改变Z中的任何关系来对水平因果转换ta+和tb+进行排序，因为所有转换都同时触发以创建初始区域;因此，两个分组同时启用tc+。然而，如果区域Z被给定为{−2≤tb+−ta+≤ 2}，则对set order的调用会将区域Z更改为{0 ≤ tb+− ta+≤ 2}，这意味着tb+总是在t a+之后的零到两个时间单位之间触发;因此，tc−，ta+分组总是导致tc+从该区域启用。集合顺序函数只改变区它不添加任何新关系。如果在区域中的任何关系中都不存在过渡，则它在区域中不按设置顺序排序。从一个区域触发转换的最早时间是当它的所有规则都满足时。在这个例子中，tc+最早可以触发的时间是tc−触发后的六个时间单位，并且它的表达式ab的值为真;因此， 是tc+和tc−，ta+，和tb+。 如果有另一条规则进入了tc+转换，那么与该规则相关联的任何转换也将在T c+上设置最小间隔。 在LPN语义中，除 非 转换的规则是美世191C+联系我们都是满意的或过期的。设cg为使能转换t的因果分组，并且设Z为区域。函数set min separations（cg，t，Z）将必要的关系添加到Z，以强制延迟t的触发，直到满足其每个规则再考虑一下从下面的例子中触发tc+初始区域Z ={0 ≤ ta+− tb+≤ 0，0 ≤ tc−− ta+≤ 0，0 ≤ tc−− tb+≤ 0}。设因果分组cgbe{tc−，ta +}。 集合min分离s（cg，tc+，Z）函数给 Z 增加了两个 关系：6 ≤ tc+− tc−和6 ≤ tc+− ta+。 这些关系将tc+与两个转换tc−和ta+之间的间隔设置为根据t c+的规则，至少是六个时间单位;因此，无论因果分组中对t c+的因果分配如何，区域都包含满足其规则的关系。然而，如果区域Z被给定为 {− 2 ≤tb+−ta+≤2} ， 那 么 设 置 minseparatio s （ cg ， tc+ ， Z ） 只会 将6≤tc+−ta+关系加到Z上，因为tc−跃迁不在Z中。当区域中缺少来自因果分组的转换时，则不会为该转换添加任何关系。从区域触发转换的最晚时间是在其所有规则到期之前。这意味着转换可能在其任何规则的最晚触发时间触发。令tc为使能转换t的因果分配，令Z为区域。set max separations（tc，t，Z）函数将一个关系添加到Z，以根据与t和tc相关联的规则上的最新触发时间，相对于tc设置t的最新触发。 考虑从初始区域Z={0 ≤ta+−tb+≤0，0 ≤tc−−ta+≤0，0≤tc−−tb+≤0}在r（M ，tc+，s）函数中成功发射t c+的例子。 设因果分组c g为{tc−，ta+}，因果赋值为ta+。集合最大分离度s（ta+，tc+，Z）函数将关系tc+−ta+≤9添加到Z。对于给定的因果群和赋值，在集合顺序、集合最小分离和集合最大分离，Z在成功或（M，tc+，s）中的最终状态为0≤ta+−tb+≤0，0≤tc−−ta+≤0，0 ≤ tc−− tb+≤ 0，6 ≤ tc+− tc−≤ ∞，6≤t−t≤9,a+如果函数success或r（M，tc+，s），however，从初始标记和布尔状态调用，但区域Z =2tb+ta+2，则对于相同的因果群和赋值，在集合顺序、集合最小分离和集合最大分离之后，Z的最终状态是{0≤tb+−ta+≤ 2，6 ≤tc+−ta+≤9}。在时间依赖的选择语义下，集合maxseparations（tc，tf，Z）函数是保守的. 时间相关选择（TDC）语义通过时间来解决冲突。考虑图2（a）中所示的LPN，其中t1与t3相连。事件t3在此LPN中从未触发。在t2被触发之后到达的状态不能在不被强制触发t1的情况下时间转换超过9个时间单位;因此，LPN语义默认实现TDC解析。 现在考虑图2（b）中的选择结构。在这个构造中，t1和t3都再次被启用，只是这一次t3的触发永远不会发生在其规则的最晚触发时间这是因为t1在其规则到期之前被强制触发，美世192t2p[6、9][10，15]t2p[6、9][9、15]C+不t1t3t1t3(a)（b）第（1）款图二、一种定时，允许（a）仅t1点火，（b）t1和t3都点火。Lft（t1）≤Lft（t3）。在这种情况下，设置max separations（t2，t3，Z）将允许t3在其最近的点火时间点火;因此，它是保守的。无效的因果赋值是在将因果分组和赋值的添加的排序关系和分离所产生的区域放入其规范形式中时识别的。一个区域的标准形是通过将最短路径算法应用于由其关系集所隐含的图结构而获得的，其中出现在Z的任何关系中的每个转移都是图的节点，并且节点通过它们的定义的分离连接为加权有向边。如果区域中的两个节点不通过不等式相关，则它们的分离是无限的。一个区域被认为是有效的，如果没有负权重循环存在于图结构中所暗示的它的一组关系。令函数valid（Z）将区域Z置于其标准形式中，如果规范形式有效，则返回true，否则返回false。如果对t的因果赋值阻止规则r∈R（t）在至少Eft（r）时间单位内被启用，则valid（Z）将返回false，因为将存在负权重循环。后继（M，tf，s）函数将来自tf的所有因果分组和分配的所有有效状态添加到集合S。从初始状态调用的函数successor（M，s，tc+）从触发t c+返回单个后继状态。 该状态被给出为sJ=（μJ，νJ，ZJ）其中μJ是（pa+，pb+，pc+），νJ是（1，1，1），Z是0≤ta+−tb+≤0， 0≤tc−−ta+≤0，0 ≤ tc−− tb+≤ 0，6 ≤ tc+− tc−≤ 9，6≤t-t≤9，6≤t-t≤9a+ c+ b+所有的因果分组和赋值都导致这个状态，因为ta+、tb+和tc−在初始状态下同时被激发。然而，这个新国家的区域包含对继承国不重要的关系，在这个新的状态下触发转换。例如，任何关于tc−的触发时间的关系都不再有用，因为它不被新状态中启用的任何转换使用 捕获所有行为所需的TSC数量如果从每个后继状态中的区域中移除不必要的关系，则可以减少LPN。find（M，s，）中的函数remove non causal（M，s j）从sJ中的区域删除不再需要从sJ导出新的未来状态的关系。考虑由触发tc+生成的新状态sJ=（μ，ν，Z），美世193--图1中的LPN的初始状态。在这个例子中，函数remove non causal（M，sJ）从Z（sJ）中删除了变迁tc−、ta+和tb+的关系。s j中的新区域ZJ为{0 ≤ tc+− tc+≤ 0}。因为tc−在任何使能事件的因果分组中不需要，所以删除了涉及t c −的关系 涉及ta+和tb+的关系被删除，因为Z j中的关系表明ta+和tb+永远不会分别与ta−和tb−有因果关系。这是因为tc+总是在t a+和t b+之后至少触发六个时间单位;因此，ta−和tb−的规则永远不会因为ta+或tb+的触发而被启用。在find中，将来自触发t c+的新TSC添加到T中，并进行递归调用以计算来自此新TSC的可触发事件集。在这种情况下，T en集合是ta−，tb−;因此，该函数必须探索这些转换的因果分组和分配，以找到那些可以并发触发的转换来自酿脓链球菌将算法3中的函数扩展到集合，以导出这组转换。对于一个有序的转移集，Ten=（t1，t2，···，tn），令因果分组（Ten）是T en中转移的因果分组的所有可能组合的集合，这意味着因果分组（Ten）=t∈Ten（因果分组（t）），其中是笛卡尔积;因此，如果Ten=（t，u）和因果分组（t）={{a1，a2}，{b1}}和因果分组（u）={{c1，c2}，{d1}}，则因果分组（Ten）={（{a1，a2}，{c1，c2}），（{a1，a2}，{d1}），（{b1}，{c1，c2}），（{b1}，{d1}）};因此，考虑了因果分组的每一种组合 对于本例中的Ten=（ta−，tb−），因果分组（Te n）是{（{ta+，tc−}，{tb+，tc−}）}b，因为ta−和tb−只有一个因果分组。Cg集是因果分组（Ten）中的一个组合函数因果赋值（Cg，Z（s））将因果赋值的所有组合返回到Cg中因果分组的组合。 对于Ten=（t，u），Cg=（{a1，a2}，{c1，c2}），且Z包含Cg中所有跃迁的关系，因果赋值（Cg，Z）={（a1，c1），（a1，c2），（a2，c1），（a2，c2）}. 对于Ten=（ta−，tb−），它的单一因果分组，以及只包含tc+的区域，因果赋值s（Cg，Z（s））=（tc+，tc+）b，因为在Z中找不到ta+和tb+。设置顺序、设置最小分色和设置最大分色函数以类似的方式扩展，只是这些函数不考虑所有的组合。相反，它们可以被定义为单独考虑Ten集合的每个成员;因此，集合顺序函数将C g中的因果分组中的电平因果信号排序为在所有其他因果分组中的电平因果信号之前出现。设置最小分色和设置最大分色功能类似。由此产生的标准形式的有效区域对于这个例子，在集合顺序之后，集合最小分离度和集合最大分离度是{4 ≤ta−− tc +≤ 6，4 ≤tb−− tc+≤ 6，−2≤ ta−− tb−≤ 2}。算法2中的函数can fire first（Ten，Z）返回Ten中可以同时从Z中触发的transi- tions的集合。这个集合是从Z中的关系导出的。 对于每一个转移t f∈ Ten，can firefirst函数检查Z中的所有关系t − t f≤ c，其中t∈ Ten。 如果在这些关系中c ≥ 0，美世194不不{pa+，pb+，pc−}110C+{pa+，pb+，pc+}111 a−b−{pa−，pb+，pc+}011{pa+，pb−，pc+}101B+{pa−，pb−，pc+}001c−{pa−，pb−，a+a+ B+{pa+，pb−，pc−}100{pa−，pb+，pc−}010{pa+}10C+{pa+}11a+ a−{pa−}01c−{pa−}00{pa+，pb+，pc−}110C+{pa+，pb+，pc+}111b−{pa+，pb−，pc+}101 a−B+{pa−，pb−，pc+}001c−{pa−，pb−，a+a+ B+{pa+，pb−，pc−}100{pa−，pb+，pc−}010(a)（b）（c）图三. (a)通过常规合成发现的TSC集合。 (b)的缩减集合 图1（b）的TSC。(c)通过模块化合成发现的TSC集合。然后tf可以在所有其他启用的转换之前触发;因此，tf被添加到返回集合。 对于这个例子，can fire first（Ten，Z）返回{ta−，tb−}，因为−2≤ta−−tb−≤2关系表示ta−和tb−可以在两个时间单位内以任意顺序发生。fireable（M，s）函数添加了将此集合转换为可并发触发的事件集合，并返回以查找（M，s，）。虽然这个例子包含一个单一的组合，其因果分组和分配，其他例子有许多组合;因此，如果T f= Ten的算法返回T f停止探索过程，如上所示。将find（M，s，）应用于图1所示的模块集合，可以找到8个TSC，其中包含10个TSC转换。 图3（a）中示出了可达状态，其中省略了定时信息。4定时电路考虑一个闭模集M={E，S1，···，Si，···，Sn}，其中E是整个电路的环境，Si是第i个子电路的一个特例。设Si=（Ni，Ei）.模块化合成的目标是合成一个由Si指定的子电路。注意，该方法期望合成子电路相对于M中的Si正确工作。然而，它可能在不同的模块集合中相对于Si不正确地工作;因此，合成过程以其他模块E、Si、… …、Sn的方式结束。对于TSCS的集合T和模块Si，简化状态图如下：rsg（T，Si）={（proj（s，Si），t，proj（sJ，Si））| t ∈ T i ii，i（t）sJ∈T}其中proj（s，Si）导致非定时状态，其包括仅具有来自Si中的转变的位置的标记和仅由Si中的输入和输出导线的值组成的状态向量（即，pro j（s，Si）=（μπιPi，ν|IiOi）for不美世195不TT我的天不→我→TJs=（μ，ν，Z））。这表示在T中发生的投射到Si的未定时状态转换的集合，并且改变Si中的连线的值;因此，rsg（T，Si）指定了Si的状态图，不包括任何定时信息。 如果Si被选择为图1（b）中所示的模块，则将rsg（T，Si）应用于图1（b）中的状态图3（a）将导致图中的状态图3（b）款。令T（M）表示M的TSCS的集合，使得每个TSCS从M的初始TSCs0开始。通过将[21]中用于定时电路的合成算法（由合成表示）应用于rsg（T（M），Si）来完成关于M中的Si因此，Ci=synthesis（rsg（T（M），Si））是我们的目标。如果我们考虑S1，，Sn将其作为一个模块，并假设环境中没有内部信号，则等效于非模块综合方法。在模块化合成中，状态图（即，rsg（（M），Si））的值比非模块综合的值小得多，因为许多变量表在rsg（（M），Si）中投影出来。 然而，为了获得（M），该方法必须生成系统的完整状态空间，即使一次只考虑一个子电路Si;因此，只要该方法使用 T（M），则模块综合没有优势本文提出了一个-另一种方法是通过部分的降阶偏序方法的优点有两个方面：首先，不考虑不可见行为的并发顺序;其次，总是合成最佳电路。偏序方法的缺点是仍然需要考虑一部分不可见行为。注意，可以应用抽象技术，然后应用偏序约简。5偏序约简本节扩展了[4，19，28，31]中所示的部分降阶算法，以便它可以处理用于定时电路合成的LPN（M）是通过从每个可达