Formal Verification Design Example
Equivalence checking between a golden (reference) design and the revised design is a formal verification technique to verify that both designs are logically equivalent. Both golden and revised designs could be in synthesizable HDL or gate-level netlist form. The method of formal verification does not involve any vectors, stimulus, or testbench. This technique is usually used when your HDL design (golden side) is transformed (synthesized) to another domain like a gate-level netlist. Compared to the gate-level netlist simulation technique, this technique quickly verifies that all the HDL design intent is transformed correctly, though this technique is not a complete replacement for gate-level timing simulations. This design example illustrates the formal verification flow with the Altera® Quartus® II software-generated, post-fit netlist files and the Cadence Encounter Conformal tool.
After going through this design example, you will be able to perform formal verification between your register transfer level (RTL) HDL and the post-fit netlist generated from the Quartus II software. You will learn how to set up the Quartus II software for formal verification and understand the Quartus II software outputs that are necessary for performing this process.
In this example, you will do the following:
- Load an existing project in the Quartus II software
- Set up the Quartus II software to acquire the files necessary for formal verification
- Compile the project with these settings
- Understand the outputs generated for formal verification
- Run the formal verification
This example was developed using the Quartus II software version 6.0 service pack 1 running on a Red Hat Linux machine and the Cadence Encounter Conformal tool version 06.10-p100 (25-May-2006) running on the same host. You can use the same design example with the Quartus II software and the Cadence Encounter Conformal tool running on hosts with Windows or Sun Solaris operating systems.
This design example consists of a simple 8-bit multiplier block and a phase-locked loop (PLL) block implemented in a Stratix® II device. All the libraries necessary for formal verification are provided with the Quartus II software. To use this design example, perform the following steps:
- Download the Quartus II Archive File (.qar) for the multiplier design.
- At the Linux system command prompt, type
quartus multiplier.qar and press Enter.
- The Quartus II software starts, displaying the Restore Archived Project dialog box. In the Restore Archived Project dialog box, specify the desired location for the restored project and click OK.
- On the Assignments menu choose Settings.
- On the EDA Tool Settings page of the Settings dialog box, under Formal Verification, select Conformal LEC.
- On the Incremental Compilation page of the Settings dialog box ensure Full Incremental Compilation is turned on.
- Click OK to close the Settings dialog box.
- Compile the design. After compilation, multiplier.vo is created at <project_dir>/fv/conformal. This is the post-fit netlist generated by the Quartus II software to be used in formal verification with the Cadence Encounter Conformal tool. The Quartus II software also generates scripts at <project_dir>/fv/conformal for use with the Cadence Encounter Conformal tool.
- Close the Quartus II software.
- Navigate to the <project_dir>/fv/conformal directory by typing
cd <project_dir>/fv/conformal, at the Linux command prompt.
- Start the Cadence Encounter Conformal software by typing
lec –dofile multiplier.ctc. This command invokes the Cadence Encounter Conformal tool and also runs formal verification between your HDL design files and the Quartus II software-generated, post-fit netlist. Observe the results in the Cadence Encounter Conformal tool.
If you compiled the project with the Quartus II software running on a Windows machine and the Cadence Encounter Conformal tool running on a UNIX/Linux machine, you may have to edit the scripts produced by Quartus II software to run the design example.
For more detailed information on performing formal verification using Quartus II software and Cadence Encounter Conformal tool, refer to the Cadence Encounter Conformal Support (PDF) chapter in volume 3 of the Quartus II Handbook.
Related Links
Design Examples Disclaimer
These design examples may only be used within Altera Corporation devices and remain the property of Altera. They are being provided on an “as-is” basis and as an accommodation; therefore, all warranties, representations, or guarantees of any kind (whether express, implied, or statutory) including, without limitation, warranties of merchantability, non-infringement, or fitness for a particular purpose, are specifically disclaimed. Altera expressly does not recommend, suggest, or require that these examples be used in combination with any other product not provided by Altera.
|
Literature
> 
