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

    Rasmussen, O. S. (1997). Transformational VLSI Design. Department of Information Technology, Technical University of Denmark.
    Rasmussen, Ole Steen. / Transformational VLSI Design. Department of Information Technology, Technical University of Denmark, 1997. 250 p.
    @book{ff416cf39a314a8ca72cc687c34a96cb,
    title = "Transformational VLSI Design",
    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.",
    author = "Rasmussen, {Ole Steen}",
    year = "1997",
    language = "English",
    publisher = "Department of Information Technology, Technical University of Denmark",

    }

    Rasmussen, OS 1997, Transformational VLSI Design. Department of Information Technology, Technical University of Denmark.

    Transformational VLSI Design. / Rasmussen, Ole Steen.

    Department of Information Technology, Technical University of Denmark, 1997. 250 p.

    Research output: Book/ReportBookResearchpeer-review

    TY - BOOK

    T1 - Transformational VLSI Design

    AU - Rasmussen, Ole Steen

    PY - 1997

    Y1 - 1997

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

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

    M3 - Book

    BT - Transformational VLSI Design

    PB - Department of Information Technology, Technical University of Denmark

    ER -

    Rasmussen OS. Transformational VLSI Design. Department of Information Technology, Technical University of Denmark, 1997. 250 p.