AR# 12811: 6.1i Formal Verification - Can I use equivalency checking to re-target an FPGA to an ASIC? If so, how?
6.1i Formal Verification - Can I use equivalency checking to re-target an FPGA to an ASIC? If so, how?
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: