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

FPGA也做formal?

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

在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.

    楼上NB

受教了