Extending VLSI design with higher-order logic

Anand Chavan, Shiu Kai Chin, Juin Yeu Lu

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

Abstract

Extending VLSI CAD with higher-order logic integrates formal verification with synthesis. The benefits of doing so are: 1) relating instruction-set descriptions to implementations, 2) designing at a higher level of abstraction than at the level of schematics, 3) verifying by proof, 4) reusing verified parameterized designs, 5) automatically compiling designs in higher-order logic to parameterized cell generators and layouts, and 6) validating electrical and functional properties by simulation. Such an integration is demonstrated by linking the Cambridge Higher-Order Logic (HOL) theorem-prover with the Mentor Graphics GDT design environment. We illustrate its application by creating a parameterized macro-cell generator for an n-bit Am2910 microprogram sequencer, whose design is formally verified with respect to its instruction-set architecture specification.

Original languageEnglish (US)
Title of host publicationProceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors
Editors Anon
PublisherIEEE Computer Society
Pages85-94
Number of pages10
StatePublished - 1995
EventProceedings of the 1995 IEEE International Conference on Computer Design: VLSI in Computers & Processors - Austin, TX, USA
Duration: Oct 2 1995Oct 4 1995

Other

OtherProceedings of the 1995 IEEE International Conference on Computer Design: VLSI in Computers & Processors
CityAustin, TX, USA
Period10/2/9510/4/95

ASJC Scopus subject areas

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Extending VLSI design with higher-order logic'. Together they form a unique fingerprint.

Cite this