Accession Number:

ADA390708

Title:

HOL2GDT a Formal Verification-Based Design Methodology

Descriptive Note:

Final rept. Sep 1997-Mar 1999

Corporate Author:

SYRACUSE UNIV NY

Report Date:

2001-04-01

Pagination or Media Count:

122.0

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 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.

Subject Categories:

  • Electrical and Electronic Equipment

Distribution Statement:

APPROVED FOR PUBLIC RELEASE