Exercise 5: Formalising CMOS in HOL

A New Theory for CMOS

Before we can make any new definitions in HOL, we must first give a name to the new theory that will result from extending the HOL logic with those definitions. The command to do so is new_theory, which takes a string argument naming the new theory. In these exercises we will be creating a theory of CMOS logic gates.

To begin the exercises, enter the following command:

new_theory "CMOS";

Basic CMOS Circuit Elements

We will model the wires in a CMOS circuit with boolean variables. The value T will correspond to a high voltage, and the value F to a low voltage. The atomic components of CMOS circuits are power, ground, n-type transistors and p-type transistors, which are represented graphically as follows:

power	ground	n-type	p-type

One simple operation in designing a circuit is to tie a wire to either power or ground. We will represent the fact that some wire a has been tied to either power or ground with the predicates PWR a and GND a respectively. We must now define those predicates to give them the meaning we intended. To do this, issue the following commands to HOL:

 
val PWR_DEF = new_definition ("PWR_DEF", Term `PWR a = (a = T)`);
val GND_DEF = new_definition ("GND_DEF", Term `GND a = (a = F)`);

The command to make a new definition in HOL is called new_definition, and it takes a pair of parameters. The first parameter is a string that gives the name under which the definition is stored in the theory. Theories can be saved, and loaded again in subsequent HOL sessions, and particular definitions retrieved from them by name. The second parameter is a term that describes the definition. Essentially this term must have the following form:

name = closed-expression

name x₁... x_n = expression[x₁... x_n]

name = \x₁... x_n. expression[x₁... x_n]

The new_definition creates a new axiom that captures the definition, and returns it. In the example just given we bound those axioms to the ML names PWR_DEF and GND_DEF for easy access later.

Let us now consider the operation of the transistors. Both kinds transistor join together tree wires called the gate, source and drain. Both kinds of transistors function like a switch. When a high voltage is applied to the gate of an n-type transistor, the source and drain wires are connected, and current is allowed to flow between them. When a low voltage is applied to the gate of an n-type transistor, then the source and drain wires are disconnected. A p-type transistor is exactly the opposite kind of switch. When a low voltage is applied to the gate of a p-type transistor, then the source and drain wires are connected; and when a high-voltage is applied to the gate they are disconnected. Note that the terms `source' and `drain' are misleading since they tend to imply that current flows from the source to the drain. In fact, current can flow in either direction.

We can use the following definitions to describe the behaviour of n-type and p-type transistors.

Enter the following definition to HOL to describe the operation of an n-type transistor, then construct and enter your own definition to describe the operation of a p-type transistor.

 
val NTRAN_DEF = new_definition
    ("NTRAN_DEF", Term `NTRAN g (a:bool) b = (g ==> (a = b))`);

Constructing a Not-Gate in CMOS

Using CMOS transistors it is relatively easy to construct logic gates that implement the functions NOT, NAND and NOR. These are the basic gates of CMOS logic. All logic circuits are then constructed in terms of these gates.

A NOT gate joins together two wires such that if the input wire is low then the output wire is high, and visa-versa. We can capture this description of a NOT gate in HOL as follows:

val NOT_DEF = new_definition
    ("NOT_DEF", Term `NOT a b = (b = ~a)`);

A CMOS Not-Gate

By labelling the internal and external wires of the circuit, as in the diagram, it can be translated fairly directly into the HOL logic as follows.

val NOT_IMP_DEF =
    new_definition("NOT_IMP_DEF",
		   Term `
		   NOT_IMP a b =
		   ?x y. PWR x /\ 
		   GND y /\ 
		   PTRAN a x b /\ 
		   NTRAN a y b`);

Our goal is to prove that the CMOS implementation of the NOT circuit meets its specification. That is, we wish to prove the following:

!a b. NOT_IMP a b ==> NOT a b