58 舒适等：ASC综合后的静态验证方法的研究 2004年 V plation的尺度可以大于0，如果这样的话，Tmng 做ASC设计的验证，将是高效而且快捷的。 path的延时就必须更小，对电路时序的要求就更 形式验证的工具有很多，其中包括Synop sys公 高。 司的Fom ality。当我们对电路进行了修改，比如说 T工ming path 更改了流水线结构，改变了有限状态机，或是从 52 RTL级综合到门级，从门级布局布线转为晶体管 组合逻辑电路 级，都可以做形式验证，比较改变前后两者在功能上 是否改变。形式验证提供了一种静态的回归验证方 法，取代了传统的验证工具。这样做有两个非常明显 的优点：大大节约了验证时间和全面彻底的验证，具 体的原因在介绍静态验证方法时已经提到过。 形式验证是多层次验证，可以比较的类型有 t/ns RTL-to-RTL,RTL-to-gate,还有gate-to-gate R TL- 0 20 30 to-RTL是为了检查新的RTL与改变之前的RTL 图3单时钟同步电路建立/保持时间分析示意图 功能是否一致，在设计不断地修改，加上一些新的功 同理可以分析Hold check。总的来说，它就是要 能，或是改变流水线，改变有限状态机，以提高电路 检测数据是否传得太快。假设当time=0的时候， 性能的情况下，以前的电路己经验证是逻辑正确的， FFI的上升沿时钟使得D端的数据进入触发器，那 但改变后是否仍然正确，就需要将改变前后的RTL 么，数据从FF1的D端传到FF2的D端的时间一定 电路作一个全面的比较，以确保电路的逻辑功能没 要比FF2在time=0的第一个上升沿时钟到达FF2 有改变。RTL~to-gate和gate~to~gate则是比较电路 的CLK端的时间长，否则，就会报Holdtie的 综合前后和布局布线前后的电路，确保电路的逻辑 Vpolatine 功能没有改变。比如，当RTL电路综合后，想改进电 如果设计电路中的静态时序分析结果显示没有 路的性能，为了不用重新综合而直接修改了门级网 V platin,那么电路就没有时序错误，否则，就要根 表，那么就需要用形式验证比较修改前后的门级网 据具体情况，决定是否重新综合。如果对电路的时序 表逻辑是否仍然一致。这一步骤如果采用动态验证 性能要求比较高，可以另外加最大（最小）延迟时间 需要几个星期的话，那么用形式验证只需要几个小 的约束条件，最大（最小）时钟有效宽度，或最大（最 时。 小)时钟的skew tme的约束条件，让静态时序分析 对设计做 建立reference电路 非功能性修政 工具检查电路的时序是否满足这些约束条件。 以上分析了造成电路延时的一些因素，静态时 保存并建立为 序分析建立的时序模型基础和静态时序分析检查的 電路 方法。静态时序分析工作量的大小是由设计电路的 复杂程度和电路中一些特殊情况决定的。设计电路 中还可能出现时钟分频和多时钟的情况，这些本文 验证reference Vs implementation是否一致 中就不再详细讨论了。 4ASC中的形式验证 功能 是否一致多 修改不匹配的地方 形式验证在ASC设计中是一个新的概念，对 是 设计进行形式验证不需要考虑工艺的因素，即可以 不用考虑电路的时序和物理效应。形式验证将需 验证通过 要验证的电路与参考电路进行比较，通过分析两者 图4形式验证流程 在功能方面是否一致。前面我们论述了静态时序分 析的特点和方法。联系形式验证的特点不难发现，这 形式验证的流程如图4所示。从流程图中可以看 两种方法是一种互补的关系，如果将两者结合起来 到，将修改前的设计作为Reference电路，将修改后 1995-2004 Tsinghua Tongfang Optical Disc Co..Ltd.All rights reserved.V iolation 的尺度可以大于0, 如果这样的话, T im ing path 的延时就必须更小, 对电路时序的要求就更 高。 图3 单时钟同步电路建立ö保持时间分析示意图 同理可以分析 Hold check。总的来说, 它就是要 检测数据是否传得太快。假设当 tim e= 0的时候, FF1的上升沿时钟使得D 端的数据进入触发器, 那 么, 数据从 FF1的D 端传到 FF2的D 端的时间一定 要比 FF2在 tim e= 0的第一个上升沿时钟到达 FF2 的 CL K 端的时间长, 否则, 就会报 Holdtim e 的 V iolation。 如果设计电路中的静态时序分析结果显示没有 V iolation, 那么电路就没有时序错误, 否则, 就要根 据具体情况, 决定是否重新综合。如果对电路的时序 性能要求比较高, 可以另外加最大(最小) 延迟时间 的约束条件, 最大(最小) 时钟有效宽度, 或最大(最 小) 时钟的 skew tim e 的约束条件, 让静态时序分析 工具检查电路的时序是否满足这些约束条件。 以上分析了造成电路延时的一些因素, 静态时 序分析建立的时序模型基础和静态时序分析检查的 方法。静态时序分析工作量的大小是由设计电路的 复杂程度和电路中一些特殊情况决定的。设计电路 中还可能出现时钟分频和多时钟的情况, 这些本文 中就不再详细讨论了。 4 A S IC 中的形式验证 形式验证在A S IC 设计中是一个新的概念, 对 设计进行形式验证不需要考虑工艺的因素, 即可以 不用考虑电路的时序和物理效应[ 4 ]。形式验证将需 要验证的电路与参考电路进行比较, 通过分析两者 在功能方面是否一致。前面我们论述了静态时序分 析的特点和方法。联系形式验证的特点不难发现, 这 两种方法是一种互补的关系, 如果将两者结合起来 做A S IC 设计的验证, 将是高效而且快捷的。 形式验证的工具有很多, 其中包括 Synop sys 公 司的 Form ality。当我们对电路进行了修改, 比如说 更改了流水线结构, 改变了有限状态机, 或是从 R TL 级综合到门级, 从门级布局布线转为晶体管 级, 都可以做形式验证, 比较改变前后两者在功能上 是否改变。形式验证提供了一种静态的回归验证方 法, 取代了传统的验证工具。这样做有两个非常明显 的优点: 大大节约了验证时间和全面彻底的验证, 具 体的原因在介绍静态验证方法时已经提到过。 形式验证是多层次验证, 可以比较的类型有 R TL 2to2R TL , R TL 2to2gate, 还有 gate2to2gate。R TL 2 to2R TL 是为了检查新的 R TL 与改变之前的 R TL 功能是否一致, 在设计不断地修改, 加上一些新的功 能, 或是改变流水线, 改变有限状态机, 以提高电路 性能的情况下, 以前的电路已经验证是逻辑正确的, 但改变后是否仍然正确, 就需要将改变前后的 R TL 电路作一个全面的比较, 以确保电路的逻辑功能没 有改变。R TL 2to2gate 和 gate2to2gate 则是比较电路 综合前后和布局布线前后的电路, 确保电路的逻辑 功能没有改变。比如, 当R TL 电路综合后, 想改进电 路的性能, 为了不用重新综合而直接修改了门级网 表, 那么就需要用形式验证比较修改前后的门级网 表逻辑是否仍然一致。这一步骤如果采用动态验证 需要几个星期的话, 那么用形式验证只需要几个小 时。 图4 形式验证流程 形式验证的流程如图4所示。从流程图中可以看 到, 将修改前的设计作为 R eference 电路, 将修改后 58 舒 适等: A S IC 综合后的静态验证方法的研究 2004年 © 1995-2004 Tsinghua Tongfang Optical Disc Co., Ltd. All rights reserved