Filter
Top Products
Development System Reference Guide www.xilinx.com 331
NetGen Equivalence Checking Flow
R
Output files for NetGen Equivalence Checking
The NetGen Equivalence Checking flow uses the following files as output:
• Verilog (.v) file—This is a IEEE 1364-2001 compliant Verilog HDL file that contains the
netlist information obtained from the input file. This file is a equivalence checking
model and cannot be synthesized or used in any other manner than equivalence
checking.
• Formality (.svf) file—This is an assertion file written for the Formality equivalence
checking tool. This file provides information about some of the transformations that a
design went through, after it was processed by Xilinx implementation tools.
• Conformal-LEC (.vxc) file—This is an assertion file written for the Conformal-LEC
equivalence checking tool. This file provides information about some of the
transformations that a design went through, after it was processed by Xilinx
implementation tools.
Note:
For specific information on Conformal-LEC and Formality tools, please refer to the
Synthesis and Simulation Design Guide.
Options for NetGen Equivalence Checking Flow
This section describes the supported NetGen command line options for equivalence
checking.
–aka (Write Also-Known-As Names as Comments)
The –aka option includes original user-defined identifiers as comments in the VHDL
netlist. This option is useful if user-defined identifiers are changed because of name
legalization processes in NetGen.
–bd (Block RAM Data File)
–bd [filename] [.elf|.mem] [tag [tagname]}
The –bd option specifies the path and file name of the .elf file used to populate the Block
RAM instances specified in the .bmm file. The address and data information contained in
the .elf (from EDK) or .mem file allows Data2MEM to determine which ADDRESS_BLOCK
to place the data. Multiple use of the -bd option is allowed.
Optionally, a tagname can be specified with the –bd option. If a tagname is specified, only
the address spaces with the same name in the .bmm file are used for translation, and all
other data outside of the tagname address spaces are ignored. See Chapter 24,
“Data2MEM” for additional information.
–dir (Directory Name)
–dir [directory_name]
The –dir option specifies the directory in which the output files are written.
–ecn (Equivalence Checking)
–ecn [tool_name] [conformal|formality]
The –ecn option generates an equivalence checking netlist. This option generates a file that
can be used for formal verification of an FPGA design.