诸论 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 的各种技巧