Via:  uk.ac.nsf; 30 May 89 20:12 BST  (UK.AC.Cam.Cl.scaup)
Date: Tue, 30 May 89 10:20:25 PDT
From: "Paul N. Loewenstein" <paul@edu.stanford.tina>
Message-Id: <8905301720.AA02536@tina>
To: info-hol@edu.ucdavis.clover
Subject: Yet more on n-bit words in HOL
Sender: paul <paul%edu.ucdavis.tina@edu.ucdavis.clover>
Status: R


I feel that is is potentially useful to have 0-width words.

For instance, my serial-parallel multiplier that I have been working
to death as an example for the last year or so has internal registers
that are one bit less than the parallel input. The one-bit multiplier
therefore has internally zero-length words! It is nothing more than an
AND gate. If zero-length words were not available, the one-bit multiplier
would have to be considered a special case. Of course currently I have
to treat the 0-bit multiplier as a special case; it merely supplies
a stream of zeros at its output. However, zero-bit devices can be
useful for degenerate cases; often they translate into zero hardware -
much cheaper than non-zero hardware. On the whole I feel that for
operations which have a reasonable 0-bit meaning, one should allow
zero-bit words. If the zero-bit meaning is clumsy one can always
prove theorems of the form "0 < LENGTH w ==> .....".

I use boolean lists for n-bit words. I try to define combinational
logic as functions on n-bit lists, and allow all reasonable input
wordlengths. For instance my binary adder is characterised by the
following theorem:

|- (! c. bin_add c [] [] = [c]) /\
  (! c x u. bin_add c (CONS x u) [] = CONS (c xor x) (bin_add (c /\ x) u [])) /\
  (! c y v. bin_add c [] (CONS y v) = CONS (c xor y) (bin_add (c /\ y) [] v)) /\
  (! c x u y v. bin_add c (CONS x u) (CONS y v) =
    CONS (sum c x y) (bin_add (carry c x y) u v))

The theorem relating bin_add to addition is:

|- ! u v c. bin_val (bin_add c u v) = bit_val c + bin_val u + bin_val v

and is valid for all wordlengths of u and v.

Once the theorem specifying the length of the output is added, the spec
is complete.

I prefer (bool)list to num->bool because lists have a length; one does
not need any "n" parameter for the binary adder, it adjusts itself
to the input wordlengths, and produces an output one bit longer than the
longer input. If the range of the output permits pruning of the
word, this can be performed and justified separately.

In sequential circuits, one has to worry about wordlength, since the
wordlength of an input to a circuit can depend on the wordlength of
the circuit's output. I don't think there is any elegant solution to
this problem; one has to specify the lengths of internal registers
somehow.

     Paul.