Even though FPGAs are reprogrammable, an error detected late in the design cycle, or even after the board has gone into production, can still be very expensive. In addition, some FPGA vendors offer migration to structured ASICs, in which a fabricated design cannot be reprogrammed. Therefore, it is even more important for designs targeted towards structured ASIC device families that implementation errors are caught early in the development phase.

For all of the above reasons, customers want to verify the functional correctness of the RTL-to-bitstream design transformations. Formal methods are becoming increasingly popular in the FPGA design methodology, as they offer several advantages over the traditional method of vector-based simulation. Some of these advantages are shorter runtime, better functional coverage, and no need for test vectors.

Figure 1 shows the application of formal verification in the FPGA design flow.

Figure 1 — Formal verification support in the FPGA design flow

Verification challenge

When comparing revisions of the same design using formal verification, formal verification tools rely heavily on information provided by the compilation tool used to transform the design. This information includes:

• State machine encoding
• Register duplication and merging
• Combinational loop detection
• Redundant register removal
• Register name changes

For efficient and easy verification of the design transformations using formal verification, the compilation tools (synthesis or place and route) have to record all the transformations and make available those transformations to customers in the form of scripts. The following section addresses some of the best techniques to generate a netlist that is easy to verify, and to generate formal verification scripts enabling one-click comparison.