Via:  uk.ac.nsf; 28 May 89 15:17 BST  (UK.AC.Cam.Cl.scaup)
Date: Sun, 28 May 89 14:40:57 BST
From: Jeffrey Joyce <jjj%uk.ac.cam.cl@uk.ac.nsf>
To: info-hol <info-hol%edu.ucdavis.clover@uk.ac.nsf>
Subject: n-bit words in HOL
Message-Id:  <8905281444.aa07331@scaup.Cl.Cam.AC.UK>
Sender: jjj <jjj%uk.ac.cam.cl%uk.ac.nsf@edu.ucdavis.clover>
Status: R

Representing n-bit words in HOL
===============================

Tom's proposal for an n-bit word theory to replace the postulated
wordn types would be a useful addition to HOL88 especially for the
register-transfer level upwards.  However, I have some concerns
about the suggestion not to provide 0-bit words.

I think it would be a mistake not to provide 0-bit words.  It's true
that you can't purchase off-the-shelf "0-bit adders", etc., but the
ability to parameterized specifications by word width, where n = 0 is
allowed, tends to result in lucid, succinct specifications and proofs of
correctness.

For example, compare the n-bit ripple-carry adder proofs in Cambridge
tech. reports. TR77 [1] and TR91 [2].  In the case of TR77, where 0-bit
adders are NOT allowed, you end up with the slightly confusing situation
where ...

        "... the parameter n determines an adder operating on
        words of size n+1 ("n+1" because n counts from 0; e.g.,
        if n is 0 we get a 1-bit adder)."  (TR 77, p 14)

The proof in TR77 is also slightly more work than Camilleri's version in
TR91.  Both use mathematical induction, but differ in the basis step of the
induction.  In TR77, the basis of the induction is a 1-bit adder (where
you actually have to do a little work).  In TR91, the basis is a 0-bit
adder (which is absolutely trivial and requires no effort).  In the
former situation, you effectively do a separate proof of correctness
for the 1-bit adder apart from all other sizes n, n > 1.  The latter
situation is better because all the work is done in the induction step.

Of course, these observations have to do with mathematical induction
and primitive recursion on the natural numbers which require the
n = 0 case to be considered in one way or another.  The proposed
n-bit word theory would have facilities for inductive proofs and
recursive definitions on the n-bit words directly.  However,
if 0-bit words are not allowed, you still carry over the old problem
of having to deal the 1-bit case separately instead of a nice-and-clean
treatment of all non-zero size adders in the induction step.

The case of a ripple-carry adder with extra circuitry for under/overflow
for integer addition may be problematic for the case n = 0, but in my
own experience, "phoney circuitry" is not generally needed to implement
the 0-bit version of a device ... where I take "phoney circuitry" to
mean extra components.  The 0-bit case is usually a matter of specifying
a very simple relation betweens inputs and outputs.  For instance, the
Boolean output of a 0-bit parallel OR-gate is "F".  For a 0-bit adder,
the carry-in signal is logically identical to the carry-out signal.
In otherwords, the implementation of an n-bit device, for n > 1, can
be seen as the extension of an idealised 0-bit device.

The last reason is a philosophical one.  I think that the use of
formal methods to verify hardware should be doing a little more than
using logic to imitate conventional engineering practice:  we should be
looking for a mathematical theory to support what we are doing at the
engineering level.  An example of what I mean here is understanding what
the 0-bit version of a device does and viewing physical realizations of
this device as an extension of the 0-bit device.

As matter of interest, the wordn types are not essential for reasoning
about n-bit devices.  Both of the technical reports mentioned above,
TR77 and TR91, do not use the built-in wordn types of the HOL system.
Instead, n-bit words are represented by functions mapping bit positions
to bit values.  For example, the 3-bit word #011 is represented by the
function f, such that f(0) = T, f(1) = T, f(2) = F and for n > 2, f(n)
is a fixed, but unknown Boolean value.   I have used this representation
for several years for microprocessor verification and have developed a
theory which includes the functions "Valn" and "Wordn" (which convert
between natural numbers and n-bit words); parts of this theory are
described in [3] and [4].

The main reasons for switching over to this representation were to avoid
the logical gaps due to the built-in postulated word type and to be able
to reason about specifications parametized by word width.  The single
disadvantage of this representation is that mis-matched word widths
in a specification (e.g., using a 3-bit bus as input to a 4-bit adder)
are not automatically detected by the type-checker.  I think that this
is a serious disadvantage because anything that helps get a specification
right because starting to prove theorems is valuable.  Certainly such
mis-matches in word size would be detected automatically by type-checking
with the fixed-width word types, but I don't know if the variable width
word types (section 1 and 2 of Tom's proposal) would allow mis-matches
to be detected automatically by type checking.  If this was possible,
then the variable word-widths would be "the best of both worlds",
i.e., the flexibility of variable word width and the power of type-checked
fixed width words.

[1] M. Gordon, "Why Higher-Order Logic is a Good Formalism for Specifying
    and Verifying Hardware", Technical Report no. 77, Computer Laboratory,
    Cambridge University, September 1985.  Also in: G. Milne and P.
    Subrahmanyam, eds., Formal Aspects of VLSI Design, North-Holland, 1986.

[2] A. Camilleri, M. Gordon and T. Melham, "Hardware Verification Using
    Higher Order Logic", Techical Report no. 91, Computer Laboratory,
    Cambridge University, June 1986.  Also in: D. Borrione, ed., From HDL
    Descriptions to Guaranteed Correct Circuit Designs, North-Holland, 1987.

[3] J. Joyce, Hardware Verification of VLSI Regular Structures, Technical
    Report no. 109, Computer Laboratory, Cambridge University, July 1987.

[4] J. Joyce, Generic Structures in the Formal Specification and
    Verification of Digital Circuits, in: G. Milne, ed.,  The Fusion of
    Hardware Design and Verification, North-Holland, 1988.