在最近的一次项目中，跑RTL vs APR ECO Netlist的Formality时，工具报了Fail，单条log如下：
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 0 0 0 0 0 0 0 0
Failing (not equivalent) 0 0 0 0 0 1 0 1
****************************************************************************************对Failing Points进行Analyze和Diagnose后，提示Cone Input不匹配，Recommendations是一个clock gate cell。怀疑是不是clock gate cell没有穿过去，RTL里没有clock gate，而apr网表里有。但点Show Logic Clones之后也没有发现什么明显的异常。
再点Show Patterns之后发现，clock gate cell确实是好的，而异常发生在复位信号上。Reference里是异步Set，而Implement里是异步复位。所以，突然想到这个DFF在ECO时改过默认值，由0改成了1，但没有换DFF类型。所以猜测Formality没有识别到inv push的关系。
然后在formality脚本里match之后加了条set_user_match -inverted，再重新Run，就PASS了。
match
set_user_match -inverted r:/WORK/XXX/u_reg_file/reg_00_reg[6] i:/WORK/XXX/u_reg_file/reg_00_reg_6_
verifyLog如下：
********************************* Verification Results *********************************
Verification SUCCEEDED
----------------------
Reference object: r:/WORK/XXX/u_reg_file/reg_00_reg[6]
Implementation object: i:/WORK/XXX/u_reg_file/reg_00_reg_6_
1 Passing compare points
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 0 0 0 0 0 1 0 1
Failing (not equivalent) 0 0 0 0 0 0 0 0
****************************************************************************************总结一下：
当Formality报Fail后，优先利用工具的Analyze和Diagnose命令来分析一下，看看是否有明显的提示。如果没有，就先分析logic cone的的input是否相同，然后再打开logic cone的电路进行对比。优先对比clock和reset/set路径，因为clock和复位的关系相对简单，容易查找。最后再对比数据path，借助Show Patterns，对ref和imp施加激励，来分析从哪一个stdcell开始不等价的。
