请问一下，ISE综合的结果，怎样进行formality验证

chanon

rt, 那个进行Formality的ISE库不道怎样可以得到，谢谢！

solarwafer

FPGA也做formal？

acgoal

综合器会保证RTL和gate的一致性的，不需要特别的做formal验证的。
ASIC之所以要做是因为后端有DFT，p&r插入很多buffer，时钟树啊什么的对netlist有比较大的改动等等。而且往往这些工具比较杂，所以formal是一定要的。而FPGA往往都是用厂家提供的工具，工具应该有自带类似formal的东西来保证功能一致性，不需要特别的做formal。

aurora9325

在xilinx官网上下xeclib库，在读入Reference或Implementation的时候，选择Option，修改Library type 为Read technology library files into library，再通过“Verilog”按钮将xeclib中的库文件读入，load完后设置top design就可以了。友情提醒，unmatch点很多哟~~
下面是官方的回复，可参考下：

Verilog source files for the Unisims/Simprims libraries is available with the Xilinx install for >=12.1 at "%Xilinx%/verilog/xeclib/".

These files are not synthesizable and can only be interpreted as a technology library.  Synopsys Library Compiler can read these files to generate a .db technology library, if you have a Library Compiler license.
In Synopsys Formality, the verilog files can be loaded into your container by adding all of the source files as a "technology library" instead of into your source library "work" ("Read Design Files" tab -> "Options..." button -> "Library type" tab -> "Read technology library files into library:" radio button).  The library source files will not successfully compile as a source library but they are accepted fine as a technology library.  Since you can only load files to one library at a time, you have to load the files for each technology/source library in a seperate transaction.

chencsw

在xilinx官网上下xeclib库，在读入Reference或Implementation的时候，选择Option，修改Library type 为Read ...
aurora9325 发表于 2014-9-18 10:38

                               
登录/注册后可看大图

    楼上NB

diyangguang

受教了

zhangroot

真的NB，我现在是看到pt和FM就头大，fpga去用它们，文件这个也不对那个也不对，连个库都没有。