对FPGA设计做formality过程中遇到的一点问题

Synplify在对rtl网表进行FPGA综合时，会有一些正常的优化，比如对一些输出驱动比较多的D触发器会综合成两个D触发器，输入和输出逻辑一样的D触发器又会合并成一个。问题是，在对综合后的网表和rtl做形式验证时，formality似乎不兼容这些优化，在match的时候就会报unmatched point，如果无视这些unmatch，verify也会failed。碰到这种问题，该怎么办呢?

FPGA的formal还不完善，还没见过有人做fpga的formal的，你是第一个，自己探索探索，记得分享经验啊

DC在综合的时候也会优化，不过它有一个guide输出给formality用，synplify没有研究过，不晓得。小编可以研究一番

    synplify pro有个verification mode选项，可以生成类似DC的svf文件。formality可以读入指导比较。另外，synopsys私下有个脚本可以做这种文件的转换，可以非正式渠道要一下。
FPGA厂家对formality的支持还不是十分完善，有些DSP block除非显式调用，否则FPGA没有lib可供比较。

   确实是有个vif文件的,这个文件我看了下,是不能被formality直接调用的.我试了下,对于一些简单的优化,比如两个D触发器综合成一个D触发器,这些是可以通过观察vif文件,然后在formality中set_equivalence来解决.但是有些比较复杂一点的优化还是没办法解决.
   请问下,你说的非正式渠道是指什么呢?

    私下跟synopsys的AE要。

是在Linux环境吗?window下怎么产生不了vif文件.我的版本是2013.03

   我没有生成verifi目录，也没有vif文件，我用的是2015.03的版本，请教下是怎么回事