Overviews

Commands

See Also

You can use the Verplex Conformal LEC software to perform formal verification of a Synplicity Synplify-generated Verilog Quartus^® Mapping File (.vqm) and a corresponding VQM File generated by the Quartus^® II software. The Conformal LEC software compares whether or not the Quartus II software correctly interprets the logic in the VQM File during synthesis and fitting.

To perform formal verification using the Conformal LEC and Quartus II software:

1. If you have not already done so, perform 1. Set Up the Conformal LEC Working Environment.

2. Generate a VQM File with the Synplify software. Guidelines

3. Create a new project in the Quartus II software.

4. Set the Preserve Hierarchical Boundaries logic option to Firm for all black box entities in the design. If any black box entities contain an instatiation of another black box entity, set the logic option on the top-level black box entity only.

5. Make sure all options in the Netlist Optimizations page of the Settings dialog box (Assignments menu) are turned off. Leaving these options turned on may result in mismatches between the original (golden) and Quartus II-generated (revised) VQM Files.

6. Specify EDA tool settings in the Quartus II software.

   Make sure you select Formal verification in the EDA Tools list and select Verplex Conformal LEC in the Tool name list in the EDA Tool Settings page of the Settings dialog box (Assignments menu).

7. Compile the design with the Quartus II software.

   The Quartus II Compiler generates the VQM File, a <design name>.vlc script file, which you can use to run the Conformal LEC software, a <design name>.v file that contains all the user-defined black box entities in the design, and places them in the /<project directory>/fv/clec directory. Additionally, for all of the black box entities which instantiate other black box entities, the Quartus II software will preserve the port interface of the entity (including the name and vector/scalar type of each port in the input and output VQM Files), and will include any name mapping information between the entity names, instances, and interface ports of the golden and revised VQM Files.

8. Start the Conformal LEC software and perform the formal verification by typing the following command at a UNIX prompt:

   lec -dofile / <path to project directory>/fv/clec/<design name>.vlc 

9. The Conformal LEC software shows the original VQM File netlist in the Golden window and the Quartus II-generated VQM 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.

The Conformal LEC software will only compare non-black box entities for logic equivalence.

10. To investigate the results of the verification, click the Mapping Manager icon in the toolbar, or choose Mapping Manager (Tools menu). The Conformal LEC software reports the mapped, unmapped, and compared points in the Mapped Points, Unmapped Points, and Compared Points windows, respectively.

    In the Compared Points window, the Conformal LEC software denotes equivalent points with a green dot, and non-equivalent points with a red dot. You can right-click on the points and choose Source Code to open the Source Code Manager and view the original source code, or choose Schematics to view the schematics of the golden and revised designs.

Back to Top