formality中出现unmatched points

RTL中有些触发器为固定状态，综合出来的网表会自动去掉这些触发器但是在做形式验证时，formality会提示这些触发器的地方为unmatched points
导致无法进行verify。
我现在不想去一一修改RLT中的触发器，在formality有没有什么选项或命令来解决这个呢?
我知道dc是可以在guidence载入.svf文件，但我是做的fpga设计的形式验证，好像并没有这个
.svf文件
多谢啊

我不明白你在做什么比对?fpga综合netlist VS RTL code?

是的

坛子里玩形式验证的dx太少啊

同样的问题呢，我也遇到了，求解，，，，

RTL中有些触发器为固定状态，综合出来的网表会自动去掉这些触发器但是在做形式验证时，formality会提示这些触发器的地方为unmatched points
导致无法进行verify。
我现在不想去一一修改RLT中的触发器，在formality有没有什么选项或命令来解决这个呢?
不同的地方：
我已经set_svf ***.svf（dc之后的svf文件，在guidance时载入.svf文件）

如果寄存器是固定的值的话，可以在setup阶段，把它设置为常数0或者1。图形界面可以操作的，不过回到setup后要重新match了。也可以在脚本中用命令，格式是：set_constant -type cell 寄存器名称 0；