Why Your FPGA Synthesis Flow Requires Verification

When you think about it, logic synthesis is a vital but rather intimidating part of modern chip design. This process takes a high-level description of intended functionality, written in an RTL language that looks more like software than hardware, and implements it using the low-level building-block library of an ASIC or FPGA device. The resulting gate-level netlist must meet a variety of requirements for speed, area and power. These same requirements must continue to be satisfied after the full place-and-route process is complete. Modern synthesis tools are complex with both advanced algorithms and many “knobs” for user guidance.

Early users of ASIC synthesis tools worried a great deal about the impact of turning over manual gate-level design to automated tools. The savings in time and resources were clear, but designers worried about how they could verify the resulting netlist. For the pioneers, the only answer was to run gate-level simulations using as large a subset as possible from the full test suite run on the RTL code. But gate-level simulations were much slower than RTL, and provided no guarantee that errors introduced by synthesis tools would be found. EDA vendors addressed this situation by offering formal equivalence-checking (EC) tools.

An equivalence checker compares two design implementations and reports differences. It can compare two RTL designs, for example, before and after insertion of scan or built-in-self-test (BIST) logic. Another example is two different netlists, for example, two synthesis runs from the same RTL code for different target technologies. Perhaps most important, RTL-to-netlist comparison verifies the synthesis process itself, either finding errors in the netlist or formally proving that no such errors exist. This provides high confidence that logic synthesis can be trusted and, when paired with static timing analysis, largely eliminates the need for gate-level simulation.

EC tools can be hard to develop, but the fact that traditional ASIC synthesis leaves the state elements (registers and memory) untouched simplifies the problem. If there is a direct mapping between state elements in the RTL code and the netlist, then equivalence can be checked combinationally between state elements across a single clock cycle. The following diagram shows that, for common input values and completely mapped state elements, it is possible to prove that the outputs and next state values are equivalent. This means that the designs match.

Fig. 1: Equivalence checking proved that the golden design and the revised design after synthesis matched.

The availability of EC tools was a key factor in driving logic synthesis into the mainstream development flow, and this technology is ubiquitous within ASIC development teams today. However, EC tools are much less common in FPGA development flows. To some extent, this is just one result of a disturbingly common belief that verification is less important for FPGAs than for ASICs because bugs found in the lab can be fixed by re-programming devices. While is it true that changing an FPGA does not require the long leadtime and high cost to turn an ASIC, the time to find, diagnose, fix and verify FPGA bugs can be prohibitive.

As FPGA-based designs have become more complex, many development teams have adopted ASIC-like design and verification flows. In the case of EC tools, there are additional benefits for their usage in FPGA development. This is due to the aggressive nature of the optimizations and transformations performed by FPGA synthesis tools to satisfy design requirements and increase device utilization. FPGA tools perform several optimizations that change the mapping of state elements between input RTL and output netlist. A common example is retiming where logic is moved from one side of a register or memory to the other side to meet timing requirements.

This means that only a subset of state elements can be directly mapped and that a more sophisticated EC tool is required. This tool must perform most or all the mapping automatically, leverage combinational EC wherever possible, and apply sequential (multi-cycle) EC as needed on limited design portions. The following diagram shows two designs in which full state mapping is not possible. Despite this, an advanced EC tool can still formally prove equivalence.

Fig. 2: Even though full state mapping of these two designs is not possible, equivalence checking can formally prove equivalence.

This same approach works well to compare RTL code and netlist in the presence of other synthesis optimizations that change state element mapping, including state machine re-encoding and implementation of registers within memory. While close partnerships with FPGA vendors is necessary to tune EC settings for each specific FPGA device and flow, thus achieving a high degree of automation, the EC tool must work independently of any hints or side files from the synthesis tools.

Only with an advanced formal equivalence-checking tool with sequential capabilities, such as OneSpin 360 EC-FPGA, can FPGA designers be sure that aggressive synthesis resulted in a functionally equivalent netlist implementation. The level of certainty this flow provides is important for project success and valuable in meeting the requirements of safety standards such as DO-254 and ISO 26262 that require high confidence.