转载于http://blog.Sina.com.cn/s/blog _ a55 a710 c 0102 vcwm.html
1 .静态时序分析对STA仿真来说，电路逻辑功能的正确性可以通过RTL或门级功能仿真来保证； 其次，电路时序是否满足可以通过静态时序分析(STA )获得。 确保两种验证手段相辅相成，有效可靠地进行验证工作。 时序分析的主要作用是检查FPGA内部的逻辑和布线延迟，以确认是否符合设计者的限制。
synopsys的STA工具是pt(primetime )，这是signoff的独立工具。
在初期的过程中，SDF的动态后期模拟是标准的过程，但在现在的过程中不需要进行后期模拟，而是被STA formality形式的验证所代替。
基于动态模拟的验证与STA FORMALITY的区别在于需要开发模拟的pattern和不需要输入的pattern。
另外，用基于模拟的方法可以验证的path依赖于输入pattern的完整性(覆盖率不高)，VCS可以统计模块验证的覆盖率，但STA Formality以数学为基础，所有的pattern都可以
但在以下三个方面，还是要进行后模拟，后模拟要效仿以下三种情况。
1。 异步逻辑设计部分
2。 ATPG矢量验证
3。 初始化状态验证
对于完全同步的设计，在进行RTL仿真后，可以不进行门级仿真，但对于存在异步电路的设计，需要对异步电路进行相应的门级仿真。
其实不需要模仿。 只是，这可能太费时间了，所以人们想用形式上的验证来代替STA。 然而，该方法存在漏洞。 因为STA只检查边缘timing，而格式验证只查看register和combination的抽象功能。 后者在异步逻辑设计部分、ATPG矢量验证、初始化状态验证3种情况下是必要的。 此外，通过后仿方式创建的VCD文件还可以分析功耗。
目前常用的策略是采用格式验证手段来保证门级网表在功能上与RTL设计一致，并配合静态时序分析工具来保证门级网表的时序，对于全同步的设计，无需进行门级模拟即使对于存在异步电路的设计，也只需要对异步电路执行极少量的门级操作。 这无疑将加快设计进度，加快产品上市时间。
总结：
STA Formality并不能完全代替后模拟，但由于后模拟时间太长，不能完全进行后模拟，而是进行STA Formality，进行异步设计和初始化等后模拟
PT和DC的定时分析大致相同，但以下功能是特殊的。
Bottleneck Analysis :
提取与violation path通用的蜂窝。
report_bottleneck
2 .形式验证公式形式验证是一种基于数学意义的验证方法，通过比较两个设计a、b :
在a的逻辑功能包含在b中的情况下，认为通过了形式验证。
必须注意的是，两个设计在逻辑上具有包含性关系，而不是说它们完全相等。
IC进程通常用于比较不同进程步骤的netlist。
合并逻辑netlist、floorplannetlist、placement netlist、CTSinserted netlist，在每个步骤之后新的逻辑被添加到netlist，但是这个新逻辑的添加是以前的
动态仿真过程需要开发一个验证pattern作为输入，验证覆盖率取决于pattern开发的完整性； formality基于数学比较，不需要在pattern中输入。 因此，与动态模拟相比的优点是：
不需要开发验证pattern
速度快
覆盖率100%
不考虑物理信息和定时信息的纯逻辑验证
缺点如下。
因为不考虑timing，所以必须结合STA工具使用。
2.1.formality包含两个工具Equivalence checkers。 逻辑等效检查检查两个设计在逻辑上是否相等。
模型检查：检查设计是否满足特定逻辑属性，如assert断言。
从该流程可以看出，
最初的比较是将原来的verilog代码和DC合并的netlist的比较；
第二次比较是逻辑合并的netlist和插入DFT后的netlist的比较；
第三次比较是DFT插入后的netlist和后端生成的netlist的比较。
两个术语：
referencedesign :设计为golden
Implementation design :修改中的design需要证明与参考设计具有等价性。
如果implmentationdesign被证明与referencedesign等价，则implmentationdesign可以成为新的refer
encedesign。2.2.Logic Cones：逻辑锥的概念
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。
2.3.Black Box的概念
A black box is an instance of a design whose function isunknown. axdyt are
commonly used for components of a design that are not synthesized. Examples ofcommon
魔幻的日记本 include RAMs, ROMS, analog circuits, and hard IP blocks.
The inputs to 魔幻的日记本 are treated as compare points andthe outputs of the 魔幻的日记本 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。
2.4.比较算法(matching)有了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产生
如下表所示：
2.5.compare point对应的算法和优先级2.5.1. Exact-Name Matching包括区分大小写和不区分大小写的对应。
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]；
2.5.2. Topological Equivalence
假设两个没有对应的comparepoint的logicclone拓扑上是一样的，认为这两个comparepoint是对应。 相同的logicclone 驱动的comparepoint认为是对应point。
2.5.3. Signature Analysis
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(有新的逻辑加入).