CN1344394A

CN1344394A - 使用相对时的电路综合和验证

Info

Publication number: CN1344394A
Application number: CN99815365A
Authority: CN
Inventors: K·S·斯蒂芬斯; S·罗特姆; R·吉诺萨
Original assignee: Intel Corp
Current assignee: Intel Corp
Priority date: 1998-11-02
Filing date: 1999-11-02
Publication date: 2002-04-10
Anticipated expiration: 2019-11-02
Also published as: WO2000026826A1; DE19983695T1; GB2359167B; GB2359167A; GB0112696D0; AU1461200A; US6314553B1; CN100476832C

Abstract

从电路的特性说明综合和/或验证电路的系统和方法。限定了电路中信号的信号排序,其中限定电路中信号的信号排序包括规定电路内多个事件的相对排序。特性说明被修改作为信号排序的函数。然后,电路被综合和或验证作为修改的特性说明的函数。

Description

使用相对时的电路综合和验证

发明领域

本发明涉及集成电路制造，更具体地，本发明涉及根据特性说明来综合和验证定时电路的系统和方法。

背景信息

数字电路中时序的设计是极其困难的挑战。传统的时钟数字设计通过把电路分解成无循环组合逻辑(CL)级和级间时钟锁存器而解决这个问题；时钟周期只被调谐来适应CL级中最坏的传播延时。组合逻辑的特性然后可被规定和被综合，而不用考虑时序。速度无关(SI)的异步电路类似于时钟的CL设计，因为SI电路是与时间无关的，-该特性对于任何门延时都是正确的。

高性能电路，诸如时钟同步的和异步的，从更积极的定时方法得到好处。时钟同步的电路可以本地化地处理时间，允许在电路的不同部分中的调整的和可变的时间。时间上异步的和顺序的电路可以具有大大地增强的性能，代价是对于延时变化的较低的鲁棒性。

度量时序需要传播时间的技术规范或传播时间范围的技术规范。不幸地，度量时序分析会使得复杂性大大地增加，即使在使用简单的本地化的时序时。所以，即使中等大小的定时电路的综合和验证也变得难以驾驭的。而且，精确的度量范围需要布局配置的参量，而在电路被综合时，这些参量可能不存在。

所需要的是规定一个电路的系统和方法，它使得电路不取决于传播延时或传播延时的估值，同时保持无冒险设计的综合和验证。

发明概述

按照本发明的一个方面，描述了根据电路的特性说明执行逻辑综合的系统和方法。限定了电路中信号的信号排序，其中限定电路中信号的信号排序包括规定电路内多个事件的相对排序。特性说明作为信号排序的函数被修改。然后，电路作为修改的特性说明的函数被综合。

按照本发明的另一个方面，描述了根据电路的特性说明执行逻辑综合的系统和方法。限定了电路中信号的信号排序，其中限定电路中信号的信号排序，包括规定电路内多个事件的相对排序。特性说明作为信号排序的函数被修改。然后，电路作为修改的特性说明的函数被验证。

按照本发明的再一个方面，电路包括多个晶体管和连接多个晶体管的两个或两个以上的晶体管的导线。导线作为电路的特性说明的函数被限定和被综合，其中特性说明包括规定在电路内多个事件之间的相对排序的信息。

按照本发明的再一个方面，计算机可读的媒体包括在电路的特性说明中用于代表电路的程序代码，用于限定电路中信号的信号排序的程序代码，其中限定包括规定在电路内多个事件之间的相对排序，用于作为信号排序的函数来修改特性说明的程序代码，以及用于作为修改的特性说明的函数来综合电路的程序代码。

附图简短描述

按照本发明的再一个方面，计算机可读的媒体包括在电路的特性说明中用于代表电路的程序代码，用于限定电路中信号的信号排序的程序代码，其中限定包括规定在电路内多个事件之间的相对排序，用于作为信号排序的函数来修改特性说明的程序代码，以及用于作为修改的特性说明的函数来验证电路的程序代码。

图1a显示按照本发明的逻辑综合系统；

图1b显示按照本发明的逻辑验证系统；

图2显示按照本发明的综合和/或验证逻辑的方法；

图3显示应用图2的协议的计算机可读媒体存储程序代码；

图4a-c显示设置-复位跳动的综合；

图5a-c显示通过应用按照本发明的一系列相对时序假定，简单的二输入端通用的C-单元的演进；

图6a-e显示通过应用按照本发明的一系列相对时序假定，静态AND-ORC-单元的演进；

图7是比较图6a-e的电路的属性的表；

图8a-d是通过应用按照本发明的一系列相对时序假定简化的FIFO的Petri网说明；

图9a-d是通过应用按照本发明的一系列相对时序假定的FIFO的演变；

图10显示3D状态机；

图11显示图9b的电路限定的物理实施方案；

图12显示相对定时的脉冲模式FIFO小区；

图13显示图12的FIFO小区的重排的版本；

图14显示四周期请求-应答握手；

图15是比较图9a-d的属性的表；

图16a和b显示通过应用按照本发明的一系列相对时序假定的Tag Unit(标记单元)的演进；

图17显示图16a所示的Tag Unit(标记单元)的各种元件；

图18是事件排序中时序假定的说明；

图19是同时性时序假定的说明；

图20是早先使能假定的说明；

图21是xyz电路的例子；

图22是对于图21的电路的序假定的自动产生的例子；

图23是按照本发明的、图21的电路的最佳化版本；

图24a和b显示VME总线控制器的I/O接口；

图25a和b显示读和写周期的状态图，分别用于图24a和b的I/O接口；

图26a和b显示状态图的另一个版本，描述图24a和b的I/O接口的完全的特性；

图27显示被使用来代表通用的C单元的符号；

图28a和b显示图24a和b的VME总线控制器的技术规范，以及该技术规范的一个速度无关的实施例；

图29显示假定慢环境的、图28a的电路的一个相对定时的实施例；

图30显示假定慢环境的、图28a的电路的另一个相对定时的实施例；

图31显示假定慢环境和慢总线控制逻辑的、图28a的电路的一个相对定时的实施例；

图32显示图31的电路的时序分析；以及

图33显示图31内的延时垫整，以便满足时序假定。

优选实施例描述

在以下的优选实施例的详细说明中，参考了作为本发明的一部分的附图，以及其中通过说明显示了其中可以实施本发明的特定的实施例。应当看到，其它实施例可被利用，以及可以作出结构性改变，而不背离本发明的范围。

图1a上显示了逻辑综合系统10。图1a显示具有被连接到显示器14与数据输入装置16的处理单元12的工作站。处理单元12包括存储器装置18，被使用来存储按照本发明的程序代码。

逻辑综合系统10使用电路的特性说明来综合该电路。在一个实施例中，被安装在工作站中的程序代码，在被执行时，作为电路中一个或多个信号的相对排序的函数修改特性说明，以及作为修改特性说明的函数来综合该电路。

图1b上显示逻辑验证系统40。图1b显示具有被连接到显示器44与数据输入装置46的处理单元42的工作站。处理单元42包括存储器装置48，被使用来存储按照本发明的程序代码。

逻辑验证系统40使用电路的特性说明来验证该电路的运行。在一个实施例中，被安装在工作站中的程序代码，在被执行时，修改特性说明作为电路中一个或多个信号的相对排序的函数，以及验证该电路作为修改特性说明的函数。

相对定时是代表和对在同步和异步电路中的延时推理的新方法。在一个实施例中，设计者通过对于事件的相对排序作出断言(例如，在信号B进到低电平以前，信号A进到高电平)，而对电路的特性说明加上新的定义。综合和验证算法使用这些断言来限制大的状态空间和改进综合的质量，以及增加验证的容量。在一个实施例中，相对定时约束条件被表示为不等性的系统，它可以通过检验路径延时，而被证明保持在任何系统中。

如上所述，速度无关的电路的综合假定一个延时模型，它对于从被使用来实施它的电路和技术的实际环境所预期的时间特性，可被看作为太保守。相对定时约束条件，通过对环境和电路本身的特性作出某些时序假定，允许设计者简化被综合的电路。然而，这样的电路不一定保持速度无关电路的关键性质，即，电路对于系统元件的所有可能的延时不一定都作出正确反应。为此，重要的是知道在哪些条件下，电路正确地运行。

图2显示把相对定时应用到特性说明的例子。在图2上，在20，电路通过特性说明来描述。在22，在电路内两个或多个信号之间规定一个排序。当信号随时间改变状态时，例如通过限定，这个排序没有被规定。而是，它由更无定形的相对定时关系规定，被限制为描述“信号a有时在信号b之前发生”的关系。在24，特性说明作为对于信号限定的相对定时关系的函数被修改，以及在26，电路作为修改的特性说明的函数被综合或被验证。在一个实施例中，逻辑综合系统10和逻辑验证系统40自动从特性说明产生相对定时假定。在一个这样的实施例中，逻辑验证系统40识别和验证在不是速度无关的电路中的相对定时约束条件。

应用这些方法的程序代码可以通过使用计算机媒体30被分布，如图3所示。

相对定时可以在异步和同步设计中被使用来减小电路的复杂性、功率和面积，以及增加设计的性能和可测试性。例如，相对定时应用到在微处理器设计中使用的电路，当比起400MHz Pentium(奔腾)处理器中的电路时，在性能上提高3倍以及在功率上减小两倍，只是在电路的面积上增加15％。另外，新的电路具有95％伪固定型测试度。

应用相对定时设计方法的其它的好处包括简化了到时钟同步的设计的接口，对于突发模式和复杂门综合机的验证支持，脉冲模式电路，以及手工设计的定时电路。现在通过设计例子描述相对定时的多种利益和应用项，正如下面详细描述的。

在以下的讨论中，采用方程来描述电路中信号之间的关系。在讨论中，输入信号由信号名字下面加杠来表示，倒相信号由在信号名字后面加放一个#来表示，上升沿由在符号名称后面加放一个↑来表示，而下降沿由在符号名称后面加放一个↓来表示。信号名字下面不加杠的信号是输出信号。这些惯例被表示在表1。对于CCS，“.”是顺序运算符，“+”是非确定性选择符，“|”是并行组合，以及“\{a}”是加到信号a的限制运算符。

信号	说明	实例
信号	说明	实例	输入信号	下面加杠	Input
输出信号		Output	输入信号	下面加杠	Input
输出信号		Output	倒相(声称为低的)	井号标记	z#
上升沿	向上箭头	a↑	倒相(声称为低的)	井号标记	z#
上升沿	向上箭头	a↑	下降沿	向下箭头	B↓

表1：符号惯用法

以下的例子是根据采用单个p器件的非时钟触发的多米诺门。异步工具，诸如3D，ATACS和Petrify，可以典型地综合设置-复位跳动以及适当的功能(一个例子被显示在图4a上)。然后，可以使用技术映射来把图4a的功能映射为单变量复位(等效地设置)功能，以及通过使用标准的立足的多米诺门来实施它们，如图4b所示。(图4b显示实施设置-复位跳动的立足的多米诺门(符号和电路)，具有f_r＝ x#，f_s＝ xx ax( b+ c)图4c。)当在设置函数中没有使用复位变量时，代之以使用立足的多米诺门，如图4c所示。(图4c显示实施设置-复位触发器的立足的多米诺门(符号和电路)，具有f_r＝ x#，f_s＝ ax( b+ c)。)

图5a上显示简单的两输入端通用的C单元C＝( a| b).z.C(如在CCS中定义的)和它的CMOS实施方案。给定假定为：

RT1： a＜ bC单元被归结为缓存器：C＝ b.z.C。如果假定被限制为负沿，

RT2： a↓＜ b↓

复位函数只包含 b↓，以及C单元可被实施为立足的多米诺门(图5b)；C＝ a↓. b↓.z↓.( a↑| b↑).z↑.C。通过对于正沿的同样的假定，

RT3： a↑＜ b↑

倒相输入可被应用，以及可以使用多米诺门的非缓存的z#输出。图5c上显示了一个这样的方法。替换地，输出可被缓存用于高负载。“不稳定的”C单元C＝ a. b.z.C+ b.( a.z.C+ b.C)，它是不安全的(允许输入b跳动和撤除)，也可以如上地被同步。

图6a上显示静态AND-ORC单元。这个电路不是电路无关的，但是安全的，只要环境是足够慢的。如果环境快速地动作，则在节点 ac稳定在“1”以前， b↓会立即跟随z↑。以下的要求可被加上，以便校正情形：

RT4：bc↑＜ a↓

RT5：ac↑＜ b↓

RT1-5被称为相对定时(RT)预测。它们规定对于系统10和40的各种时序假定。

在一个实施例中，RT4和RT5由验证工具产生。验证工具通过使用验证算法识别系统中的竞赛。

这些技术规范应用到输入和中间变量，因此，综合电路应当确保根据环境的延时的这些排序。这些要求是与突发模式要求相同的；它们保证电路在新的输入到达之前，是稳定的。以下是另一组预测，它们是较少的限制，因为它们不需要电路稳定性：

RT6：bc↑＜ab↓

RT7：ac↑＜ab↓

图6b上显示一个可能的、可以保证这些预测值保持的实施方案，其中缓存器被加在输出端处。所有的限制可被做成对于电路是本地的，如果缓存器延时足够大，可保证ac↑和bc↑领先于z↑的话。替换地，Petrify综合如图6c所示的静态复合门电路，它可被验证速度无关的。

假定RT2或RT3分别导致图的更简单的静止电路。应当指出，这两个电路实际上是速度无关电路的子电路。

图7概述五个替换的设计。这些结果是基于通过使用驱动六个标准倒相器作为负载的标准库单元器件尺寸而进行的仿真。它们可以在Spice软件中使用MOSIS 0.5μ处理过程参量被仿真。除了静态C单元(SC)以外，所有的实施方案都是无冒险的。

如图7上看到的，速度无关电路(SIC)比所有其它的电路慢，虽然导致一半大小的电路的相对定时假定(SIC-RT)，也提高性能30％。原先的静态C需要最大的电路，但它也相当快。减小的多米诺C单元(GC-RT)上升快15％(只有单个上拉晶体管)，但实际上在下降沿处比gC慢。

相对定时应用于电路开发的一个方法是作为速度无关设计来综合该电路。然后，通过细心应用相对定时假定，设计被简化。在显示单个FIFO单元的设计的图9a-d上，显示这样的方法的一个例子。

单个FIFO单元在CCS中可被规定为如下：

LEFT ＝ li↑.c.lo↑.li↓.lo↓.LEFT

RIGHT＝c.ro↑.ri↑.ro↓.ri↓.RIGHT (1)

FIFO ＝(LEFT|RIGHT)\{c}

其中 c是标记符号以及c是互补标记符号。

表示式(1)包含两个握手处理过程，LEFT和RIGHT. c信号综合两个处理过程，以使得在处理过程可以进行之前 ri必须较低，以及 li必须上升。这个基于处理过程的技术规范可以容易地被映射到图8a的等价的petri网。FIFO的速度无关的版本可以通过使用Petrify被综合。结果的电路显示于图9a。

这种电路限定使用复合门假定，其中倒相器是零延时，或与复合门相组合。这个限定，以及包括分立的倒相器的实际电路实施，通过使用被称为Analyze的软件包，可被证明为遵从在技术规范(1)中的FIFO的技术规范。

图9a的电路为达到速度无关付出重大的延时代价。应当指出，例如，lo↑在三个复合门延时后产生，以及ro个是在四个复合门延时后。如果假定电路可被构建成保证同时的输出比它们由环境应答更快地产生，则性能可被改进。这个假定可用公式表示为：

RT8：lo↑＜ ri↑

RT9：ro↑＜ li↓

通过把这两个相对定时预期值加到技术规范，产生新的技术规范。技术规范可被表示为：

FIFO∧lo↑＜ ri↑∧ro↑＜ li↓ (2)

其中FIFO是来自技术规范(1)的技术规范。这可用图8b的petri-网格表示，其中虚线箭头是相对定时约束条件。

应当指出，两个相对定时约束条件，RT8和RT9，具有输出领先输入的形式。另外，从技术规范看到，能够同时从一对输入进行输出。这正好是突发模式约束条件，其中输入突发是{ li↑ ri↓}，以及输出突发是{lo↑ro↑}。相对定时(RT)预期值限制环境，以使得输出在输入传送到电路之前产生。显示这种突发模式特性的网格图从图8b的petri-网格得出。它显示在图8c。把RT预期值RT8和RT9直接引入技术规范(1)产生图10的Mealy状态机。这个新的形式适用于通过3D进行综合，以及导致图9b的对称电路限定，它对于用零延时倒相器时是无冒险的。

这种对称电路限定遵从技术规范(2)，以及达到对于速度无关的限定的很大的性能改进。无论如何，把图9b的电路限定映射到物理实施方案，带来一个问题。电路不一致，除非倒相器具有零延时。倒相器中不受控制的延时导致严重的竞争，这会做成网络实施方案无法符合技术规范。幸运地，相对定时可被加到物理电路，这样地进行排序，以使得电路可符合技术规范。以下是电路为了避免竞争所必须满足的RT约束条件。

RT10： y2#↑＜ li↑

RT11： y2#＜ ri#

RT12： li2#↓＜ro↑

这些限制由验证算法产生；它们只应用到实际实施方案，以及必须由时序验证器验证，以确保竞争不是严重的。

图9a的速度无关电路的另一个修改方案是可能的。假定技术规范(2)的电路可被放置在带有单个标记的大的环中。如果该环足够大，电路延时将确保标记总是到达空闲的单元。所以，在大的环中，处理过程RIGHT中的握手总是完成，以及RIGHT接口在LEFT接口成为工作的之前将成为空闲的。

SI或BM电路将被安全地使用于这样的环境下。然而，如果利用系统的定时，则可以综合大大地改进的电路(按照功率，性能，面积和可测试性)。RT13是对于这种环境的预期值：

RT13： ri↓＜ li↑

这个假定可用如图8d所示的图形来表示，其中点弧线是在RT13中显示的相对定时关系。

应当指出，点弧线不是因果的弧线； ri在 li可上升之前必须较低，但 ri不能迟于 li。也就是，设计者假定，在点弧线上总是有一个标记；所以，设计者必须查明， ri变成低电平总是在lo变成低电平之前发生。这代表电路运行中的主要改变；LEFT处理不再直接与RIGHT处理过程同步。而是，同步是通过系统时序达到的。

图9c上的电路可以用来自技术规范(2)的3D而与RT预测值RT13同步。信号lo必须被产生成在 li后面足够长，以使得多米诺AND门被完全设置之前不会被禁止。这导致对电路中严重竞争的多个RT约束条件。然而，如果lo信号的时序可以在系统中被正确地调整来满足RT约束条件和消除竞争，则结果是如图9c所示的、快速的、小的、可测试的电路。

脉冲模式FIFO单元也可以通过使用被加到程序(例如，ATACS)的相对定时约束条件而被设计。作为替换的方法，脉冲模式电路可以从RT13得出。

通过如图8d所示的时序假定的过渡特性，ro↓必须领先于 li↑，允许我们一起去除信号 ri↑。这可以通过观看如图12所示的部分的环而被证明。

显然，lo信号正好是 li信号的延时的版本。重排lo器件和磁泡，导致图13的电路，它把LEFT处理过程与RIGHT过程分离。这个重排去除输出lo和输入 ri，把它们做成本地信号。

应当指出，图13上的信号 li#正好是 li倒相。当两个信号 li和 li#都是高电平时，过渡 li↑产生一个短的时间间隔，这将设置多米诺门的输出。这些信号为高电平的持续时间取决于在 li#路径上的延时。这个信号对可被组合到单条线 li中，如果在这条线上的信号作为脉冲运行的话。在图9d上可以看到最后的电路的导出。

对于脉冲模式电路的技术规范为如下：

LEFTP ＝ li↑. c. li↓.LEFT

RIGHTP＝ c：ro↑.ro↓：RIGHT (3)

PULSE ＝(LEFTP|RIGHTP)\{c}

ro＜ li↑

设计可靠的脉冲模式电路是非常困难的。通过了解对于本例来说脉冲模式电路如何被得出，可以看到脉冲电路的某些约束条件。图14显示四周期请求-应答握手。约束条件1到4是与速度无关信令成因果关系的。通过去除应答信号(在本例中是lo和 ri)，我们只留下要求约束条件2p和4p的请求信号。这些约束条件包含最小和最大度量界限。然而，对于这些界限的尺寸的实际需要可以用相对定时弧线来表示。有趣地，这些弧线相应于非常类似于标准请求应当握手的协议。图9d的 li上的脉冲造成输出脉冲ro，如技术规范(3)需要的。如果我们在图14上把 req映射到 li以及 ack映射到ro，则我们看到弧线1是因果的。

然而，如果脉冲太短以致于lo↑( ack↑)不出现，则这个电路失败。这可以通过放置一个相对定时过渡(它需要lo↑( ack↑)在 li↓( req↓)之前)而得以防止。这使得图14上的弧线2是一个RT预测值，稍微限制技术规范。(也可能不限制技术规范特性，如果内部信号跳动，保证多米诺门改变状态的话。)

如果li( req)脉冲太长，则电路也将失败。如果ro↓(ack↓)和y↑在 li↓( req↓)之前出现，则电路将失败。所以，图14上的弧线3是电路工作的必要的RT预测。最后，弧线4被假定为保持给定的RT13。因此，我们具有因果的、和在脉冲模式电路中必须保持的相对定时关系的系统，它直接模仿四个周期的握手。

图15上概述简单FIFO型控制器从速度无关演进到脉冲模式电路的的结果。不同的电路特征根据鲁棒性，性能，面积，功率和可测试性而不同。在图15显示的表上，延时以pS为单位，能量以nJ为单位，面积以晶体管计数为单位，以及可测试度是以固定型覆盖计。

包含无冒险实施方案的唯一电路，即使在技术规范定时假定下，是速度无关电路。然而，该电路的等待时间比使用相对定时的电路慢3到4倍。而且，图9a所示的电路不是完全可测试的，以及可测试度随着电路被使用于更限制的环境而恶化。更积极的定时假定趋向于提高电路的性能，减小面积和功率，以及通常增加可测试度。通过使用相对定时而提高可测试度覆盖的一个原因是因为当电路被不断地最佳化时许多冗余覆盖被去除。

使用相对定时设计的另一个例子可以在一部分可变长度指令译码的设计中看到，这里被称为“标记单元(Tag Unit)”。可变长度指令的译码固有地是串行处理过程，因为任何指令的长度直接取决于所有先前的指令的长度。对于许多计算机结构的指令长度译码的性能直接取决于这种串行译码运行的速度。在这样的结构中的关键部件是用来实施指令串行排序的标记单元。

图16a上显示了一种速度无关的标记单元。在本例中，所有的接口被处理为速度无关接口。关于所有接口是速度无关接口的假定是指所有的接口需要请求/应答握手；这个例子假定四个周期协议。

为完成这个方块需要三个处理过程：

PA＝ r↑.sr↑. sa↑.(sr↓. sa↓|a↑. r↓).a↓.PA

PB＝sr↑. sa↑(sr↓. sa↓|r↑. a↑).r↓. a↓.PB

C4＝( go0| go1| go2| go3).sa.C4

两个PA处理过程在接收到r请求后同步四个阶段握手，而两个PB处理过程是被动的，以及在握手前同步。所以，当 irdy和 ti请求到达和bufreq与to完成时， ti和 irdy信号将被应答以及to与bufreq周期将开始。这是在技术规范中通过重新命名信号和如下组合处理过程而完成的：

IRDY＝ PA[ irdy/r， irdyack/ a， go0/ sr]

TAGIN＝ PA[ ti/r， tia/ a， go2/ sr]

TAGOUT＝ PB[ to/r， toa/ a， go3/ sr]

BUFREQ＝ pB[ bufreq/r， bufack/ a， go2/ sr]

TAGUNIT＝(IRDY|TAGIN|TAGOUT|BUFREQ|C4)\{ go0， go1，

go2， go3， sa}

图17上显示这些处理过程通过使用诸如ATACS那样的程序的实施方案。处理过程PA和PB导致非常有效的实施方案。然而，在本实施方案中，大的或门(OR门)，C-单元，和从标记路径的输入端到输出端传送通过三个状态机的必要性造成重大的延时。

图16b上显示更有效的电路。这个有效的电路是通过使用如上所述的相对定时约束条件而得出的。例如，在速度无关实施方案中的mutex假定导致对于 tagin和tagout接口的后向路径握手的消除。前向信号作为脉冲来处理，所以，如在上面的FIFO例子中处理的。在 irdy和 bufreq路径上请求和应答协议是四个周期和脉冲模式信令的组合，irdyack和bufreq是脉冲。

图16a的速度无关电路与图16b的RT电路的比较表明，RT电路在可测试性，功率和性能方面提供重大的好处。在实时应用项中，来自这种方法的面积的好处甚至是更高的。例如，在可被缩放成达到较高的性能的微处理器中，如果使用较慢的部件，则必须采用较高的缩放因子来满足目标性能。如果使用较慢的SI标记单元，所需要的面积必须大大地激增，如果严格的性能目标要被满足的话。

在一个实施例中，RT约束条件是通过包含支持RT的Analyze版本被产生和验证的。所有的限制可被附加到初始的处理过程技术规范上作为预测值。这简化和澄清电路的初始功能以及所需要的假定，因为每个接口可被规定为呼吁因果同步的、简单的处理过程。把全部的特性限制或定时限制表示为网络，正如以上的FIFO例子中表示的，对于理解小的例子是有帮助的，但对于较大的、实际领域的例子，诸如标记单元，这会是混淆的和不实际的。

在一个实施例中，综合工具的修改版本，诸如Petrify，采用在定时假定下综合无冒险电路的方法。例如，在一个实施例中，为了输送相对定时约束条件，加上了“时间”参量。另外，在一个实施例中，把一个算法加到综合工具中，以便自动得出“合理的”定时假定。最后，在一个实施例中，综合工具提供后向表示法，它表示对于电路的正确的作用所需要的定时限制。下面将详细描述这些特性的每个特性。

在一个综合工具环境下，可以规定三种类型的定时假定：同时发生的事件的点火次序，同时发生的事件的同时发生，和早先使能。为了正确地理解相对定时约束条件的语义，必须引入使能区域和点火区域的概念。给定状态图后，事件a的使能区域EN(a)被定义为其中a是使能的状态组。事件a的点火区域FR(a)被定义为其中允许a进行点火的状态组。

虽然在速度无关电路中，两个概念是相同的(一旦一个事件是使能的，它就可以点火)，但当考虑到定时假定时它们是很大地不同的。在某个状态下一个事件可以是使能的，但在系统达到它的点火区域之前这个事件不能点火。所有这些假定在其中描述STG的输入文件中被规定。它们应当出现在图形(或状态图)技术说明之后和在。end语句之前。

基于同时发生事件的点火次序的定时假定用以下的句法被规定：

.time a＜|b

这个语句的意义为如下，“无论何时a和b同时发生时(即，同时使能但不冲突)，a总是在b之前点火”。

为了说明如何由综合工具(诸如Petrify)作出这个假定，我们将使用图18的例子。我们可以看到，事件和具有不同的关系。它们可以是同时发生的(都在状态s₀被使能)或被排序的(a在s₂被使能，以及b在s₇被使能)。定时假定只应用到其中事件是同时发生的那些状态。

定时假定的应用是指b将不在s₀点火。结果，状态s₁在时域中将成为不可达到的。

对于事件b，Petrify认为，对于事件b的使能来说s₀是“不关心的”状态，即，在逻辑综合后将报告两个不同的解决方案。第一个解决方案是其中b是在s₀时使能的情形。而且，定时假定将使得s₀是不能达到的，因此，b在s₆被达到之前不点火。

第一个解决方案是其中b在s₀时不是使能的情形。这样，将由电路的逻辑来迫使次序a→b，即，对于这个解决方案成为正确的，不需要定时假定。

这两个解决方案可以形式上表示为如下：

{s₆}＝FR(b)EN(b){s₀，S₆}以及Petrify将选择使得逻辑化费最小的、EN(b)的解决办法。

基于同时发生事件的同时出现的定时假定用以下的句法来规定：

.time a＝b@c

图19上显示这个假定的例子。同时性定时假定的意义为如下，“我们取其中a和b是使能的和同时发生的状态。事件c在a和b进行点火以前在任何接连的状态下都不点火。这个假定只应用在c是由a，或b，或二者触发时的情形”。

非正式地，这个假定描述其中在a和b之间的点火时间差是事件c不能区分的情形。察看这个例子，这是指如果c是由b，或由事件a和b“触发”，则系统将产生相同的、可看到的特性。

察看图19的状态图，同时性限制表示，c在状态s₆时不点火，所以，状态s₅将成为不能达到的。另一方面，事件c将被允许在状s₁，s₄和s₆下被使能的。因此，

{s₄}＝FR(c)EN(c){s₁，s₄，s₆}

同时性定时假定可被如下地扩展到更大的数目的事件：

.time a＝b＝c＝d@x，y，z这是指事件a，b，c和d的点火时间被认为是相对于事件x，y和z不可区分的。

基于早先使能的定时假定可用以下的句法被规定：

.time c＞b

这个假定的例子被显示于图20。这个假定的正式的意义为如下，“我们取其中c没有被使能、但在点火b(即，b触发c)以后成为使能的、所有那些状态s-I。然后，状态s_i可潜在地属于EN(c)。”

非正式地，这个假定表示事件c在它必须点火之前可以被使能的。然而，逻辑实施c的延时将保证，c在b以后点火。实际上，这可被看作为冒险的假定，因为信号b和c的逻辑在逻辑综合之前是不知道的。相对定时假定所以需要后验证，以便确保它们的正确性。如果它们在综合后不被保持，则之后必须采取某些动作。例如，设计者可以重新综合电路，而不用不正确的假定，或改变电路的部件的延时(例如，提供晶体管尺寸改变或延时添加)，以使得假定成为正确的。

在以前的例子中，EN(c)和FR(c)被规定为如下：

{s₆，s₈}＝FR(c)EN(c){s₃，s₄，s₆，s₈}

早先使能假定可被扩展到事件链。在先前的例子中，以下的假定也可被规定：

c＞b＞a表示EN(c)可被扩展直到事件的使能。然而，关于b相对于a的使能，没有作出假定。

定时假定可以在Petrify综合熟知的xyz例子时被使用，如图21所示。带有复合门的、速度无关的特性实施方案将为如下：

[x]＝z′(x+y′)；

[y]＝x′z′；

[z]＝y′z+x；

假定x，y和z是输出信号以及y+点火总是在x-点火之前发生。这可以通过察看y+总是在x-之前被使能而从图21直觉推论出，以及在速度无关实施方案中对于信号x的逻辑看来比对于信号y的逻辑更复杂。(当然，所有这些假定将在电路综合后被验证。)

根据这些假定，以下的定时假定可被加到特性技术规范上：

.outputsxyz

.graph

x+y+z+

z+x-

y+z-

x-z-

z-y-

y-x+

.marking{＜y-，x+＞}

.time y+＜|x-

.end

然后，电路可以用以下命令被综合：

petrify xyz.g-cg-topt-eqn xyz.eqn-no

其中任选项“-topt”表示Petrify必须考虑定时假定来导出逻辑。以下的逻辑被得到：

[x]＝z′(x+y′)；

[y]＝x′z′；

[z]＝x；

综合的逻辑是对于信号z的逻辑的巨大的简化。Petrify利用定时假定，认为状态001是不能达到的，以及把z实施为简单的缓存器。

但与解一样重要的是Petrify关于用于每个解的定时假定给出的反馈。在一个实施例中，文件petrify.log包括对于每个信号的不同的解决方案。在一个这样的实施例中，对于z报告以下的解：

z＝x

＞triggers(SET)： x+-＞z+

＞triggers(RESET)： x--＞z-

＞4transistors(2n，2p)

＞Estimated delay：rising＝18.19，falling＝16.69

＞Timing assumptions(concurrency)：y+＜x-

[…other solutions…]

z＝y′z+x

＞triggers(SET)：x+-＞z+

＞triggers(RESET)：(y+，x-)-yz-

＞10transistors(5n，5p)

＞Estimated delay：rising＝18.81，falling＝29.19

＞Speed independent(no timing assumptions)

第一个解相应于对于定时假定得到的解。第二个解相应于速度无关实施方案。对于定时假定和触发信号的解，有两段报告的、重要的信息。

在所示的实施例中，Petrify在定时假定下指示：解决方案z＝x只在y+在之前点火的假定下是正确的。相反，解z＝y’z+x在任何定时假定下是正确的(即，它是速度无关的)。在一个实施例中，由Petrify报告的定时假定不总是与任何定时假定(它是技术规范的一部分)相同的。而是，Petrify将试图报告使得解是正确的、不太严格的假定。

在一个实施例中，在触发信号下，Petrify指示哪些事件被信号的上升和下降过渡触发。应当注意对于z-的触发事件的差别。在“定时的”解中，y+不再触发z-，因为假定它在x-之前点火。当对于综合作出“早先使能”的假定时，这个信息是非常恰当的。

可以作出另一种类型的定时假定。例如，在xyz电路中，y+和z+同时被使能。如果它们的门的延时是相同的，则我们可以认为，y+和z+的点火时间对于事件x-是不能区分的。技术规范现在被读为以下：

.outputsxyz

.graph

x+y+z+

z+x-

y+z-

x-z-

z-y-

y-x+

.marking{＜y-，x+＞}

.time y+＝z+@x-

.end

在执行与以上相同的命令后，得到以下的解：

[x]＝y′；

[y]＝x′z′；

[z]＝x；

算法上产生的、或基于同时使能的、任何定时假定不一定导致正确的解以及必须对于正确性进行检验。再次地，在一个实施例中，文件petrify.log将提供关于定时假定的相关的信息。在一个这样的实施例中，文件petrify.log包含对于x的多个解。这些解可以与速度无关解进行比较(在“其它解”中)：

x＝y′

＞triggers(SET)：y--＞x+

＞triggers(RESET)：y+-＞x-

＞2transistors(1n，1p)

＞Estimated delay：rising＝13.44，falling＝10.75

＞Concurrency reduction：y+＝＞x-

＞Timing assumptions(early enabling)：z+＜x-

x＝y′z′

＞triggers(SET)：y--＞x+

＞triggers(RESET)：(y+，z+)-＞x-

＞4transistors(2n，2p)

＞Estimated delay：rising＝27.50，falling＝11.00

＞Timing assumptions(early enabling)：z+＜x-[...other solutions...]x＝z′(x+y′)

＞triggers(SET)：y--＞x+

＞triggers(RESET)：z+-＞x-

＞8transistors(4n，4p)

＞Estimated delay：rising＝29.38，falling＝11.00

＞Speed independent (no timing assumptions)

解x＝y′是通过在状态101禁止x-(在其中它一开始是使能的)而产生的。这使得状态001不能达到的。但应当指出，在这种情况下，由于定时假定，而不是由于对于x的逻辑没有使能在状态101中的x-，它是不能达到的．这是以下的消息表示的内容：

＞Concurrency reduction： y+＝＞x+换句话说，y+在x-点火之前点火的事实，不需要通过进行定时假定而被验证。这是电路的逻辑已保证的内容。

而且，对于该解有另一个重要的假定：

＞Timing assumptions (early enabling)： z+＜x-这表示x-被使能，以使得它成为与z+同时的(现在，x-在状态110中也是被使能的)。对于正确性的假定是，z+应当在x-之前点火。为了验证在电路级别上的那个假定，可能需要某些附加信息，即，x-在多早的时间被使能？再次地，该信息被提供在触发信号段中。我们可以认识到现在是y+触发x-(在速度无关解决方案中它是z+)。因此，通过组合这些信息，可以确定何时启动事件的使能(触发事件)，以及何时允许该事件点火(当其它同时发生的事件已点火时)。现在，这是设计者决定这些假定是否现实的，或是否可以由实施方案满足。

再者，有另一个感兴趣的、出现在文件中的解决方案，即，x＝y’z’。这个解决方法使得状态001再次可达到的，因为x-在状态101中被使能。但x-也能在状态110中较早地被使能，以及z+＜x-的假定仍旧必须满足。

在一个实施例中，由Petrify的相对定时实施方案提供的信息的重要方面是，不同的定时假定必须被保证用于每个信号的每个不同的解。对于一个信号一个解的选择不影响对于其它门作出的假定。然而，对于每个门的所有的解的组合可以导致一组更简单的限制。在上述的Petrify的实施例中，设计者弄明白限制是如何互动的，仍旧是重要的。Petrify的这个实施例保证的内容是，如果对于每个信号的每个单独的解报告的定时假定被满足，则解将是正确的。

在一个实施例中，Petrify试图自动产生“合理的”定时假定。因为许多假定可以通过观察技术规范的结构而容易地得到，这样的方法允许设计者主要工作在改进电路性能的领域。也就是，Petrify是用于简化设计者的工作的工具，而不是代替设计者工作。实际上，在一个实施例中，Petrify识别已被自动产生的假定，和实际上被使用于每个解的假定。设计者的责任正是保证定时假定的正确性。

以下的模型被考虑用于信号过渡的延时(从它的使能时间到它的点火时间的延时)：

非输入信号：实施非输入信号的每个门具有范围为[1-∈，1+∈]的延时，其中∈＜1/3。因此，两个门的延时总是大于一个门的延时。

输入信号：具有范围为[1+∈，∞]的延时。因此，环境的延时总是大于一个门的延时。

慢输入信号：具有范围为[k，∞]的延时，其中k是任何任意大的常数。延时k表示，使能进行慢输入信号过渡总是允许完成电路中的任何内部活动(例如，使能的非输入信号的点火)。

延时垫整：实施任何非输入信号的任何的门的延时可以在逻辑综合后被伸长，例如，通过晶体管尺寸改变或延时垫整，以满足需要的定时假定。

通过使用这种延时模型的定时假定的自动产生，将用图22的例子来说明。其中i₁，...，i₄是输入信号，以及其中其余信号是输出信号。而且，通过使用以下语句宣布事件i₄+是“慢的”：

.s1ow i₄+

对两个同时发生事件，a和b，的相对次序所作的假定为以下：

(1)如果a总是在b以前被使能，以及a不是输入事件，则a被假定为在(.time a＜|b)之前点火。在图22的例子中，这个假定特别是应用到事件对a+→i₄+和b+→g+。

(2)如果a和b同时被使能，a是非输入事件以及b是输入事件，则a被假定为在(.time a＜|b)之前点火。在图22的例子中，没有这样的情形，但它相应于事件对a+→b+，如果是b输入事件的话。

(3)如果a和b同时被使能，以及二者是非输入事件，则Petrify试探地选择在二者之间的次序(典型地，这个次序确定具有较简单的逻辑的事件将首先点火，虽然当实际的门在逻辑综合后得出时它是不一定是正确的)。

(4)对于可以在非定时的领域中以不同的次序被使能的事件对，不作假定。例如，对于事件i₄+和f+，我们可以发现事件轨迹，其中i₄+首先被使能(例如，i₁+，b+，c+)，以及其中f+首先被使能(例如，i₁+，c+，b+)。

在一个实施例中，如果两个非输入事件，和，被同时使能，以及另一个事件c由a或b(或二者)触发，同时性假定被自动产生(a＝b@c)。在一个这样的实施例，Petrify只对同时事件对进行这种分析。对两个以上的同时事件的假定留给设计者来规定。在图22上有同时性假定的几个例子(例如，b+＝c+@f+和r+＝s+@h+)。

在一个实施例中，当几个非输入事件在它们中间具有触发关系，Petrify自动产生早先使能假定，考虑到门延时可被适当地伸长来满足技术规范的排序关系。在图22的例子中，有在它们中间具有触发关系的事件链(例如，c+→f+→g+→h+和r+→h+)。以下的假定被自动产生：

.time f+＞c+

.time g+＞f+＞c+

.time h+＞g+＞f+＞c+

.time h+＞r+

在一个实施例中，慢输入事件的排序是基本模式假定的推广。在一个实施例中，Petrify用以下约束条件进行设计，即，当其它内部活动在进行中时慢输入事件的延时足够长，以使得电路能够稳定。因为这个约束条件，Petrify可以自动产生对慢事件点火次序的假定。

在一个这样的实施例中，时序分析这样地进行，以使得只有带有慢输入事件的、具有公共的前趋历史的同时发生的非输入事件被假定为首先点火。在察看图22的例子后，其中只有i₄+是慢输入事件，这种直观的概念将更清楚。

通过查验图22可以看到，事件i₄+和g+在它们的历史上具有公共的前趋事件：i₁+。而且，因为i₁+的点火，没有其它输入事件领先于使能i₄+和g+。如果，i₁+的点火时间作为时间分析的起始点来对待(即，t＝0)，则用于自动假定的延时模型表示：g+将在间隔[3(1-∈)，3(1+∈)]中点火，即，三个门延时。另一方面，对于i₄+的点火间隔将是在间隔[k+1-∈，∞)中，其中k可以是任意大。所以，Petrify将得出，对于g+的点火时间总是在对于i₄+的点火之前。

应当指出，这个假定在考虑的事件是h+时不成立的，因为i₄+和g+在它们的历史上没有公共的前趋事件。由于相同的原因，对于i₄+和d+没有作排序假定，因为在满足i₁+公共的前趋事件之前，输入事件(i₃+)领先于d+。

技术上，在两个事件的历史上的这个共同点被称为本地节点。基于本地节点的分析概括被使用于突发模式技术规范的综合的基本节点的概念。突发模式机制工作在假定下，技术规范的每个状态是总的节点，即，在该状态下没有非输入活动是使能的。从技术规范看来，基本模式不允许在环境与电路之间同时发生。

慢输入事件的表示法利用基本模式假定(即，逻辑可被简化)和速度无关假定(即，同时发生没有被牺牲)。作为例子，慢输入事件的定义允许综合具有几个握手信号组的系统。它是通过假定具有每个各个握手的“本地”基本模式运行，但通过在不同的独立的握手组之间也保持同时发生，而做到这一点。一个这样的例子是在下一段中描述的VME总线控制器。

最后，在下面列出对于图22的例子的所有的自动产生的假定：

.time b+＜|a+

.time c+＜|a+

.time a+＜|i4+

.time a+＜|e+

.time a+＜|f+

.time a+＜|g+

.time a+＜|h+

.time c+＜|b+

.time b+＜|i3+

.time b+＜|d+

.time b+＜|f+

.time b+＜|g+

.time b+＜|h+

.time c+＜|i3+

.time c+＜|d+

.time c+＜|i4+

.time c+＜|e+

.time s+＜|h+

.time s+＜|r+

.time a+＜|i4+

.time c+＜|i4+

.time f+＜|i4+

.time g+＜|i4+

.time f+＞c+

.time g+＞f+＞c+

.time h+＞g+＞f+＞c+

.time h+＞r+

.time a+＝c+@f+

.time b+＝c+@f+

.time r+＝s+@h+

即使xyz例子是简单的，在逻辑中重要的改进可以通过把自动定时假定应用到其上而被得到。对于图21所示的xyz例子和不用任何定时假定，将执行以下命令：

petrify xyz.g-cg-atopt-eqn xyz.eqn-no

任选项“-atopt”表示Petrify必须产生自动定时假定。在其中设计者已规定某些假定的情形下，新的假定被加到设计者的假定中。无论如何，Petrify注意使得自动产生的假定与设计者规定的假定是不矛盾的。结果的电路显示于图23。

图23所示的电路是在文件xyz.eqn中由Petrify报告的解。因为定时假定是算法上被产生的，必须对于正确性对它们进行检验。在一个实施例中，这可通过检验文件petrify.log而被完成。例如，在一个实施例中，自动产生以下的假定：

.time z+＜|y+ #concurrency reduction(automatic&

simultaneous) .time y+＜|x- #concurrency reduction(automatic)

.time x+＞y-＞z-＞y+ #early enabling(automatic)

.time x+＞y-＞z- #early enabling(automatic)

.time x-＞z+ #early enabling(automatic)

.time z-＞y+ #early enabling(automatic)

.time z-＞x- #early enabling(automatic)

.time y-＞z- #early enabling(automatic)

.time y-＞z-＞x-＞z+ #early enabling(automatic)

.time y+＝z+@x- #simultaneity(automatic)以及对于解报告以下的信息：

x＝y′

＞triggers(SET)：y--＞x+

＞triggers(RESET)：y+-＞x-

＞2transistors(1n，1p)

＞Estimated delay：rising＝13.44，falling＝10.75

＞Concurrency reduction：y+＝＞x-

＞Timing assumptions(concurrency)：z+＜y+

...

y＝z

＞triggers(SET)：z+-＞y+

＞triggers(RESET)：z--＞y-

＞4 transistors(2n，2p)

＞Estimated delay：rising＝18.19，falling＝16.69

＞Concurrency reduction：z+＝＞y+

＞Speed independent(no timing assumptions)

...

z＝x

＞triggers(SET)：x+-＞z+

＞triggers(RESET)：x--＞z-

＞4transistors(2n，2p)

＞Estimated delay：rising＝18.19，falling＝16.69

＞Timing assumptions(concurrency)：y+＜x-

定时信息可被概括为如下：

(1)要求点火次序z+→y+对于解x＝y’是正确的，但点火次序z+→y+由解y＝z来强制实施，这减小同时发生性，以及使得状态110是不能达到的；以及

(2)要求点火次序y+→x-对于解z＝x是正确的，但点火次序y+→x-由解x＝y’来强制实施，这减小同时发生性，以及使得状态001是不能达到的。

所以，强制实施的同时性减小，保证定时假定的正确性，以及得到速度无关电路。所以，这是关于同时性减小如何不总是意味着性能的损失的例子。逻辑的减小导致更有效的电路。

接着将综合更复杂的电路，强调综合方法具有相对定时假定。图24a和24b上显示VME总线控制器100的I/O接口。控制器100通过使用信号D控制数据收发信机102而控制一个装置104与VME总线106的通信。控制器100也包括信号DSr，DSw，DTACK，LDS和LDTACK。信号LDS和LDTACK是遵从四阶段协议的一对握手信号。信号DSr和DSw遵从带有输出信号DTACK的四阶段协议。DSr和DSw分别表示读(READ)和写(WRITE)周期的开始。相应于读周期的时序图显示于图24b。

相应于控制器100的读周期和写周期的STG分别显示于图25a和25b。

为了综合VME总线控制器100，必须规定技术规范，包括读周期和写周期的特性。这可以通过使用在作为环境的非确定性的模型的Petri网格形式中的选择位置，而被完成。在这种情况下，非决定性起源于：环境可以在先前的周期完成后选择发起读周期或写周期。描述控制器的完整的特性的STG110显示于图26a。某些信号过渡，例如lds+，具有在STG110中的多个事例。在图26a上，下标1和2分别被使用来辨别在读周期和写周期中的事件。

在对于每个不同的标记只有一个过渡的STG120中也有代表整个特性的可能性。STG可以由Petrify通过使用以下命令得到：

petrify vme.g-o vme.1 label

这个结果显示于图26b。然而，这个代表比起先前的是非常不好读的。为此，图26a的STG110被使用来综合控制器100的电路。通过使用该代表，定时假定的技术规范变成为直观得多，因为定时假定对于读和写周期可以独立地被规定。

首先，得出VME总线控制器100的速度无关实施方案。图27上显示对于通用化的C单元的代表所使用的表示法。在执行以下命令后：petrify vme.g-gc-fr10-eqn vme.eqn-log vme.log-o vme.csc

导致图28a和28b描绘的解，其中图28a显示图24a和24b的VME总线控制器的技术规范，以及图28b显示该技术规范的一个速度无关实施例。任选项-fr10在解决CSC冲突时增加探查的广度。一个内部信号，csc0，被插入用来编码状态。

接着，描述慢环境综合。如果假定环境的响应时间足够长，能够使得电路完成它的正在进行的内部活动，则Petrify可以被使能，在规定输入事件为“慢”后产生自动定时假定。这可以通过把“.slowenv”语句包括在技术规范中，以及使用任选项“-atopt”用于自动产生定时假定，而被达到。在一个实施例中，技术规范为如下的形式：

.inputs dsr dsw ldtack

.outputs dtack lds d

.graph

p0dsr+dsw+

p1 lds+/1 lds+/2

#Readcycle

dsr+lds+/1

lds+/1 ldtack+/1

ldtack+/1 d+/1

d+/1 dtack+/1

dtack+/1 dsr-

dsr-d-/1

d-/1 p2p3

#Write cycle

dsw+d+/2

d+/2 lds+/2

lds+/2 ldtack+/2

ldtack+/2 d-/2

d-/2 dtack+/2

dtack+/2 dsw-

dsw-p2p3

#Return to zero

p2lds-

p3 dtack-

lds-ldtack-

dtack-p0

ldtack-p1

.marking{p0 p1}

#Assuming an slow environment

.slowenv

.end以及命令为如下：

petrify vme.g-gc-atopt-eqn vme.eqn-log vme.log-no结果被显示于图29上。注意，在这个解中，没有插入状态信号来解决状态编码问题。这是由于：通常，定时假定使得具有冲突的某些状态不能达到。在本特定的事例中，所有的冲突消失。由Petrify产生的自动定时假定在文件vme.log中被报告为如下：

.time lds-＜|dsr+ #concurrency reduction(automatic)

.time lds-＜|dsw+ #concurrency reduction(automatic)

.time lds-＜|d+/2 #concurrency reduction(automatic)

.time dtack-＜|lds- #concurrency reduction(automatic&

simultaneous)

.time dtack-＜|ldtack- #concurrency reduction(automatic)

.time lds-＜|dsr+ #concurrency reduction(automatic)

.time lds-＜|dsw+ #concurrency reduction(automatic)

.time dtack-＜|ldtack- #concurrency reduction(automatic)

.time lds+/2＞d+/2 #early enabling(automatic)

.time dtack+/1＞d+/1 #early enabling(automatic)

.time dtack+/2＞d-/2 #early enabling(automatic)

.time lds-＞d-/1 #early enabling(automatic)

.time dtack-＞d-/1 #early enabling(automatic)

注意，第四假定(.time dtack-＜|lds-)相应于被使能为同时的两个输出事件的排序。消息“自动与同时”表示两个重要的事情：(1)已自动产生假定，以及(2)两个时间被同时使能，以及当决定点火次序时Petrify给予其中之一以优先权。

这是其中设计者的干预可以是有用的事例之一。例如，设计者可通过把一个定时假定加到技术规范：.time lds-＜|dtack-而选择另一个点火次序。如果对于这个新的定时假定执行相同的命令，vme.log将为如下：

.time lds-＜|dtack- #concurrency reduction(specification)

.time lds-＜|dsr+ #concurrency reduction(automatic)

.time lds-＜|dsw+ #concurrency reduction(automatic)

.time lds-＜|d+/2 #concurrency reduction(automatic)

.time dtack-＜|ldtack- #concurrency reduction(automatic)

.time lds-＜|dsr+ #concurrency reduction(automatic)

.time lds-＜|dsw+ #concurrency reduction(automatic)

.time dtack-＜|ldtack- #concurrency reduction(automatic)

.time lds+/2＞d+/2 #early enabling(automatic)

.time dtack+/1＞d+/1 #early enabling(automatic)

.time dtack+/2＞d-/2 #early enabling(automatic)

.time lds-＞d-/1 #early enabling(automatic)

.time dtack-＞d-/1 #early enabling(automatic)注意，第一定时假定(.time lds-＜|dtack-)现在起源于“技术规范”。所以，Petrify不能产生诸如“.time dtack-＜|lds-”的假定，它与由设计者规定的假定相矛盾。结果的电路显示于图30；可以看到，通过颠倒dtack-和lds-的点火次序，在电路综合方面有改进。

这里可以作出其它的定时假定。例如，从控制器100的技术规范，可以看到，在控制器的两方面(总线和器件)的协议的return-to-zero路径被同时完成。所以，我们能够假定，总线控制路径是这样慢，以致于在与器件的握手完成之前，对于读或写周期(dsr+或dsw+)的任何新的请求决不到达控制器100。这可以通过加上如下的两个新的定时假定而被规定：

.time dtack-＜|dsr+ldtack-＜|dsw+结果的电路显示于图31。这是最低化费的解。

图31的电路(或，被选择用于制造的无论哪个电路)必须被分析，用来确定该假定是否保持。为了进行该分析，首先必须研究在有关每个门的文件vme.log中报告的信息。

SET(dtack′)＝lds′

RESET(dtack′)＝ldtack lds

[dtack]＝duck′ (output inverter)

＞triggers(SET)： lds--＞dtack-

＞triggers(RESET)： ldtack+/1-＞dtack+/1 ldtack+/2-＞

dtack+/2

＞5transistors(3n，2p)

＞Estimated delay：rising＝22.94，falling＝16.69

＞Concurrency reduction：lds-＝＞dtack-

＞Timing assumptions(early enabling)：d+/1＜cdtack+/1

d-/2＜dtack+/2…

lds′＝dsw′dsr′

[lds]＝lds′(output inverter)

＞triggers(SET)：(dsr-，dsw-)-＞lds-

＞triggers(RESET)：dsr+-＞lds+/1 dsw+-＞lds+/2

＞6transistors(3n，3p)

＞Estimated delay：rising＝18.44，fallmg＝24.50

＞Timing assumptions(concurrency)：ldtack-！dsw+ldtack-！dsr+

＞Timing assumptions(early enabling)：d+/2＜lds+/2 d-/1＜lds-

…

SET(d′)＝dsr′ldtack

RESET(d′)＝dsw ldtack′+dsr ldtack

[d]＝d′(outputinverter)

＞triggers(SET)：dsr--＞d-/1 ldtack+/2-＞d-/2

＞triggers(RESET)：ldtack+/1-＞d+/1(dsw+，ldtack-)-＞d+/2

＞10transistors(6n，4p)

＞Estimated delay：rising＝29.88，falling＝29.25

＞Concurrency reduction：ldtack-＝＞d+/2

＞Timing assumptions(concurrency)：ldtack-＜dsr+

在图32上给出和概括定时假定。在该图上，我们可区分三种类型的时序弧线：

(1)同时性减小弧线，它表示由路径(1ds-→dtack-和ldtack-→d+/2)增强的附加因果性关系。这些不是必须对于电路是否正确而进行验证的定时假定。

(2)点火次序弧线，它表示对于电路的同时发生事件的假定的点火排序。这些是必须通过对电路的延时垫整而被验证或增强的定时假定。

(3)早先使能弧线，它表示对于早先使能的事件的新的触发事件。例如，在读周期中由d-/1触发的事件lds-现在由dsr-触发。这个信息通过组合早先使能定时假定和对于每个解报告的触发事件表而被提取的。这些是必须对于电路是否正确而进行验证的定时假定。在上述的例子中，例如，必须验证：事件d-/1将在事件lds-之前发生。

作出假定ldtack-→dsr+和ldtack-→dsw+，特征是总线控制逻辑的速度。所以，它们可被认为是满意的。然而，对早先使能的假定必须被细心地分析，因为它们的正确性取决于得出的逻辑的实际延时。

所有的早先使能假定依赖于，门电路d的延时短于lds和dtack的延时。不幸地，通过查看图31，可以看到，门d比其它的门复杂。关于门d的延时短于lds和dtack的延时的假定不能保持；所以，图31的电路必须被修改成使得这些假定保持正确。图33显示一个可能的解。延时d1应当保证，lds+/2和lds-将分别比d+/2和d-/1更迟地点火，即使它们被同时触发。延时d2应当保证，dtack+/1和dtack+/2将分别比d+/1和d-/2更迟地点火，

注意，图33所示的解只是将信号ldtack+对dtack+的触发影响延时。另一个解是在门电路dtack的输出端处加上延时，但这也将dtack-延时，这对于电路的正确的功能是不必要的。因此，可以看到，由Petrify报告的信息允许设计者定做电路，以使得定时假定对于信号的单独的事件是满足的，而不是对于信号的所有事件。

相对定时是推导出设计的有用的方法。数据手册中的波形被呈现成使得突出信号与过渡之间的关系。可以使用相对定时来归档系统，以及综合控制器和验证系统的正确性。综合和验证算法可被设计来直接支持这个概念，其中时间被表示为类似于特性的或因果的关系的关系。相对定时可以按希望地主动地或保守地被应用。在限制的形式下，可以发现由于倒相器延时造成的在速度无关实施方案中的竞争，以及相对定时可被使用来表明竞争是否严重。

相对定时不排除度量的或绝对的时序。度量的时序在实施方案中，实质上必须被加到RT预测值，证明它们保持。而且，许多RT预测值在关系中需要一定量的备用部分，或建立和保持时间。电路的鲁棒性和可靠度可以直接依赖于RT约束条件上的备用量。

虽然这里显示和描述特定的实施例，但本领域技术人员将会看到，被计算来达到同一个目的的任何安排可被替换用于所显示的特定的实施例。所以，打算本发明只由权利要求及其等价物限制。

Claims

1.一种从电路的特性说明执行逻辑综合的方法，包括：

限定电路中信号的信号排序，其中限定包括规定电路内多个事件的相对排序；

修改特性说明作为信号排序的函数；以及

综合电路作为修改的特性说明的函数。

2.按照权利要求1的方法，其中规定相对排序包括接收设计者特定的定时假定。

3.按照权利要求2的方法，其中设计者特定的定时假定被表示为相对定时(RT)预测值。

4.按照权利要求1的方法，其中规定相对排序包括在处理器内自动产生定时假定。

5.按照权利要求4的方法，其中定时假定被表示为RT预测值。

6.按照权利要求1的方法，其中综合包括验证电路保持多个事件的相对排序。

7.按照权利要求6的方法，其中相对排序被表示为RT预测值。

8.从电路的特性说明执行逻辑验证的方法，包括：

修改特性说明作为信号排序的函数；以及

验证电路作为修改的特性说明的函数。

9.按照权利要求8的方法，其中规定相对排序包括接收设计者特定的定时假定。

10.按照权利要求9的方法，其中设计者特定的定时假定被表示为RT预测值。

11.按照权利要求8的方法，其中规定相对排序包括在处理器内自动产生定时假定。

12.按照权利要求11的方法，其中定时假定被表示为RT预测值。

13.按照权利要求8的方法，其中综合包括验证电路保持多个事件的相对排序。

14.按照权利要求13的方法，其中相对排序被表示为RT预测值。

15.一种使用电路的特性说明来综合该电路的逻辑综合系统，系统包括：

工作站，具有显示装置和输入装置；以及

被安装在工作站中的程序代码，其中程序代码在被执行时，规定电路内多个事件的相对排序，修改特性说明作为信号排序的函数；以及综合该电路作为修改的特性说明的函数。

16.按照权利要求15的逻辑综合系统，其中相对排序被表示为RT预测值。

17.按照权利要求15的逻辑综合系统，其中系统还包括验证程序代码，其中验证程序代码在被执行时，验证该电路作为修改的特性说明的函数。

18.按照权利要求15的逻辑综合系统，其中输入装置能够输入设计者特定的定时假定，以及其中程序代码修改特性说明作为设计者定时假定的函数。

19.按照权利要求15的逻辑综合系统，其中系统还包括相对定时程序代码，其中相对定时程序代码包括用于从特性说明自动产生定时假定的代码。

20.一种使用电路的特性说明来验证该电路的逻辑验证系统，系统包括：

工作站，具有显示装置和输入装置；以及

被安装在工作站中的程序代码，其中程序代码在被执行时，规定电路内多个事件的相对排序，修改特性说明作为信号排序的函数；以及验证该电路作为修改的特性说明的函数。

21.按照权利要求20的逻辑验证系统，其中相对排序被表示为RT预测值。

22.按照权利要求20的逻辑验证系统，其中输入装置能够输入设计者特定的定时假定，以及其中程序代码修改特性说明作为设计者特定的定时假定的函数。

23.按照权利要求20的逻辑验证系统，其中系统还包括相对定时程序代码，其中相对定时程序代码包括用于从特性说明中自动产生定时假定的程序代码。

24.一种电路，包括：

多个晶体管；以及

连接多个晶体管的两个或两个以上的晶体管的导线；其中导线被限定以及被综合为电路的特性说明的函数，其中特性说明包括规定在电路内多个事件之间的相对排序的信息。

25.按照权利要求24的电路，其中规定相对排序的信息被表示为一个或多个RT预测值。

26.一种包括其上具有指令的、计算机可读的媒体的物体，其中指令在计算机中被执行时创建一个系统，用于：

通过电路的特性说明，表示一个电路；

修改特性说明作为信号排序的函数；以及

综合电路作为修改的特性说明的函数。

27.一种包括其上具有指令的、计算机可读的媒体的物体，其中指令在计算机中被执行时创建一个系统，用于：

通过电路的特性说明，表示一个电路；

修改特性说明作为信号排序的函数；以及

验证该电路作为修改的特性说明的函数。