形式验证

一、Formal Verification与Simulation的区别

这一节研究的是：formal verification（形式验证）验的是什么，它和用UVM做的simulation（仿真）差在哪。

Simulation：testbench发激励（sequence），scoreboard比结果。跑了多少条用例，就只有这些用例走过的情况被检查过，没跑到的情况没有被检查。SVA assertion（断言）在simulation里也一样，只在跑过的那些波形上检查。

Formal verification：不发激励。验证工程师只写规则，也就是property（性质），再把RTL和规则一起交给solver（求解器）。solver把所有可能的输入序列一起考虑，结果只有两种：

• proof（证明）：这条规则在任何输入下都不会被违反
• counterexample（反例）：一条具体的波形，第几拍给什么输入就违反了规则

二、一个Formal工程里有什么

这一节研究的是：一个formal工程由哪些文件组成，分别由谁写。

和UVM环境对应着看：

三样都由验证工程师自己写：checker几十行到几百行，formal top和配置文件各几十行。DUT是被验的RTL，不改。

三、工具链

这一节研究的是：formal工具怎么把RTL和规则变成一个数学问题，开源和商用工具的差别在哪。

SymbiYosys /ˈsɪm.bi.joʊ.sɪs/（命令行叫sby）是开源的formal前端，装在OSS CAD Suite里。它自己不证明，它调两样东西：

• Yosys：把Verilog读成逻辑模型，assertion变成模型里的检查点
• solver：在逻辑模型上搜所有输入序列，SMT solver（yices、z3）或者abc

流程：RTL + checker + 配置文件 → Yosys读成逻辑模型 → solver搜索 → proof，或者counterexample（VCD波形）

SymbiYosys没有图形界面，结果是文本日志，counterexample是VCD文件，用gtkwave打开看。商用工具是Cadence的JasperGold和Synopsys的VC Formal，有图形界面，原理相同，差别在SVA支持的完整度、多时钟怎么建模，以及证明收敛不了时有多少辅助手段。

四、例：Clock Gating怎么用Formal验

这一节研究的是：时钟本身是被验对象时，assertion怎么写、加了门控以后功能没变怎么证。clock gating是在寄存器空闲时把送给它的时钟停在低电平，省时钟网络的功耗；做这件事的单元叫ICG（integrated clock gating cell），内部是一个latch加一个AND门，en为0时输出gclk停在低电平。为什么不能直接用AND门、latch怎么保证gclk没有glitch，在《低功耗设计》「Clock Gating」第3到5小节，这里只讲验证。

1. 时钟当数据

assertion平时挂在时钟沿上采样，可是这里被验的正是时钟gclk：挂在gclk自己的沿上，只看得到「有沿」，看不到脉冲多宽，被截短的半截脉冲照样有上升沿。做法是引一个比所有时钟都快的参考时钟ref_clk，把gclk当普通信号在ref_clk上采样，数它每段高电平持续了几个ref_clk周期。

gclk第二个脉冲只有1拍ref_clk宽，是被截短的glitch，「每段高电平至少MIN拍」的assertion在这里报错：

assert property (@(posedge ref_clk) $rose(gclk) |-> gclk[*MIN]);

同一套手法还查另一条：gclk的每个上升沿都对应clk的上升沿、且当时使能为1，不能凭空多出沿。formal里ref_clk就是solver的全局时钟：所有时钟都当成输入，在全局时钟下采样，时钟自己的波形才能被检查，这叫时钟当数据。

用库里的ICG单元时，单元本身不用这样验，厂家验过；要验的是用法，见下一小节。

2. 加了门控以后功能没变

加门控前后是同一个设计，只是停掉了某些拍的时钟，功能不该变。证明两版功能一样叫等价检查，两种方法查的对象不同：

• LEC（logic equivalence checking）：比模块内部的每个寄存器，两版每一拍的值都一样才等价
• SEC（sequential equivalence checking）：只比模块的输出，两版从同一个复位状态出发、给同样的输入，每一拍的输出都一样就等价

r在第2、4、5拍不一样，LEC报不等价；out每一拍都一样，SEC能证。

参考

• Wikipedia, Formal verification
• YosysHQ, SymbiYosys documentation
• YosysHQ, OSS CAD Suite
• Wikipedia, Formal equivalence checking