Xilinx 8.2i manual Output files for NetGen Equivalence Checking, Ecn Equivalence Checking

R

NetGen Equivalence Checking Flow

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] [conformalformality]

The –ecn option generates an equivalence checking netlist. This option generates a file that can be used for formal verification of an FPGA design.

Development System Reference Guide www.xilinx.com 331