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.
- 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
Stratix® 10 project in the
Quartus® Prime Pro Edition software, and add the following assignments to
.qsf file. These assignments direct the Compiler
to generate the onespin.tcl script during
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_simulationNote: 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
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.tclThe -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 Intel® Quartus® Prime compilation messages for any warning that relates to this failed point before further debugging the designs in 360 EC-FPGA®.
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.
|Document Version||Intel® Quartus® Prime Version||Changes|
Refer to the following user guides for comprehensive information on all phases of the Intel® Quartus® Prime Pro Edition FPGA design flow.