formality svf guidence Rejected了咋办？ | iLoveIC的IC技术圈专栏

在一个项目中，用formality给两个网表做等价性检查。给formality一个网表变化的guidence，如下：

# 在imp网表中复制了一个flipflop
guide_reg_duplication \
    -design { top } \
    -from { u_1/cnt_reg_9_ } \
    -to { u_1/cnt_reg_9__rep1 }

# 在imp网表中删除了复制的flipflop
guide_reg_merging \
-design { top } \
    -from { u_0/cnt_reg_6__rep1 } \
    -to { u_0/cnt_reg_6_ }

然而，formality拒绝了我给的svf guide命令。

***************************** Guidance Summary *****************************
                                         Status
Command                 Accepted   Rejected  Unsupported  Unprocessed  Total
----------------------------------------------------------------------------
reg_duplication     :          0          1          0          0          1
reg_merging         :          0          1          0          0          1

Note: If verification succeeds you can safely ignore unaccepted guidance commands.

查看unmatch point也正好就是这两个点没有match上。

fm_shell (verify)> report_unmatched_points -point_type DFF
**************************************************
Report         : unmatched_points
                 -point_type DFF
Reference      : r:/WORK/top
Implementation : i:/WORK/top
**************************************************
2 Unmatched points (1 reference, 1 implementation):
  Ref  DFF        r:/WORK/top/u_1/cnt_reg_6__rep1
  Impl DFF        i:/WORK/top/u_0/cnt_reg_9__rep1

既然formality不听劝，那怎么办呢？

还是有办法的，在match之前用rewire_connection把网表给临时改一下，就是在ref和imp网表中分别把rep flipflop给改回去。

# 在imp网表中，把复制的flipflop输出load接回到原flipflop上
rewire_connection \
    -type pin \
    -from i:/WORK/top/u_1/cnt_reg_9__rep1/Q \
    -to i:/WORK/top/u_1/cnt_reg_9_/Q
	
# 在ref网表中，把复制的flipflop输出load接回到原flipflop上
rewire_connection \
    -type pin \
    -from r:/WORK/top/u_0/cnt_reg_6__rep1/Q \
    -to r:/WORK/top/u_0/cnt_reg_6_/Q

然后重跑formality，就可以正常match上了，并且Verification SUCCEEDED。