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

对于仿真而言，电路的逻辑功能的正确性可以由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

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工具使用。

Equivalence checkers： 逻辑等价性检查,检查两个design是否是逻辑上相等的。

Model checkers：检查design是否满足某些逻辑属性比如assert断言。

从这个流程中可以看到，

第一次比较是原始的verilog代码和DC综合后的netlist的比较；

第二次比较是逻辑综合后的netlist和DFT插入后的netlist的比较；

第三次比较是DFT插入后的netlist和后端生成的netlist的比较。

两个术语： 

Reference design ： 作为golden的designImplementation design ： 正在修改的design，需要证明和参考设计有等价性。

如果implmentationdesign被证明是和referencedesign等价的话，implmentationdesign可以成为新的referencedesign。

logic cones从一个design object作为起始，往回回溯，到某一个design object结束的中间所有的组合逻辑。

logic cones的起始点是formality中的compare point：

primary outputs, internal registers, black box input pins, ornets driven by multiple drivers where at least one driver is a port or blackbox.

logic cones的终止点是：

primary inputs or compare points.

因为formality中register是作为compare point的，因此logic cone只能是组合逻辑的集合。

上图是一个logiccone：起点是primaryoutput，回溯的终点是primaryinput。

A black box is an instance of a design whose function isunknown. Black boxes arecommonly used for components of a design that are not synthesized. Examples ofcommonblack boxes include RAMs, ROMS, analog circuits, and hard IP blocks.

The inputs to black boxes are treated as compare points andthe outputs of the black boxes are treated as input points to other logic cones.

主要是一些内部功能未知的模块。blackbox的输入被认为是一个comparepoint。

由于blackbox的内部功能未知，因此blackbox的中间逻辑不作为logiccone。

Formality uses the following design objects to createcompare points automatically:•Primary outputs•Sequential elements•Black box input pins•Nets driven by multiple drivers, where at least one driver is a port orblack box

formality依据上面的规则自动创建comparepoint。用户也可以自定义的创建一些comparepoint。

有了comparepoint，需要有一个方法将referencedesign中的comparepoint和implementationdesign中的comparepoint能一一对应起来(如果需要进行completeverification)。如何进行comparepoint的对应：

(1) 通过objectname来进行对应，有相同objectname的comparepoint进行对应。

Name-based matching technique

(2) 如果在其他design中objectname有了改动，导致无法进行对应，那么需要采用其它的

方法进行对应。Non-name-based matching technique包括signature analysis 算法

(3) 手工进行对应。User-match

在基于name-basedmatch中如果有一些comparepoint没有找到对应，可以通过下面的命令report：

report_unmatched_points

这种不匹配的问题可能导致的原因是：

object name被流程的其它部分更改导致无法对应

implementation design 中加入了新的逻辑比如black box导致有新的compare point产生

如下表所示：

包括区分大小写和不区分大小写的对应。

Reference: /WORK/top/memreg(56)Implementation: /WORK/top/MemReg(56)

ft_shell > set name_match [all | none | port | cell ]

后面的参数来指定哪一类的comparepoint使用exact-namematching方法：

all: 所有的

None: 只有primaryinput使用

Port：top-level output ports使用

cell：register,black box input/output pin

Name Filtering：

大小写不敏感的，使用filter来进行对应。

Reference: /WORK/top/memreg__[56][1]Implementation: /WORK/top/MemReg_56_1

Reference: /WORK/top/BUS/A[0]Implementation: /WORK/top/bus__a_0

以上case可以形成对应，下面这个不行：

Reference: /WORK/top/BUS/A[0]Implementation: /WORK/top/busa_0

命令：

ft_shell > setname_match_filter_chars {~!@#$%^&*()_-+=|[]{}"':;?,./V}

Reverse the Bit Order in Multibit Registers:

多bitregister中bit位置反一下也认为是一致的。

register a[31:0]；

register a[0:31]；

假设两个没有对应的comparepoint的logicclone拓扑上是一样的，认为这两个comparepoint是对应。 相同的logicclone 驱动的comparepoint认为是对应point。

set signature_analysis_match_compare_points false

Signature analysis is an iterative analysis of the comparepoints’functional and topological signatures. Functional signatures are derivedfrom random pattern simulation; topological signatures are derived from fanincone topology.

Compare Point Matching Based on Net Names：

Matches can be made through either directly attached drivenor driving nets。

通过分析comparepoint的驱动net或者被驱动的net是否相同来进行对应。

set name_match_based_on_nets false

概念：

Design Consistency： 设计一致性，对于相同的inputpattern产生了相同的输出响应.

但是如果一个存在don’tcare (X) 状态，而另外一个design的响应为0、1都认为是等价的。

Design Equality： 设计相等，同DesignConsistency 类似但是对于dontcare状态，比较的另外

一方也必须输出dontcare状态才认为是相等(而不像DesignConsistency中输出什么值都认为相同)

可见，DesignEquality成立的要求要高于DesignConsistency。

可见，formality是基于logiccone来做等效性检查的，如果referencedesign的所有comparepoint的

logic cones和implementation design中的comparepoint 都是一致的，那么就认为等效；

当然implementationdesign中包含的comparepoint可能多于referencedesign(有新的逻辑加入).