Performing Formal Verification with Encounter Conformal Software
You can use the Cadence Encounter Conformal software to perform formal verification of a Synplicity Synplify-generated Verilog Quartus Mapping File (.vqm) and a corresponding Verilog Output File (.vo) generated by the Quartus II software. The Encounter Conformal software determines whether or not the Quartus II 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 II software:
Make sure the Perform gate-level register retiming option is turned off in the Synthesis Netlist Optimizations page of the Settings dialog box. Leaving this option turned on may result in mismatches between the original (golden) and Quartus II-generated (revised) netlists.
Make sure thatIncremental Compilation is turned on, and select Full incremental compilation.
The formal verification flow uses entities defined as black boxes rather than user-created partitions. The Quartus II software preserves the boundaries of those black box entities as internally generated partitions when you turn on Full incremental compilation.
Note: When generating a gate-level Verilog Out 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).
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 II 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 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.
Additionally, for all the black box entities that instantiate other black box entities, the Quartus II 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 UNIX 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 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 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.
Literature
> 
