You can optionally use the third-party OneSpin 360 EC-FPGA® sequential equivalence checking tool to verify
the logic equivalence between specific netlists following compilation. The 360 EC-FPGA® software can help you to
confirm that aggressive Compiler optimizations do not introduce unexpected results.
For example, in the current version of the
Quartus® Prime Pro Edition software, you can use the OneSpin 360 EC-FPGA® software to confirm the logic equivalence
between the routed and retimed netlists after circuit retiming in
Stratix® 10 designs, or after making changes to initial conditions. The 360 EC-FPGA® tool can confirm that the
routed and retimed netlists remain functionally equivalent after those changes.
Note: OneSpin 360 EC-FPGA® logic equivalence checking is supported only for
Stratix® 10 designs in the
Quartus® Prime Pro Edition software.
Verifying Post-Route Retiming with OneSpin 360 EC-FPGA software
Enabling OneSpin logic equivalence for
Stratix® 10 devices involves obtaining the 360 EC-FPGA® software and license, adding commands to the
Quartus® Prime Settings File (.qsf), compiling the design, and running the 360 EC-FPGA® tool.
Follow these steps to verify functional equivalence
between the routed and retimed netlists with OneSpin 360 EC-FPGA® software:
To enable formal verification in the flow, open your
Stratix® 10 project in the
Quartus® Prime Pro Edition software, and add the following assignments to
the <project_name>.qsf file. These assignments direct the Compiler
to generate the onespin.tcl script during
Note: Although your RTL can be Verilog HDL, SystemVerilog, or VHDL, the
Quartus® Prime EDA Netlist Writer requires that you
specify the assignments only in Verilog HDL, as the example shows.
To run full compilation (including Synthesis, Plan, Place,
Route, and Retime stages), click Start
Compilation on the Compilation Dashboard. The Compiler preserves
a snapshot of the results at each stage.
To generate a Verilog Output File (.vo) containing a snapshot of the routed netlist, type the
following command in the Console:
quartus_eda --snapshot=routed <project_name>
The .vo generates to <project_directory>/simulation/modelsim/routed/<project_name>.vo.
To generate a .vo
containing a snapshot of the retimed netlist, type the following command in the
quartus_eda --snapshot=retimed <project_name>
The .vo generates to <project_directory>/simulation/modelsim/retimed/<project_name>.vo.
To launch OneSpin 360 EC-FPGA®, type the following command in the Console
within the project directory:
onespin -i verification/retimed/onespin.tcl
-i option opens the 360 EC-FPGA® software GUI.
Follow the instructions in OneSpin's 360 EC-FPGA® software documentation to run
360 EC-FPGA® and confirm
logic equivalence of the routed and retimed netlists. 360 EC-FPGA® compares the routed and retimed
netlists and reports the functional equivalence.
If 360 EC-FPGA®
reports that the netlists are functionally equivalent, then retiming optimization
did not change the functionality of the design.
If 360 EC-FPGA®
reports failed points in the netlist, review the
Quartus® Prime compilation messages for any warning that relates to this
failed point before further debugging the designs in 360 EC-FPGA®.
EC-FPGA® Shows Failed Points in Netlist
If the 360
EC-FPGA® reports open states without failure, this indicates that the design
complexity may exceed the capability of the 360 EC-FPGA® software. Contact OneSpin support for assistance
with designs that exceed 360
EC-FPGA® software capabilities.
OneSpin 360 EC-FPGA Software Support Revision History