The aim of this CAD project is to verify the equivalence of two different levels of abstractions by relying only on formal verification methods without the use of simulation. Provided with an RTL design (VHDL/VERILOG), a gate level description must be synthesized in order to formally test its correspondence to the RTL using equivalence checking tools. Next, a buggy gate level description of the same design will be provided to compare it with the synthesized gate level in order to identify and fix the existing bugs.
The used CAD tools in this project are:
A thorough read of the Digital Logic Synthesis and Equivalence Checking Tools Tutorial document, as well as reviewing other reference material and tutorials on Synopsys Design Vision, Synopsys Formality, and Cadence Conformal Logical Equivalence Checker, will be very helpful during the work on the project. The behavioral RTL models are taken from the OPENCORES.ORG web site (see http://www.opencores.org). From that page, we will assign following designs to the groups of the class (click here for a list of group member names and project assignments).
The main tasks of the CAD project are listed as follows:
(2) Describe the system function using state machines, block diagrams or circuit structures.
(3) Synthesize the RTL code that is acceptable by Formality and Conformal LEC
(4) Starting from submodules of the design, incrementally synthesize the design and verify equivalence between RTL and gate level descriptions at each level.
(5) You will be provided with a buggy gate level description of the design that you will compare against both the Reference RTL and your gate level designs. You have to find the bugs in the design and correct them.
(6) Use BOTH "Synopsys Formality" and "Cadence Conformal Logical Equivalence Checker" to perform Formal Equivalence Checking and provide a comparative study of the obtained results.
(7) Write a detailed project report documenting above tasks and illustrating the main challenges you faced in this project (including where you were unable to show equivalence).
The CAD project shall be carried out on our ENCS machines on which the CAD tools Synopsys and Cadence are installed under Linux OS (not Windows). You will need to be able to run these CAD tools remotely via a ssh session and X-server (for example by installing an ssh client such as PuTTy and an X-Server software such as Xming). Detailed instructions about remote access to our CAD tools can be found at this document).
The projects can be carried out in the AITS lab H-823 on the 8th floor of the Hall Building. However, the PCs must be booted in Linux since all the project tools are installed under Linux and not Windows. In order to access the laboratories with Linux machines running VLSI tools (Cadence/Synopsys), check on this web site for the door codes
More information on how to use Modelsim and Precision (Digital logic Design Tools) can also be found at this document).
References:
Schedule
Technical Support:
For questions related to the project itself, please contact