SYNS formality 形式验证常见debug 步骤

formality 是synopsys 用来验证两个design是否等价的工具，也是IC实现中sign off tool，常用在design ECO 验证，tptg 前后由于design hierarchy变动的功能一致性验证，以及DC综合/DFT insert （OCC/SMS ) /PR(布局布线) 前后 design的function (功能等价性)的验证.

formality正常分为以下流程：

setup （set var /read lib）-> read data ->set constraint -> preverify -> match -> verify

如遇到formality fail可尝试以下方式进行逐步debug：

一：FM command 命令/输入文件是否正确

首先检查运行formality cmd过程中是否存在错误，常用方法是查看log文件，然后检查formality 输入的ref data /impl data是否正确及 svf data 是否完整.

二：查看failing point 数量及类型

查看formality 的failing point ，先观察是否有unmatched（tool match 阶段未能根据svf及name rule进行自动match 的point）的reg,若存在unmatch的 point ，请先查看unmatch的原因及类型,或者根据design function 进行手动match （set_user_match）

若failing point > 1000 ,大概率与setting有关，如 failing point < 100 ,请跳转步骤六 debug

三：分割定位

如综合阶段采用了多次compile 策略或drived block 综合，可进行分布验证，依次对compile1/compile2/block 进行formalty 检查

四：放松检查条件

1.放松对clock gate 的检查，以解决由于不同类型的clock gate 的影响，可set verification_clock_edge_analyze true

2.若DC 采用了MBB/retiming/ungroup 策略可逐一关闭再进行formality check

3.可以将可以一些不相关的逻辑，例如sync cell /sram/ submodule 设置成black box

五：尝试使用不同的formality strategy及formality tool version

不同的版本和不同的check strategy也会对formality 产生影响，可以尝试切换tool 版本及strtegy （set verification_alternate_strategy）

六：GUI界面 debug

save_session 可以保存formality session ，可以根据session start_gui界面查看failing point，在gui界面点击show patterns ，可以看到failing point 的所有关联点以及pattern.

1.查看ref/impl 两边的关联design是否匹配，若不匹配，确定是否是有dft的逻辑引起，根据情况添加dft的constraint

2.failing point的关联design是一致的，根据failing point的具体pin进行value追踪定位

欢迎大家一起学习！

如需IC岗位内推可加Eason_yi1 交流