一、静态验证
1.1 概述
在之前的文章中，我们介绍了动态仿真，但是动态仿真用于百万门以上电路时所需时间极长，而且其功能覆盖率取决于所设计的输入激励向量，很难达到100%，因此静态时序分析和等效性检查这样的静态验证是必须的。静态时序分析比动态仿真快得多，无需输入激励向量，可以穷尽 所有门级电路的时序验证，但无法发现逻辑功能错误，逻辑综合后、布局后和布线后都能做，但后者更为准确而重要。等效性验证用于比较RTL代码与RTL代码之间、RTL代码与网表之间、网表与网表之间的一致性，常用于判断设计递进或修改后（比如加入了扫描链）逻辑是否发生了变化。
1.2 静态时序分析（STA）
STA可仿真四类时序路径（Timing Path），分别是：（1）引脚到寄存器（从芯片的输入端口到目的寄存器的数据输入端口）（2）寄存器到寄存器（从源寄存器的时钟端口到目的寄存器的数据输入端口）（3）寄存器到引脚（从源寄存器的时钟端口到芯片的输出端口） （4）引脚到引脚（从芯片的输入端口到芯片的输出端口）。
关于时序路径的详细内容，可以阅读：
FPGA时序分析与约束（5）——时序路径
https://ztzhang.blog.csdn.net/article/details/132641522
1.2.1 最长路径和最短路径
1.2.2 端口检查
对于静态时序分析来说，最重要的就是检查芯片上所有寄存器的端口，包括输入、输出、置位和复位、其对应检查的内容分别是建立时间、保持时间、恢复时间和移除时间。
- 建立时间（Setup time）：时钟信号变化之前寄存器输入数据保持不变的最短时间。建立时间违例多发生在最慢的PVT条件下，故分析时应使用最坏（WORST）条件下的时序库。因建立时间不够发生的违例，对策是让时钟更晚地到达寄存器（比如增加时钟周期），或者缩短数据路径的延迟
-
保持时间（Hold time）：时钟信号变化之后寄存器输入数据保持不变的最短时间。保持时间违例多发生在最快的PVT条件下，故分析时应使用最好（BEST）条件下的时序库。因保持时间不够而发生的违例，对策是增加数据路径的延迟，或者让时钟更早地到达寄存器（比如缩短时钟周期）
-
恢复时间（Recovery time）时钟信号变化之前置位或复位信号保持有效的最短时间，应采用最坏情况分析
-
移除时间（Removal time）时钟信号上升沿与置位或复位信号上升沿之间的时间，应采用最好情况分析
https://ztzhang.blog.csdn.net/article/details/134095643
https://ztzhang.blog.csdn.net/article/details/132626131
1.2.3 时序违例的可能原因与对策
- 设计约束不合理 某些设计约束或许根本不能实现，这只能通过更改或修正时序约束文件来解决
- 线负载模型（WLM）不合理 逻辑综合时使用的WLM产生的网表在物理设计时不可能实现，这需要根据当前的结果去产生新的WLM（CWLM，customized WLM），再次进行逻辑综合（也称物理综合physical synthesis）
- 布局布线不合理 对于大规模或者复杂的设计，由于初学者经验不足或者有经验者的疏忽而出现时序违例，需要重新对布局布线进行优化
较小的优化可以不改变网表的逻辑，只是通过改变逻辑单元的尺寸、复制单元或者添加缓冲器来解决，这称为“原地优化（IPO，in-place optimization）”
1.3 形式验证
- 作用：判断当前设计与参考设计在逻辑功能上是否相同，不能验证时序
- 常用方法：等效性检查、模型验证和定量证明等，等效性检查最为常用
- 常用EDA工具：Synopsys的Formality，Cadence的Encounter Conformal Equivalent Checker
1.4 等效性检查
二、小结
考虑到动态仿真用于百万门以上电路时所需时间极长，而且其功能覆盖率取决于所设计的输入激励向量，很难达到100%，因此静态时序分析和等效性检查这样的静态验证是必须的。本文着重介绍了静态时序分析、形式验证和等效性验证。
