Forum Discussion
Cyclone 10 GX Simulation Files
- 2 years ago
Below is engineering's feedback:
---
Simulation netlist (which customer is using) is not meant for formal verification.
having said that we should be including all parameters in the ATOM instances in simulation netlist.
---
From engineering feedback, it seems that the simulation netlist generated is not meant for OneSpin formal verification.
When formal verification is enabled(set_global_assignment -name ENABLE_FORMAL_VERIFICATION ON), I checked that these are the verilog netlist generated under the project directory:
verification/
rtl/ (This directory contains all rtl files)
elaborated/ (Directory contains files used in RTL vs Elaborated Verification)
synthesized/ (Directory contains files used in Elaborated vs Synthesized Verification)
planned/ (Directory contains files used in Synthesized vs Planned Verification)
placed/ (Directory contains files used in Planned vs Placed Verification)
routed/ (Directory contains files used in Placed vs Routed Verification)
retimed/ (Directory contains files used in Routed vs Retimed Verification)
final/ (Directory contains files used in Routed/Retimed vs Finalized Verification)
You could perform Formal Verification at each stage
elaborated : To verify RTL vs elaborated netlist
synthesized : To compare elaborated vs synthesized netlist
planned: To compare synthesized vs planned netlist
placed: To compare planned vs placed netlist
routed: To compare placed vs routed netlist
retimed: To compare routed vs retimed netlist
final: To compare routed/retimed vs finalized netlist
Will inform if there is further update from the engineering.
Regards,
Richard Tan
Below is engineering's feedback:
---
Simulation netlist (which customer is using) is not meant for formal verification.
having said that we should be including all parameters in the ATOM instances in simulation netlist.
---
From engineering feedback, it seems that the simulation netlist generated is not meant for OneSpin formal verification.
When formal verification is enabled(set_global_assignment -name ENABLE_FORMAL_VERIFICATION ON), I checked that these are the verilog netlist generated under the project directory:
verification/
rtl/ (This directory contains all rtl files)
elaborated/ (Directory contains files used in RTL vs Elaborated Verification)
synthesized/ (Directory contains files used in Elaborated vs Synthesized Verification)
planned/ (Directory contains files used in Synthesized vs Planned Verification)
placed/ (Directory contains files used in Planned vs Placed Verification)
routed/ (Directory contains files used in Placed vs Routed Verification)
retimed/ (Directory contains files used in Routed vs Retimed Verification)
final/ (Directory contains files used in Routed/Retimed vs Finalized Verification)
You could perform Formal Verification at each stage
elaborated : To verify RTL vs elaborated netlist
synthesized : To compare elaborated vs synthesized netlist
planned: To compare synthesized vs planned netlist
placed: To compare planned vs placed netlist
routed: To compare placed vs routed netlist
retimed: To compare routed vs retimed netlist
final: To compare routed/retimed vs finalized netlist
Will inform if there is further update from the engineering.
Regards,
Richard Tan
Sorry I went on vacation last week and have been side tracked. I am glad to see there is a solution to this that seems to solve this. I do have a question about this though.
Inside the verification directory it produced an IO with the differential_mode attribute.
The only issue is that the component is a twentynm_io_ibuf. Should this be expected, because the input was a cyclone10gx_io_ibuf?
If this is the solution, we can adapt to it, but I just wanted to get a little verification here first.
Thanks for the information thus far.