EDA软件巡礼6：Formality

EDA软件巡礼6：Formality

参考链接：http://poqsoft.com/eda/1116.html
                http://poqsoft.com/eda/page/5
                http://bbs.eetop.cn/thread-156365-1-1.html

Synopsys Formality 2018.06 SP1 Linux64

Synopsys Formality是一种等效性检测工具，采用形式验证的技术来判断一个设计的两个版本在功能上是否等效。
等效性检测是一种静态分析方法，无需测试向量即可快速而全面的完成验证。
Formality具有一个流程化的图形界面和先进的调试功能，令设计者可以很快地检测出设计中地错误并将之隔离，这一功能可以大大缩短得到验证结果所需的时间。
Formality业界领先的功能和性能使之成为设计团队的首选产品。
与传统的仿真或是竞争对手的工具相比，Formality具有很多优点。
        ● 通过完备的验证覆盖将流片失败的可能性降到最低
        ● 对一个几百万门的设计进行验证以分钟记数，加快了产品上市时间
        ● 降低了工具设置的需求并提供快速错误隔离的功能，显著的缩短了传统的等效性检测的周期
        ● 工具简单易学，无需艰苦的培训，最大化的方便工程师的使用
        ● 提供了为业界所证实的先进功能，能充分利用现有的硬件资源


Synopsys Formality 2018.06 SP1 Linux64 (等效性检测工具) | 460 Mb
The Formality Equivalence Checker uses formal techniques to prove or disprove equivalence between two versions of the same design.
Equivalence checking is a type of static analysis that verifies large designs both quickly and completely without the use of test vectors.
The high performance and reduced risk of static analysis has led to the rapid adoption of equivalence checking within leading verification flows, making it a must for all competitive design processes.


Key Benefits
        Exhaustive verification, without test vectors, in a fraction of the time consumed by traditional dynamic techniques
        Proves functional correctness of register retiming, complex datapath, ECO, and low power implementations–from within a single product
        Reduces manual setup with verified automated setup guidance
        Verifies full-custom and memory designs when including ESP technology

Design Challenges
        Verification engineers often have limited knowledge of logic transformations that can occur during a designs implementation, making the optimal setup of an equivalence checking tool difficult to achieve.
        Missing or incorrect setup information prevents peak verification performance.
        In some cases, EC tools may produce a non-equivalent result when the designs are indeed equivalent (a false difference).
        Even when an engineer is aware of the numerous implementation optimizations, manual setup can be time consuming and error prone.
        These issues are exacerbated as new and unique design challenges drive further design optimizations.

参考链接：https://www.cnblogs.com/asic/archive/2011/05/22/2053415.html

〓 PrimeTime
　　        PrimeTime 是针对复杂、百万门芯片进行全芯片、门级静态时序分析的工具。
        PrimeTime可以集成于逻辑综合和物理综合的流程，让设计者分析并解决复杂的时序问题，并提高时序收敛的速度。
        PrimeTime是众多半导体厂商认可的、业界标准的静态时序分析工具。

〓 Formality
　　        Formality 是高性能、高速度的全芯片的形式验证：等效性检查工具。
        它比较设计寄存器传输级对门级或门级对门级来保证它没有偏离原始的设计意图。
        在一个典型的流程中，用户使用形式验证比较寄存器传输级源码与综合后门级网表的功能等效性。
        这个验证用于整个设计周期，在扫描链插入、时钟树综合、优化、人工网表编辑等等之后，以便在流程的每一阶段都能在门级维持完整的功能等效。
        这样在整个设计周期中就不再需要耗时的门级仿真。
        将Formality和PrimeTime这两种静态验证方法结合起来，一个工程师可以在一天内运行多次验证，而不是一天或一周只完成一次动态仿真验证。

参考链接：https://wenku.baidu.com/view/884 ... ;sxts=1550908071258

Formality_Jumpstart_2008.pdf

Formality Jumpstart Training                 Formality 快速入门培训
2008

参考链接：https://www.synopsys.com/zh-cn/i ... ormality-ultra.html

Formality 与 Formality Ultra

可验证由 Design Compiler 综合的最难的设计

        Formality® 是一款等效性检查 (EC) 解决方案，该解决方案使用形式静态技术来确定某一设计的两个版本之间是否具有等效功能。
        当今的设计规模大、复杂度高，同时面临时序、面积、功耗和进度等诸多挑战，要求最新、最先进的综合优化必须可被完全验证。
        Formality 支持所有 DC Ultra 和 Design Compiler Graphical 的优化，因此可提供完全可验证的最佳结果质量。
        Formality 支持对上电和断电状态、多电压、多电源和门控时钟设计进行验证。

        Formality Ultra 新增创新的匹配和验证技术，能够高效地指导设计人员实现功能性 ECO，并把对设计的影响降到最低，而且还能在几分钟内对有着数百万例化单元的设计验证其 ECO 的正确性。
        这些功能有助于设计者在设计周期后期缩短一半用于完成 ECO 的时间，并获得费时更短且更具有可预测性的进度。

        Formality 的易于使用且基于流程的图形化用户界面和自动设置模式有助于用户（即使是新用户）在最短的时间内成功完成验证。

优势
        与 DC Ultra/Design Compiler Graphical 完美匹配 — 支持所有默认优化
        直观且基于流程的图形化用户界面
        可验证低功耗设计，包括上电和断电状态
        Formality Ultra 向 Formality 中添加了 ECO 实现辅助、 快速 ECO 验证和高级调试等功能
        自动设置模式可以减少因设置信息不正确或者缺失而导致的“假故障”
        多核验证提升性能
        自动化的指导提高了与 DC Ultra/Design Compiler Graphical 配合的形式验证的完成度
        采用 ESP 技术时可验证全定制设计和存储器设计

Formality：最全面的等效性检查解决方案

        Formality 可以让经 DC Ultra 综合得到的设计更好地完成形式验证，DC Ultra/Design Compiler Graphical 采用拓扑技术，实现了与版图后时序、面积和功耗结果间准确的相关性，并提供重定时、反相和取消逻辑层次等高级优化功能。
        Formality 也完全兼容 Design Compiler Graphical，可用于预测和缓解路由拥塞。
        设计人员不再需要禁用 Design Compiler 强大的优化功能来通过等效性检查。
        DC Ultra/Design Compiler® Graphical 与 Formality 相结合，提供可完全验证的最高结果质量 (QoR)。

参考链接：https://www.synopsys.com/content ... mality-ultra-ds.pdf

Formality and Formality Ultra - Synopsys        数据手册

formality-and-formality-ultra-ds.pdf

参考链接：http://vlsiip.com/formality/ug.pdf

Formality User Guide        用户手册

参考链接：https://blog.csdn.net/a389085918/article/details/80078519
                http://blog.sina.com.cn/s/blog_a55a710c0102vcwm.html

STA静态时序分析/Formality形式化验证


1.    静态时序分析STA
对于仿真而言，电路的逻辑功能的正确性可以由RTL或者门级的功能仿真来保证；其次，电路的时序是否满足，通过STA（静态时序分析）得到。
两种验证手段相辅相成，确保验证工作高效、可靠地完成。
时序分析的主要作用是查看FPGA内部逻辑和布线的延时，确保其是否满足设计者的约束。

synopsys的STA工具是PT（primeTime),这是一个signoff的独立工具。
在早期的流程中，反标SDF的动态后仿真是标准的流程，现在的流程中后仿真已经不再需要进行，而是由STA+ formality形式验证 来代替。

基于动态仿真的验证和STA+FORMALITY的差别在于：一个需要开发仿真的pattern，另外一个不需要任何输入pattern。
另外，基于仿真的做法能验证到的path取决于输入pattern的完备性(覆盖率不高)，VCS可以统计模块验证的覆盖率，而STA+Formality是基于数学的，可以分析所有的path。

但是在下面三个方面，还是需要进行后仿真，后仿在下面三种情况是必要的：
1。异步逻辑设计部分
2。ATPG向量验证
3。初始化状态验证
对于全同步的设计，在做了RTL仿真后，可以不作门级仿真，而对于存在异步电路的设计，需要针对异步电路进行相应的门级仿真。

其实不是后仿不需要，只是这可能花的时间太多，所以人们想用形式验证+STA代替。
但是这种方法还是有漏洞的，因为STA只检查边沿timing，而形式验证只看register和combination的抽象功能。
后仿在下面三种情况是必要的：异步逻辑设计部分、ATPG向量验证和初始化状态验证。
另外，后仿产生的VCD文件还可以做功耗分析。

现在通常的策略是：采用形式验证手段来保证门级网表在功能上与RTL设计保持一致，配合静态时序分析工具保证门级网表的时序，对于全同步的设计，甚至可以不做门级仿真；
        对于存在异步电路的设计，也只需要针对异步电路进行极少的门级仍真工作。
这无疑会加快设计进度，加快产品上市时间。

总结下来：
        STA + Formality 不能完全替代后仿真，但是因为后仿真的时间太长，因此也不能完全进行后仿真，而是进行STA+Formality，并且对异步设计和初始化等提供后仿真的case来进行简单的后仿真。



PT和DC的timing分析差不多，下面一个功能比较特殊：

Bottleneck Analysis：
        提取violation的path中共同的cell。

report_bottleneck

2.    形式验证Formality
Formality形式验证是一个基于数学意义的验证方法，通过比较两个设计A,B：

如果A的逻辑功能被B包含，那么形式验证认为是通过的。

需要注意的是并不是说着两个design是完全相等的，而是逻辑上具有包含的关系。



在IC的流程中通常用于进行不同流程步骤的netlist的比较：
        逻辑综合netlist，floorplannetlist，placement netlist ，CTSinserted netlist,P&R netlist，在每一个步骤后都有新的逻辑加入到netlist中，但是这个新的逻辑的加入不能改变之前netlist的功能。

在dynamicsimulation的流程中，需要开发验证pattern作为输入来进行验证，验证的覆盖率取决于pattern的开发的完备性；
而formality是基于数学比较的，不需要任何的输入pattern。
因此相比于动态仿真的优势在于：
        不需要开发验证pattern
        速度比较快
        覆盖率100%
        纯逻辑上的验证，不考虑物理和timing信息

缺点在于：
        由于不考虑timing，因此需要配合STA工具使用。

                             
EDA软件巡礼6：Formality

EDA软件巡礼6：Formality

                           
Synopsys的Formality 是高性能、高速度的全芯片的形式验证：等效性检查工具。