Assignment 2: Verification of an n-bit Adder

Important Information

The Problem

For your second assignment you will need to specify, design, and verify an n-bit adder circuit using the collection of gates you developed for the first assignment. The figure below depicts an n-bit adder.

n-bit adder
z + cout · 2n = x + y + cin

Step 1: A Simple Adder Circuit

Your solution will need to use a number of definitions and theorems about arithmetic. You should begin by loading the arith library to gain access to these definitions and theorems.

The first step to building an n-bit adder is to build a simple adder circuit capable of adding 1-bit quantities. Such an adder is depicted below.

n-bit adder
z + cout · 2 = x + y + cin

In describing the meaning of this circuit I have treated the wires as if they were numbers. In fact, we represent wires with booleans in HOL, so instead you might say I was taking the liberty of assuming the `obvious' interpretation of booleans to numbers, which maps false to 0 and true to 1. Unfortunately, HOL isn't very keen on people taking liberties with its logic - and just as well too - so before we begin, we will have to formalise this interpretation.

Define a HOL function BVAL: bool -> num, for `bit value', that maps false to 0 and true to 1.
Hint: Use the ternary conditional expression syntax `_=>_|_' to capture the desired meaning. This syntax is explained in the table at the start of exercise 4.

Having defined BVAL, you should now define a predicate ADDER such that ADDER x y cin z cout holds if the wires x, y, cin, z, and cout have the numeric relationship described in figure above.

Now for the hardest part of step 1, devise an implementation for this ADDER specification using the gates you verified for assignment 1. Formalise your implementation as the predicate ADDER_IMP, and then prove it correct.
Hint: You will get a long way here using the GEN_BOOL_CASES_TAC tactic you developed for exercise 8, rewriting with definitions, and the reduce library. (Refer to exercise 9 for how to use the reduce library.)

Step 2: Specifying the n-bit Adder

If my initial description of the simple adder took some logical liberties, then my description of the n-bit adder was downright rude. This description assumed an implicit translation from n wires in a bus (a function from numbers to booleans) to a number. The translation assumed is one where for some bus v (for `vector'), BVAL (v 0) is the least-significant bit in the binary representation of the number, BVAL (v 1) is the second-least-significant bit, and so on up to BVAL (v (n-1)), the most-significant bit in the number.

Define a function VVAL (for `vector value') such that VVAL n v is the value of the wires v 0 through v (n-1) interpreted as a binary number as described above.
Hint 1: You will need to make this a recursive definition, exercise 11 contains examples of how to make such definitions in HOL.
Hint 2: You will doubtless need to use exponentiation in your definition. In the HOL logic, 2ⁿ is expressed as 2 EXP n.

Using the function VVAL just developed, you should now be able to define the predicate nADDER to capture the meaning of an n-bit adder.

Step 3: Design your n-bit Adder

You should now design your implementation of an n-bit adder, and formalise your design as the HOL predicate nADDER_IMP.
Hint: Your design should essentially be n copies of the simple 1-bit adder implementation you verified earlier, all daisy-chained together. To represent this you will first need to define an auxiliary hardware replication function in HOL. You can find just such a function in exercise 11.

Step 4: A Crucial Lemma

The proof of correctness of the n-bit adder is a bit tricky. Things will go much more smoothly if you first prove the following lemma and bind it to the ML constant nADDER_IMP_LEMMA, so you can use it later in the main proof.

!n a b cin sum cout.
nADDER_IMP (SUC n) a b cin sum cout ==>
    ?x.
    ADDER_IMP (a n) (b n) x (sum n) cout /\ 
    nADDER_IMP n a b cin sum x`;

Hint: Be careful as you do this proof, avoid speculatively rewriting and stripping the goal. The best way to proceed is to look at the goal and think of how you would like to change it, and then choose a tactic to do just what you want. The final solution of the goal (at least in my proof) required some manipulation of the ordering of the existential (?) quantifiers and supplying a couple of well chosen witnesses for them (using EXISTS_TAC). There are a few conversions for manipulating the order of existential quantifiers in a term. I used RIGHT_AND_EXISTS_CONV and SWAP_EXISTS_CONV. To find more you should use the LAL HOL web pages to search for identifiers containing both `EXISTS' and `CONV' in the HOL reference manual. To apply these conversions to your goal you will need to use functions like CONV_TAC and DEPTH_CONV.

Step 5: Prove It

You should now have all the tools you need to prove the final goal, that your implementation of the n-bit adder implies your specification, so go a head and try it.

Hint 1: As with the previous goal, blindly rewriting, stripping and applying boolean case-analysis on this goal is going to take you to a very dark place, don't go there. The way to proceed to is carefully inspect the goal at each step, consider a small simplification to the goal, and choose a tactic to do it.
Hint 2: Start this proof by using INDUCT_TAC to induct over the size of the adder. (this involves loading in the appropriate code, see exercise 11 for an example of how to use INDUCT_TAC.)
Hint 3: The base case of your inductive proof should be straightforward, but the step case requires a deal of care. You will need to rearrange and eliminate arithmetic terms in the goal quite precisely. For this you will need to exploit the properties of commutativity, associativity and distributivity of addition and multiplication. All the theorems you will need about these properties are available in the arithmetic theory. You can see all the theorems available from this theory by searching for the keyword `arithmetic' in the HOL Theorem Manual on the LAL HOL web pages. Look for theorems with the strings `SYM', `ASSOC' and `DISTRIB' in their names. (You must select the Theorem Manual from the menu otherwise you will search the Reference Manual and not find anything.)
Hint 4: Remember, if you find a equation you would like to use, but you want to rewrite with it from right to left, rather than from left to right, then you can reverse the order of the equation with the function GSYM.
Hint 5: I found the theorem EQ_MONO_ADD_EQ from the arithmetic theory to be useful in my proof.

What to Submit

You should prepare your solution as well commented program, and submit it by mailing it to me.