HOL2GDT a Formal Verification-Based Design Methodology
Abstract
HOL2GDT is a VLSI design methodology. It starts with a design implementation description that is formally verified using the Higher Order Logic (HOL) theorem prover. This implementation description is translated into a hardware description language model by using a HOL2GDT compiler, and with this model a physical design layout is generated by using IC design placement and routing tools in Mentor Graphic's Generator Design Technology (GDT) package. Thus, the final IC layout is generated from a formally verified description. This document illustrates the design methodology in detail to serve as a manual for the HOL2GDT system. It covers (1) how to define formal implementation descriptions of the hardware design, (2) how to translate implementation descriptions into L language schematic generator models, and (3) how to get physical IC layouts from schematic models. A complete example of an n-bit Serial Multiplier design is used to illustrate the HOL2GDT design methodology.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 2001
- Accession Number
- ADA390708
Entities
People
- Anand Chavan
- Byoung Woo Min
- Shiu-kai Chin
Organizations
- Syracuse University