by Walter Dosch, Universität Augsburg
A computer program is the implementation of an algorithm in terms of the constructs provided by a programming language. Similarly we view a digital circuit as the implementation of an algorithm where the primitive elements are electronic devices. With this analogy in mind, we formally derive two combinatorial circuits --- a parallel and a carry-look-ahead successor --- and two sequential circuits --- a parallel and a serial counter --- from a common specification. The formal derivation disentangles the design decisions concerning
First, we introduce the data structures, viz. natural numbers and digit sequences, together with their algebraic properties. In the derivation, digit sequences model the succession of digits in space or in time.
Then we specify the successor function as an operation induced by changing the representation from natural numbers to digit sequences. A first algorithmic solution is obtained by eliminating the abstraction and representation function.
Next we study the transformational synthesis of two combinatorial circuits, viz. a parallel and a carry-look-ahead successor function. We achieve a uniform recursion by introducing the carry bit as a continuation parameter. The recursion of the parallel successor function determines a regularly structured network where the half-adder components are cascaded into the breadth of the network. For every input sequence of fixed length, we obtain a non-recursive network by successively unwinding the recursion. Isolating the carry computation and decomposing the recursion then leads to the carry-look-ahead successor function.
Afterwards we formally derive two sequential circuits, viz. a parallel and a serial counter. In a first step we transform the successor function into repetitive form; this allows us to keep the network static by reusing the elementary components. Then we merge the input and output parameter into a sequence of constant length; in this way we achieve a static component determining the state. Depending on the way of merging, we end up with a parallel counter where the state is an array, or with a serial counter where a shift register determines the state.
In summary, the synthesis leads to a series of more and more refined circuit descriptions which are all by construction correct with respect to the initial specification. It gives insight into the algorithmic principles of a counter by exhibiting the high-level design decisions. The synthesis is motivated by algorithmic reasoning and based on pure algebraic calculation; it widely exploits the algebraic properties of sequences enriched by suitable induction principles.
For details see [Dosch 94, Dosch 95].