Transformational VLSI Design

Ole Steen Rasmussen

    Research output: Book/ReportBookResearchpeer-review

    Abstract

    This thesis introduces a formal approach to deriving VLSI circuits by the use of correctness-preserving transformations. Both the specification and the implementation are descibed by the relation based language Ruby. In order to prove the transformation rules a proof tool called RubyZF has been constructed. It contains a semantical embedding of Ruby in Zermelo-Fraenkel set theory (ZF) implemented in the Isabelle theorem prover. A small subset of Ruby, called Pure Ruby, is embedded as a conservative extension of ZF and characterised by an inductive definition. Many useful structures used in connection with VLSI design are defined in terms of Pure Ruby and their properties proved. The design process is illustrated by several non-trivial examples of standard VLSI problems.
    Original languageEnglish
    PublisherDepartment of Information Technology, Technical University of Denmark
    Number of pages250
    Publication statusPublished - 1997

    Cite this