Assured VLSI design with formal verification

Jang Dae Kim, Shiu Kai Chin

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

1 Scopus citations

Abstract

Design and verification using formal logic extends existing VLSI design methods and tools. Such an extension provides rigorous support for design and verification at various levels of abstraction. Our design methodology combines design verification by mechanized theorem proving with conventional CAD tools. The theorem proving environment allows us to relate low level boolean implementations and high level arithmetic and instruction set specifications. We use the Higher-Order Logic theorem prover (HOL) to verify correctness relations between implementations and specifications. We use existing CAD tools to synthesize physical layouts and validate low level electrical and timing properties. Our CAD systems are Mentor Graphics GDT and MAGIC. To verify our design methodology, we fabricated a serial pipelined multiplier that is formally verified. Bit-serial circuits are widely used in signal processing. The multiplier chip was fabricated through MOSIS and worked correctly.

Original languageEnglish (US)
Title of host publicationCOMPASS - Proceedings of the Annual Conference on Computer Assurance
Editors Anon
PublisherIEEE Computer Society
Pages13-22
Number of pages10
StatePublished - 1997
EventProceedings of the 1997 12th Annual Conference on Computer Assurance, COMPASS'97 - Gaithersburg, MD, USA
Duration: Jun 16 1997Jun 19 1997

Other

OtherProceedings of the 1997 12th Annual Conference on Computer Assurance, COMPASS'97
CityGaithersburg, MD, USA
Period6/16/976/19/97

ASJC Scopus subject areas

  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Assured VLSI design with formal verification'. Together they form a unique fingerprint.

Cite this