教程

Formality实际上使用起来很简单，照着下面的PPT做就行了

Formality使用指南.ppt

fm中文.pdf

在DC中使用tcl脚本综合和Formality一致性检查_孜孜不倦-CSDN博客

这个博客里面有很多有用的链接，尤其是下面相关文章部分

Bug

形式验证在读取网表(imp → read_netlist)的时候会报错

formality验证中有很多rtl中有vhdl和verilog文件，怎么读入reference？ - 后端讨论区 - EETOP 创芯网论坛 (原名：电子顶级开发网) -

set hdlin_warn_on_mismatch_message {FMR_ELAB-147 FMR_ELAB-130}

Match 和 verify的结果

*********************************** Matching Results ***********************************
 138130 Compare points matched by name
 1 Compare points matched by signature analysis
 0 Compare points matched by topology
 20 Matched primary inputs, black-box outputs
 362(0) Unmatched reference(implementation) compare points
 0(0) Unmatched reference(implementation) primary inputs, black-box outputs
 234(0) Unmatched reference(implementation) unread points
----------------------------------------------------------------------------------------
Unmatched Objects                                                        REF        IMPL
----------------------------------------------------------------------------------------
 Registers                                                               362           0
   DFF                                                                    94           0
   Constrained 0X                                                        268           0
****************************************************************************************

Info:  Formality Guide Files (SVF) can improve matching performance and success by automating setup.
1

Untitled

Untitled

Untitled