The Case For FPGA Equivalence Checking

Formal Equivalence Checking (EC) has become a standard part of the ASIC development flow, replacing almost all gate level simulation with a rigorous consistency check between pre- and post-synthesized code.

In the Field Programmable Gate Array (FPGA) space, EC is still a relatively new concept, but is rapidly becoming important given the large devices being employed today. For the largest FPGA, debugging a synthesis mismatch, some of the hardest systematic errors to discover, can take days through the traditional method of prototyping on the actual final device.

Furthermore, the latest FPGA synthesis tools employ advanced optimizations, including retiming the circuit, and these can lead to errors. Often the only way to effectively discover an issue is to switch off those optimizations until the problem disappears, leaving the device to operate at less efficiency than its potential.

Let’s explore how FPGA equivalence checking technology can impact the speed and quality of results through the lens of a leading data center provider.

OneSpin’s EC-FPGA enabled this data center provider to develop crucial competitive advantages and accelerate verification for its high-end FPGA designs when other verification methods failed. EC-FPGA assured that the synthesis optimizations that were used to achieve competitive functionality, power, and performance capabilities didn’t introduce new bugs. This ultimately resulted in zero design bug escapes.

The data center provider had to meet several goals to deem the use of FPGA equivalence checking a success. First and foremost, exhaustively verifying the functional equivalence of Register Transfer Level (RTL) code to synthesized netlists and the final placed & routed FPGA designs was mandatory.  But they also had to assure that no bugs were introduced through advanced synthesis, place and route, and engineering change orders. In order to meet the critical time-to-market window, the use of gate-level simulation had to be minimized. Simulation was proving ineffective in other ways as well. Simulation failed to detect the root cause of a bug discovered in the lab within the Vivado synthesis tool. This bug could have had devastating consequences with the final product was deployed.

Using hierarchical synthesis and equivalence checking, the company was able to achieve easier, faster bug detection. The following methodology was used.

• Automatic bottom-up verification between the individual modules was done with EC-FPGA
• The modules that were equivalent were black boxed
• Modules that had issues were isolated
• The next step for the verification team was to analyze the modules with issues and debug them.

Synthesis tool is set up and forced to preserve the hierarchy and disable any cross-boundary optimization.

As a result, the critical bug that simulation missed was detected in a matter of hours compared to weeks of trying other methods without success.

There are many more success stories involving OneSpin’s 360 EC-FPGA solution. To read more case studies, I invite you to visit https://www.onespin.com/customer-stories.