Performing Formal Verification with Quartus II Integrated Synthesis and the Encounter Conformal Software
You can use the Quartus II software to compile a design and then use the Cadence Encounter Conformal software to perform formal verification of a design. The Encounter Conformal software performs a functional equivalence verification on the original RTL-level Verilog HDL and VHDL design versus the gate-level Verilog Output File (.vo) produced by Quartus II Integrated Synthesis and the Quartus II Fitter. In the Encounter Conformal software, the original RTL-level netlist is the golden netlist and the Quartus II-generated netlist is the revised netlist.
To compile the design in the Quartus II software and perform formal verification using the Encounter Conformal software:
Make sure the Perform gate-level register retiming option is turned off in the Synthesis Netlist Optimizations page and the Perform register retiming option is turned off in the Physical Synthesis Optimizations page of the Settings dialog box. Leaving these options turned on may result in mismatches between the RTL-level (golden) and Quartus II-generated (revised) netlists. Turn off Incremental Compilation on the Incremental Compilation page of the Settings dialog box to turn off incremental synthesis and fitting.
In the Formal Verification page of the Settings dialog box, select Conformal LEC in the Tool name list.
Make sure None is selected in the Tool name list in the Design Entry/Synthesis page of the Settings dialog box.
During compilation, the EDA Netlist Writer generates a Verilog Output File and a <design name>.ctc script file, which you can use to run the Encounter Conformal software, and places them in the /<project directory>/fv/conformal/ directory. The Quartus II software also generates a file that contains all the user-defined black box entities in the design and places it in the /<project directory>/fv/<project_revision>_blackboxes/ directory.
Note: When generating a gate-level Verilog Output File (.vo) netlist for use with the Synopsys Formality and Encounter Conformal formal verification tools, the Quartus II software automatically creates black boxes for entities that do not have a corresponding formal verification model, including:
Megafunctions and library of parameterized modules (LPM) functions that do not have an equivalent formal verification model.
Encrypted intellectual property (IP) cores.
Entities defined in any format other than Verilog HDL or VHDL, for example, AHDL or Block Design Files (.bdf).
RAM or any entity implemented in RAM. Any entities containing inferred RAM are converted to black box entities (Quartus II Integrated Synthesis/Encounter Conformal formal verification flow only).
Start the Encounter Conformal software and perform formal verification by typing the following command at a UNIX prompt:
lec -dofile /<path to project directory>/fv/conformal/<project_revision>.ctc
The Encounter Conformal software shows the original RTL netlist in the Golden window and the Quartus II-generated Verilog Output File netlist in the Revised window. The status window reports the results of the verification as either Equivalent or Non-equivalent. The status window also shows the number of compared DFFs and PO (Primary Outputs), and the number of each that are equivalent and non-equivalent, respectively.
Note: The Encounter Conformal software will only compare non black box entities and block box entity interfaces for logic equivalence.
To investigate the results of formal verification, click the Mapping Manager icon in the toolbar, or click Mapping Manager. The Encounter Conformal software reports the mapped, unmapped, and compared points in the Mapped Points, Unmapped Points, and Compared Points windows, respectively.
Note: In the Compared Points window, the Encounter Conformal software denotes equivalent points with a green dot, and non-equivalent points with a red dot. You can right-click the points and click Source Code to open the Source Code Manager and view the original source code, or click Schematics to view the schematics of the golden and revised designs.
For more information on using the Encounter Conformal software to perform formal verification, refer to the Encounter Conformal documentation.
文档资料
> 
