HOL2GDT a Formal Verification-Based Design Methodology
Final rept. Sep 1997-Mar 1999
SYRACUSE UNIV NY
Pagination or Media Count:
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 Graphics 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.
- Electrical and Electronic Equipment