AR# 12811


6.1i Formal Verification - Can I use equivalency checking to re-target an FPGA to an ASIC? If so, how?


General Description:

Can I use equivalency checking to re-target an FPGA to an ASIC? If so, how?


When you re-target from one technology to another, you can use equivalency checking in two ways:

Method 1: RTL-to-Gate

If the source RTL is the same for both FPGA and ASIC, you can perform RTL-to-Gate checking for the ASIC. (This flow does not require formal verification tools to support a FPGA flow.)

If you use this method, state machine encoding differences may be problematic. Synthesis and formal verification tools that read the FSM description from RTL code may encode the FSM differently. For example, synthesis may be using the one-hot encoding method, while the equivalency-checking tool is using binary encoding. These differences in encoding the FSM can lead to verification failure unless the equivalency-checking tool is instructed to use the same one-hot encoding scheme.

Method 2: FPGA Gate-to-ASIC Gate

Use this method if you want to compare the FPGA gate-level netlist to the ASIC gate-level netlist. (Xilinx has not validated this flow and recommends contacting your formal verification tool vendors for additional information.)

This flow may not successfully perform an equivalency check, as there may be differences in the ASIC and FPGA technology primitives. For example, if the design uses RAMs, MULT18x18s, and SRL16s, the tools may not functionally verify these if the ASIC technology does not have the exact same primitives. The flow does not work if both netlists were created from the same RTL.

The ASIC and FPGA synthesis tools can use both different sequential optimization (e.g., retiming, etc.) and different technology libraries to synthesize the RTL code. The corresponding gate-level netlists can have very different compare points (number of flip-flops and sequential elements), which causes the equivalency-checking tool to fail.

NOTE: If you are using netlists that were created from the same source RTL, Xilinx recommends using Method 1.

For related PrimeTime information, please see the following Answer Records:

(Xilinx Answer 12802) - "What is formal verification?"

(Xilinx Answer 12803) - "What types of users will be interested in the formal verification flow?"

(Xilinx Answer 12804) - "Does Xilinx support equivalence checking and model checking?"

(Xilinx Answer 12805) - "Does Xilinx support equivalency checking for RTL-to-RTL, RTL-to-gate, or gate-to-gate?"

(Xilinx Answer 12806) - "Why does Xilinx support equivalency checking?"

(Xilinx Answer 12807) - "Does Xilinx plan to support model checking?"

(Xilinx Answer 12808) - "Should equivalency checking replace simulation?"

(Xilinx Answer 12809) - "When should I use equivalency checking?"

(Xilinx Answer 12810) - "How will I benefit from using equivalency checking?"

(Xilinx Answer 12812) - "Which equivalency-checking tool vendors does Xilinx support?"

(Xilinx Answer 12813) - "What platforms does Xilinx support?"

(Xilinx Answer 12814) - "I am a current Formality or Conformal customer. Who do I contact for support-related issues?"

(Xilinx Answer 12815) - "Are application notes regarding verification flow available?"

(Xilinx Answer 12816) - "What are the limitations of the verification flows?"

(Xilinx Answer 12817) - "Does the verification flow work with the Synopsys FCII, Synplicity Synplify, and Mentor Leonardo Spectrum synthesis tools?"

(Xilinx Answer 12818) - "Does the verification flow work with all languages?"

(Xilinx Answer 12820) - "Who supplies libraries?"

(Xilinx Answer 12821) - "What libraries does Xilinx provide?"

(Xilinx Answer 12822) - "How do I install the libraries that are referenced by Xilinx Application Note 411?"

(Xilinx Answer 12823) - "What Xilinx product families are supported?"
AR# 12811
日期 11/28/2011
状态 Archive
Type 综合文章
People Also Viewed