UPGRADE YOUR BROWSER

We have detected your current browser version is not the latest one. Xilinx.com uses the latest web technologies to bring you the best online experience possible. Please upgrade to a Xilinx.com supported browser:Chrome, Firefox, Internet Explorer 11, Safari. Thank you!

AR# 25007

Formal Verification - Frequently Asked Questions (FAQs)

Description

This Answer Record provides answers to Frequently Asked Questions (FAQs) related to formal analysis.

 

Q1. Does Xilinx support both equivalency checking and model checking?

Q2. What is formal verification?

Q3. Why does Xilinx support equivalency checking?

Q4. When will Xilinx support model checking? 

Q5. Does equivalency checking replace simulation? 

Q6. When should I use equivalency checking? 

Q7. Does Xilinx support post-XST flow? 

Q8. How will I benefit from using equivalency checking? 

Q9. What vendors does Xilinx support? 

Q10. Whom should I contact regarding support-related issues? 

Q11. Do any Xilinx Application Notes discuss flow? 

Q12. Does the flow work with all languages?  

Q13. What platforms are supported?  

Q14. How do I use equivalency checking to retarget an FPGA to an ASIC?  

Q15. What libraries does Xilinx provide?  

Q16. Where can I find Formal Verification Libraries for supported Formal Verification Tools?  

Solution

Q1. Does Xilinx support both equivalency checking and model checking?

A1. Xilinx supports only equivalency checking in the current ISE software. 



Q2. What is formal verification?

A2. Formal verification is an algorithmic-based approach to logic verification that exhaustively proves functional properties about a design. 

Typically, there are two types of formal verification, as follows:

Equivalence Checking

Verifies the functional equivalence of two designs that are at the same or different abstraction levels (for example, RTL-to-RTL, RTL-to-Gate, or Gate-to-Gate). 

Equivalence checking is used for design implementation verification.

Model Checking

Verifies that the implementation satisfies the properties of the design. 

Model checking is used early in the design creation phase to uncover functional bugs.



Q3. Why does Xilinx support equivalency checking?

A3. As device size and complexity increase, functional simulation is becoming very time-consuming for both testbench generation and simulation run time. 

Formal verification is attractive because its run time is short, and it has complete functional coverage.

In addition, formal verification is a proven technology/flow in an ASIC design environment. 

As more ASIC designers design with FPGAs, formal verification becomes a more important flow for design.



Q4. When will Xilinx support model checking?

A4. Model checking is not a mature technology, and customer acceptance has been very slow because each vendor has its own proprietary property description language.

Adoption of this technology might increase when a single standard language for describing the design properties is established. 

Xilinx will evaluate support for model checking based on customer demand.


Q5. Does equivalency checking replace simulation?

A5. Equivalency checking augments functional simulation.

For multi-million gate designs, equivalency checking is the only viable solution since simulation runs can take days or weeks to complete.

Also, coverage of the design with simulation is not complete; equivalency checking provides 100% coverage with no test vectors in a fraction of the time needed for simulation.


Q6. When should I use equivalency checking?

A6. You should use equivalency checking throughout the FPGA implementation flow.

You can use it to validate design re-optimization, synthesis, and place and route results against a golden RTL model.


Q7. Does Xilinx Support post-XST flow?

A7. No.


Q8. How will I benefit from using equivalency checking?

A8. Equivalency checking helps you verify designs more quickly. 

It helps ensure that the function in the final netlist matches the golden RTL design specification.

Equivalency checking also helps you isolate and debug problems more efficiently.


Q9. What vendors does Xilinx support?

A9. The following vendors are supported in ISE Design Suite:

Synopsys Formality:

http://www.synopsys.com

Cadence Conformal LEC:

http://www.cadence.com/

Mentor Graphics Formal Pro (supported directly by vendor):

http://www.mentor.com/

Vivado currently only supports OneSpin.


Q10. Whom should I contact regarding support-related issues?

A10. For tools and flow issues:

Synopsys Formality: 

http://solvnet.synopsys.com

Cadence Conformal: 

http://www.cadence.com/support/

Prover eCheck:

http://www.prover.com/contact/

For Library issues:

Xilinx Support: 

http://support.xilinx.com/support/clearexpress/websupport.htm


Q11. Do any Xilinx Application Notes discuss flow?

A11. All Xilinx Application Notes on formal verification are now obsolete.

For information on using formal verification, see the following:

Synopsys Formality: (Xilinx Answer 12815)

Cadence Conformal: (Xilinx Answer 20617)

Prover eCheck: (Xilinx Answer 20685)


Q12. Does the flow work with all languages?

A12. RTL Level: can be either VHDL or Verilog; contact the formal verification vendors for more information.

Gate Level: only the Verilog flow is supported by Xilinx.


Q13. What platforms are supported?

A13. The following platforms are supported:

Synopsys Formality

Sun OS Unix*: Yes

Linux Enterprise Edition*: Yes

Windows XP/2000*: No

Cadence Conformal

Sun OS Unix*: Yes

Linux Enterprise Edition*: Yes

Windows XP/2000*: No

Prover eCheck

Sun OS Unix*: Yes

Linux Enterprise Edition*: Yes

Windows XP/2000*: Yes

 *Xilinx ISE supported versions only


Q14. How do I use equivalency checking to retarget an FPGA to an ASIC?

A14. You can use either of the following two methods to retarget an FPGA to an ASIC:

  • RTL-to-Gate: Use this method if the source RTL is the same for both the FPGA and the ASIC.
  • FPGA Gate-to-ASIC Gate: Use this method to compare the FPGA gate-level netlist to the ASIC gate-level netlist.

Note: For more information on these flows, contact the formal verification vendor directly.


Q15. What libraries does Xilinx provide?

A15. Xilinx provides the following two libraries for formal verification:

  • UniSim Library* - Used for designs that have technology-specific instantiated cells for RTL instantiations.
  • SimPrim Library* - Used for post-NGDBuild and post-Place and Route netlists.

 *These are different from the simulation libraries provided by Xilinx.


Q16. Where can I find Formal Verification Libraries for supported Formal Verification Tools?

A16. For old ISE releases, refer to the CAE Vendor library offerings at:

http://www.xilinx.com/support/download/index.htm#tab-cl

Starting with the 12.1 release of the ISE Design Suite, the libraries are made available with the software. 

The files can be obtained at: at $XILINX/verilog/xeclib/.

The Vivado delivered libraries are available at $XILINX_VIVADO/data/verilog/src/xeclib/.

AR# 25007
Date Created 10/28/2007
Last Updated 07/07/2015
Status Active
Type General Article
Tools
  • ISE - 10.1
  • ISE Design Suite - 11.1
  • ISE Design Suite - 11.2
  • More
  • ISE Design Suite - 11.3
  • ISE Design Suite - 11.4
  • ISE Design Suite - 11.5
  • ISE Design Suite - 12.1
  • ISE - 8.1i
  • ISE - 8.1i sp1
  • ISE - 8.1i sp2
  • ISE - 8.1i sp3
  • ISE - 8.2i
  • ISE - 8.2i sp1
  • ISE - 8.2i sp2
  • ISE - 8.2i sp3
  • ISE - 9.1i
  • ISE - 9.1i sp1
  • ISE - 9.1i sp2
  • ISE - 9.1i sp3
  • ISE - 9.2i
  • ISE - 9.2i sp1
  • ISE - 9.2i sp2
  • ISE - 9.2i sp3
  • ISE - 9.2i sp4
  • ISE - Legacy
  • ISE Design Suite
  • Vivado Design Suite
  • Less