A Mechanised Definition of Silage in HOL ^{∗}

Andrew D. Gordon University of Cambridge Computer Laboratory

February 1993

Abstract If formal methods of hardware verification are to have any impact on the practices of working engineers, connections must be made between the languages used in practice to design circuits, and those used for research into hardware verification. Silage is a simple dataflow language marketed for specifying digital signal processing circuits. Higher Order Logic (HOL) is extensively used for research into hardware verification. This paper presents a formal definition of a substantial subset of Silage, by mapping Silage declarations into HOL predicates. The definition has been mechanised in the HOL theorem prover to support the transformational design of Silage circuits as theorem proving in HOL.

Silage [13, 14, 8] is a simple dataflow language designed for specifying digital signal processing (DSP) algorithms, and is in use at several sites for research into DSP technology. Silage is suitable for high-level synthesis in which a specification expresses the desired behaviour of a circuit, but is free of any architectural commitment. The design process used in practice at IMEC is to develop a Silage program using a software compiler [19], and then to synthesise for a particular architecture—bitserial or microcoded—with one of the CATHEDRAL synthesis systems [5]. Other synthesis tools for Silage include the DSParchitect silicon compiler developed by EDC for Mentor Graphics^{1} [7], the Philips PIRAMID and Phideo compilers [16], and the Berkeley Hyper system.

This paper presents a formal definition of a substantial subset of the language, called Mini-Silage. The meaning of the language is given in terms of Higher Order Logic or HOL, a formal notation for mathematics that has been mechanised in several theorem provers, including the Cambridge HOL system [11].

There is an immediate practical motivation for this work. Silicon compilers can cope mechanically with all the details of mapping a Silage program’s highlevel behavioural description down to some particular implementation, but they cannot currently find an implementation that is best in terms of clock-rate or area. The typical design methodology used with Silage at present is for the engineer to start with an initial Silage program that describes the desired behaviour, and to transform it by hand into a tuned program, intended to have the same behaviour, but a better performance against a particular silicon compiler. There are several reports of experience with this transformational design style using Silage [17, 22, 21]. At present the only way to check that the initial and tuned programs have the same behaviour is to use simulation. Designers ought to be able to get their work done faster if transformations could be done interactively, with a machine-checked guarantee that the meanings of the initial and tuned programs are equal. In principle simulation results from the two programs should be the same, so design time is saved because only one simulation is necessary. We make this claim only tentatively, pending practical experience, because it depends on factors beyond the scope of the project, such as compiler correctness.

∗Work funded as part of the CHEOPS ESPRIT Basic Research Action 3215. Author’s current address: Programming Methodology Group, Department of Computer Science, Chalmers Technical University, Göteborg S–412 96, Sweden. Email: gordon@cs.chalmers.se.

1Silage is renamed DFL by EDC, presumably for marketing reasons.

A formal definition is essential if Silage programs are to be represented within the HOL system, but no formal definition of the full Silage language exists,^{2} though there are compiler manuals [19, 7] and an informal reference manual [14]. Two other papers in the CHEOPS project discuss specific semantic issues in Silage. Kalker [15] discusses how to model datatypes and proposes the design of an improved language called Silage+. Angelo [1] discusses how features such as multi-rate and irregular rate signals might be modelled using HOL. In contrast, the present paper, summarised elsewhere [9], presents a formal definition of a synchronous single-rate subset of IMEC Silage. The framework of this paper could be smoothly extended to deal with multi-rate signals or the details of Silage datatypes.

There are further potential benefits of this work. If formal methods of hardware verification are to have any impact on the practices of working engineers, connections must be made between the languages used in practice to design circuits, and those used for research into hardware verification. By bringing together the Silage language and the HOL logic, we make possible, for instance, use of the HOL system to prove properties of an individual specification, to increase confidence that it expresses the intended circuit behaviour. This description of Mini-Silage should be of interest to the Silage community because it can form the basis of a precise and complete reference standard, independent of any compiler or the interpretation of an informal description.

Section 1 is an informal introduction to Silage. Section 2 is the formal definition itself. Program transformation is illustrated by an example in Section 3. Section 4 discusses the differences between Mini-Silage and Silage. Section 5 discusses how the definition has been mechanised in HOL. Section 6 summarises the contribution.

2Personal communication with Paul Hilfinger, January 1992.

1 Elements of Silage

As a toy example, here is the Fibonacci series:

Fib@@1 = 1; Fib@@2 = 1;

     Fib = Fib@1 + Fib@2

Expressions in general stand for signals, which are infinite streams of samples, indexed by time. Time is modelled by the integers—negative times are used for initialisation of delays. The first two lines say that the signal Fib is to have the sample 1 at times −1 and −2 respectively. The third line says that for all non-negative times, the stream Fib is to equal the sum of itself delayed by 1 and 2 samples, Fib@1 and Fib@2 respectively. In other words, for all i ≥ 0, the ith sample equals the sum of the (i − 1)th and (i − 2)th samples.

As is common with specification languages, one can think of a Silage program in two ways. One way is behavioural, in the sense that a Silage program can be read simply as a set of equations between signals that specify what is to be computed, but not how. The other way is structural, in the sense that a Silage program can be read as an executable specification suggesting the structure of an implementation, given a particular target architecture. In fact, only a subset of the well-formed specifications is executable: for instance, neither of the following is executable:

A = 1; A = 2 and A = B; B = A.

The left-hand definition violates a single-assignment condition: that no variable be assigned more than once. The right-hand definition violates an acyclicity condition: that no sample be defined in terms of itself. Although they are not executable, these definitions make sense as specifications, albeit useless ones: respectively unsatisfiable and ambiguous. Unlike the case in other specification languages, Silage programs such as these which are type-correct but not executable do not appear to be very useful. The semantics given here for Silage only reflects the behavioural interpretation of Silage programs. We have not formalised a structural interpretation nor notions of single-assignment or acyclicity.

The samples of a signal can be vectors as well as scalars. Here is a user-defined function to compute the scalar product C of two vectors A and B [17]:

     funcSP64(A:Nat[], B:Nat[])C:Nat =

S:Nat[], T:Nat[]

     begin

S[0] = 0; (i : 1..64) ::

       begin

S[i] = S[i − 1] + T [i − 1]; T [i − 1] = A[i − 1] × B[i − 1]

       end;

C = S[64]

     end

The function header declares that the function is called SP64, has vector inputs A and B, output C, and uses local signals S and T. The compiler is expected to infer the size of vectors in Silage, which need not be declared. Each sample in the scalar signal C is the scalar product of the corresponding vector samples of the signals of vectors A and B. The compound definition beginning (i : 1..64) :: … is an iterator whose meaning is equivalent to the macro-expansion of its body, with i ranging from 1 up to 64. Here is how a user-defined function can be called:

C = SP64(D, D) + SP64(E, E)

Silage has conditionals and tuples:

(max[i + 1], pos[i + 1]) = ifIn[i] > max[i]\begin{matrix}→ (In[i], i) \\ ||(max[i], pos[i]) \end{matrix} fi

The usage of tuples is rather restricted, for implementation reasons. Tuples cannot be nested and no variable can stand for a tuple. The main use of tuples is to return multiple results from user-defined functions.

There are two special forms of expression. Manifest expressions are combinations of numeric constants, arithmetic operators and iterator variables. Selectors are tuples of indexed signal variables, such as (max[i + 1], pos[i + 1]). Any wellformed expression can be interpreted as a signal; any manifest expression can also be interpreted as a scalar. Expressions used as iterator bounds or as vector indices are required to be manifest. Expressions on the left-hand side of equations are required to be selectors. These restrictions contribute to making Silage specifications executable.

Here is a digital filter from Hilfinger’s reference manual [14], as a final example:

     funch transform(in:Nat, coefs:Nat[])return:Nat =
       filter:Nat[], S:Nat[]
     begin
       filter[15] = in;

(i : 0..14) :: filter[i] = filter[i + 1]@2;

S[16] = 0;

(i : 0..15) :: S[i] = S[i + 1] + (filter[i] × coefs[i]);

       return = S[0]
     end

The function takes an input signal, in, and a vector of coefficients, coefs, and computes a filtered version of the input signal as the output signal, called return.

2 The definition of a Silage subset

What follows is meant as a precise definition of a subset of IMEC Silage, called Mini-Silage. The definition is intended to be precise and ambiguous; the reader new to Silage should look elsewhere for tutorial material [14, 19]

The definition of Mini-Silage consists of three parts:

• Production rules for the abstract syntax describe the underlying structure of the language without surface details of operator precedence, punctuation, and so forth. There are syntactic categories of types, expressions, definitions, parameters and functions. Concrete syntax is not redefined because the existing texts do so already.

• Static semantics rules determine when a phrase of abstract syntax is wellformed and well-typed. We use the method of Structural Operational Semantics (SOS) [20, 18], in which the rules are driven algorithmically by the structure of the abstract syntax. The rules determine the type and attributes of an expression—such as whether it is a selector or a manifest expression.

• Denotational semantics rules^{3} translate those definitions and expressions that satisfy the static semantics into predicates and terms of the HOL logic. We follow the method of specifying circuits as HOL predicates [10], in which a Silage function is specified by a predicate relating its input and output signals that must be satisfied by any implementation.

We do not address the issue of whether a Silage program is executable. This issue is irrelevant to program transformation, since for that purpose programs are viewed simply as logical specifications. But if the user is to know what is a valid input to the compiler and if programs are to be portable, there would need to be a precise account of which programs are executable.

We first establish notations for logic and set theory. The sections that follow are a commentary on the definition of each part of the language: types, expressions, definitions and functions. The definition itself consists of formal descriptions in a series of figures; the commentary is intended to be explanatory and to state consequences of the definition, but not to be part of it. We summarise the components of the definition at the end of the paper in Figure 9 on page 22.

The HOL logic

The object language used to express the definition of Silage is Higher Order Logic, as used in the Cambridge HOL system and in other theorem provers. We sketch here enough of the syntax and meaning of the logic to understand this paper; a full description is available in the HOL book [12].

Here is a description of the HOL types, τ, used here:

τ ::= bool | num | int | (τ_{1} → τ_{2}) | (τ_{1} × τ_{2}) | (τ) list | α

HOL types can be thought of as sets. The basic types bool, num and int consist of the sets of Booleans, natural numbers and integers, respectively. The function type, τ_{1} → τ_{2} consists of total functions from τ_{1} to τ_{2}. The product type, τ_{1} × τ_{2}, consists of pairs of elements of τ_{1} and τ_{2}. The list type, (τ) list, consists of finite lists of elements of τ. Finally, types containing type variables, α, called polymorphic types, describe families of structurally related types. A monomorphic type is one containing no type variables.

3These rules are denotational in the sense that they assign meanings, denotations, to phrases of an object language (Silage) in terms of a metalanguage (HOL). This is not the classical denotational semantics of Scott and Strachey based on domain theory.

Logical sentences are represented by terms of a simply-typed λ-calculus. A preterm of the logic, M, is either a constant, c^{τ}, a variable x^{τ}, a combination (M M′), or an abstraction (λx^{τ}. M). Let HolConst be the set of HOL constants. Variable and constant type superscripts are often omitted for the sake of clarity. A term of the logic is a preterm that has a type according to the usual λ-calculus rules: a constant c^{τ} has type τ; a variable x^{τ} has type τ; a combination (M M′) has type τ if M has type τ′ → τ and M′ has type τ′; and an abstraction (λx^{τ}. M) has type τ → τ′ if M has type τ′. If a term M has type τ we write M:τ.

There are constants to construct terms of each type. The Boolean constants, T and F are terms of type bool. The numerals, written 0, 1, 2, …, as usual, are terms of type num. The integers, written here with explicit signs, …, −2, −1, +0, +1, +2,… are of type int. The usual logical and arithmetic constants, including =, ¬, ∧, ∨, ⟹, ∀, ∃, +, −, ×, DIV, >, <, ≥, and ≤, are available and have their usual interpretation. The conditional (M_{C} → M_{T} |M_{F}) means the same as M_{T} if M_{C} is true; otherwise M_{F}.

If each term M_{i} has type τ_{i}, then (M_{1}, M_{2}) is a pair with type τ_{1} × τ_{2}, and we write (M_{1}, …, M_{n}) for a tuple with type τ_{1} × (τ_{2} × (⋯ × τ_{n}) ⋯), where n > 0. If each term M_{i} has the same type τ, then the term [M_{1}, …, M_{n}] is a finite list of n ≥ 0 elements, of type (τ) list. We use list operations MAP and EL that satisfy the equations:

\begin{aligned}MAP f [x_{1}, …, x_{n}] & = & [f x_{1}, …, f x_{n}] \\ EL i [x_{1}, …, x_{n}] & = & x_{i} & if 1 ≤ i ≤ n \end{aligned}

New constants can be defined as abbreviations for existing terms. For instance, if x:α and t: int, then the equation:

VAL x t =^{def} x

introduces the constant VAL to be of the curried type α → (int → α), and such that any function application VAL M N is equal to the term M.

A HOL theorem is a predicate that can be proved correct using the axioms and inference rules of the logic. The Cambridge HOL system is a mechanisation of the syntax, axioms and inference rules of the logic.

Mathematical notation

We adopt a conventional set-theoretic notation as a metalanguage with which to express how a Silage program is translated into the HOL object language.

If S is a set, then write S^{∗} for the set of finite lists of the form [s_{1}, …, s_{n}], where each s_{i} ∈ S, and S^{+} for the set of non-empty elements of S^{∗}. Let the decorated variable s̃ range over elements of S^{∗}. Write s . t̃ for the outcome of consing an element s onto the front of a list t̃. We often apply set-theoretic predicates like ∈ or ∩ to lists, intending the list to be interpreted as the set of its members.

If S_{1}, …, S_{n} are sets, then write S_{1} × ⋯ × S_{n} for the set of tuples of the form (s_{1}, …, s_{n}), where each s_{i} ∈ S_{i}.

If S and T are sets, then write S →^{fin} T for the set of finite functions from S to T of the form {s_{1}:t_{1}, …, s_{n}:t_{n}}, which means the function that maps each element s_{i} ∈ S to t_{i} ∈ T. If f ∈ (S →^{fin} T), write Dom(f) for the domain of f, a subset of S. If both f and g are functions in S →^{fin} T, write f + g for the function with domain Dom(f) ∪ Dom(g), such that,

(f + g)(s) = \{ \begin{matrix}g(s) & if s ∈ Dom(g) \\ f(s) & otherwise \end{matrix}

Beware that both the HOL object language and the set theoretic metalanguage use the same notation for tuples and lists, but the context should make clear which language is meant.

2.1 Types

Silage supports a hierarchy of types, used to classify variables, expressions and functions. The abstract syntax of types is shown in Figure 1. For ease of reference, we label every item apart from productions of the abstract syntax. Items that exist as theorems in the HOL system are labelled with their name; other items are numbered.

There are two atomic types, Nat and Bool, and two kinds of compound type, Vec(σ) and Prod(σ_{1}, σ_{2}). The concrete syntax for Vec(σ) is σ[]. There is no concrete syntax for product types. As a general policy, a meta-variable σ stands for Silage types, and a meta-variable τ stands for HOL types.

Silage signal variables are allowed to stand only for signals whose types do not include the product constructor. This is formalised by the rules in item 1, which define a predicate, ⊢ σ sigType, by induction on the structure of the type. We say that σ is a signal type just when ⊢ σ sigType holds.

The denotational semantics rules, (2)–(5), assign a HOL type to each Silage type. We assume vectors are indexed from 0 up to some finite upper bound, and model vector types as HOL lists.

The metalanguage function Tuple, in rule (6) constructs an n-tuple given a list of element types.

Since Silage signals are infinite arrays of samples indexed by time, we model a signal whose samples are of HOL type τ, by the type int → τ. Such types are constructed using the metalanguage function Signal defined in rule 7 of Figure 1. Time has to be the integers rather than just the naturals because Silage initialisations specify the samples of a signal at negative times. Any Silage expression of type σ can be modelled by a HOL term of type Signal[[σ]].

Silage functions map a possibly-empty list of argument signals to a non-empty list of result signals. A function type, (σ̃, σ̃′) ∈ FunType, is a finite list of argument types σ̃ paired with a non-empty list of result types σ̃′.

2 THE DEFINITION OF A SILAGE SUBSET 8

Abstract Syntax

σ ∈ Type  (types)
σ ::= Nat  (natural numbers)
| Bool  (Booleans)
| Vec(σ)  (vectors)
| Prod(σ_{1}, σ_{2}) (pairs)

Static Semantics

⊢ Nat sigType ⊢ Bool sigType ⊢ σ sigType ⊢ Vec(σ) sigType (1)

Denotational Semantics

[[Nat]] =^{def} num  (2)
[[Bool]] =^{def} bool  (3)
[[Vec(σ)]] =^{def} [[σ]] list  (4)
[[Prod(σ_{1}, σ_{2})]] =^{def} [[σ_{1}]] × [[σ_{2}]] (5)

Semantic Operations

Tuple[σ_{1}, …, σ_{n}] =^{def} Prod(σ_{1}, …, Prod(σ_{n−1}, σ_{n}) …) (n > 0) (6)
Signal(τ) =^{def} int → τ  (7)

Semantic Object

FT ∈ FunType = Type^{∗} × Type^{+} (function types)

Figure 1: Types

Abstract Syntax

x, y, … ∈ Var  (variables)
op ∈ Operator =  {!, &, |, <, >, <=, >=, ==,!=, +, -, *, div}
e ::= x  (variable)
| x(e_{1}, …, e_{n})  (function application)
| e_{1}[e_{2}]  (indexing)
| e_{1}@e_{2}  (delay)
| (e_{1}, …, e_{n})  (tuple)
| {e_{1}, …, e_{n}}  (vector literal)
| \underline{n}  (numeric literal)
| \underline{b}  (Boolean literal)
| (op e)  (prefix combination)
| (e_{1} op e_{2})  (infix combination)
| (ife_{1} → e_{2} || e_{3} fi) (conditional)

Figure 2: Abstract syntax of expressions

2.2 Expressions

Abstract syntax of expressions

The abstract syntax of expressions appears in Figure 2. We assume given an infinite set of variables, Var, and define a finite set of operators, Operator. From these sets we construct the syntax of expressions, e ∈ Exp.

Static semantics of expressions

The job of the static semantics is to determine whether an expression is well-typed and whether it has the form of a selector or a manifest expression, and to resolve overloaded operators.

Variables in Silage stand for three kinds of thing: signals, iterator indices, and functions. An environment, E, is a finite function from variables to entries, where the set of entries is defined as follows:

Entry = {Sig(σ), Ind, Fun(FT) | σ ∈ Type, FT ∈ FunType}

A signal variable of type σ is mapped to the entry Sig(σ); an iterator index is mapped to the entry Ind; and a function variable of function type FT is mapped to the entry Fun(FT). All iterator indices are of type Nat so there is no need to record their types explicitly. An environment would typically be implemented as a compiler symbol table.

Silage operators can be overloaded on different types; for instance, the equality operation == acts on expressions of type Bool and also Nat. Each possible overloading of a Silage operator is defined in terms of a typing, which is a pair of 2 THE DEFINITION OF A SILAGE SUBSET 10

Semantic Objects

Entry = \begin{cases}Sig(σ), Ind, Fun(FT) \\ | σ ∈ Type, FT ∈ FunType\} \end{cases}  (entries)
E ∈ Env = Var →^{fin} Entry  (environments)
a ∈ Attrib = {Sel, Man, Hol(c_{1}, c_{2}) | c_{i} ∈ HolConst} (attributes)

Logical Constants

x NOTEQ y =^{def} ¬ (x = y) (NOTEQ)
(SIGNOT A) t =^{def} ¬ (A t)  (SIGNOT)
(A ⊕ B) t =^{def} (A t) ⊕ (B t) (8)

Semantic Operations

Arith =^{def} ([Nat; Nat], Nat)
BoolOp =^{def} ([Bool; Bool], Bool)
NumRel =^{def} ([Nat; Nat], Bool)
sigOp(!) =^{def} [(([Bool], Bool), ( ¬ , SIGNOT))]
sigOp(|) =^{def} [(BoolOp, ( ∨ , ∨ ))]
sigOp(&) =^{def} [(BoolOp, ( ∧ , ∧ ))]
sigOp(>) =^{def} [(NumRel, (>, > ))]
sigOp(<) =^{def} [(NumRel, (<, < ))]
sigOp(<=) =^{def} [(NumRel, (≤, ≤ ))]
sigOp(>=) =^{def} [(NumRel, (≥, ≥ ))]
sigOp(==) =^{def} [\begin{matrix}(BoolOp, (=, = )), \\ (NumRel, (=, = ))] \end{matrix}
sigOp(!=) =^{def} [\begin{matrix}(BoolOp, (NOTEQ, NOTEQ )), \\ (NumRel, (NOTEQ, NOTEQ ))] \end{matrix}
sigOp(+) =^{def} [(Arith, (+, + ))]
sigOp(-) =^{def} [(Arith, (−, − ))]
sigOp(*) =^{def} [(Arith, (×, × ))]
sigOp(div) =^{def} [(Arith, (DIV, DIV ))]

Figure 3: Semantic objects and operations 2 THE DEFINITION OF A SILAGE SUBSET 11

Static Semantics

All(a, [ã_{1}, …, ã_{n}]) =^{def} if a ∈ ã_{i} for each i then [a] else []  (9)

E(x) = Ind E ⊢ x ⇒ Nat, [Man]

(10)

{E(x) = Sig(σ) \atop E ⊢ x ⇒ σ, [Sel]}  (11)

E(x) = Fun([σ_{1}, …, σ_{n}], σ̃′) E ⊢ e_{i} ⇒ σ_{i} (1 ≤ i ≤ n) E ⊢ x(e_{1}, …, e_{n}) ⇒ Tuple(σ̃′), []

(12)

E ⊢ e_{1} ⇒ Vec(σ), ã_{1} (Sel ∈ ã_{1}) E ⊢ e_{2} ⇒ Nat, ã_{2} E ⊢ e_{1}[e_{2}] ⇒ σ, if Man ∈ ã_{2} then[Sel] else[]

(13)

E ⊢ e_{1} ⇒ σ, ã_{1} (Sel ∈ ã_{1}) E ⊢ e_{2} ⇒ Nat, ã_{2} (Man ∈ ã_{2}) E ⊢ e_{1}@e_{2} ⇒ σ, []

(14)

E ⊢ e_{i} ⇒ σ_{i}, ã_{i} ⊢ σ_{i} sigType (1 ≤ i ≤ n, n > 1) E ⊢ (e_{1}, …, e_{n}) ⇒ Tuple[σ_{1}, …, σ_{n}], All(Sel, [ã_{1}, …, ã_{n}])

(15)

E ⊢ e_{i} ⇒ σ, ã_{i} (1 ≤ i ≤ n, n > 0) ⊢ σ sigType E ⊢ {e_{1}, …, e_{n}} ⇒ Vec(σ), []

(16)

E ⊢ \underline{n} ⇒ Nat, [Man]  (17)
E ⊢ \underline{b} ⇒ Bool, [Man]  (18)

E ⊢ e ⇒ σ_{1}, ã_{1} (([σ_{1}], σ_{2}), p) ∈ sigOp(op) E ⊢ (op e) ⇒ σ_{2}, (Hol(p) . All(Man, [ã_{1}]))

(19)

E ⊢ e_{1} ⇒ σ_{1}, ã_{1} E ⊢ e_{2} ⇒ σ_{2}, ã_{2} (([σ_{1}, σ_{2}], σ_{3}), p) ∈ sigOp(op) E ⊢ (e_{1} op e_{2}) ⇒ σ_{3}, (Hol(p) . All(Man, [ã_{1}, ã_{2}]))

(20)

E ⊢ e_{1} ⇒ Bool, ã_{1} E ⊢ e_{2} ⇒ σ, ã_{2} E ⊢ e_{3} ⇒ σ, ã_{3}

E ⊢ (ife_{1} → e_{2} || e_{3} fi) ⇒ σ, [] (21)

Figure 4: Static semantics of expressions pairs, ((σ̃, σ′), (c_{man}, c_{sig})), where σ̃ is a list of the argument types, σ′ is the result type, and c_{man} and c_{sig} are HOL constants that model the behaviour of the operator on scalars and signals respectively. The behaviour on scalars of all the Silage operators, except for !=, can be modelled by constants present in the basic HOL system; the exception is modelled by the constant NOTEQ, defined in rule (NOTEQ) of Figure 3. The behaviour on signals of the one unary operation, !, is modelled by constant SIGNOT in rule (SIGNOT). If HOL constant ⊕ models the behaviour on scalars of a binary operator, then constant ⊕ (defined schematically in rule (8)) models the operator’s behaviour on signals. The function sigOp in Figure 3 assigns to each Silage operator a list of typings; one typing for each overloading of the operator. Although there are only two overloaded operators in Mini-Silage, there are many more in the full language, so it is worth setting up a general mechanism for overloading.

The static semantics assigns a list of attributes to each well-formed expression, drawn from the set Attrib:

Attrib = {Sel, Man, Hol(c_{man}, c_{sig}) | c_{i} ∈ HolConst}

Attributes Sel and Man indicate a manifest expression or selector respectively. An attribute Hol(c_{man}, c_{sig}) is assigned to each expression (op e) or (e_{1} op e_{2}) to indicate the HOL operator, c_{man} or c_{sig}, that models Silage operator op acting on scalars or signals, respectively.

The static semantics, which corresponds to the type-checker in an implementation, is specified formally using judgments. A judgment is a predicate between environments, phrases of the abstract syntax and semantic objects, inductively defined by a set of inference rules. As a general convention, judgments are written in the form E ⊢ ϕ ⇒ ψ, where E is an environment, and ϕ and ψ are phrases of abstract syntax or semantic objects; ϕ is the phrase or object being analysed, and ψ is the outcome of the analysis.

The static semantics inference rules, (10)–(21) in Figure 4 define a judgment, written E ⊢ e ⇒ σ, ã, and intended to mean, “in environment E expression e elaborates to type σ and has attributes ã.” There are no special rules to indicate when an expression is not well-typed; in that case it is impossible to derive a type for the expression.

Often whether an expression possesses an attribute Man or Sel depends on whether all its subexpressions do. This dependency is expressed using the operation All defined in rule (9),

All(a, [ã_{1}, …, ã_{n}]) =^{def} if a ∈ ã_{i} for each i then [a] else []

It is worth commenting on some of the rules:

(10), (11), (12) These three rules correspond to the three ways in which a variable can occur in an expression: as an iterator index, as a signal variable and as a function variable respectively.

(13) An expression e_{1}[e_{2}] is only well-formed if the vector expression e_{1} is a selector and if the index expression e_{2} is numeric. The whole expression is a selector only if the index expression is manifest. These restrictions come from the Silage Reference Manual [14] and are for implementation reasons.

(14) A delay expression e_{1}@e_{2} is only well-formed if the signal expression e_{1} is a selector and if the delay e_{2} is a manifest expression.

(15) A tuple expression is a selector if and only if all its component expressions are. A tuple type is only well-formed if all its components are signal types; this restriction is unnecessary for the logical interpretation of tuples, but is made to simplify implementation.

(16) All the expressions in a vector must have the same type, which must be a signal type for implementation reasons.

(19), (20) The types of operator combinations are determined from the function sigOp that resolves overloading.

One of the benefits of a formal semantics is that one can verify desired properties by mathematical proof. We can prove that in a particular environment types and attributes are assigned uniquely to each expression:^{4}

Proposition 1 For any environment E expression e, types σ, σ′ and attribute lists ã, ã′, if E ⊢ e ⇒ σ, ã and E ⊢ e ⇒ σ′, ã′ then σ = σ′ and ã = ã′.

Given the functional nature of the static semantics, it makes sense to define two partial functions, Type and Attrib, to denote the type and attribute lists of a particular pair (E, e), as shown in Figure 5.

Denotational semantics of expressions

We define a collection of HOL constants to construct and manipulate HOL terms of signal type. These are shown in Figure 5, and a commentary follows:

(IND), (SIGIND) The operators !! and SIGIND both take a signal of vectors and an index, and return a signal of vector elements. The difference between them is that the index for !! is a constant, whereas the index for SIGIND is a signal, that is, can vary with time.

(22) If M_{1},…,M_{n} are signals, with each M_{i} of type Signal(τ_{i}), then the notation ⟨M_{1}, …, M_{n}⟩ stands for the signal of type Signal(τ_{1} × ⋯ × τ_{n}) obtained by iteratively zipping together all of the signals. In the base case, when n = 1, ⟨M_{1}⟩ means just M_{1} itself.

4This proposition together with the others in the report have been proved in manuscript, but the proofs are omitted for the sake of brevity. None of the proofs is of any intrinsic interest; they are mostly inductions on the structure of a syntactic term, or on the depth of inference of a judgment.

2 THE DEFINITION OF A SILAGE SUBSET 14

Static Semantics as Functions

Type(E, e) =^{def} σ where there is ã such that E ⊢ e ⇒ σ, ã
Attrib(E, e) =^{def} ã where there is σ such that E ⊢ e ⇒ σ, ã

Logical Definitions

VAL : α → Signal(α)
<> : Signal(α) → num → Signal(α)
!! : Signal(α) → num → Signal(α)
SIGIND : Signal(α) → Signal(num) → Signal(α)
VEC : Signal(α list) → (Signal(α)) list
SIGPAIR : Signal(α) → Signal(β) → Signal(α × β)
SIGCOND : Signal(bool) → Signal(β) → Signal(β) → Signal(β)
VAL x t =^{def} x  (VAL)
(A<>n)t =^{def} A(t − n)  (DELAY)
(A !! n) t =^{def} EL n (A t)  (IND)
(A SIGIND B) t =^{def} (A !! (B t)) t  (SIGIND)
VEC ℓ t =^{def} MAP(λx. x t)ℓ  (VEC)
SIGPAIR A B t =^{def} (A t, B t)  (SIGPAIR)
SIGCOND A B C t =^{def} (A t) → (B t) | (C t)  (SIGCOND)

⟨M_{1}, …, M_{n}⟩ (n > 0) =^{def} (SIGPAIR M_{1}

…
(SIGPAIR M_{n−1} M_{n}) …)

(22)

Figure 5: Functions and definitions used in expression semantics 2 THE DEFINITION OF A SILAGE SUBSET 15

Denotational Semantics

[[x]]_{E}^{M} =^{def} x^{[[Type(E,x)]]}  (23)
[[\underline{n}]]_{E}^{M} =^{def} n  (24)
[[\underline{b}]]_{E}^{M} =^{def} b  (25)

[[op e]]_{E}^{M} =^{def} c_{man}[[e]]_{E}^{M}

where Hol(c_{man}, c_{sig}) ∈ Attrib(E, op e)

(26)

[[e_{1} op e_{2}]]_{E}^{M} =^{def}

c_{man}[[e_{1}]]_{E}^{M}[[e_{2}]]_{E}^{M} where Hol(c_{man}, c_{sig}) ∈ Attrib(E, e_{1} op e_{2})

(27)

[[x]]_{E} =^{def} \{ \begin{matrix}VAL(x^{[[Nat]]}) & if Man ∈ Attrib(E, x) \\ x^{Signal[[Type(E,x)]]} & otherwise \end{matrix} (28)
[[x(e_{1}, …, e_{n})]]_{E} =^{def} \{ \begin{matrix}x FUN & if n = 0 \\ x FUN([[e_{1}]]_{E}, …, [[e_{n}]]_{E}) & otherwise \end{matrix}  (29)
[[e_{1}[e_{2}]]]_{E} =^{def} \begin{cases}[[e_{1}]]_{E} !! [[e_{2}]]_{E}^{M} if Man ∈ Attrib(E, e_{2}) \\ [[e_{1}]]_{E} SIGIND[[e_{2}]]_{E} otherwise \end{cases}  (30)
[[e_{1}@e_{2}]]_{E} =^{def} [[e_{1}]]_{E}<>[[e_{2}]]_{E}^{M}  (31)
[[(e_{1}, …, e_{n})]]_{E} =^{def} ⟨[[e_{1}]]_{E}, …, [[e_{n}]]_{E}⟩  (32)
[[{e_{1}, …, e_{n}}]]_{E} =^{def} VEC[[[e_{1}]]_{E}, …, [[e_{n}]]_{E}]  (33)
[[\underline{n}]]_{E} =^{def} VAL(n)  (34)
[[\underline{b}]]_{E} =^{def} VAL(b)  (35)

[[op e]]_{E} =^{def} c_{sig}[[e]]_{E}

where Hol(c_{man}, c_{sig}) ∈ Attrib(E, op e)

(36)

[[e_{1} op e_{2}]]_{E} =^{def}

c_{sig}[[e_{1}]]_{E}[[e_{2}]]_{E} where Hol(c_{man}, c_{sig}) ∈ Attrib(E, e_{1} op e_{2})

(37)

[[ife_{1} → e_{2} || e_{3} fi]]_{E} =^{def} SIGCOND[[e_{1}]]_{E}[[e_{2}]]_{E}[[e_{3}]]_{E}  (38)

Figure 6: Denotational semantics of expressions

The two interpretations of an expression—as a scalar and as a signal—are formalised as two different meaning functions: written [[e]]_{E}^{M} and [[e]]_{E} respectively. The “M” symbol is used to distinguish the two functions, both of which take an environment argument, E. Figure 6 defines the denotational semantics of expressions: equations (23)–(27) define [[e]]_{E}^{M}, while equations (28)–(38) define [[e]]_{E}.

The following proposition expresses desired connections between the static semantics of expressions, and the two meaning functions:

Proposition 2

(1) If E ⊢ e ⇒ σ, ã and Man ∈ ã then [[e]]_{E}^{M} is a HOL term of monomorphic type [[σ]].

(2) If E ⊢ e ⇒ σ, ã then [[e]]_{E} is a HOL term of monomorphic type Signal[[σ]].

(3) If E ⊢ e ⇒ σ, ã and Man ∈ ã then VAL[[e]]_{E}^{M} = [[e]]_{E}.

These proofs depend on each of the HOL variables generated by either of the meaning functions being tagged with a monomorphic type (rules (23) and (28)). The mechanisation of the denotational semantics constructs an untyped HOL preterm corresponding to each Silage expression, and turns it into a typed HOL term at the end, by asking HOL to type-check it. This is simpler to program than directly constructing a HOL term. The HOL system’s type-checker accepts a preterm if every subterm of the preterm is monomorphically typed; a feature of the type-checker is that it rejects certain preterms containing subterms of polymorphic type, even though they are well-typed. The significance of parts (1) and (2) of the proposition is if a Silage program is well-typed according to the static semantics, then typechecking its translation into the HOL logic will not go wrong.

In rule (29), x FUN is a HOL constant defined to represent the behaviour of the Silage function x, as explained in Section 2.4.

2.3 Definitions

Figure 7 shows the abstract syntax of definitions in Silage. The job of the static semantics of definitions is to check that all the expressions contained in a definition are well-typed, and of a suitable form. No value is computed by the static semantics rules, so the judgment takes the form E ⊢ d ok, intended to mean “in environment E definition d is well-formed.” The judgment is defined by rules of inference (39)–(43) in Figure 7.

Here is a commentary on the static semantics of definitions:

(39) An initialisation e_{1}@@e_{2} = e_{3} is well-formed just when e_{1} and e_{2} have the same type, e_{2} and e_{3} are manifest expressions, and e_{1} is a selector.

(40) An equation e_{1} = e_{2} is well-formed just when e_{1} and e_{2} have the same type, and e_{1} is a selector.

2 THE DEFINITION OF A SILAGE SUBSET 17

Abstract Syntax

d ::= (e_{1}@@e_{2} = e_{3}) (initialisation)
| (e_{1} = e_{2})  (equation)
| d_{1}; d_{2}  (composition)
| (x : e_{1}..e_{2}) :: d (iteration)
| begindend (parenthesis)

Static Semantics

E ⊢ e_{1} ⇒ σ, ã_{1} E ⊢ e_{2} ⇒ Nat, ã_{2} E ⊢ e_{3} ⇒ σ, ã_{3}

(Sel ∈ ã_{1}, Man ∈ ã_{2}, Man ∈ ã_{3}) E ⊢ (e_{1}@@e_{2} = e_{3}) ok

(39)

E ⊢ e_{1} ⇒ σ, ã_{1} (Sel ∈ ã_{1}) E ⊢ e_{2} ⇒ σ, ã_{1} E ⊢ (e_{1} = e_{2}) ok

(40)

E ⊢ d_{1} ok E ⊢ d_{2} ok

E ⊢ (d_{1}; d_{2}) ok (41)

E ⊢ e_{1} ⇒ Nat, ã_{1} E ⊢ e_{2} ⇒ Nat, ã_{2} E + {x: Ind} ⊢ d ok

(Man ∈ ã_{1}, Man ∈ ã_{2}, x ∉ Dom(E)) E ⊢ (x : e_{1}..e_{2}) :: d ok

(42)

E ⊢ d ok

  E ⊢begindend ok

(43)

Logical definitions

A ∼ B =^{def} ∀n: num . A(+n) = B(+n) (SIGDEF)
(m TO n)p =^{def} (m ≤ p) ∧ (p ≤ n)  (TO)
∀x :: P. Q =^{def} ∀x. (P x) ⟹ Q  (RES FORALL)

Denotational Semantics

[[e_{1}@@e_{2} = e_{3}]]_{E} =^{def} [[e_{1}]]_{E}(− [[e_{2}]]_{E}^{M}) = [[e_{3}]]_{E}^{M}  (44)
[[e_{1} = e_{2}]]_{E} =^{def} [[e_{1}]]_{E} ∼ [[e_{2}]]_{E}  (45)
[[(d_{1}; d_{2})]]_{E} =^{def} [[d_{1}]]_{E} ∧ [[d_{2}]]_{E}  (46)
[[(x : e_{1}..e_{2}) :: d]]_{E} =^{def} ∀x^{[[Nat]]} :: [[e_{1}]]_{E}^{M} TO[[e_{2}]]_{E}^{M}. [[d]]_{E+{x: Ind}} (47)
[[begindend]]_{E} =^{def} [[d]]_{E}  (48)

Figure 7: Definitions (42) An iteration (x : e_{1}..e_{2}) :: d introduces a new iterator index x, which must not

already occur in the environment. For the iteration to be well-formed, e_{1} and e_{2} must be manifest numeric expressions, and d must be well-formed, when x is treated as an iterator index.

We desire to interpret a well-formed definition d as a HOL predicate [[d]]. We do not suggest how the implementation should go about computing the signals specified in a Silage program, but state a predicate that places constraints on the signal variables being defined.

One might think that a Silage equation e_{1} = e_{2} could be interpreted simply as HOL equality between [[e_{1}]] and [[e_{2}]]. But such an approach would interpret the Silage definition

A@@1 = 1; A = 0,

as the HOL predicate

A(−1) = 1 ∧ A = VAL(0)

which is unsatisfiable, since then A(−1) = VAL(0)(−1) = 0 but A(−1) = 1. Contradiction! In fact a Silage equation only holds for non-negative times, so we define the new equivalence relation ∼, called SIGDEF in Figure 7, such that A ∼ B just when the two signals A and B have the same samples for all non-negative times. The HOL predicate

A(−1) = 1 ∧ A ∼ VAL(0)

is perfectly satisfiable, and correctly reflects the intuitive interpretation of initialisations and equations.

Given SIGDEF here is the interpretation of the Fib definition as a HOL predicate:^{5}

Fib(−1) = 1 ∧ Fib(−2) = 1 ∧

     Fib ∼ (Fib<>1) SIGPLUS (Fib<>2)

We use two other logical abbreviations. The notation ∀x :: P. Q, a restricted quantification, means “for all x satisfying the predicate P, Q holds.” This notation, together with the predicate m TO n—that holds for the numeric range m up to n inclusive—is used to interpret iterated definitions.

Rules (44)–(48) in Figure 7 define [[d]]_{E}, the interpretation of a definition d as a HOL predicate, provided d is well-formed in environment E. We can prove the following proposition to check that the interpretation is well-defined:

Proposition 3 If E ⊢ d ok then [[d]]_{E} is a HOL predicate.

2 THE DEFINITION OF A SILAGE SUBSET 19

Abstract Syntax

p ::= (x:σ)  (parameter)
fd ::= (func x(p̃_{1})p̃_{2} = p̃_{3} begindend) (function)

Static Semantics x_{i} = x_{j} only if i = j ⊢ σ_{i} sigType (1 ≤ i ≤ n)

⊢ [x_{1}:σ_{1}, …, x_{n}:σ_{n}] ⇒ [x_{1}, …, x_{n}], [σ_{1}, …, σ_{n}], {x_{i}: Sig(σ_{i}) | 1 ≤ i ≤ n}

(49)

⊢ p̃_{i} ⇒ x̃_{i}, σ̃_{i}, E_{i} (i = 1, 2, 3) p̃_{2} ≠ []

x̃_{i} ∩ x̃_{j} = {} (i, j ∈ {1, 2, 3}, i ≠ j) x ∉ x̃_{i} (i = 1, 2, 3)

x ∉ Dom(E_{0}) (E_{0} + E_{1} + E_{2} + E_{3}) ⊢ d ok

E_{0} ⊢ (func x(p̃_{1})p̃_{2} = p̃_{3} begindend) ⇒ (σ̃_{1}, σ̃_{2})

(50)

Denotational Semantics

[[[x_{1}:σ_{1}, …, x_{n}:σ_{n}]]] =^{def} x_{1}^{Signal[[σ_{1}]]}, …, x_{n}^{Signal[[σ_{n}]]}  (51)
R[[(σ̃, σ̃′)]] =^{def} Signal[[σ_{1}]] × ⋯ × Signal[[σ_{m}]] × Signal[[σ′_{1}]] × ⋯ × Signal[[σ′_{n}]] → bool where σ̃ = [σ_{1}, …, σ_{m}] and σ̃′ = [σ′_{1}, …, σ′_{n}] (52)

R[[func x(p̃_{1})p̃_{2} = p̃_{3} begindend]]_{E} =^{def} ∀[[p̃_{1}]], [[p̃_{2}]]. x^{R[[(σ̃_{1},σ̃_{2})]]}([[p̃_{1}]], [[p̃_{2}]]) = ∃[[p̃_{3}]]. [[d]]_{(E+E_{1}+E_{2}+E_{3})}

where ⊢ p̃_{i} ⇒ x̃_{i}, σ̃_{i}, E_{i}  (53)
F[[(σ̃, σ̃′)]] =^{def} \{ \begin{matrix}Signal[[σ_{1}]] × ⋯ × Signal[[σ_{m}]] → Signal[[Tuple(σ̃′)]] & if m > 0 \\ Signal[[Tuple(σ̃′)]] & otherwise \end{matrix} where σ̃ = [σ_{1}, …, σ_{m}] and σ̃′ = [σ′_{1}, …, σ′_{n}] (54)

F[[func x(p̃_{1})p̃_{2} = p̃_{3} begindend]]_{E} =^{def}

∀[[p̃_{1}]]. x FUN^{F[[(σ̃_{1},σ̃_{2})]]}([[p̃_{1}]]) =

ϵy. ∃[[p̃_{2}]]. y = ⟨[[p̃_{2}]]⟩ ∧ x^{R[[(σ̃_{1},σ̃_{2})]]}([[p̃_{1}]], [[p̃_{2}]])
where ⊢ p̃_{i} ⇒ x̃_{i}, σ̃_{i}, E_{i} and y = x OUT^{Signal(Tuple(σ̃_{2}))} (55)

Figure 8: Functions

2.4 Functions

Figure 8 shows the abstract syntax of parameters and function definitions in Silage. A parameter is a variable paired with a type. A function definition

     func x(p̃_{1})p̃_{2} = p̃_{3} begindend,

is meant to introduce x as a function, with inputs and outputs in parameter lists p̃_{1} and p̃_{2}, local variables in list p̃_{3}, and specified by the definition d.

The static semantics of parameter lists and function definitions are represented by the two judgments

⊢ p̃ ⇒ x̃, σ̃, E and E ⊢ (func x(p̃_{1})p̃_{2} = p̃_{3} begindend) ⇒ FT,

which are defined by rules (49) and (50) respectively in Figure 8.

The judgment for parameter lists checks that all the variables are distinct, and that each of the types is a signal type—variables cannot stand for tuples in Silage. The rule returns lists x̃ and σ̃ of the variables and types declared in the parameter list, and an environment E recording the types of the variables.

Inference rule (50) for function definitions has six antecedents: (1) that the three parameter lists are well-formed; (2) that the output parameter list, p̃_{2}, is not empty;

(3) that no variable is defined twice; (4) that the function variable x is not declared also as a signal parameter; (5) that the function variable x does not occur in the initial environment E_{0}; and (6) that the definition d is well-formed.

Each Silage function definition is interpreted in HOL in two ways: as a relation holding between its input and output parameters, and as a function mapping from its input to its output parameters. Rules (52) and (54) specify the HOL types of the relational and functional interpretations of Silage functions. If x is the name of the Silage function, rules (53) and (55) specify HOL equations to define first a relation constant called x, and then a function constant x FUN, in terms of the relation x. These rules have the following properties:

Proposition 4 If fd is (func x(p̃_{1})p̃_{2} = p̃_{3} begin d end), and if E ⊢ fd ⇒ FT, then

(1) R[[e]]_{E} is a closed equation defining new constant x of type R[[FT]]; and

(2) F[[e]]_{E} is a closed equation defining new constant x FUN of type F[[FT]].

Consider function SP64 from Section 2 as an example. The rules define two constants, SP64 and SP64 FUN with types:

SP64: Signal(num list) × Signal(num list) × Signal(num) → bool SP64 FUN: Signal(num list) × Signal(num list) → Signal(num)

5SIGPLUS is the name used in the implementation for the signal operation + .

Here is the defining equation for the relation constant SP64:

∀A B C.
SP64(A, B, C) =
(∃S T.
(A !! 0) ∼ (VAL 0) ∧
(∀i :: 1 TO 64.
(S !! i) ∼ ((S !! (i − 1)) SIGPLUS (T !! (i − 1))) ∧
(T !! (i − 1)) ∼ ((A !! (i − 1)) SIGMULT (B !! (i − 1))))) ∧
C ∼ (S !! 64)

Similarly, here is the defining equation for the function constant SP64 FUN:

∀A B. SP64 FUN(A, B) = ϵSP64 OUT. ∃C. (SP64 OUT = C ∧ SP64(A, B, C))

Hilbert’s ϵ-operator, written ϵx^{τ}. P, and pronounced “that x such that P,” stands for some term of type τ that satisfies the predicate P, unless there is none, in which case it stands for some arbitrary element of type τ. The equation uses Hilbert’s operator to cast the relation SP64 as a function SP64 FUN: one can read it as: “given inputs A and B, if one can pick a C such SP64(A, B, C) holds, then the output is such a C”. The functional constant is generated by subsequent applications of the function, by rule 29 in Figure 6.

2.5 Summary

All of the mathematical entities used in the definition are summarised in Figure 9, which is meant to be a notational reference guide.

3 An example transformation

We illustrate how the HOL semantics of Silage can be used in practice with a pipelining transformation taken from Lippens’ study of Silage transformations [17]. The initial program is the scalar product function SP64 from Section 1. Here is the iterator that does the work of the function:

(i : 1..64) ::

     begin

S[i] = S[i − 1] + T [i − 1]; T [i − 1] = A[i − 1] × B[i − 1]

     end;

Lippens supposes that the target architecture has both an adder and a multiplier. The form of the iterator in the initial program suggests that S[i] and T [i − 1] be computed on each cycle of the iteration, which would mean that the two execution

Abstract Syntax

σ ∈ Type  (types)
x, y, … ∈ Var  (variables)
op ∈ Operator (operators)
e ∈ Exp  (expressions)
d ∈ Defn  (definitions)
p ∈ Param (parameter definition)
fd ∈ FunDefn (function definitions)

Semantic Objects

FT ∈ FunType = Type^{∗} × Type^{+}  (function types)
a ∈ Attrib = {Sel, Man, Hol(c_{1}, c_{2}) | c_{i} ∈ HolConst} (attributes)
Entry = \begin{cases}Sig(σ), Ind, Fun(FT) \\ | σ ∈ Type, FT ∈ FunType\} \end{cases}  (entries)
E ∈ Env = Var →^{fin} Entry  (environments)

Static Semantics ⊢ Type sigType

Env ⊢ Exp ⇒ Type, Attrib^{∗}

Env ⊢ Defn ok ⊢ Param^{∗} ⇒ Var^{∗}, Type^{∗}, Env Env ⊢ FunDefn ⇒ FunType Denotational Semantics

[[Type]]  (HOL type)
R[[FunType]]  (HOL relation type)
F[[FunType]]  (HOL function type)
[[Exp]]Env^{M}  (HOL term (manifest sample))
[[Exp]]_{Env}  (HOL term (signal))
[[Defn]]_{Env}  (HOL term (predicate))
[[Param^{∗}]]  (list of typed HOL variables)

R[[FunDefn]]_{Env}

(HOL constant definition)

F[[FunDefn]]_{Env}

(HOL constant definition)

Figure 9: Outline of the definition units cannot be used concurrently because the computation of S[i] depends on the value of T [i − 1]. Lippens suggests the following tuned replacement for the iterator:

T [0] = A[0] × B[0];

(i : 1..63) ::

     begin

T [i] = A[i] × B[i];

S[i] = S[i − 1] + T [i − 1]

     end;

S[64] = S[63] + T [63]

Here the computation of T [i − 1] occurs in the cycle before that of S[i], so there is no data dependency between the addition and multiplication in the loop body, allowing concurrent use of the execution units.

Lippens had no semantics to prove the transformation correct, but it has been proved as the following HOL theorem:

⊢ (∀i :: 1 TO 64. (S !! i) ∼ ((S !! (i − 1)) SIGPLUS (T !! (i − 1))) ∧ (T !! (i − 1)) ∼ ((A !! (i − 1)) SIGMULT (B !! (i − 1)))) = (T !! 0) ∼ ((A !! 0) SIGMULT (B !! 0)) ∧ (∀i :: 1 TO 63. (T !! i) ∼ ((A !! i) SIGMULT (B !! i)) ∧ (S !! i) ∼ ((S !! (i − 1)) SIGPLUS (T !! (i − 1)))) ∧ (S !! 64) ∼ ((S !! 63) SIGPLUS (T !! 63))

The following general theorems about restricted quantifications are needed in the proof of the example:

⊢ ∀P Q R. (∀i :: P. Q i ∧ R i) = (∀i :: P. Q i) ∧ (∀i :: P. R i)

⊢ ∀P m n. m < n ⟹ ((∀i :: m TO n. P i) = m ∧ (∀i :: (SUC m) TO n. P i))

⊢ ∀P m n. m ≤ n ⟹
((∀i :: m TO(SUC n). P i) = (∀i :: m TO n. P i) ∧ P (SUC n))
⊢ ∀P m n k. (∀i :: (m + k) TO(n + k). P i) = (∀i :: m TO n. P (i + k))

4 Relationship between Mini-Silage and Silage

The Berkeley Silage Reference Manual [14], the IMEC Silage compiler manual [19] and the Mentor Graphics DFL manual [7] each describe a dialect of Silage. The intention in the selection of the Mini-Silage subset was to obtain a simple subset of IMEC Silage, expressive enough to cope with realistic program transformations. We enumerate what has been omitted from the present definition of Mini-Silage and whether the present semantics could be extended to include them.

Types. The three versions of Silage offer fixed-point and floating-point data, as well as just the unsigned integers used in Mini-Silage. The machine representation of data can be specified, and a rich collection of arithmetic, relational, bitwise and vector operations is offered. Vectors need not be indexed from 0 as they must be in Mini-Silage. Expressions can be cast from one type to another. Formal signal parameters can have their rate and phase information specified in DFL, and in both IMEC Silage and DFL formal vector parameters can have their dimensions specified. It would be straightforward to model the omitted fixed-point or floating-point types in HOL, given suitable HOL theories.

Executability. The Mini-Silage static semantics ensures that a program has a well-defined logical meaning, but does not check that a program is executable. The three Silage texts mention the single-assignment condition, that each signal be defined exactly once, and implicitly assume an acyclicity condition, that no sample be defined in terms of itself. These conditions could in principle be added to the Mini-Silage definition, by macro-expanding iterator bodies. The indices of vector accesses could be checked to be within the vector bounds statically if indices were manifest expressions.

Recursive functions. All three dialects of Silage allow functions to be recursive, provided that each application has a finite expansion, but Mini-Silage allows no recursive functions. None of the texts specifies precisely what kinds of recursion are allowed. At the cost of additional complexity the denotational semantics of functions could be extended to deal with recursion.

Syntax. In Mini-Silage all local variables used in a function have to be declared in its header, but in the full language local variables do not have to be declared. It would be fairly straightforward to extend the static semantics to infer what local variables are used. Berkeley Silage and DFL allow nested local variables, but this construct was omitted because it is not part of IMEC Silage. It would be easy to add.

Multi-rate and aperiodic signals. In Mini-Silage the samples of all signals are generated at the same regular rate; signals are modelled as functions mapping an integer time to a sample. IMEC Silage allows different signals to be generated at different rates and phases, but every signal is periodic. Berkeley Silage and DFL allow irregular or aperiodic signals, as well as multi-rate periodic signals. Both multi-rate and aperiodic signals could be modelled as a HOL type, for instance by using rational numbers to represent time as described by Hilfinger [14], but operations on signals would then be more complex than at present. Angelo [1] discusses modelling such signals in HOL.

Multiple assignment. The IMEC Silage data-dependent iteration construct and the DFL indefinite iteration construct allow multiple assignment to the same signal variable, and are essentially imperative while-loops. It is not clear how to extend this definition to cover such features.

5 Mechanisation

The Mini-Silage definition has been mechanised within the HOL system. Each of the syntactic categories and semantic objects from Figure 9 is mechanised as an ML type, and each of the static semantics judgments and denotational semantics functions is mechanised as an ML function. In this section we outline the highlevel behaviour of the mechanisation, and discuss other approaches to mechanising language definitions in HOL.

The high-level behaviour of the system is represented by the function compile, of type

     Env → FunDefn → Var × FunType × (string × term) × (string × term),

where Env, FunDefn, Var, FunType are the ML types corresponding to the metalanguage sets Env, FunDefn, Var, and FunType respectively, and string and term are the builtin types of strings and HOL terms. The HOL-Silage system is specified as follows:

(1) For all E ∈ Env, fd ∈ FunDefn, FT ∈ FunType, if E ⊢ fd ⇒ FT, and x is the name of the function being declared, then evaluation of (compile E fd) converges to the quad

(x, FT , (x, R[[fd]]_{E}), (x FUN, F[[fd]]_{E})).

(2) For all E ∈ Env, fd ∈ FunDefn, if there is no FT ∈ FunType, such that E ⊢ fd ⇒ FT, then evaluation of (compile E fd) fails (that is, raises an exception, but does not loop).

There can be no formal proof within the HOL system that the HOL-Silage system is correct, because its statement of correctness mixes HOL and ML statements. On the other hand, the ML program is structured exactly in accordance with the Mini-Silage definition, and is only about 650 lines of ML, so it is feasible to convince oneself of its correctness by close examination of its text. At present the HOL-Silage system takes Silage abstract syntax as its input; in the future we intend to write a parser for the concrete syntax so that real Silage source files can be input into HOL.

It is worth comparing the mechanisation of Silage in HOL to earlier work on Ella. The HOL-Ella system [3, 4] embeds the hardware description language Ella in HOL by treating Ella declarations as predicates. Ella is mechanised in HOL in a similar way to that adopted here, in that an ML program maps phrases of abstract syntax into HOL terms. The two embeddings are compared elsewhere [2]; essentially there are two differences in approach between HOL-Ella and HOL-Silage.

First, there is no formalisation of the translation of Ella into HOL terms. In particular, the well-formedness of Ella programs is defined only informally. There are two advantages of formalising the translation process itself: theorems can be stated and proved about the language itself; and the specification can be turned almost immediately into an executable program.

Second, in HOL-Ella the semantics of every production of abstract syntax is represented by a unique constant. To see the difference, consider the translation of Silage iterators:

[[(x : e_{1}..e_{2}) :: d]]_{E} =^{def} ∀x^{[[Nat]]} :: [[e_{1}]]_{E}^{M} TO[[e_{2}]]_{E}^{M}. [[d]]_{E+{x: Ind}}

Instead of this, one could define a new constant

ITER m n d =^{def} ∀x :: m TO n. (d x)

and then translate iterators as follows:

[[(x : e_{1}..e_{2}) :: d]]_{E} =^{def} ITER [[e_{1}]]_{E}^{M} [[e_{2}]]_{E}^{M} λx. [[d]]_{E+{x: Ind}}

Logically, the two approaches confer exactly the same meaning on an iterator. Practically, the claim of the HOL-Ella approach is that it is easy to translate mechanically to and from the HOL representation and concrete syntax of an Ella phrase. It would be straightforward to recast the Mini-Silage definition to use additional constants; whether this would be worthwhile must await practical experience.

6 Summary

A substantial subset of the dataflow language Silage has been selected, and given meaning in terms of the HOL logic. The original contribution is to combine the methods of Structural Operational Semantics [20, 18] and circuits as HOL predicates [10] to make a language definition that is precise, amenable to formal proof and directly implementable.

The immediate application is to support study of Silage program transformation, but the definition should be of interest to the Silage community because it is a step towards a formal definition of the non-imperative part of the language. More generally, the framework developed here ought to be applicable to other programming languages.

Acknowledgements. I wish to thank Mike Gordon for the opportunity to work on this project, which was part of the Esprit CHEOPS Basic Research Action 3215. Luc Claesen of IMEC has been helpful in various ways, and enabled me to see Mentor Graphics’ DFL manual. Catia Angelo, Wim Ploegaerts and Hans Samsom of IMEC have been very hospitable during my visits to IMEC. I am particularly indebted to Catia Angelo for discussions of how to give semantics to Silage, and in particular for suggesting the relational approach.

References

[1] C.M. Angelo, L. Claesen, and H. De Man. Modelling DSP specification semantics for formal transformational design in HOL. In Luc Claesen and Michael Gordon, editors, HOL’92 International Workshop on Higher Order Logic Theorem Proving and its Applications, Leuven, Belgium, 21–24 September 1992. Elsevier North Holland, 1992.

[2] Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, John Herbert, and John Van Tassel. Experience with embedding hardware description languages in HOL. In V. Stavridou, T. F. Melham, and R. T. Boute, editors, Theorem Provers in Circuit Design: Theory, Practice and Experience: Proceedings of the IFIP TC10/WG 10.2 International Conference, Nijmegen, June 1992, IFIP Transactions A-10, pages 129–156. North-Holland, 1992.

[3] Richard Boulton, Mike Gordon, John Herbert, and John Van Tassel. The HOL verification of ELLA designs. In Proceedings of the International Workshop on Formal Methods in VLSI Design, Miami, 1990. Also available as Technical Report 199,Computer Laboratory, University of Cambridge (Revised November 1990).

[4] Rochard J. Boulton. A HOL semantics for a subset of ELLA. Technical Report 254, Computer Laboratory, University of Cambridge, April 1992.

[5] H. De Man, J. Rabaey, P. Six, and L. Claesen. Cathedral–II: A silicon compiler for digital signal processing. IEEE Design & Test of Computers, pages 13–25, December 1986.

[6] EDAC–91, Amsterdam, February 25–28, 1991.

[7] European Development Centre, Leuven. DSParchitect DFL User’s and Reference Manual, December 1991.

[8] D. Genin, P. Hilfinger, J. Rabaey, C. Scheers, and H. De Man. DSP specification using the SILAGE language. In IEEE International Conference on Acoustics, Speech and Signal Processing, pages 1057–1060, April 1990.

[9] Andrew D. Gordon. The formal definition of a synchronous hardwaredescription language in higher order logic. In International Conference on Computer Design, Cambridge, Massachusetts, October 11–14, 1992. IEEE Computer Society Press, 1992.

[10] Michael J. C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design. North-Holland, 1986.

[11] Michael J. C. Gordon. HOL: A proof generating system for higher order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer, 1987.

[12] Mike Gordon and T. F. Melham. Introduction to HOL: A Theorem-proving Environment for Higher-order Logic. Cambridge University Press, 1993. To appear.

[13] Paul N. Hilfinger. Silage, a high-level language and silicon compiler for digital signal processing. In IEEE Custom Integrated Circuits Conference CICC–85, pages 213–216, Portland, Oregon, May 1985.

[14] Paul N. Hilfinger. Silage Reference Manual. Computer Science Division, University of California, Berkeley, December 1987.

[15] Ton Kalker. Formal methods for silicon compilation. In EDAC–91 [6], pages 395–400.

[16] P. Lippens, J. van Meerbergen, A. van der Werf, W. Verhaegh, B. McSweeney, J. Huisken, and O. McArdle. Phideo: a silicon compiler for high speed algorithms. In EDAC–91 [6], pages 436–441.

[17] Paul Lippens. Defining control flow from an applicative specification. Internal report, Philips Research Laboratories, Eindhoven, December 22, 1988.

[18] Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, Cambridge, Mass., 1990.

[19] Lode Nachtergaele. User Manual for the S2C Silage to C Compiler. IMEC, Leuven, March 22, 1990.

[20] Gordon D. Plotkin. A structural approach to operational semantics. Technical Report FN–19, DAIMI, Aarhus University, September 1981.

[21] J.G. Samsom, L.J.M. Claesen, and H.J. De Man. Correctness preserving transformations on the Hough algorithm. In CompEuro 92, The Hague, May 4–8, 1992.

[22] Ingrid Verbauwhede. VLSI Design Methodologies for Application-Specific Cryptographic and Algebraic Systems. PhD thesis, Catholic University, Leuven, July