Linking higher order logic to a VLSI CAD system

Juin Yeu Lu, Shiu Kai Chin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We show how hardware implementation descriptions written in Higher Order Logic (HOL) are transformed into VLSI layouts. The intent is to link formally verified designs to physical implementations. Once HOL structural descriptions are transformed to structural descriptions and parameterized cell generators in a VLSI CAD system, the tools associated with the VLSI CAD system can be used such as standard cell libraries, automatic placement and routing, and simulation. The cell generator programs derived from verified HOL descriptions provide a means by which verified and parameterized HOL designs can augment a cell library within a CAD system. The particular VLSI CAD system used here is the GDT system from Mentor Graphics. The GDT system includes a CMOS standard cell library, a macrocell synthesis tool which includes automatic placement and routing, and the Lsim multilevel simulator. GDT uses a structural language called L. HOL structural descriptions are first mapped to L, then layouts corresponding to the L descriptions are created using the standard cell library and the layout generation tools. We illustrate this design process by creating the layout for an 8-bit serial/parallel multiplier which has been verified in HOL.

Original languageEnglish (US)
Title of host publicationHigher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings
PublisherSpringer Verlag
Pages199-212
Number of pages14
Volume780 LNCS
ISBN (Print)9783540578260
StatePublished - 1994
Event6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993 - Vancouver, Canada
Duration: Aug 11 1993Aug 13 1993

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume780 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993
CountryCanada
CityVancouver
Period8/11/938/13/93

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Linking higher order logic to a VLSI CAD system'. Together they form a unique fingerprint.

  • Cite this

    Lu, J. Y., & Chin, S. K. (1994). Linking higher order logic to a VLSI CAD system. In Higher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings (Vol. 780 LNCS, pp. 199-212). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 780 LNCS). Springer Verlag.