Exercise 11: The peANUt Logic Unit

This exercise deals with proving the the Logic Unit component from the CPU of a peANUt like machine. You will need to load in your definitions of the basic, combinatorial, gates like AND and OR before you start the exercises.

The Logic Unit is a piece of hardware with 2 n-bit wide inputs, which are the input data words, 2 single bit inputs, which select the logical operation to be performed, and a single n-bit wide output. The operations that can be performed are to take the bitwise AND, OR or XOR of the inputs, or simply to pass the first input through to the output unchanged. We will implement the Logic Unit using gates to perform all the operations, and a multiplexor to selected the desired output.

A Hardware Replication Construct

And another one's one, another one's one
Another one rides the bus
Weird Al Yankovic, `Another One Rides the Bus'

Implementing an n-bit Logic Unit requires the ability to make n copies of a hardware component. Rather than doing this by hand, ltes make a definition so that if P[n] is a predicate describing a hardware component, then the predicate

replicate n (\n. P[n])

describes describing n copies of the component, that is

P[0] /\ P[1] /\ ... P[n-1]

The following recursive definition will capture this meaning. Note, since the definitions uses numbers, you will have to load the library num before you can sucessfully enter the defintiion.

val replicate_DEF = new_recursive_definition
    {name="replicate_DEF",
     rec_axiom = prim_recTheory.num_Axiom,
     fixity = Prefix,
     def = Term `(replicate 0 P = T) /\  
                 (replicate (SUC n) P =
		  (P n) /\ (replicate n P))`};

Before HOL can accept such a definition it must be sure that it will maintain the consistency of the logic. The parameter prim_recTheory.num_Axiom captures the fact that this deifnition has that property. Examine this theorem before you go on.

An n-bit AND (and induction)

One of the operations to be performed by the Logical Unit is to perform an n-bit AND of its inputs. We can define the predicate nAND to describe this behaviour as follows:

val nAND_DEF = new_definition
    ("nAND_DEF",
     Term `nAND n a b c =
           (!m. m < n ==> AND (a m) (b m) (c m))`);

The usual implemenation for such a device would be to replicate n copies of an AND gade as follows:

An n-bit AND

Define an implementation for the n-bit wide AND operation using replicate and AND_IMP, and prove it correct with respect to the specification nAND.

Hints:

• Many proofs like this, about predicates that have been defined recursively, are best proved using induction. You must load induction suppot into HOL before you can use it. To do so, enter the following command:

  load "Num_induct";

  Once this is loaded, you will be able to use the tactic Num_induct.INDUCT_TAC to reduce a goal of the form !n:num. P[n] to two subgoals, one for the base case, and one for the step case.
• You will need to rewrite with some preproved theorems to complete this proof. In particular, check out the theorems NOT_LESS_0 and LESS_THM from the theory prim_rec. Have a look at these theorems before you go any further.
• Your basic strategy for the step case of this proof should be to transform the goal from a proof about nAND_IMP (SUC n) into one about AND_IMP and nAND_IMP n. To do this you will need to be able to rewrite with the definition of nAND_IMP in reverse. Check out the function GSYM to figure out how to do this.

n-Bit OR and XOR Gates

We will also need n-bit wide OR and XOR operations to build the peANUt Logic unit. Describing and proving these gates is a straight forward process of reworking your description and proof of the n-bit AND gate.

A 2-bit Multiplexer (and Constant Specification)

The Logic Unit performs four operations, and it will achieve this by implementing all four operations and selecting the correct output. We will need to implement a multiplexer component to perform this selection operation.

The job of the multiplexor will be to connect one of several n-bit wide inputs to an n-bit wide output. We could say that the n-bit wide data-path a is connected to the n-bit wide data-path b as follows:

!m. (m < n) ==> ((a m) = (b m))

Using your definition of nEQ, we can now give a concise specification for the multiplexor. The following code defines a multiplexer with two selection bits, enabling it to select one of four n-bit wide inputs.

val nMUX2_DEF = new_definition
    ("nMUX2_DEF",
     Term `
     nMUX2 n s1 s0 a b c d out =
     (~s0 /\ ~s1 ==> (nEQ n out a)) /\ 
     (~s0 /\  s1 ==> (nEQ n out b)) /\ 
     ( s0 /\ ~s1 ==> (nEQ n out c)) /\ 
     ( s0 /\  s1 ==> (nEQ n out d))`);

If we were to continue following the bottom-up pattern of development we have used up until now, our next step would be to describe and verify an implementation of this component, which we could then use to build an implementation for the Logic Unit. Lets take a different, top-down, approach with this component. Rather than defining an implementation for this component, let is just assert that such an implementation could be built, and go on to build and verify the Logic Unit using this hypothetical implementation. Later we can revise out development to replace this hypothetical implementation with a concrete one.

Until now, if we wanted to add a new constant to the HOL logic we have had to give a precise definition for it. However, we can introduce constants using a looser scheme by simply stating a property that we wish the new constant to have. In order to ensure that this extension preserves the soundness of the logic, we must first prove that there exists at least one value that has the specified property. In general, you can add several related constants at a time. This is done by first proving a theorem of the following form:

|- ?x₁ x₂ ... x_n. P[x₁, x₂, ... x_n]

|- P[K₁, K₂, ... K_n]

Using this technique we can add a constant called nMUX2_IMP to the logic together with a new axiom that states that it implements the specification nMUX2. This property must hold of any actual implementation of nMUX2. This means that later, when we replace this definition with one of a concrete implementation, no subsequent proofs will be effected.

Before we can add the constant nMUX2_IMP, we must first prove the following theorem:

|- ?X. !n s1 s0 a b c d out.
	  X n s1 s0 a b c d out ==>
	    nMUX2 n s1 s0 a b c d out

Hint: Use EXISTS_TAC.

Once the proof is complete, the following code will declare the constant:

val nMUX2_IMP_THM = new_specification
    {name="nMUX2_IMP_THM",
     sat_thm=nMUX2_IMP_EXISTS_THM,
     consts=
       [{const_name="nMUX2_IMP",fixity=Prefix}]};

The Logic Unit, At Last

You should now be able to define the specification of the logic unit. (Hint: Your specification should have the same structure as the specification of the multiplexer.) You should also now be able to define an implementation for the Logic Unit in terms of nAND_IMP, and the other n-bit logic operations you defined, and nMUX2_IMP.

The next challenge is to prove your implementation correct. The proof is likely to be tedious, but straight forward. The following hints are worth having:

• Avoid the temptation to rewrite with the specification of the Logic Unit too early. Once you do this, a (REPEAT STRIP_TAC) will result in several subgoals, and you might want to do some work in common to all these goals before they are separated out.
• Most tactics effect only the conclusion of a goal and not its assumptions. For this reason you will sometimes wish to move an assumption back into the conclusion in the form of an implication. That tactic UNDISCH_TAC can do this for you.