Performing Formal Verification with Quartus® Prime Standard Edition Integrated Synthesis and the Encounter Conformal Software

You can use the Quartus® Prime Standard Edition 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 VerilogHDL and VHDL design versus the gate-level Verilog Output File (.vo) Definition produced by Quartus® Prime Standard Edition Integrated Synthesis and the Quartus® Prime Standard Edition Fitter. In the Encounter Conformal software, the original RTL-level netlist is the golden netlist and the Quartus® Prime Standard Edition-generated netlist is the revised netlist.

To compile the design in the Quartus® Prime Standard Edition software and perform formal verification using the Encounter Conformal software:

  1. If you have not already done so, set up the Encounter Conformal working environment.
  2. Create a new project or open an existing project.
  3. Turn off Incremental Compilation on the Incremental Compilation page of the Settings dialog box.
  4. In the Formal Verification page of the Settings dialog box, select Conformal LEC in the Tool name list.
  5. Make sure None is selected in the Tool name list in the Design Entry/Synthesis page of the Settings dialog box.
  6. Before compilation in the Quartus® Prime Standard Edition software, refer to the Design Guidelines for Using Quartus® Prime Standard Edition Integrated Synthesis and the Encounter Conformal Software topic for design guidelines to avoid mismatches when performing formal verification.
  7. On the Processing menu, click Start Compilation.

    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® Prime Standard Edition 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® Prime Standard Edition software automatically creates black boxes for entities that do not have a corresponding formal verification model, including:
    1. Megafunctions and library of parameterized modules (LPM) functions that do not have an equivalent formal verification model.
    2. Encrypted intellectual property (IP) cores.
    3. Entities defined in any format other than VerilogHDL or VHDL, for example, AHDL or Block Design File (.bdf) Definition.
    4. RAM or any entity implemented in RAM. Any entities containing inferred RAM are converted to black box entities (Quartus® Prime Standard Edition Integrated Synthesis/Encounter Conformal formal verification flow only).
  8. Start the Encounter Conformal software and perform formal verification by typing the following command at a Linux prompt:
    lec -dofile /<path to project directory>/fv/conformal/<project_revision>.ctc
  9. The Encounter Conformal software shows the original RTL netlist in the Golden window and the Quartus® Prime Standard Edition-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.
  10. 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 clickSource 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
Related concepts

About the Project Navigator
Related tasks

Setting Up the Encounter Conformal Working Environment
Setting Up the EDA Tool Environment
Related reference

Design Guidelines for Using Integrated Synthesis and the Encounter Conformal Software
Incremental Compilation Page (Settings Dialog Box)
Formal Verification Page (Settings Dialog Box)

Contact Altera | Legal Notice

Copyright© 2015 Altera Corporation. All rights reserved. ALTERA, ARRIA, CYCLONE, HARDCOPY, MAX, MEGACORE, NIOS, QUARTUS, STRATIX, and all other brands, unless noted otherwise, and/or trademarks of Altera Corporation in the U.S. and other countries.