Third-party Logic Equivalence Checking Tools User Guide: Intel Quartus Prime Pro Edition

RSS

UG-20189 | 2018.06.28

OneSpin 360 EC-FPGA Software Support

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 Intel^® 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 Intel^® 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 Intel^® Stratix^® 10 designs in the Intel^® Quartus^® Prime Pro Edition software.

Verifying Post-Route Retiming with OneSpin 360 EC-FPGA software

Enabling OneSpin logic equivalence for Intel^® Stratix^® 10 devices involves obtaining the 360 EC-FPGA^® software and license, adding commands to the Intel^® 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:

Obtain the 360 EC-FPGA^® software and license for Intel^® Quartus^® Prime Retiming Verification from OneSpin Solutions.
To enable formal verification in the flow, open your Intel^® Stratix^® 10 project in the Intel^® 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 compilation:
```
set_global_assignment -name ENABLE_FORMAL_VERIFICATION ON
set_global_assignment -name EDA_GENERATE_FUNCTIONAL_NETLIST ON -section_id eda_simulation
set_global_assignment -name EDA_SIMULATION_TOOL "ModelSim (Verilog)"
set_global_assignment -name EDA_TIME_SCALE "1 ps" -section_id eda_simulation
set_global_assignment -name EDA_OUTPUT_DATA_FORMAT "VERILOG HDL" 
-section_id eda_simulation
```
Note: Although your RTL can be Verilog HDL, SystemVerilog, or VHDL, the Intel^® 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 Console:
```
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
```
The -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.

Figure 1. 360 EC-FPGA^® Shows Functionally Equivalent Design

If 360 EC-FPGA^® reports failed points in the netlist, review the Intel^® Quartus^® Prime compilation messages for any warning that relates to this failed point before further debugging the designs in 360 EC-FPGA^®.

Figure 2. 360 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

This document has the following revision history.

Document Version	Intel^® Quartus^® Prime Version	Changes
2018.06.28	18.0.0	Initial release of document.

Intel Quartus Prime Pro Edition User Guides

Refer to the following user guides for comprehensive information on all phases of the Intel^® Quartus^® Prime Pro Edition FPGA design flow.