A Formal Semantic Model to fit SIL for Transformational Design

A Formal Semantic Model to fit SIL for Transformational Design

Corrie Huijs and Thijs Krol

University of Twente, P.O. Box 217, 7500 AE Enschede, The Netherlands,

e-mail: chuijs@cs.utwente.nl, tel: +31 53 893697, Fax: +31 53 333895

Abstract

SIL (SPRITE Input Language) is a single token signal

flow graph representation developed as an intermediate

format between specification languages and silicon

compilers. This paper presents a part of a formal

semantic model for SIL which is nicely intuitive because

of the use of tables as mathematical representation of the

semantics. Together with this semantic model SIL

becomes a useful language backbone for

transformational design.

1: Introduction

Transformational design integrates synthesis and

verification and is therefore considered as a practical

solution for the design correctness problem [1, 2, 3].

Both interactive design and automatic synthesis can be

based on transformational design. In the first case the

designer is offered a large set of transformations to

compose the design process. Each design step is a

transformation which results in an intermediate design.

In the second case the choice and order of the design

transformations is determined by the synthesis tool. If

each design transformation as well as the sequential

composition of design transformations is correctness

preserving then correctness by construction is achieved

and the design correctness problem is solved.

Any design process requires a method for design

representation which ranges from the specification to the

description of the final implementation. In order to avoid

the necessity to define similar transformations for

different design representations, the transformational

design process should be based on a single intermediate

design representation. This intermediate design

representation should be provided with formal semantics

in order to prove the correctness preserving property ofthe transformations and their compositions. Notice that

formal semantics and proof systems primarily support

the understanding of the transformational design process

and the understanding of the applicability of the various

transformations. Once the transformational design steps

are understood the correctness proofs are only of

secondary importance.

A large number of specification languages is known,

all having their own characteristics. In the design of

large complex systems it is useful to be able to integrate

the use of several specification languages [4]. Therefore

the intermediate format should cover the functionality of

the specification languages used in the current design

practice. Flow graphs appeared to satisfy these

requirements and to be useful in the definition of

synthesis activities[4]. SIL (SPRITE Input Language

[5]), developed in the EC ESPRIT project SPRITE, is an

intermediate design representation based on signal flow

graphs and appears to be suitable in transformational

design [6,7].

The issue of this paper is the presentation of

principles on which the formal semantic model of SIL is

based [8]. In transformational design the

compositionality of the used semantics is important.

Which means that the semantics of a composition has to

be a composition of the semantics of the components.

Besides compositionality transformational design needs

semantics which include a representation of the

functional (I/O) behaviour, described by the design, in

order to check whether the specification is satisfied. This

paper is restricted to the part of the formal semantics of

SIL that is related to functional behaviour. In this part,

tables are used as mathematical model of the semantics,

the functional behaviour. Operations are defined on these

tables to describe composition of semantics. Together

with these operations the set of tables becomes an

algebra which is a useful and nicely intuitive semantic

algebra.

HALFADDHALFADD:

IN

INAND

XOROUTa

band1

xor1generate

OUTtransmissionXOR:

IN

INANDNOT

OROUTin1

in0and1

or1not1

and2out0AND

HALFADD: generate:= a AND b; transmission := a XOR b; XOR: out0:=(NOT(in0 AND in1)) AND (in0 OR in1);

Figure 1: Example of simple SIL description existing of 1 node and 2 SIL graphs, HALFADD and XOR

2: SIL

SIL [5] is a single token signal flow graph

representation. A SILgraph (figure 1) exists of nodes

representing operations and edges representing data

communication or precedence relations. Nodes are

represented by circles, except for constant nodes which

are represented by squares. Edges are represented by

arrows between the ports of these nodes. These ports are

called access points and are represented by small bullets

on the nodes. Two kinds of edges are defined: data flow

edges which are normal arrows representing data