形式验证和formality debug

Formality 形式验证流程

导入设计文件。Reference Design（参考设计）：读入 RTL 设计文件，通常是 Verilog 或 SystemVerilog 文件。Implementation Design（实现设计）：读入综合后的门级网表或布局布线后的网表。库文件：读入相关的库文件，如工艺库。

设置约束。设置路径约束，例如某些路径只走某1端，或者某些引脚在不同设计阶段的值。设置其他验证约束，如时钟域交叉等。

匹配（Match）： 将 Reference Design 和 Implementation Design 中的逻辑锥（Logic Cones）和比较点（Compare Points）进行匹配。匹配过程会尝试将两个设计中的逻辑结构对齐，以便后续的验证。

验证（Verify）。Formality 使用多种算法来验证两个设计的逻辑等价性。对于每个比较点，验证算法会检查两个设计的输出是否一致。

Formality 将设计分解为逻辑锥和比较点。逻辑锥是从输入到输出的一组逻辑门，比较点是逻辑锥的输出点。通过比较点的输出结果来验证两个设计的逻辑等价性。

Formalitylogic cone

可以在gui界面点开logic cone（逻辑锥视图）trace一下ref design和imp design中有没有明显不太一样的输入点。

Formality show pattern

再不行可以点“show pattern”。形式验证跟 dft 的 atpg 类似，就是找出一组输出向量使得 ref design和 imp design 中的 compare point 的输出值不一致。“show pattern”就是展示向量通过数据路径抵达该逻辑锥过程中的值的变化。

Patter视图颜色的含义。黑色 “0/1”表示Ref 和 Imp 该位都是 0 或都是 1；表示匹配、正常、无问题。红色“ 0/1”（或 X）表示 Ref 是 0，Imp 是 1；或 Ref 是 1，Imp 是 0；或一边是 X（不定态），另一边是 0/1；表明这一位不相等，验证失败点。

。C0表示常数 0，C1表示常数 1，und / U表示未驱动（undriven）。

红色出现的常见原因。逻辑功能真不等价： RTL 与syn netlist、ECO 前后逻辑真的不一样。常数/约束不一致： 一边用  set_case_analysis 0/1 ，另一边没设端口/使能被固定为不同常值。 时钟/复位极性、插入反相器：综合/PR 插了 inverter 改相位，Formality 没识别。 DFT 扫描链、测试逻辑差异：一边插了 scan cell，另一边没有。黑盒（Black-box）匹配/设置不对-：输入输出假设不一致。未驱动（undriven）信号：一边悬空被视为 0，另一边视为 1 或 X。

案例

我最近遇到了一个undrive net综合后被工具tie住了，导致formal fail 了。在DC综合里，undriven net(无驱动网络) 被自动tie到0/1(tie-low/tie-high),是DC的标准安全修复机制，核心是为了避免X 态传播、防止时序/功能异常、满足后端LVS/DRC要求。

知芯朋友，欢迎加入

截至到20260412。文章共250945字。文档（手册）共232份。中后端面试题解析累计20道（尽量日更）。