The Formal Definition of a Synchronous Hardware-Description Language in Higher Order Logic ^{∗}^{†}

Andrew D. Gordon

University of Cambridge Computer Laboratory New Museums Site, Pembroke Street,

Cambridge CB2 3QG, UK.

Email: Andrew.Gordon@cl.cam.ac.uk

Abstract

If formal methods of hardware verification are to have any impact on the practices of working designers, 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 used for specifying digital signal processing circuits. Higher Order Logic (HOL) is extensively used for research into hardware verification. We have used a novel combination of operational and predicative semantics to define formally a substantial subset of Silage by mapping Silage definitions into HOL predicates. Here we sketch the method used, discuss what is gained by a formal definition, and explain an immediate practical application—secure transformational design of Silage circuits as theorem proving in HOL.

1 Introduction

Silage [10] is a hardware description language (HDL) designed for specifying digital signal processing (DSP) algorithms, and is in use at several sites for research into DSP technology. Silage is a dataflow language intended for high-level synthesis [16] in which a specification expresses the desired behaviour of a circuit, but is free of any architectural commitment. Silage is the source language for synthesis environments including IMEC’s Cathedral-II [6], Philips’ PI-RAMID and Phideo [13] and Berkeley’s Hyper [19]. Silage is translated to a signal flowgraph format upon which synthesis tools act to produce a layout for a particular architecture. Development of Silage designs is helped by software simulators such as IMEC’s S2C compiler [18].

The classic problem with high-level synthesis is the poor performance of automatically synthesised designs. In Silage environments, two kinds of high-level transformations are used to improve the quality of synthesis: (1) Silage-to-Silage transformations applied manually by the human designer—transformational design as described by Samsom [21] for instance— or (2) flowgraph-to-flowgraph transformations applied algorithmically by automatic tools, such as Hyper or Phideo.

In either case, the problem arises of whether the initial and final designs have the same behaviour. Current Silage environments offer only lengthy repeated simulation as a remedy. The goal of this project— a collaboration between Cambridge and IMEC—is to build a system to support human-directed Silageto-Silage transformations as interactive theoremproving. In such a system, the transformation of a specific design is proved correct by instantiating HOL theorems that represent general Silage transformations. We obtain a correctness proof for part of the design— and in principle reduce dependence on simulation— but as ever correctness of the whole design depends on factors—such as compiler correctness—that are not formally proved [16].

A formal definition is essential if transformations are to be proved using the HOL system, but no formal definition of the Silage language exists.^{1} We report here the first formal definition of a substantial subset of Silage, called Mini-Silage [8]. Apart from the immediate application, this work could be of use as the basis of a language standard, and also for verifying algorithmically applied transformations.

2 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. 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 respectively.

∗Work funded as part of the CHEOPS ESPRIT Basic Research Action 3215.

†To appear in ICCD’92: International Conference on Computer Design, Cambridge, Mass., October 11–14, 1992. IEEE Computer Society Press.

1Personal communication with Paul Hilfinger, January 1992.

The samples of a signal can be vectors as well as scalars. Here is how to compute the scalar product [14] of two vectors A and B:

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]

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.

There are two special categories of expression: a manifest expression is a combination of numeric constants, arithmetic operators and iterator variables, and is intended to be computable at compile-time to a numeric value; a selector, such as T [i−1], consists of a signal variable, with a possibly empty series of indexing expressions. Expressions used as iterator bounds and 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.

3 Silage definitions as HOL predicates

HOL is a polymorphically typed classical logic, supporting a conventional collection of operators, including =, ¬, ∧, ∨, ⟹, ∀ and ∃, with their usual meaning, and with mechanisms to define new types and constants.

The idea of specifying circuits by predicates is wellknown in the hardware verification field [9]. Earlier CHEOPS work [12] proposed to model Silage definitions as predicates, but concentrated on how to model bitstring datatypes, and suggested designing an extended language Silage+. In defining Mini-Silage [8] we have ignored the issues of low-level datatypes or multi-rate signals, wishing to concentrate on support for transformations, and have defined precisely how to map from a true subset of Silage into HOL predicates.

We take time to be the integers and model signals with samples of type τ by the HOL function type:

(τ) signal =^{def} int → τ

We model each Silage operation by defining a HOL constant. With these constants one can model each Silage definition as a predicate that must hold of the signals in a correct implementation. Given the constants,

A ∼ B =^{def} ∀t ≥ 0. A(t) = B(t)
(A<>n)t =^{def} A(t − n)
(A SIGPLUS B)t =^{def} A(t) + B(t)

we can model the Fibonacci specification:

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

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

We model vectors in HOL as finite lists of samples, so the numeric vector S, say, in the scalar product example is modelled by a term of HOL type ((num) list) signal. Given some more constant definitions,

∀i :: m TO n. P =^{def} ∀i. (m ≤ i ≤ n) ⟹ P
(A !! n) t =^{def}  EL n (A t)
(A SIGMULT B)t =^{def}  A(t) × B(t)

where EL i [a_{1}, …, a_{n}] = a_{i}, here is the HOL meaning of the iterator from the scalar product example:

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

4 A sketch of the definition

There are two parts of the definition of Mini-Silage in HOL: a written definition [8] and its implementation running in the HOL system. The machineindependent definition on paper is important as a precise human-readable account of Mini-Silage, and as a specification of the implementation. The machine implementation was written after the paper definition was considered complete, and under the discipline that each set or rule in the paper definition corresponded exactly to a type or function in the implementation. Of course, this discipline exposed several defects in the paper definition, which evolved during its implementation, but on completion there is an exact correspondence between the two.

The written definition of Mini-Silage follows the style of Standard ML [17] and consists of three parts: BNF rules determine the abstract syntax; static semantics rules determine the well-typed and wellformed expressions and definitions; predicative semantics rules map definitions into HOL terms. Existing informal Silage texts [11, 18] define the concrete syntax precisely, so it has not been redefined. The point of having a formal definition is to make precise certain aspects of well-formedness or program behaviour left vague in the informal texts.

The implementation consists of a tool running in the HOL system that allows the user to have Silage function definitions translated mechanically into HOL constant definitions.

To illustrate the definition we discuss the semantic treatment of initialisations—such as the first two lines of the Fibonacci example—whose abstract syntax takes the form e_{1}@@e_{2} = e_{3}, where each e_{i} is an expression. Here is the static semantics rule:

⊢ e_{1} ⇒ σ, sel ⊢ e_{2} ⇒ Nat, man ⊢ e_{3} ⇒ σ, man

⊢ e_{1}@@e_{2} = e_{3} ok

The predicate on the bottom says that the initialisation is well-formed, and the rule says that this is so just when the three predicates on the top line hold, each of the form ⊢ e ⇒ σ, a, pronounced “expression e has type σ and attribute a”. An attribute a ∈ {man, sel, other} indicates whether an expression is manifest, or is a selector, or neither. The rule above requires that expression e_{1} and e_{3} have the same type, σ, that e_{1} is a selector, and that e_{2} and e_{3} are manifest numeric expressions. The Silage texts attempt to use BNF rules to assert type and well-formedness conditions; the rules used here are more lucid and precise.

Here is the predicative semantics:

[[e_{1}@@e_{2} = e_{3}]] =^{def} [[e_{1}]](−[[e_{2}]]^{M}) = [[e_{3}]]^{M}

If ϕ is a phrase of abstract syntax, [[ϕ]] is its translation into the HOL logic. Any well-formed expression, such as e_{1}, can be translated to a signal, written [[e_{1}]]. A manifest expression, such as e_{2}, can also be interpreted as a scalar in HOL, written [[e_{2}]]^{M}. The predicate requires that the signal denoted by e_{1} have the sample denoted by e_{3} at negative time e_{2}.

One can prove desired properties of the definition itself, for instance: Theorem. If expression e has type σ, its translation [[e]] is a HOL term of type [[σ]] signal, where [[σ]] is the translation of type σ as a HOL type.

5 Application of the definition

We illustrate how the HOL semantics of Silage can be used in practice with a pipelining transformation taken from Lippens’ study of Silage transformations [14]. The initial program is the scalar product program from Section 2. 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 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 we have proved his example as a HOL theorem, by appealing to the following equational transformations, which are also proved within the HOL system:

[[(i : m..n) ::begind_{1}; d_{2} end]] = [[((i : m..n) :: d_{1}); ((i : m..n) :: d_{2})]]

[[(i : m..n) :: d]] = [[d{m/i}; (i : (m + 1)..n) :: d]] if m < n

[[(i : m..n) :: d]] = [[(i : m..(n − 1)) :: d; d{n/i}]] if m < n

[[(i : (m + k)..(n + k)) :: d]] = [[(i : m..n) :: d{i + k/i}]]

The notation d{e/i} stands for the outcome of substituting expression e for each occurrence of variable i in the definition d.

Other loop pipelining and retiming examples have been mechanically proved, demonstrating the feasibility of this approach for transformational design.

6 Related work

McFarland and Parker [15] report the seminal work on proving HDL transformations correct in terms of a behavioural semantics. Their emphasis was on proving algorithmic transformations correct manually; conversely, our emphasis is on proving manually-applied transformations correct mechanically.

We have deliberately adopted the simplest semantic embedding—programs as predicates—able to support behaviour-preserving transformation so as to focus on the practicality of using an interactive proof assistant to construct correct transformations. Our embedding follows that used for Ella in HOL [3]; in comparison, our work focuses on transformational design and the need for a written formal definition [2]. Other embeddings of HDLs in theorem provers [20, 7] employ more expressive but more complex semantic embeddings. Busch [5] uses a theorem-prover to develop refinements, but expresses hardware using logic rather than an HDL. We have not investigated refinement of Silage programs; if desired, refinements could be represented in HOL as implicative theorems.

There are mechanical transformation systems not based on a general-purpose theorem-prover, such as the Indiana DDD system [4]. The advantage of using an LCF-style theorem-prover such as HOL is that theorems are an abstract type distinguished from sentences of the logic, and so programming errors are unlikely to lead to a proof of a false transformation. Any such ‘proof’ would imply either an inconsistency in higher order logic or an undiscovered bug in the HOL system. Vemuri [22] considers the completeness of a set of interactively-applied transformations. An interactive system for transformational design based on a theorem-prover need not be based on a fixed set of transformations: any logically provable transformation can be made available by resorting to interactive theorem-proving.

7 Conclusions

We have reported work on the first formal definition of a substantial subset of Silage. We combine the language semantics methodology of ML [17] with the idea of circuits as HOL predicates [9] to make a language definition that is precise and amenable to formal proof. We have implemented the definition in HOL, mechanised the denotations of several Silage programs as predicates, and examined how transformational design can be rendered as theorem proving in HOL. Work is in progress in collaboration with IMEC to tackle realistic examples that have arisen in practice, and to find suitable user interfaces to the system.

It is a pleasure to thank Catia Angelo, Richard Boulton, Luc Claesen, Mike Gordon, Brian Graham, Sara Kalvala, Mats Larsson, Wim Ploegaerts and Hans Samsom for fruitful discussions about this work, and for comments on drafts of this paper. Catia Angelo first suggested to me the idea of modelling Silage definitions as predicates.

References

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

[2] Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, John Herbert, and John Van Tassel. Experience with embedding hardware description languages in HOL. In IFIP TC10/WG10.2 Conference on theorem provers in circuit design: theory, practice and experience, Nijmegen, June 22–24, 1992. North-Holland.

[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] C. David Boyer and Steven D. Johnson. Using the Digital Design Derivation system. In J. A. Darringer and F. J. Rammig, editors, Computer Hardware Description Languages and their Applications, pages 235–246. Elsevier Science Publishers B.V., 1990.

[5] Holger Busch and Gerd Venzl. Proof-aided design of verified hardware. In 28th ACM/IEEE Design Automation Conference, San Francisco, California, pages 391–396, June 1991.

[6] 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.

[7] K. G. W. Goossens. Embedding a CHDDL in a proof system. Technical Report ECS–LFCS– 91–155, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, May 1991.

[8] Andrew D. Gordon. A mechanised definition of silage in HOL. Internal report, ESPRIT BRA 3215, Computer Laboratory, University of Cambridge, 1992.

[9] 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.

[10] 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.

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

[12] Ton Kalker. Formal methods for silicon compilation. In EDAC–91, Amsterdam [1], pages 395– 400.

[13] 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, Amsterdam [1], pages 436–441.

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

[15] Michael C. McFarland and Alice C. Parker. An abstract model of behavior for hardware descriptions. IEEE Transactions on Computers, C– 32(7):621–637, July 1983.

[16] Michael C. McFarland, Alice C. Parker, and Raul Camposano. The high-level synthesis of digital systems. Proceedings of the IEEE, 78(2):301–318, February 1990.

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

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

[19] J. M. Rabaey, C. Chu, P. Hoang, and M. Potkonjak. Fast prototyping of datapath-intensive architectures. IEEE Design & Test of Computers, pages 40–51, June 1991.

[20] Lars Rossen. Ruby algebra. In Designing Correct Circuits, Oxford 1990, Workshops in Computing, pages 297–312. Springer-Verlag, September 1990.

[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] Ranga Vemuri. How to prove the completeness of register level transformations. In 27th ACM/IEEE Design Automation Conference, Orlando, Florida, pages 207–212, June 24–28, 1990.