Abstract
This paper describes the T-Ruby system for designing VLSI circuits, starting from formal specifications in which they are described in terms of relational abstractions of their behaviour. The design process involves correctness-preserving transformations based on proved equivalences between relations, together with the addition of constraints. A class of implementable relations is defined. The tool enables such relations to be simulated or translated into a circuit description in VHDL. The design process is illustrated by the derivation of a circuit for 2-dimensional convolution.
Original language | English |
---|---|
Journal | Formal Methods in System Design |
Volume | 11 |
Issue number | 3 |
Pages (from-to) | 239-264 |
ISSN | 0925-9856 |
DOIs | |
Publication status | Published - 1997 |
Keywords
- Hardware description languages
- Relational specification
- Ruby
- Correctness-preserving transformations
- Synchronous circuit design