The T-Ruby Design System.
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.
Introduction
This paper describes a computer-based system, known as T-Ruby [12], for designing
VLSI circuits starting from a high-level, mathematical specification of their behaviour:
A circuit is described by a binary relation between appropriate, possibly complex domains
of values, and simple relations can be composed into more complex ones by the
use of a variety of combining forms which are higher-order functions.
The basic relations and their combining forms generate an algebra, which defines
equivalences (which may take the form of equalities or conditional equalities) between
relational expressions. In terms of circuits, each such equivalence describes a general
correctness preserving transformation for a whole family of circuits of a particular form.
In the design process, these equivalences are exploited to transform a "specification" in
the form of one Ruby expression to an "implementation" in the form of another Ruby
expression, in a calculation-oriented style [4, 9, 13].
T-Ruby is based on a formalisation of Ruby, originally introduced by Jones and
Sheeran [3], as a language of functions and relations, which we refer to as the T-Ruby
language. The purpose of the paper is to demonstrate how such a general language
can be used to bridge the gap between a purely mathematical specification and the
implementable circuit. The design of a circuit for 2-dimensional convolution is used to
illustrate some of the features of the method, in particular that the step from a given
mathematical specification to the initial Ruby description is small and obvious, and
that the method allows us to derive generic circuits where the choice of details can be
postponed until the final actual synthesis.
The T-Ruby system enables the user to perform the desired transformations in the
course of a design, to simulate the behaviour of the resulting relation and to translate
the final Ruby description of the relation into a VHDL description of the corresponding
circuit for subsequent synthesis by a high-level synthesis tool. The transformational
style of design ensures the correctness of the final circuit with respect to the initial
specification, assuming that the equivalences used are correct. Proofs of correctness
are performed with the help of a separate theorem prover, which has a simple interface
to T-Ruby, so that proof burdens can be passed to the prover and proved equivalences
passed back for inclusion in T-Ruby's database.
The division of the system into the main T-Ruby-system, a theorem prover and a
VHDL translator has followed a "divide and conquer" philosophy. Theorem proving
can be very tedious and often needs specialists. In our system the designer can use the
proved transformation rules in the computationally relatively cheap T-Ruby system,
leaving proofs of specific rules and conditions to the theorem prover. When a certain
level of concretisaion is reached efficient tools already exist to synthesise circuits.
Therefore we have chosen to translate our relational descriptions into VHDL.
Ruby
The work described in this paper is based on the so-called Pure Ruby subset of Ruby,
as introduced by Rossen [10]. This makes use of the observation that a very large
class of the relations which are useful for describing VLSI circuits can be expressed
in terms of four basic elements: two relations and two combining forms. These are
usually defined in terms of synchronous streams of data as shown in Figure 1. In the

Figure

1: The basic elements of Pure Ruby
figure, the type sig(T ) is the type of streams of values of type T , usually represented
as a function of type Z ! T , where we identify Z with the time. The notation aRb
means that a is related to b by R, and is synonymous with (a; b) 2 R.
The relation spread f is the lifting to streams of the pointwise relation R of type
ff - fi, whose characteristic function is f (of type ff such that (f a b) is
true R. The type of spread f is then sig(ff) - sig(fi), the type of relations
between streams of type ff and streams of type fi. For notational convenience, and to
stress the idea that it describes the lifting to streams of a pointwise relation of type
ff - fi, this type will be denoted ff
sig
Thus spread f , for suitable f , describes (any) synchronously clocked combinational
circuit, while the relation D - the so-called delay element - describes the basic sequential
circuit. F ; G (the backward relational composition of F with G) describes the serial
composition of the circuit described by F with that described by G . If F is of type
ff
sig
- fl and G is of type fl
sig
fi, then this is of type ff
sig
- fi. Finally, [F ; G ] (the relational
product of F and G) describes the parallel composition of F and G . For F of type
sig
sig
this is of type (ff 1 \Theta ff 2 ) sig
The types of
the relations describe the types of the signals passing through the interface between
the circuit and its environment. However, it is important to note that the relational
description does not specify the direction in which data passes through the interface.
"Input" and "output" can be mixed in both the domain and the range.
R
ff fi
(a)
(b)
(c)
F
G
(d)

Figure

2: Graphical interpretations of:
A feature of Ruby is that relations and combinators not only have an interpretation
in terms of circuit elements, but also have a natural graphical interpretation,
corresponding to an abstract floorplan for the circuits which they describe. The conventional
graphical interpretation of spread (or, in fact, of any other circuit whose
internal details we do not wish to show) is as a labelled rectangular box. The components
of the domain and range are drawn as wire stubs, whose number reflects the
types of the relations in an obvious manner: a simple type gives a single stub, a pair
type two and so on. The components of the domain are drawn up the left hand side
and the components of the range up the right.
The conventional graphical interpretation for D is as a D-shaped figure, with the
domain up the flat side and the range up the rounded side, while F ; G is drawn with
the range of F "plugged into" the domain of G , and [F with the two circuits F
and G in parallel (unconnected). These conventions are illustrated in Figure 2. For
further details, see [3].
3 The T-Ruby Language
In T-Ruby all circuits and combinators are defined in terms of the four Pure Ruby
elements using a syntax in the style of the typed lambda calculus. Definitions of
some circuits and combinators with their types are given in Figure 3. ff, fi and so on
denote type variables and can thus stand for any type. The first five definitions are
of non-parameterised stream relations, which correspond to circuits. +, defined using
the spread element applied to a function which evaluates to true when z equals the
sum of x and y , pointwise relates two integers to their sum. ' is the (polymorphic)
identity relation, dub pointwise relates a value to a pair of copies of that value and
reorg pointwise relates two ways of grouping three values into pairs. These all describe
combinational circuits; all except just describe patterns of wiring, and are known as
wiring relations. The fifth, SUMspec, describes a simple sequential circuit : an adding
machine with an accumulator register.
The remaining definitions are examples of combinators, which always have one
or more parameters, typically describing the circuits to be combined. Applying a
combinator to suitable arguments gives a circuit. Thus (Fst R) is the circuit described
by [R; '], R l S (where the combinator l is written as an infix operator) is the circuit
where R is below S and the second component in the domain of R is connected to the
first component of the range of S . In the definition of l (and elsewhere), R -1 denotes
the inverse relation to R. The graphical interpretations of Fst and l are shown in

Figure

4.
The dialect of Ruby used in the T-Ruby system is essentially that given by Rossen
in [8]. This differs from the standard version of Ruby given by Jones and Sheeran in [3]
in that "repetitive" combinators and wiring relations are parameterised in the number
of repetitions. This is reflected in the type system which includes dependent product
types [5], a generalisation of normal function types. This enable us explicitly to express
the size of repetive structures in the type system. For example, the combinator map
(which "maps" a relation over all elements in a list of streams) has the polymorphic
dependent type:
where nlist[n]T is the type of lists of exactly n elements of type T . Thus map is a
function which takes an integer, n, and a relation of type ff
sig
- fi as arguments and
int \Theta int sig
int
': ff
sig
dub: ff
sig
dub 4
reorg: ((ff \Theta fi) \Theta fl)
sig
(int \Theta control) sig
(bool \Theta int)
loop4 (Fst (Snd D) ; ALU a ; (Snd dub))
Fst
sig
Fst 4
sig
l: (ff \Theta fi)
sig
sig
sig
l 4
Fst (R)
sig
sig
sig
sig
sig
else Fst (apr n-1
sig
sig
sig

Figure

3: Examples of circuit and combinator definitions in T-Ruby.
Fst (R) R l S map 3 R tri 3 R colf 3 R rdrf 3 R
R
R
R
R
R
R

Figure

4: Graphical interpretation of some combinators
returns a relation whose type, nlist[n]ff sig
- nlist[n]fi, is dependent on n, the so-called
\Pi -bound variable. A full description of the T-Ruby type system can be found in [11].
The relation apr n , used in the definition of map, pointwise relates an n-list of values
and a single value to the (n 1)-list where the single value is appended "on the right"
of the n-list 1 .
The combinator mapf is similar to map but the second parameter is a function
from integers to relations, so that the relation used can depend on its position in the
structure. creates a triangular circuit structure, colf a column structure where each
relation is parametrised in its position in the column. Finally rdrf , called "reduce
right", is a kind of column structure. It has its name from functional programming
and will, if for example used with the relation + as argument, calculate the sum of a
list of integers. The graphical interpretations of some of these repetitive combinators
are shown in Figure 4.
Note that the definitions are all given in a point-free notation, reflecting the fact
that they are all expressed in terms of the elements of Pure Ruby. It is easy to show
that they are equivalent to the expected definitions using data values; for example,
However, defining circuits in terms of Pure Ruby elements offers several advantages: it
greatly simplifies the definition and use of general rewrite rules; it simplifies reasoning
about circuits in a theorem prover; and it eases the task of translating the language
into a more traditional VLSI specification language such as VHDL.
4 The Transformational Phase of T-Ruby Design
The design process in T-Ruby involves three main activities, reflecting the overall design
of the system: (1) Transformation, (2) Proof and (3) Translation to VHDL. In
this section we consider the first phase, which involves transforming an initial specification
by rewriting, possibly with the addition of typing or timing constraints, so as
to approach an implementable design described as a Ruby relation.
1 Note that the size argument n here, as elsewhere, is written as a subscript to improve readibility.
4.1 Rewriting
Rewriting is an essential feature of the calculational style of design which is used in
Ruby. The T-Ruby system allows the user to rewrite Ruby expressions according to
pre-defined rewrite rules. Rewriting takes place in an interactive manner directed by
the user, using basic rewrite functions, known as tactics, which can be combined by
the use of higher order functions known as tacticals. This style of system is often
called a transformation system to distinguish it from a conventional rewrite system.
T-Ruby is implemented in the functional programming language Standard ML (SML),
which offers an interactive user environment, and the tactics and tacticals are all SML
functions, applied in this environment.
In the T-Ruby system, a rewrite rule is an expression with the form of an equality
or an implication between two equalities, with explicit, typed universal quantification
over term variables and in most cases implicit universal quantification over types via
the use of type variables. Apart from this there are no restrictions on the forms of the
rules which may be used. In practice, however, the commonly used rules are equalities
between relational expressions, corresponding to equivalences between circuits,
which can be used to manipulate a circuit description in Ruby to another, equivalent
form. Rules for manipulating integer or Boolean expressions could, of course, also be
introduced, but most such manipulations are performed automatically by a built-in
expression simplifier based on traditional rewriting to a normal form.
Some examples of rules can be seen in Figure 5. The first rules express simple facts
about the combinators, such as the commutativity of Fst and Snd (fstsndcomm), the
fact that the inverse of a serial composition is the backward composition of the inverses
(inversecomp), and the distributivity of Fst over serial composition (fstcompdist). The
fourth rule, maptricomm, is an example of a conditional rule: the precondition that R
and S commute over serial composition must be fulfilled in order for tri n R and map n S
to commute. Similarly, forkmap states that if R is a functional relation then a single
copy on the domain side of an n-way fork is equivalent to n copies on the range side
of the fork. Finally, rules such as retimecol, are used in Ruby synthesis to express
timing features, such as the input-output equivalence of a circuit to a systolic version
of the same circuit. Note that since all these rules contain universal quantifications
over relations of particular types, they essentially express general properties of whole
families of circuits.
In the T-Ruby system, the directed rules used for rewriting come from three sources.
They may be explicit rewrite rule definitions, implicit definitions derived from circuit or
combinator definitions (which permit the named circuit or combinator to be replaced
by its definition or vice-versa), or lemmata derived from previous rewrite processes
which established the equality of two expressions, say t and t 0 .
In T-Ruby, the correctness of the explicit rules is proved by the use of a tool [7]
based on the Isabelle theorem prover [6], using an axiomatisation of Ruby within ZF
set theory. To make life easier for the user, conjectured rewrite rules can, however,
be entered without having been proved. When rewriting is finished, all such unproved
rewrite rules are printed out. Together with any instantiated conditions from the
conditional rules, they form a proof obligation which the user must transfer to the
theorem prover, in order to ensure the soundness of the rewriting process.
fstsndcomm=
sig
-
sig
sig
-
sig
(R
fstcompdist 4
sig
-
sig
Fst (R
sig
-
sig
(R
sig
(R
retimecol=
sig
(col

Figure

5: Rewrite rules in T-Ruby.
4.2 Constraints
The transformation process in the T-Ruby system primarily involves rewriting expressions
as described above. However, rewriting can only produce relations which are
exactly equivalent to the original, abstract specification. These relations are often too
large and have to be restricted to obtain an implementable circuit. As a trivial exam-
ple, the relation described above is defined as being of type (int \Theta int) sig
- int. For
implementation purposes we want to restrict the integers to values representable by a
finite number of bits. From a mathematical point of view this means restricting our
relation to the subtype given by:
- int n+1
where int n is a subtype of integers representable by n bits. In T-Ruby we describe this
subtyping by adding relational constraints [13] to the expression. The initial specifi-
Bint n
int n
O
n-bit
n-bit
(n+1)-bit
int n+1
int
int
int
int n
int n+1
(b)
(a)
id n+1
int n
(c)
Bits

Figure

Adding constraints to a relation
cation of + is depicted in Figure 6(a). We narrow the type of + by adding relational
constraints to the domain and the range, in this case instantantions of id n , the identity
relation for integers representable by n bits. This can be defined by:
id n= (Bits n ; Bits n
where Bits n relates an integer to a list of n bits which represent it. The constrained
relation is:
as shown in Figure 6(b). The definition of id n can then be expanded, giving:
[(Bits
as shown in Figure 6(c), and the relations Bits n can be manipulated into the original
relation by using the general rewrite rules.
Another style of constraint is to add delay elements, D, to the domain or range
of the relation. Since Ruby relations relate streams of data, where each element in
the stream corresponds to a specific time instant, this changes the timing properties
of the circuit. As a simple example, the relation + defined in Figure 3 describes a
purely combinational circuit. Adding n delay elements on the range side would give a
specification of an adder with a total delay of n time units. Now we can use the same
general relational rewrite rules to "push" the delay elements into the combinational
part, thus obtaining a description of an adder with the same external timing properties,
but with a different internal arrangement of the registers. This style of manipulation
is illustrated in more detail by the convolution example in the following section. Note
that the same relational framework is used to describe and manipulate both type and
timing constraints.
An interesting variation is to mix the two methods above. For example, by adding a
relational specification of a bit-serial to integer converter as a constraint on the domain
side of + and its inverse on the range side, we obtain a specification of a bit-serial adder
and can manipulate it to get an implementable circuit as above.
Finally, the specification can be constrained by instantiation of free type or term
variables. Free term variables are typically used to describe otherwise unspecified
circuit elements or to give the size of regular structures in a generic manner. By
instantiation we obtain a description of a more specialised circuit with a particular
circuit element or particular dimensions.
In general the transformation process starts from a relational specification, spec, of
a circuit, at some suitably high level of abstraction. spec is then rewritten by a number
of equality rewrites in order to reach a more implementable description. During the
rewrite process the relation can be narrowed by adding relational constraints. The
process can be illustrated by a series of transformations:
where the primes denote the added constraints. The original specification is changed
accordingly from spec to spec 00:::0 , reflecting the addition of the constraints and ensuring
equality between impl and the final constrained specification. From a logical point
of view [15], the constraints can be regarded as the assumptions under which the
implementation fulfills the original specification:
constraints ' (impl , spec)
4.3 An Example: 2-dimensional Convolution
As an example of the tranformation process, we present part of the design of a VLSI
circuit for 2-dimensional discrete convolution. The mathematical definition is that from
a known as the convolution kernel, and a stream of values
a, a new stream of values c should be evaluated, such that:
+r
+r
The intuition behind this is that the stream a represents a sequence of rows of length
w , and that each value in c is a weighted sum over the corresponding value in the
a-stream and its "neighbours" out to distance \Sigmar in two dimensions, using the weights
given by the matrix K. This is commonly used in image processing, where a is a stream
of pixel values scanned row-wise from a sequence of images, and K describes some kind
of smoothing or weighting function. Note that for each i , the summation over j is
equal to the 1-dimensional convolution of a with the i 'th row of K with a time offset
of w 1-dimensional convolution is defined by:
+r
4.3.1 Formulating the problem in Ruby
The first step in the design process is to formulate the mathematical definitions in
Ruby. Following the style of design used for a correlator in [3], we now divide the
relation between a and c into a combinational part, which relates c-values at a given
time to a 0 -values at the same time (for convenience we let the summation run from 1
applying the substitution i new
and a temporal part which relates the a 0 values at time t to the original a-values:
a 0
The temporal part, the matrix a 0
, can be further split into parts which can easily be
specified directly in Ruby. First we for a given i find a relation which relates b i to a
1)-list of a 0
1. An offset dependent on the position j , such that a 0
which in
Ruby can be specified by stating that (a 00 ; a 0 ) are related by (tri 2r+1 D
2. A (2r 1)-way fork, such that a 00
specified by (a 000 ; a 00
3. A fixed offset, such that a 000
specified by (b
4. Assembling 1-3 we get:
(b 0
Next we find a relation relating a to a (2r + 1)-list of b i 's:
1. An offset dependent on position i , such that b 0
specified by
(b
2. A (2r 1)-way fork, such that b 00
specified by (b
3. Another fixed offset, such that b 000 specified by (a; b 000
4. Assembling 1-3 we get:
(a; [b 0
It is convenient to rewrite the two relations above (the two (4)) as follows:
(b 0
butterfly 2r+1 D) (5)
(a; [b 0
butterfly 2r+1 D w
where the combinator butterfly is defined by:
sig
(app n+1;n
Fst (irt n+1 R
The combinational part of the convolution relation is easily expressed in Ruby in
terms of a combinator Q , of type int ((int \Theta int) sig
- int), such that (Q
relates (a; x ) to (K ij a + x ), which expresses the convolution kernel as a function of
position within the matrix K. If we then define c i
(t), it is easy
to demonstrate that, for all t and arbitrary x , ([a 0
(t)]; x (t)) is related
to c i (t) by the Ruby relation (rdrf 2r+1 (Q i )), where rdrf defined in Figure 3.
Combining this with the temporal relations given in definitions 5 and 6 we find that
the entire 2-dimensional convolution relation CR 2 , which relates (a; x ) and
a given w , r , x and Q can be expressed in terms of the one-dimensional convolution
relation (CR 1 i ), which relates (b 0
((int \Theta int) sig
butterfly r D) ; rdrf 2r+1 (Q i
(int \Theta int) sig
int
CR 2= Fst (fork butterfly r D w
CR 1 corresponds to the inner summation over j in the specification. The graphical
interpretation of CR 2 for is shown on the left in Figure 7, and the interpretation
of (CR on the right. The butterflies contain increasing numbers of delay
elements, D, above the mid-line and increasing numbers of "anti-delay" elements, D -1
below the mid-line. As follows from the definitions, the small butterflies use single delay
elements, corresponding to the time difference between consecutive elements in the data
stream, while the large butterflies use groups of w delay elements, corresponding to
the time difference between consecutive lines in the data stream.
To define these relations in T-Ruby, it is convenient to parameterise them, so that
they become combinators dependent on r , w and Q . The final definitions are:
(int \Theta int) sig
(Fst (fork butterfly r D) ; rdrf 2r+1 Q)
(int \Theta int) sig
(Fst (fork butterfly r (D w
With these definitions, the actual circuit for 2-dimensional convolution is described by
the relation (conv2 r w Q) for suitable values of r , w and Q .

Figure

7: Two dimensional convolution for
4.3.2 Transformation to an implementable relation
Unfortunately, the relation given above does not describe a physically implementable
circuit, if we assume (as we implicitly have done until now) that the inputs appear in
the domain of the relation (as x and a) and the outputs in the range (as c). This is
because of the "anti-delays", D -1 , in the butterflies. So instead of trying to implement
the relation (conv2 r w Q) as it stands, we implement a retimed version of it, formed
by adding a constraint on the domain side which delays all the input signals:
Fst (D r ; (D w
This will result in the anti-delays being cancelled out, as the delay elements in the
constraint are moved "inwards" into the original relation. The resulting circuit will, of
course, produce its outputs r units later than the original circuit, but
this is the best we can achieve in the physical world we live in!
From here on we use a series of rewrite rules to manipulate the relation into a
more obviously implementable form. The output from the T-Ruby system during this
derivation is shown, in an annotated and somewhat abbreviated form, in Figure 8. In
the concrete syntax produced by the T-Ruby prettyprinter, free variables are preceded
by a %-sign, repeated composition R n is denoted by R-n, and relational inverse R -1 by
R~, while "x:t.b denotes a -expression variable x of type t and
body b. The derivation finishes with the relational expression:
Fst (fork 2r+1
This is a generic description of a convolution circuit, expressed in terms of three free
variables: r and w , corresponding respectively to the kernel size for the convolution
and the line size for the 2-dimensional array of points to be convoluted, and Q , which
gives the kernel function.
To obtain a description of a particular concrete circuit, we can then use the
Ruby system's facilities for instantiating such free variables to particular values. For
definition of conv2.g
(Fst (D-%r;D-%w-%r));((Fst ((fork (2*%r+1));(butterfly %r D-%w)));
2. fstcompdist (used from right to left).g
(Fst ((D-%r;D-%w-%r);((fork (2*%r+1));(butterfly %r D-%w))));
use rule forkmap.g
(Fst (((fork (2*%r+1));(map (2*%r+1) (D-%r;D-%w-%r)));(butterfly %r D-%w)));
butterfly
(Fst ((fork (2*%r+1));((map (2*%r+1) D-%r);(tri (2*%r+1) D-%w))));
fRule maptricomm, and then rule fstcompdist.g
((Fst (fork (2*%r+1)));((Fst (tri (2*%r+1) D-%w));(Fst (map (2*%r+1) D-%r))));
(Fst (fork (2*%r+1)));((Fst (tri (2*%r+1) D-%w));
"k:int.(((Fst D-%r); "i:int.(conv1 %r (%Q i)) k))))
definition of conv1.g
(Fst (fork (2*%r+1)));((Fst (tri (2*%r+1) D-%w));
"k:int.(((Fst D-%r);((Fst ((fork (2*%r+1));(butterfly %r D)));
fNow use a similar procedure to the above to remove the remaining butterfly.g
(Fst (fork (2*%r+1)));((Fst (tri (2*%r+1) D-%w));
"k:int.((((Fst (fork (2*%r+1)));(Fst (tri (2*%r+1) D)));
using definition of Fst , then use [tri n D;
(Fst (fork (2*%r+1)));((Fst (tri (2*%r+1) D-%w));
"k:int.((((Fst (fork (2*%r+1)));((Snd D~-(2*%r+1));
(Fst (fork (2*%r+1)));((Fst (tri (2*%r+1) D-%w));
"k:int.(((Fst (fork (2*%r+1)));((Snd D~-(2*%r+1));
another constraint on the domain side: Snd (D w
(Snd D-%w-(2*%r+1));((Fst (fork (2*%r+1)));((Fst (tri (2*%r+1) D-%w));
"k:int.(((Fst (fork (2*%r+1)));((Snd D~-(2*%r+1));
fRule fstsndcomm, and Fst R ;
((Fst (fork (2*%r+1)));[(tri (2*%r+1) D-%w),D-%w-(2*%r+1)]);
"k:int.((((Fst (fork (2*%r+1)));(Snd D~-(2*%r+1)));
(Fst (fork (2*%r+1)));
(rdrf (2*%r+1) "k:int.(((Snd D-%w);((Fst (fork (2*%r+1)));((Snd D~-(2*%r+1));
(Fst (fork (2*%r+1)));
"k:int.((((Fst (fork (2*%r+1)));(Snd (D-%w;D~-(2*%r+1))));
\Gamman .g
(Fst (fork (2*%r+1)));
"k:int.((((Fst (fork (2*%r+1)));(Snd D-(%w -(2*%r+1))));

Figure

8: Derivation of the 2-dimensional convolution relation
example, we might instantiate r to 2, w to 64 and Q to -
acc 4
describes a multiply-and-add circuit with multiplication factor (i
and the kernel element described by (Q use this factor as the weight in
accumulating the weighted sum.
After suitable reduction of the integer expressions, this would give us the relational
description:
Fst (fork 5
with no free variables. The graphical interpretation of this final version of the circuit is
shown in Figure 9. As can be seen in the figure, the circuit is semi-systolic, with a latchc
a
z
s

Figure

9: Semi-systolic version of two dimensional convolution for 2.
The left-hand structure depicts the entire circuit.
The basic building element shown on the right corresponds to the
relation Snd D ; (Q k p) with Q instantiated as described in the
text.
The middle structure depicts Snd D
Only 3 of the 59 delay elements in D 59 are shown.
Arrows in the figure indicate the input/output partitioning determined
by the causality analysis.
(described by a delay element, D) associated with each combinational element, but with
a global distribution of the input stream a to all of the combinational elements.
4.4 Selection and Extraction
The rewriting system of T-Ruby includes facilities for selection of subterms from the
target expression by matching against a pattern with free variables. This can be used
to restrict rewriting temporarily to a particular subterm, or, more importantly, for
extraction of part of the target expression for implementation. In the latter case, the
remainder of the target expression gives a context describing a set of implementation
conditions that must be fulfilled for the extracted part to work
Extraction is in many respects the converse of adding relational constraints to
the specification, and the context specifies the same sorts of requirement. Firstly, it
may give representation rules which must be obeyed at the interface to the extracted
subterm, and secondly (if the context contains delay elements, D), it may give timing
requirements for the implementation of the subterm.
For the trivial example of the adder above the extracted part will typically, after
some rewriting, be the circuit inside the dashed box on Figure 6(c). The implementation
conditions in this case express the fact that integers must be represented by n
bits, as specified by Bits n .
5 VLSI Implementation
The relational approach to describing VLSI circuits offers a greater degree of abstraction
than descriptions using functions alone, since the direction of data flow is not
specified. However, real circuits offer particular patterns of data flow, and this means
that the interpretation of a relation may in general be 0, 1 or many different circuits.
In the case of zero circuits, we say the relation is unimplementable. The widest class
of relations which are generally implementable is believed to be the causal relations,
as defined by Hutton [2]. These generalise functional relations in the sense that inputs
are not restricted to the domain nor outputs to the range.
In T-Ruby, causality analysis is performed at the end of the rewriting process, when
the user has extracted the part of the relation which is to be implemented. In most
cases, in fact, the context from which the relation is extracted is non-implementable:
for example, it may specify timing requirements which (if they could be implemented)
would correspond to foreseeing the future.
5.1 Causality analysis
More exactly, a relation is causal if the elements in each tuple of values in the relation
can be partitioned into two classes, such that the first class (the outputs) are functionally
determined by the second class (the inputs), and such that the same partitioning
and functional dependency are used for all tuples in the relation. For example, the
previously defined relation + is causal, in the sense that the three elements
of each tuple of values in the relation can be partitioned as described, in fact in three
different ways:
1. With x and y as inputs and z as output, so that the relation describes an adder .
2. With x and z as inputs and y as output, so that the relation describes a subtractor
.
3. With y and z as inputs and x as output, so that the relation describes another
subtractor .
Note that the relation + -1 is also causal, although it is not functional. Essentially,
causality means that the relation can be viewed under the partitioning as a deterministic
function of its inputs.
In T-Ruby, the relation to be analysed is first expanded, using the definitions of
its component relations, to a form where it is expressed entirely in terms of the four
elements of Pure Ruby and relational inverse. The expanded relation is then analysed
with a simple bottom-up analysis heuristic. For combinational elements described by
spread relations, causality is determined by analysing the body of the spread , which
must have the form of a body part which is:
ffl an equality with a single variable on the left-hand side,
ffl a conjunction of body parts, or
ffl a conditional choice between two body parts.
In each equality, the result of the analysis depends on the form of the right-hand side.
If this is a single variable, no conclusions are drawn, as the equality then just implies
a wire in the abstract floorplan. If the right-hand side is an expression, all values in
it are taken to be inputs, and the left-hand side is taken to be an output. In choices,
all values in the condition are taken to be inputs. If these rules result in conflicts, no
causal partitioning can be found. When there are several possible causal partitionings,
as in the case of +, on the other hand, the rules enable us to choose a unique one.
For delay elements, D, values in the domain are inputs and those in the range
are outputs. Parallel composition preserves causality, and so in fact does inversion,
but serial compositions in general require further analysis, to determine whether the
input/output partitionings for the component relations are compatible with an implementable
(unidirectional) data flow between the components. Essentially, checks are
made as to whether two or more outputs are used to assign a new signal value to the
same wire, whether some wires are not assigned signal values at all or whether there
are loops containing purely combinational components. This additional analysis is exploited
in order to determine the network of the circuit in the form of a netlist with
named wires between active components. At present there is no backtracking, so if the
arbitrary choice of partitioning when there are several possibilities is the "wrong" one,
then it will not be possible to find a complete causal partitioning for the entire circuit.
As an example, let us consider the analysis of parts of the relation for 2-dimensional
convolution. The central element in this is the relation given by acc(p
describes the combinational multiply-and-add circuit for kernel element (p; k ). Using
the definition of acc, and substituting (p reduces to:
spread
The body of the spread has the form of an equality with a single left-hand side, and
thus the causal partitioning will make z an output and m and s both inputs. In this
case, the relation is functional from domain to range, but in general this need not be
so.
Since delay elements, D, can only have inputs on the domain side and outputs
on the range side, the serial composition (Snd D compatible with this
analysis of acc(p as the range of the delay element corresponds to component s
in the domain of acc(p Further analysis proceeds in a similar manner, leading to
the final data flow pattern shown by arrows in Figure 9.
5.2 Translation to VHDL
Since causality analysis gives both the network of the circuit and the direction of data
flow along the individual wires between components, the actual translation to VHDL is
comparatively simple. Each translated "top level" Ruby relation is declared as a single
design unit, incorporating a single entity with a name specified by the user. In rough
terms, each combinational relation C which is not a wiring relation within the expanded
Ruby relation is translated into one or more possibly conditional signal assignments,
where the outputs of C are assigned new values based on the inputs. For example, the
above gives rise to a single concurrent signal assignment
of the form:
where sig z, sig s and sig m are the names of the VHDL signals corresponding to
z , s and m respectively, and W is a constant equal to the value of (p for the
circuit element in question. Since the operators available for use with operands of
integer, Boolean, bit and character types in Ruby are (with one simple exception:
logical implication) a subset of those available in VHDL, this direct style of translation
is problem-free. In a similar manner, any conditional (if-then-else) expressions in the
body of a spread are directly translated into conditional assignment statements, possibly
with extra signal assignments to evaluate a single signal giving the condition.
The VHDL types for the signals involved are derived from the Ruby types used
in the domain and range of C in an obvious way. Thus for the elementary types,
the Ruby type bit is translated to the VHDL type rubybit, bool to rubybool, int to
rubyint, and char to rubychar, where the VHDL definitions of rubybit, rubybool,
rubyint and rubychar are predefined in a package RUBYDEF, which is referred to by
all generated VHDL units. Composed types give rise to groups of signals, generated
by (possibly recursive) flattening of the Ruby type, such that a pair is flattened into
its two components, a list into its n components and so on until elementary types are
reached.
If the Ruby relation refers to elementary types other than these pre-defined ones, a
package declaration containing suitable type definitions is generated by the translator.
For example, if an enumerated type etyp is used, a definition of a VHDL enumerated
type rubyetyp with the same named elements is generated.
Free variables of relational type and all non-combinational relations in the Ruby
relation are translated into instantiations of one or more VHDL components. For
example, a Delay relation, D. of Ruby type t sig
is a simple type, will
be translated into an instantiation of the component dff rubyt, where rubyt is the
type corresponding to t , as above. For composed types, such as pairs and lists,
two or more components, each of the appropriate simple type, are used. Standard
definitions of these components for all standard simple Ruby types are available in a
library. Other components (in particular those generated from free relational variables)
are assumed to be defined by the user.
The final result of translating the fully instantiated 2-dimensional convolution relation
into VHDL is shown in Figure 10. The figure does not show the entire VHDL
code (which of course is very repetitive owing to the regular nature of the circuit),
but illustrates the style. Signal identifiers starting with input and output correspond
generated code. Do not edit.
Compiled 950201, 11:58:28 from Ruby relation:
-%% ((Fst (fork 5));
-%% (rdrf 5 "k:int.
-%% ((((Fst (fork 5));(Snd D-59));
ENTITY conv264 IS
PORT
END conv264;
ARCHITECTURE ruby OF conv264 IS
COMPONENT dff rubyint
PORT
END COMPONENT;
SIGNAL
wire4546,wire4548,wire4550,wire4552,wire4554,wire4556,wire4558,
wire19943,wire20128,wire20273,wire20378,wire20478,wire20596,
wire20746,wire20928,wire21142: rubyint;
BEGIN
- Input assignments: -
output1 != wire1983;
Calculations: -
Registers: -
D3: dff rubyint PORT MAP (wire20128,wire20746,clk);
D4: dff rubyint PORT MAP (wire20273,wire20596,clk);
D5: dff rubyint PORT MAP (wire20378,wire20478,clk);
D7: dff rubyint PORT MAP (wire19730,wire19732,clk);
D319: dff rubyint PORT MAP (wire4546,wire4548,clk);
D320: dff rubyint PORT MAP (wire2540,wire4546,clk);

Figure

10: VHDL translation of the instantiated 2-dimensional convolution circuit.
to the external inputs and outputs mentioned in the formal port clause of the entity,
while names starting with wire identify internal signals. A clock input is generated
if any of the underlying entities are sequential. The assignments marked Calculations
describe the combinational components, and those marked Registers describe the component
instantiations corresponding to the Delay elements. (Instantiations of any other
user-defined components follow in a separate section if required.)
The correctness of the translation relies heavily on two facts:
1. There is a simple mapping between Ruby types and operators and types and
operators which are available in VHDL.
2. Relations are only considered translatable if an (internally consistent) causal
partitioning can be found.
These facts also imply that the VHDL code which is generated can be synthesised
into VLSI. At present, we use the Synopsys VHDL Compiler [14] for performing this
synthesis automatically.
5.3 Other Components of the System
The complete system is illustrated in Figure 11. A similar style of analysis to that
used for generating VHDL code is used for controlling simulation of the behaviour
of the extracted relation. The user must supply a stream of values for the inputs
of the circuit and, if required, initial values for the latches, and the simulation then
uses exactly the same assignments of new values to signals as appear in the VHDL
description. Obviously, only fully instantiated causal relations can be simulated.
SYSTEM
Data flow
Proof
burdens
SILICON
EQUIVALENCES
PROVED
PARSER/PRINTER
RUBY expressions
(internal representation)
RUBY terms
SYSTEM
ANALYSIS
Dynamic behaviour

Figure

11: The complete Ruby Design System.
6 CONCLUSION 19
6 Conclusion
In this paper, we have presented the T-Ruby Design System and outlined a general
design method for VLSI circuits based on transformation of formal specifications using
equality rewriting, constraints and extraction. The simple mathematical basis of the
specification language in terms of functions and relations enables us to prove general
transformation rules, and minimises the step from the mathematical description of the
problem to the initial specification in our system.
The use of the system has been illustrated by the non-trivial example of a circuit for
2-dimensional convolution. This example shows how T-Ruby can be used to describe
complex repetitive structures which are useful in VLSI design, and demonstrates how
the system can be used to derive descriptions of highly generic circuits, from which
concrete circuit descriptions can be obtained by instantiation of free parameters. Circuits
described by so-called causal relations can be implemented and their behaviour
simulated. In the T-Ruby system, a simple mapping from T-Ruby to VHDL for such
relations is used to produce a VHDL description for final synthesis.
The design system basically relies on the existence of a large database of pre-
proved transformation rules. However, during the design process, conjectured rules
can be introduced at any time, and rewrite rules with pre-conditions may be used.
In T-Ruby, proofs of conjectures and pre-conditions can be postponed without any
loss of formality, as the system keeps track of the relevant proof burdens and these
can be transferred later to a separate theorem prover. Our belief is that this "divide
and ocnquer" philosophy helps to make the use of formal methods more feasible for
practical designs.

Acknowledgements

The work described in this paper has been partially supported by the Danish Technical
Research Council.
The authors would like to thank Lars Rossen for many interesting discussions about
constructing tools for Ruby, and Ole Sandum for his work on the design of the Ruby
to VHDL translator.



--R

A framework for defining logics.
Between Functions and Relations in Calculating Programs.
Circuit design in Ruby.
Relations and refinement in circuit design.

A Generic Theorem Prover
A Ruby proof system.
Formal Ruby.

Ruby algebra.
The Ruby framework.
T-Ruby: A tool for handling Ruby expressions.
Transformational rewriting with Ruby.

Constraints, abstraction and verification.
--TR
hardware description languages;relational specification;synchronous circuit design;correctness-preserving transformations