Static Timing Analysis and Formal Verification for Digital ICs

摘要： 本文介绍了数字集成电路设计中静态时序分析(Static Timing Analysis)和 形式验证(Formal Verification)的一般方法和流程。这两项技术提高了时序分 析和验证的速度，在一定程度上缩短了数字电路设计的周期。本文使用Synopsys 公司的PrimeTime进行静态时序分析，用Formality进行形式验证。由于它们都是 基于Tcl(Tool Command Language)的工具，本文对Tcl也作了简单的介绍。 关键词： 静态时序分析形式验证PrimeTime Formality Tcl

摘要： 本文介绍了数字集成电路设计中静态时序分析（Static Timing Analysis）和 形式验证（Formal Verification）的一般方法和流程。这两项技术提高了时序分 析和验证的速度，在一定程度上缩短了数字电路设计的周期。本文使用 Synopsys 公司的 PrimeTime 进行静态时序分析，用 Formality 进行形式验证。由于它们都是 基于 Tcl（Tool Command Language）的工具，本文对 Tcl 也作了简单的介绍。 关键词： 静态时序分析 形式验证 PrimeTime Formality Tcl

目 录 第一章绪论 1.1静态时序分析 1.2时序验证技术 第二章PrimeTime简介 …(3) 2.1 PrimeTime的特点和功能 2.2 PrimeTime进行时序分析的流程 2.3静态时序分析中所使用的例子 2.4 PrimeTime的用户界面 第三章Tcl与pt_shel1的使用 …(6) 3.1Tc1中的变量 3.2命令的嵌套 3.3文本的引用 3.4 PrimeTime中的对象 3.4.1对象的概念 3.4.2在PrimeTime中使用对象 3.4.3 针对collection的操作 3.5属性 3.6查看命令 第四章静态时序分析前的准备工作 ……(12) 4.1编译时序模型 4.l.1编译Stamp Model 4.1.2编译快速时序模型 4.2设置查找路径和链接路径 4.3读入设计文件 4.4链接 4.5设置操作条件和线上负载 4.6设置基本的时序约束 4.6.1对有关时钟的参数进行设置 4.6.2设置时钟一门校验 4.6.3查看对该设计所作的设置 4.7检查所设置的约束以及该设计的结构 第五章静态时序分析 ……(18) 5.1设置端口延迟并检验时序 5.2保存以上的设置 5.3基本分析 5.4生成path timing report 5.5设置时序中的例外 5.6再次进行分析 第六章Formality简介 …(22)

目 录 第一章 绪论 ………………………………(1) 1.1 静态时序分析 1.2 时序验证技术 第二章 PrimeTime 简介 ………………………………(3) 2.1 PrimeTime 的特点和功能 2.2 PrimeTime 进行时序分析的流程 2.3 静态时序分析中所使用的例子 2.4 PrimeTime 的用户界面 第三章 Tcl 与 pt_shell 的使用 ………………………………(6) 3.1 Tcl 中的变量 3.2 命令的嵌套 3.3 文本的引用 3.4 PrimeTime 中的对象 3.4.1 对象的概念 3.4.2 在 PrimeTime 中使用对象 3.4.3 针对 collection 的操作 3.5 属性 3.6 查看命令 第四章 静态时序分析前的准备工作 ………………………………(12) 4.1 编译时序模型 4.1.1 编译 Stamp Model 4.1.2 编译快速时序模型 4.2 设置查找路径和链接路径 4.3 读入设计文件 4.4 链接 4.5 设置操作条件和线上负载 4.6 设置基本的时序约束 4.6.1 对有关时钟的参数进行设置 4.6.2 设置时钟－门校验 4.6.3 查看对该设计所作的设置 4.7 检查所设置的约束以及该设计的结构 第五章 静态时序分析 ………………………………(18) 5.1 设置端口延迟并检验时序 5.2 保存以上的设置 5.3 基本分析 5.4 生成 path timing report 5.5 设置时序中的例外 5.6 再次进行分析 第六章 Formality 简介 ………………………………(22)

6.1 Formality的基本特点 6.2 Formality在数字设计过程中的应用 6.3 Formality的功能 6.4验证流程 第七章形式验证 …(27） 7.1 fm shel1命令 7.2一些基本概念 7.2.1 Reference Design Implementation Design 7.2.2 container 7.3读入共享技术库 7.4设置Reference Design 7.5设置Implementation Design 7.6保存及恢复所作的设置 7.7验证 第八章对验证失败的设计进行Debug …(32) 8.1查看不匹配点的详细信息 8.2诊断程序 8.3逻辑锥 8.3.1逻辑锥的概念 8.3.2查看不匹配点的逻辑锥 8.3.3使用逻辑锥来Debug 8.3.4通过逻辑值来分析

6.1 Formality 的基本特点 6.2 Formality 在数字设计过程中的应用 6.3 Formality 的功能 6.4 验证流程 第七章 形式验证 ………………………………(27) 7.1 fm_shell 命令 7.2 一些基本概念 7.2.1 Reference Design 和 Implementation Design 7.2.2 container 7.3 读入共享技术库 7.4 设置 Reference Design 7.5 设置 Implementation Design 7.6 保存及恢复所作的设置 7.7 验证 第八章 对验证失败的设计进行 Debug ………………………………(32) 8.1 查看不匹配点的详细信息 8.2 诊断程序 8.3 逻辑锥 8.3.1 逻辑锥的概念 8.3.2 查看不匹配点的逻辑锥 8.3.3 使用逻辑锥来 Debug 8.3.4 通过逻辑值来分析

诸论 第一章绪论 我们知道，集成电路已经进入到了VLSI和LSI的时代，电路的规模迅速上升 到了几十万门以至几百万门。而IC设计人员的设计能力则只是一个线性增长的曲 线，远远跟不上按照摩尔定律上升的电路规模和复杂度的要求。这促使了新的设计 方法和高性能的EDA软件的不断发展。 Synopsys公司的董事长兼首席执行官Aart de Geus曾经提到，对于现在的IC 设计公司来说，面临着三个最大的问题：一是设计中的时序问题：二是验证时间太 长；三是如何吸引并留住出色的设计工程师。他的话从一个侧面表明了，随着IC 设计的规模和复杂度的不断增加，随着数百万系统门的设计变得越来越普遍，时序 分析和设计验证方面的问题正日益成为限制IC设计人员的瓶颈。 对于这些问题，设计者们提出的策略有：创建物理综合技术、开发更快更方便 的仿真器，使用静态时序分析和形式验证技术、推动IP的设计和应用等等。本文 将着重于探讨其中的静态时序分析和形式验证两项技术，在集成电路设计日益繁复 的背景下，它们为IC产品更快更成功地面对市场提供了可能。 §1.1静态时序分析 般来说，要分析或检验一个电路设计的时序方面的特征有两种主要手段：动 态时序仿真(Dynamic Timing Simulation)和静态时序分析(Static Timing Ana -1ysis)。 动态时序仿真的优点是比较精确，而且同后者相比较，它适用于更多的设计类 型。但是它也存在着比较明显的缺点：首先是分析的速度比较慢：其次是它需要使 用输入矢量，这使得它在分析的过程中有可能会遗漏一些关键路径(critical pat -hs),因为输入矢量未必是对所有相关的路径都敏感的。 静态时序分析的分析速度比较快，而且它会对所有可能的路径都进行检查，不 存在遗漏关键路径的问题。我们知道，IC设计的最终目的是为了面对竞争日益激

诸 论 1 第一章 绪论 我们知道，集成电路已经进入到了 VLSI 和 ULSI 的时代，电路的规模迅速上升 到了几十万门以至几百万门。而 IC 设计人员的设计能力则只是一个线性增长的曲 线，远远跟不上按照摩尔定律上升的电路规模和复杂度的要求。这促使了新的设计 方法和高性能的 EDA 软件的不断发展。 Synopsys 公司的董事长兼首席执行官 Aart de Geus 曾经提到，对于现在的 IC 设计公司来说，面临着三个最大的问题：一是设计中的时序问题；二是验证时间太 长；三是如何吸引并留住出色的设计工程师。他的话从一个侧面表明了，随着 IC 设计的规模和复杂度的不断增加，随着数百万系统门的设计变得越来越普遍，时序 分析和设计验证方面的问题正日益成为限制 IC 设计人员的瓶颈。 对于这些问题，设计者们提出的策略有：创建物理综合技术、开发更快更方便 的仿真器，使用静态时序分析和形式验证技术、推动 IP 的设计和应用等等。本文 将着重于探讨其中的静态时序分析和形式验证两项技术，在集成电路设计日益繁复 的背景下，它们为 IC 产品更快更成功地面对市场提供了可能。 §1.1 静态时序分析 一般来说，要分析或检验一个电路设计的时序方面的特征有两种主要手段：动 态时序仿真（Dynamic Timing Simulation）和静态时序分析（Static Timing Ana -lysis）。 动态时序仿真的优点是比较精确，而且同后者相比较，它适用于更多的设计类 型。但是它也存在着比较明显的缺点：首先是分析的速度比较慢；其次是它需要使 用输入矢量，这使得它在分析的过程中有可能会遗漏一些关键路径(critical pat -hs)，因为输入矢量未必是对所有相关的路径都敏感的。 静态时序分析的分析速度比较快，而且它会对所有可能的路径都进行检查，不 存在遗漏关键路径的问题。我们知道，IC 设计的最终目的是为了面对竞争日益激

诸论 2 烈的市场，Time-to-market是设计者们不得不考虑的问题，因此对他们来说，分 析速度的提高，或者说分析时间的缩短，是一个非常重要的优点。 §1.2形式验证技术 我们知道，验证问题往往是IC产品开发中最耗费时间的过程之一，而且它需 要相当多的计算资源。开发一个带有相应的测试向量的测试平台是很费时的工作， 而且它要求开发者必须对设计行为有很好的很深入的理解。而形式验证技术，简单 地说就是将两个设计一一或者说一个设计的两个不同阶段的版本一一进行等效性比 较的技术，由于能够很有效地缩短为了解决关键的验证问题所花费的时间，正在逐 渐地被更多的人接受和使用。这方面的工具有Synopsys公司的Formality和Verp -lex公司的Conformal LEC等。 本文将讨论使用Synopsys的工具PrimeTime和Formality进行静态时序分析 和形式验证的一般方法和流程。本文的第二章简要介绍了PrimeTime的基本功能和 特点。第三章介绍了Tcl在PrimeTime中的基本使用，重点是关于对象和属性的操 作。第四章介绍了在进行静态时序分析之前要作的准备工作。第五章介绍了对一个 具体例子进行静态时序分析的过程。第六章介绍了Formality的基本特点和验证流 程。第七章介绍了对一个具体例子进行形式验证的过程。第八章介绍了对验证失败 的设计进行Debug的各种技巧

诸 论 2 烈的市场，Time-to-market 是设计者们不得不考虑的问题，因此对他们来说，分 析速度的提高，或者说分析时间的缩短，是一个非常重要的优点。 §1.2 形式验证技术 我们知道，验证问题往往是 IC 产品开发中最耗费时间的过程之一，而且它需 要相当多的计算资源。开发一个带有相应的测试向量的测试平台是很费时的工作， 而且它要求开发者必须对设计行为有很好的很深入的理解。而形式验证技术，简单 地说就是将两个设计－－或者说一个设计的两个不同阶段的版本－－进行等效性比 较的技术，由于能够很有效地缩短为了解决关键的验证问题所花费的时间，正在逐 渐地被更多的人接受和使用。这方面的工具有 Synopsys 公司的 Formality 和 Verp -lex 公司的 Conformal LEC 等。 本文将讨论使用 Synopsys 的工具 PrimeTime 和 Formality 进行静态时序分析 和形式验证的一般方法和流程。本文的第二章简要介绍了 PrimeTime 的基本功能和 特点。第三章介绍了 Tcl 在 PrimeTime 中的基本使用，重点是关于对象和属性的操 作。第四章介绍了在进行静态时序分析之前要作的准备工作。第五章介绍了对一个 具体例子进行静态时序分析的过程。第六章介绍了 Formality 的基本特点和验证流 程。第七章介绍了对一个具体例子进行形式验证的过程。第八章介绍了对验证失败 的设计进行 Debug 的各种技巧

PrimeTime简介 3 第二章PrimeTime简介 正如本文前面所提到的，静态时序分析方法由于有着更快的分析速度等优点， 正在被更多的设计者们所重视。PrimeTime是Synopsys的静态时序分析软件，常 被用来分析大规模、同步、数字ASIC。PrimeTime适用于门级的电路设计，可以和 Synopsys公司的其它EDA软件非常好的结合在一起使用。 这一章将简要介绍PrimeTime的基本功能和特点，以及使用PrimeTime进行静 态时序分析的一般过程。 §2.1 PrimeTime的特点和功能 作为专门的静态时序分析工具，PrimeTime可以为一个设计提供以下的时序分 析和设计检查：？？ 令建立和保持时间的检查(setup and hold checks) 令时钟脉冲宽度的检查 ◇时钟门的检查(clock-gating checks) recovery and removal checks ◇unclocked registers ◇未约束的时序端点(unconstrained timing endpoints) master-slave clock separation multiple clocked registers ◇组合反馈▣路(combinational feedback loops) ◇基于设计规则的检查，包括对最大电容、最大传输时间、最大扇出的检查 等。 PrimeTime具有下面的特点： l)PrimeTime是可以独立运行的软件，它不需要逻辑综合过程中所必需的各 种数据结构，而且它对内存的要求相对比较低。 2)PrimeTime特别适用于规模较大的、S0C(system-on-chip)的设计

PrimeTime 简介 3 第二章 PrimeTime 简介 正如本文前面所提到的，静态时序分析方法由于有着更快的分析速度等优点， 正在被更多的设计者们所重视。PrimeTime 是 Synopsys 的静态时序分析软件，常 被用来分析大规模、同步、数字 ASIC。PrimeTime 适用于门级的电路设计，可以和 Synopsys 公司的其它 EDA 软件非常好的结合在一起使用。 这一章将简要介绍 PrimeTime 的基本功能和特点，以及使用 PrimeTime 进行静 态时序分析的一般过程。 §2.1 PrimeTime 的特点和功能 作为专门的静态时序分析工具，PrimeTime 可以为一个设计提供以下的时序分 析和设计检查：？？ ² 建立和保持时间的检查(setup and hold checks) ² 时钟脉冲宽度的检查 ² 时钟门的检查(clock-gating checks) ² recovery and removal checks ² unclocked registers ² 未约束的时序端点（unconstrained timing endpoints） ² master-slave clock separation ² multiple clocked registers ² 组合反馈回路（combinational feedback loops） ² 基于设计规则的检查，包括对最大电容、最大传输时间、最大扇出的检查 等。 PrimeTime 具有下面的特点： 1）PrimeTime 是可以独立运行的软件，它不需要逻辑综合过程中所必需的各 种数据结构，而且它对内存的要求相对比较低。 2）PrimeTime 特别适用于规模较大的、SOC（system-on-chip）的设计

PrimeTime简介 4 在数字集成电路设计的流程中，版图前、全局布线之后已经版图后，都可以使 用PrimeTime进行静态时序分析。 §2.2 PrimeTime进行时序分析的流程 使用PrimeTime对一个电路设计进行静态时序分析，一般要经过下面的步骤： 1)设置设计环境 在可以进行时序分析之前，首先要进行一些必要的设置和准备工作。具体来说 包括了： ◇设置查找路径和链接路径 令读入设计和库文件 ☆链接顶层设 ◇对必要的操作条件进行设置，这里包括了线上负载的模型、端口负载、驱 动、以及转换时间等 令设置基本的时序约束并进行检查 2)指定时序约束(？？timing assertions/constraints) 包括定义时钟周期、波形、不确定度(uncertainty)、潜伏性(latency),以及 指明输入输出端口的延时等。 3)设置时序例外(？？timing exceptions): 这里包括了： ◇设置多循环路径(multicycle paths) 令设置虚假路径(false paths) ◇定义最大最小延时、路径的分段(path segmentation)以及无效的arcs 4)进行时序分析： 在作好以上准备工作的基础上，可以对电路进行静态时序分析，生成constra -int reports path timing reports. 以上仅仅是PrimeTime进行静态时序分析的简单流程，在本文以下的部份中将 会有更详细的叙述

PrimeTime 简介 4 在数字集成电路设计的流程中，版图前、全局布线之后已经版图后，都可以使 用 PrimeTime 进行静态时序分析。 §2.2 PrimeTime 进行时序分析的流程 使用 PrimeTime 对一个电路设计进行静态时序分析，一般要经过下面的步骤： 1）设置设计环境 在可以进行时序分析之前，首先要进行一些必要的设置和准备工作。具体来说 包括了： ² 设置查找路径和链接路径 ² 读入设计和库文件 ² 链接顶层设计 ² 对必要的操作条件进行设置，这里包括了线上负载的模型、端口负载、驱 动、以及转换时间等 ² 设置基本的时序约束并进行检查 2）指定时序约束 (？？timing assertions/constraints) 包括定义时钟周期、波形、不确定度(uncertainty)、潜伏性(latency)，以及 指明输入输出端口的延时等。 3）设置时序例外(？？timing exceptions)： 这里包括了： ² 设置多循环路径（multicycle paths） ² 设置虚假路径（false paths） ² 定义最大最小延时、路径的分段(path segmentation)以及无效的 arcs 4）进行时序分析： 在作好以上准备工作的基础上，可以对电路进行静态时序分析，生成 constra -int reports 和 path timing reports。 以上仅仅是 PrimeTime 进行静态时序分析的简单流程，在本文以下的部份中将 会有更详细的叙述

PrimeTime简介 §2.3静态时序分析中所使用的例子 在本文中，进行静态时序分析时所用的例子是微处理器AMD2910,图2-2给 出了它的顶层的电路图。 ■INTERRUPTDRIVER EN D MAPPING ROMENABLE PIPELINE__ENABLE CARRY_N ○Y_OUTPUT[1:12 CONDITION_CODE CONDITION CODE ENABEE RELOAD INSTRUCTIOND CLOCK ○OVERFLOW D1:1D Figure?2-2AMD2910微处理器 §2.4 PrimeTime的用户界面 PrimeTime提供两种用户界面，图形用户界面GUI(Graphical User Interf -ace)和基于Tcl的命令行界面pt_shell,其运行方式分别是： PrimeTime pt shell 退出的命令是quit、exit或者ˉd。事实上，在GUI界面中通过菜单进行的每一个 操作，都对应着相应的pt_shell的命令。因此，本文以下的章节都只针对于pt shel1来完成

PrimeTime 简介 5 §2.3 静态时序分析中所使用的例子 在本文中，进行静态时序分析时所用的例子是微处理器 AMD 2910，图 2-2 给 出了它的顶层的电路图。 Figure2-2 AMD 2910 微处理器 §2.4 PrimeTime 的用户界面 PrimeTime 提供两种用户界面，图形用户界面 GUI（Graphical User Interf -ace）和基于 Tcl 的命令行界面 pt_shell，其运行方式分别是： ％ PrimeTime ％ pt_shell 退出的命令是 quit、exit 或者^d。事实上，在 GUI 界面中通过菜单进行的每一个 操作，都对应着相应的 pt_shell 的命令。因此，本文以下的章节都只针对于 pt_ shell 来完成

Tcl与pt_shell的使用 6 第三章Tcl与pt_shell的使用 Tcl是Tool Command Language的缩写，由于PrimeTime的命令语言是基于 Tcl标准的，所以在这一章里我想大致介绍一下Tcl在PrimeTime中的基本使用。 除了一些最常用的Tcl命令之外，主要介绍了pt shell中有关对象和属性的操 作。 事实上，大多数synopsys公司的EDA工具都是基于Tcl标准的。例如在第二 章的图2-l中可以看到的综合软件Design Compiler也是。由于都基于Tcl标准， PrimeTime中的大多数命令以及命令参数都和Design Compiler中是相同的。 §3.1Tc1中的变量 我们可以把T℃1看作是一种比较高级的语言，它很容易理解和使用，所以这里 对它的介绍也是很简单的。 与变量有关的有下列操作： 1)定义变量：set变量名变量值 例如： set clock period 10 2)引用变量：$变量名 例如： echo $clock period 3)删除变量：unset变量名 4)打印变量：printvar变量名（无变量名时打印所有变量） 或者： echo$变量名 举个例子，在使用PrimeTime之前，我们可以把它设置成分页显示，以便于浏 览在运行时生成的信息，此时可以使用如下的命令： set sh enable page mode true 如果希望每次运行时PrimeTime总是分页显示，可以到.synopsys_pt..setup文件 中去更改sh enable_page mode变量的设置

Tcl 与 pt_shell 的使用 6 第三章 Tcl 与 pt_shell 的使用 Tcl 是 Tool Command Language 的缩写，由于 PrimeTime 的命令语言是基于 Tcl 标准的，所以在这一章里我想大致介绍一下 Tcl 在 PrimeTime 中的基本使用。 除了一些最常用的 Tcl 命令之外，主要介绍了 pt_shell 中有关对象和属性的操 作。 事实上，大多数 synopsys 公司的 EDA 工具都是基于 Tcl 标准的。例如在第二 章的图 2-1 中可以看到的综合软件 Design Compiler 也是。由于都基于 Tcl 标准， PrimeTime 中的大多数命令以及命令参数都和 Design Compiler 中是相同的。 §3.1 Tcl 中的变量 我们可以把 Tcl 看作是一种比较高级的语言，它很容易理解和使用，所以这里 对它的介绍也是很简单的。 与变量有关的有下列操作： 1）定义变量：set 变量名 变量值 例如： set clock_period 10 2）引用变量：$变量名 例如： echo $clock_period 3）删除变量：unset 变量名 4）打印变量：printvar 变量名（无变量名时打印所有变量） 或者： echo $变量名 举个例子，在使用 PrimeTime 之前，我们可以把它设置成分页显示，以便于浏 览在运行时生成的信息，此时可以使用如下的命令： set sh_enable_page_mode true 如果希望每次运行时 PrimeTime 总是分页显示，可以到.synopsys_pt.setup 文件 中去更改 sh_enable_page_mode 变量的设置

Tcl与pt_shell的使用 §3.2命令的嵌套 在使用PrimtTime的过程中，命令的嵌套经常会被用到。嵌套命令时，用方括 号([门)分隔开每一层的命令，例如： 命令1[命令2[命令3]] 在这样一个例子中，命令3首先被执行，它的结果将被作为命令2的一个参数，然 后依次执行下去。 §3.3文本的引用 在T℃1中，可以使用两种方法来引用文本或者说字符串： 1)弱引用：使用双引号来引用文本。在双引号里出现的变量、命令和反斜杠 不会被转义，仍然保持特殊意义。 2)强引用：使用大括号来引用文本。大括号中的字符串将按照字面上被引 用。 例如：set mydelay10 echo "The value of mydelay is $mydelay" 得到的结果将是：The value of mydelay is l0,而 echo {The value of mydelay is $mydelay} 得到的结果将是：The value of mydelay is$mydelay。 除此之外，可以使用反斜杠来转义一个单一的特殊字符，以及使用expr命令 来得到算术表达式的值。 §3.4 PrimeTime中的对象 §3.4.1对象的概念 在IC设计中，“对象(object)”是一个常用的概念。一般来说，一个设计会 包含以下的对象：Design、Cell、Port、Pin、Net、Clock等。在分析和验证的过 程中，也经常要跟这些对象打交道。因此搞清楚这些概念，才不会在使用软件的过 程中遇到不必要的障碍

Tcl 与 pt_shell 的使用 7 §3.2 命令的嵌套 在使用 PrimtTime 的过程中，命令的嵌套经常会被用到。嵌套命令时，用方括 号([])分隔开每一层的命令，例如： 命令 1 [命令 2 [命令 3] ] 在这样一个例子中，命令 3 首先被执行，它的结果将被作为命令 2 的一个参数，然 后依次执行下去。 §3.3 文本的引用 在 Tcl 中，可以使用两种方法来引用文本或者说字符串： 1）弱引用：使用双引号来引用文本。在双引号里出现的变量、命令和反斜杠 不会被转义，仍然保持特殊意义。 2）强引用：使用大括号来引用文本。大括号中的字符串将按照字面上被引 用。 例如：set mydelay 10 echo "The value of mydelay is $mydelay" 得到的结果将是：The value of mydelay is 10，而 echo {The value of mydelay is $mydelay} 得到的结果将是：The value of mydelay is $mydelay。 除此之外，可以使用反斜杠来转义一个单一的特殊字符，以及使用 expr 命令 来得到算术表达式的值。 §3.4 PrimeTime 中的对象 §3.4.1 对象的概念 在 IC 设计中，“对象(object)”是一个常用的概念。一般来说，一个设计会 包含以下的对象：Design、Cell、Port、Pin、Net、Clock 等。在分析和验证的过 程中，也经常要跟这些对象打交道。因此搞清楚这些概念，才不会在使用软件的过 程中遇到不必要的障碍