Performing Formal Verification with the Encounter Conformal Software

You can use the Cadence Encounter Conformal software to perform formal verification of a Synopsys Synplify-generated Verilog Quartus Mapping File (.vqm) Definition and a corresponding Verilog Output File (.vo) Definition generated by the Quartus^® Prime Standard Edition software. The Encounter Conformal software determines whether or not the Quartus^® Prime Standard Edition software correctly interprets the logic in the Verilog Quartus Mapping File during synthesis and fitting.

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

If you have not already done so, set up the Encounter Conformal working environment.
Generate a Verilog Quartus^® Prime Standard Edition mapping file with the Synplify software.Refer to the 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.
Create a new projectin the Quartus^® Prime Standard Edition software.
Make sure thatIncremental Compilationis turned on, and selectFull incremental compilation.
The formal verification flow uses entities defined as black boxes rather than user-created partitions. The Quartus^® Prime Standard Edition software preserves the boundaries of those black box entities as internally generated partitions when you turn onFull incremental compilation.
Note:
When generating a gate-levelVerilog Output File (.vo) Definition 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).
Specify EDA tool settings in the Quartus^® Prime Standard Edition software.
Note:
Make sure you select Conformal LEC in the Tool name list in the Formal Verification page of the Settings dialog box.
Compile the design with the Quartus^® Prime Standard Edition software.
Note:
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.

Additionally, for all the black box entities that instantiate other black box entities, the Quartus^® Prime Standard Edition software preserves the port interface of the entity (including the name and vector/scalar type of each port in the input Verilog Quartus Mapping File and the output Verilog Output File), and includes any name mapping information between the entity names, instances, and interface ports of the golden (Verilog Quartus Maping File) and revised (Verilog Output File).
To start the Encounter Conformal software and perform the formal verification, type the following command at a Linux prompt:
lec -dofile /<path to project directory>/fv/conformal/<project_revision>.ctc
The Encounter Conformal software shows the original Verilog Quartus Mapping File 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 DFFs and PO (Primary Outputs) compared and the number of each that are equivalent and non-equivalent, respectively.
Note:
The Encounter Conformal software compares only non-black box entities for logic equivalence.
To investigate the results of the verification, click the Mapping Manager icon in the toolbar, or choose 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.