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.

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 (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 FPGA space, EC is still a relatively new concept but is rapidly becoming important given the large devices being employed today.

Introducing 360 EC-FPGA

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.

EC-FPGA Technology

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

Industry Support

Support for all major FPGA devices, including (but not limited to):

  • Intel: Quartus Prime flow for the following devices: Arria and Stratix (up to 10), Cyclone and Max (up to V)
  • Xilinx: Vivado flow for the following devices: Artix, Kintex, Spartan, and Virtex (up to 7 plus UltraScale/UltraScale+)
  • MicroSemi: Synplify and Libero SoC flow for the following devices: Axcelerator, Fusion/SmartFusion/SmartFusion2, IGLOO/e/2/nano/PLUS, PolarFire/PolarFire SoC, ProASIC3/3E/3L/nano, ProASICPLUS, RTG4

EC-FPGA Qualification

We see the introduction of EC for FPGA to be an important addition for the validation of safety critical applications using programmable devices. As well as providing an exhaustive check, EC will identify errors quickly with the minimum of debug.

Key Features and Benefits

  • Works with major FPGA synthesis tools, including the Xilinx Vivado Design Suite and ISE, Synopsys Synplify, Altera Quartus II and Microsemi Libero SoC design tools
  • Supported design languages: Verilog, SystemVerilog, VHDL, EDIF and Mixed Language
  • Supports all sequential optimisations in FPGA synthesis, including constant registers, register duplication and merging, renaming of flip-flop instances, FSM optimisations, local retiming and pipelining
  • Supports device specific optimisations including DSPs, SRLs, distributed RAM, and block RAM
  • Verifies single FPGA, flat netlists and imposes no restrictions on netlist size
  • Supports RTL/gate and gate/gate equivalence checking
  • Parallel and Distributed Operation