Esprit project 881 - FORFUN

In Esprit project 881 (FORFUN), the usefulness of the principle of system semantics is was tested by applying it to a specific domain: electronic systems. A special language called Glass was designed to describe electronic systems and to be suitable for computer manipulation. Semantic functions were implemented as functions in existing programming languages.

KUN and Sagantec are developing support programs (parsers, compilers, type checkers, etc.), ABT is developing example semantic functions and system descriptions for digital systems. TUD is doing the same for analog systems. ABT is also investigating the possibilities for transformational design using Glass.

System semantics

system calculus

One of the basic premises of the project was that it is possible to use one language to describe a wide range of systems (electronic systems, computer programs, mechanical systems, etc.).

Depending on the purpose of the description different interpretations are possible. This is similar to the way the notation of mathematical functions can be used to describe the behavior of a wide range of systems (e.g. electronic or economic systems), depending on the interpretation.

Systems are described by describing the composition of components. Starting with a set of atomic components, new components can be defined as a composition of existing components until the composition of the entire system has been described. Composition can be done by using a few basic composition mechanisms, or named composition patterns called combinators can be introduced. Systems can be directional (information flows in one direction) or non-directional; both types can be described.

The used language is a calculus: it only describes objects and the relations between objects, and not predicates on the objects or the operations on the objects. System calculus is based on lambda-calculus and sigma-calculus. Lambda-calculus is the theoretical basis of functional programming languages, sigma-calculus might serve as the theoretical basis of Prolog, although sigma-calculus is in fact more recent.

At the moment only the syntax of lambda-calculus and sigma-calculus is available for system calculus. To make it more useful, additional syntax (syntactic sugar) must be added for common system concepts.

Semantic functions

The different interpretations of system calculus can be described by semantic functions that map expressions in system calculus onto expressions in a suitable domain of interpretation. Semantic functions can be defined by defining the mapping of all atomic components and combinators.

Semantic functions can be used to derive different aspects of a system (e.g. structure, behavior, implementation) from system calculus by using a suitable interpretation of the components and combinators of the system. It might even be possible to derive different implementations from one system calculus expression, but that is much more speculative.

Theorems and correctness proofs

In the same way that theorems have been developed for function calculus, it is possible to develop theorems for system calculus. These theorems are only dependent on their premises, not on the interpretation that is given to system calculus. Therefore they can be more general than the theory that is developed for a specific class of systems.

An important application of the theorems is the application in correctness proofs. If sufficient theorems are available, it is possible to prove the correctness of an implementation by deriving it from the original specification of the system by using the appropriate theorems. If an implementation is constructed by only using theorems, this is called transformational design, and the implementation is correct by construction.

Glass

Glass is designed as a special form of system calculus to describe electronic systems in a form suitable for computer manipulation. Next to the essential constructs required for a system calculus, some `sugar' has been added to make description of the systems more convenient:

Typing.
A macro mechanism to handle repetition of system parts.
A library mechanism to handle libraries of definitions.

A Glass system description is started by naming the system that is described, e.g.:

system testpll.

The named system must be defined in the following list of atom specifications and component definitions.

Atomic components or combinators are introduced by specifying their type, e.g.:

/* Source Uin has an output port with two connections. */
atom Uin :: !(B, B).

/* transistor `T1' has 3 connections */
atom T1 :: (B, B, B).

/* current controlled current source,
   has input and output port. */
atom cccs :: (B, B) => (B, B).

In general types are based on one basis interconnection type B, and new types can be composed from other types by:

bundling	`(B, B, B)`
power	`B^42`	bundle of 42 connections
input annotation	`?(B, B)`	this the type of the input
output annotation	`!(B, B)`	this is the type of the output
direction annotation	`(B, B) => B`	is the same as `(?(B, B), !B)`

Components can have parameters, and this is reflected in the type by the function composition operator ->, e.g.:

/* `R' is an atom that, given a value, results in a component
   with two connections. */
atom R :: num -> (B, B).

/* 'and' is a component that, given a number of
   connections `n', results in an AND gate with `n' inputs. */
atom and :: num -: n -> B^n => B.

In general parameters can be of type num, string or the type of components. New names for compositions of types can be introduced:

type port = (B, B).
type twoport = (port, port).

These names are only synonyms, not new types. New components can be defined with a directional definition:

/* A pll (phased locked loop) consisting of
   phasedet    phase detector
   vco         voltage controlled oscillator
   filter      loop filter
 */
def
    pll :: port => port;
    pll in = vcoout
    where
        vcoout = vco (filter (phasedet (in, vcoout)).

or with a non-directional definition:

def
    pll :: (?port, !port);
    pll (in, out) =
    {
        vco (f, out),
        filter (ph, f),
        phasedet ((in, out), ph)
    }

You must specify the type of all components that you define. If a component has one or more components as parameter it is called a combinator:

/* two one-port components `Ca' and `Cb' connected in series */
def
    ser :: port -> port -> port;
    ser Ca Cb (a, b) = { Ca (a, i), Cb (i, b) }.

Of course combinators can also be atoms. The use of combinators leads to a new style of definition, e.g.:

def
    pll :: port => port;
    pll in = out
    where
        out = casc phasedet (casc filter vco) (in, out).

Glass has a number of standard constructs for interconnection:

Within a definition all occurrences of a connection variable are connected. E.g.:

/* two one-port components `Ca' and `Cb' connected
   in parallel */
def
    par:: port->port->port;
    par Ca Cb (a, b) = { Ca (a, b), Cb (a, b) }.

In this case component Ca and Cb are connected in parallel.

Reference to a component instead of a connection variable implies connection to the output of the referred component. E.g.:

/* selection of input `a' or `b' depending on the
   state of `s'. */
def
    sel :: (B, B, B) => B;
    sel (a, b, s) = or (and (s, a), and ((not s), b)).

In non-directional definitions synonym terms can occur:
```
    *(c0, c1 .. cn)
```
This indicates that c0, c1 ...cn are synonyms. This may also be interpreted as a connection between the variables.
Connections can be ``bundled''. Interconnection of a bundle implies interconnection of all connections in the bundle.

Appendices A and B give larger examples of Glass descriptions. At the moment a Glass reference manual is available where the exact definition of the language is given. A Glass user manual is currently being written.

Support programs

If semantic functions would work directly on Glass text they would require a large amount of code that is common to them all, e.g. a parser, type checker and macro expander. This would lead to unnecessary duplication and inconsistency, and for these reasons an other approach has been adopted. One central parser converts Glass text into an internal format that is used by all other programs. The structure of the internal format is also described in textual form and there are programs available to generate code for a number of languages to read and write this representation. Moreover, it is simple to add code generation for new languages. Appendix C shows the current structure description for Glass. The result of all this is a very flexible system where any change in the internal format is automatically reflected in the manipulation programs. Also, pieces of the entire system can be written in a wide range of languages, since there is a well-defined interface between the various programs.

At the moment the following support programs are available:

A parser from Glass text to internal format.
A type checker.
A `flattener' that removes all hierarchical constructs from a Glass description.

Programs to handle the library mechanism of Glass and to expand macros are under development.

Semantic functions

Semantic functions are functions that map Glass expressions onto expressions in a suitable domain of interpretation. A semantic function is defined by specifying the interpretation of the atoms of a description and the interpretation of the standard constructs of Glass. Thus, to be able to define a certain semantic function it must at least be possible to find an interpretation of the standard constructs of Glass. In addition a set of atoms must be available for which interpretation is possible. There are two possibilities to define atoms for semantic functions:

A standard set of atoms plus their interpretation is provided. This will require general atoms with parameters, e.g. a component ``resistor'' with a value as parameter.
For each system the interpretation of the atoms is given by the user. For example, there is a component ``Rb'' for which the user specifies that it is a resistor with a value of 2200 ohm.

The second solution has as advantage that it leaves the entire interpretation to the user, and therefore is much more flexible than the first one. On the other hand, it requires that the user writes (a part of) the semantic function, so that an environment must be provided where this is simple. At the moment it is not certain that such an environment can be provided.

If a system description contains more complex components as atoms (e.g. with bundles of connections or combinators), the semantic function must be able to interpret these atoms. This requires that there is a sufficiently powerful language available for the domain of interpretation. In particular suitable languages are required for:

Description of the behavior, or in general for mathematical functions and relations.
Description of the layout, or in general for layers of two-dimensional structures.

In both cases a suitable language has not been found, and it might be necessary to develop a new language for the purpose.

Integration in a design system for analog circuits

In principle the use of system semantics is very suitable in a design system for analog circuits. Since the software to support system semantics is still under development there are some important problems:

The language Glass was designed for manual use. The automatic generation and manipulation of circuit descriptions may cause problems, in particular the generation of type specifications. On the other hand, the current description languages (SPICE and ANP3 input languages) are even less suitable for that purpose.
An internal representation like the one shown in appendix C might be suitable for automatic manipulation, but the current representation will require a major cleanup.
Specific semantic functions for each system description are even more desirable for automatic generation of systems, but they require a suitable implementation environment.

Conclusion

Given the very experimental nature of system semantics there are some important achievements in the Esprit project:

There is a useful (although not perfect) system description language.
A flexible method has been found to implement semantic functions in a wide range of languages.
There is a `nearly' working path from Glass input text through a parser, type checker, flattening function and semantic function to SPICE and ANP3.

There are also some major problems:

For useful interpretation there must be suitable languages available for the domain of interpretation. For most domains this is a problem.
There must be a suitable implementation language for semantic functions. At the moment such a language is not available.

A pll test circuit in Glass

system testpll.

type
    sigcon = (B, B).

atom u_adder :: (sigcon, sigcon) => sigcon.
atom Uin :: sigcon.
atom Unoise :: sigcon.
atom pllmult :: (sigcon, sigcon) => sigcon.
atom pllfilter :: sigcon => sigcon.
atom pllvco :: sigcon => sigcon.
atom meter :: sigcon.

def
    testpll :: ;
    testpll =
    { drivecircuit in, meter out }
    where
        out = pll in.

def
    pll :: sigcon => sigcon;
    pll in = vcoout
    where
        vcoout = pllvco filterout,
        filterout = pllfilter (pllmult (in, vcoout)).

/* the driving circuit in this test */
def
    drivecircuit :: signal;
    drivecircuit = u_adder (Unoise, Uin).

An AM radio described in Glass

/* Example description of an AM radio. This only describes the
   block diagram of an AM radio.
 */

system amradio_env.

type sigcon = (B, B).

atom amsource :: !sigcon.
atom radioload :: ?sigcon.
atom hf_amp :: sigcon => sigcon.
atom hf_filter :: sigcon => sigcon.
atom loc_osc :: !sigcon.
atom if_agc :: sigcon => sigcon.
atom if_filter :: sigcon => sigcon.
atom det_vco :: sigcon => (sigcon, sigcon).
atom lf_filter :: sigcon => sigcon.
atom lf_amp :: sigcon => sigcon.

/* This describes the radio with its source and load.
   Therefore the system does not have an input or an output
   (in this description).
 */
def
    amradio_env :: ();
    amradio_env a =
    { amsource in, amradio (in, out), radioload out }.

def
    amradio :: sigcon => sigcon;
    amradio in = lf_part (if_part (hf_part in)).

def
    hf_part :: sigcon => sigcon;
    hf_part in = casc hf_amp (casc hf_filter up_converter) in.

def
    if_part :: sigcon => sigcon;
    if_part in = casc if_filter if_agc in.

def
    lf_part :: sigcon => sigcon;
    lf_part in = casc detector (casc lf_filter lf_amp) in.

def 
    up_converter :: sigcon => sigcon;
    up_converter in = hf_mixer (loc_osc, in).

def
    detector :: sigcon => sigcon;
    detector in = det_mixer fi_det in
    where
        (fi_pll, fi_det) = det_vco (pll_mixer (fi_pll, in)).

def
    casc :: (sigcon=>sigcon)->(sigcon=>sigcon)->(sigcon=>sigcon);
    casc Ca Cb in = Cb (Ca in).

Last modified Friday 23 February 2007 13:45:43 UT by Kees van Reeuwijk.