next up previous contents
Next: Further Case Studies Up: Meeting at Madrid Previous: Rigorous Specifications of

Experiments in Specification and Deductive Design of Hardware

by Bernhard Möller, Universität Augsburg

We treat two examples: The single pulser and the RS flipflop. The pulser has to emit a unit-time pulse for every input pulse (which may be of arbitrary length).

The description level is that of synchronous hardware, i.e. we may consider only stabilised values. Therefore we can model wires by streams of boolean values.

We start with specifications at a pre-functional level, using regular-like expressions to describe the ``wave patterns'' of inputs and outputs.

Functions between streams are specified using such patterns. The first step in the development of an implementation consists in deriving linear recursions which correspond to finite automata with output. The automata can then be transcribed directly into sequential circuits in which the states are both outputs and fed back into the circuit.

In the case of the single pulser, we give a series of more and more precise specifications. By taking the design decision that the output pulse should be emitted at the beginning of the input pulse the specification becomes fully deterministic. It turns out that in the corresponding circuit the feedback is only virtual and can by replaced by a simple delay. As a result a combinatorial net implementation of a rising edge detector is obtained.

For the flipflop we give a specification which does not yet determine the behaviour upon the illegal input (1,1). By taking a decision to use the weakest function satisfying the specification, again a fully deterministic specification results. From there the systematic derivation leads to a circuit containing two copies of the classical implementation of a flipflop by two NOR-gates. To get rid of duplication, a finer analysis of the values on the wires has to be performed.



Bernhard Moeller
Fri May 12 14:21:20 MET DST 1995