Functional correctness of FPGA synthesis from RTL code to final netlist
Systematic design errors, introduced by automated design refinement tools, such as synthesis, can be hard to detect, and damaging if they make it into the final device. Formal equivalence checking has been used for ASIC design flows for many years. As FPGAs become bigger and critical system components, exhaustively verifying the functional equivalence of Register Transfer Level (RTL) code to synthesized netlists and the final placed & routed FPGA designs is mandatory.
360 EC-FPGA is an automatic sequential equivalence checking tool that provides a fast and efficient method to ensure that aggressive synthesis optimizations have not introduced systematic errors that could disrupt the final design.
360 EC-FPGA Highlights
- Ensures that complex FPGAs are free of synthesis and optimization errors
- Dramatically accelerates the design implementation and debug loop
- Allows risk-free use of advanced synthesis optimization
- Eliminates gate level simulation and stimulus, easy to setup and apply
- Supports all FPGA synthesis optimizations, including complex sequential retiming
The Need for Formal Equivalence Checking
- Bus connecting ordering
- Coincident read discrepancies
- Wrong FSM re-encoding
- Undriven or unconnected wires
- Incorrectly coded pipeline
- Incorrect BRAM parameter settings
- Clock gaiting for low power issues
- P&R connecting issues
- Additional, unspecified logic added
FPGA Design Flow Issues
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.
360 EC-FPGA Enables Advanced FPGA Optimizations
A major benefit of the 360 EC-FPGA is to ensure that advanced FPGA synthesis optimizations, used to achieve competitive functionality, performance, power consumption, and cost targets, do not introduce functional errors. It supports all sequential synthesis optimizations performed in FPGA design flows. It verifies whole-chip, flat netlists, allowing for the most aggressive optimizations to be leveraged.
360 EC-FPGA verifies the optimized design 'as is' without gate-level simulation, design modifications or design restrictions, such as disabling synthesis optimizations. It eliminates the need for extensive scripting and many 'side files' generated by synthesis tools, providing a greater level of independence from the synthesis process.
The tool is “self-starting” by providing automated setup capabilities that detect mapping information, clocks and resets, and other initialization settings. An advanced debugger is also included, which displays mismatches both directly in source and schematic windows, as well as through generated waveform traces.
360 EC-FPGA handles gate representations to which all FPGA synthesis optimizations have been applied, for example:
- Stuck-at (constant) registers
- Register duplication and merging
- FSMs with safe- and unknown encodings
- TMR optimizations (triple modular redundancy)
- Asynchronous feedback loops
- IO cells and different bus resolution schemes
- Fixed gated clocks
- DSP48 optimizations
- SRL Optimizations, such as asynchronously resettable register chains and inference into different memory models
- RAM / ROM, including Distributed- & Block RAM
- Power optimizations
360 EC-FPGA supports all major FPGA technology families from Xilinx, Microsemi, and Intel FPGA (Altera). In addition, EC-FPGA includes the OneSpin Structural Analysis App to provide a focused formal-based structural code analysis that can catch other common coding errors.
360 EC-FPGA Technology
Sequential & Combinational Comparison Combined
360 EC-FPGA follows a conventional EC verification flow: design setup, mapping and comparison, and optional debug. However, the underlying sequential equivalence checking technology utilized in 360 EC-FPGA, which makes use of the OneSpin formal property checking engines, eliminates many of the design restrictions necessary with other solutions, as follows:
- Mapping: The pairing of RTL to gate flops does not need to be complete in 360 EC-FPGA to provide conclusive results
- Comparison: 360 EC-FPGA deploys sequential verification engines, generating counterexamples for some compared points independent of the mapping of other compared points
- Debug: 360 EC-FPGA utilizes simulation trace based debug. Static failing patterns are generated on demand
Simulation Trace Based Debugging in 360 EC-FPGA
A typical verification script will simply configure the flow for the respective FPGA vendor and synthesis tool and then run the steps of the flow. Synthesis independence is maintained.
The tool is designed to execute quickly and with the high capacity necessary to handle large FPGAs in both hierarchical and flat modes. It can operate over a network of multiple machines for additional performance.
OneSpin collaborates closely with its FPGA and synthesis partners including Xilinx, Intel, MicroSemi and the Synopsys Synplify team. 360 EC-FPGA is used internally at multiple companies, as a golden accuracy standard to test their design flows.
Support for all major FPGA devices:
- Intel: Quartus Prime flow for the following devices: Stratix 10, Arria 10, and Cyclone V
- Xilinx: Vivado flow for the following devices: Spartan 2/2E/3/XL/6/7, Virtex E/2/2p/4/5/6/7, Artix 7, Kintex 7, Kintex UltraScale, and Kintex UltraScale+
- MicroSemi: Synplify & Libero flow for the following devices: Fusion, ProASIC3/3E/3L, IGLOO(E), Axcelerator, 54sx(a), ex, 3200dx, 40/42mx, SmartFusion(2), IglooPlus, Igloo2, and Rad-Tolerant FPGAs
Flexible, all inclusive design flow support:
- Synthesis flows, including Xilinx Vivado™, Synopsys Synplify®, and Intel Quartus®
- Standards: Verilog, SystemVerilog, VHDL, EDIF & Mixed Language
- Platforms: Linux, Windows
- Parallel and Distributed Operation
Tool Qualification Kit
OneSpin offers an optional OneSpin 360 EC-FPGA Tool Qualification Kit (TQK) based on certification from the internationally-recognized testing body TÜV SÜD. The certification states that EC-FPGA meets the most stringent tool qualification criteria set by functional safety standards ISO 26262 (TCL3/ASIL D), IEC 61508 (T2/SIL 3) and EN 50128 (T2/SIL 3). Users can apply the TQK directly to the tool evaluation step required by the functional safety standards with no additional tool qualification effort. This removes the burden of tool qualification from users, accelerating their own certification process.