网表形式化验证：综合后网表和插入DFT后的网表

各位，想问一下，综合后的网表（未插入DFT）和插入DFT后的网表怎么做形式化验证（工具：Formlaity）?
综合后网表和RTL代码做形式化时需要用到svf文件，那综合后的网表（未插入DFT）和插入DFT后的网表做形式化需要用到svf文件吗，除了Disable scan logic，还有什么需要注意的。
现在的做法只是将相关libs和两个网表读入，在Disable scan logic。

question: how did you insert DFT scan register. I used to write a script, perl for instance, to replace non-scan DFF with scanable DFF

netlist compare netlist 不需要svf

DC