### Abstract

Original language | English |
---|

Publisher | Department of Information Technology, Technical University of Denmark |
---|---|

Number of pages | 250 |

Publication status | Published - 1997 |

### Cite this

*Transformational VLSI Design*. Department of Information Technology, Technical University of Denmark.

}

*Transformational VLSI Design*. Department of Information Technology, Technical University of Denmark.

**Transformational VLSI Design.** / Rasmussen, Ole Steen.

Research output: Book/Report › Book › Research › peer-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 -