Assignment 1: Verification of Basic Combinatorial Circuit Components

Important Information

The Problem

For your second assignment you will want to draw upon a stock of simple, verified, circuit components. Your task for this assignment is to develop that stock. Using the HOL theorem prover you should make definitions to model the operation of the basic CMOS components shown below.

power	ground	n-type	p-type

It is easier to think about building circuits using logic-gates than these more primitive CMOS components. Furthermore, it is easier to fabricate circuits that are built entirely from the one kind of gate. A nand gate (shown below) is logically complete, which means that all other logic gates can be fabricated from it.

nand
	x	y	z = NAND x y
	0	0	1
	0	1	1
	1	0	1
	1	1	0

Use HOL to define the desired behaviour of a nand gate, then describe an implementation of the nand gate in terms of the basic CMOS components, and verify your implementation.

We also want verified implementations of other common gates.

and
	x	y	AND x y
	0	0	0
	0	1	0
	1	0	0
	1	1	1

or
	x	y	z = OR x y
	0	0	0
	0	1	1
	1	0	1
	1	1	1

nor
	x	y	z = NOR x y
	0	0	1
	0	1	0
	1	0	0
	1	1	0

xor
	x	y	z = XOR x y
	0	0	0
	0	1	1
	1	0	1
	1	1	0

not
	x	y = NOT x
	0	1
	0	0

Define the desired behaviour of each of these logic gates then HOL. Next, using only your CMOS implementation of the nand gate - and connections to power and ground - describe and verify implementations of these other logic gates.

Restrictions

You must construct your proofs without using any libraries of automatic proof procedures, like the Meson library. You may, of course, use these libraries when developing your implementations, but your final proofs must be performed without them.

What to Submit

You should prepare your solution as an ML program that defines the following things:

PWR_DEF

A specification of connection to power.

GND_DEF

A specification of connection to ground.

NTRAN_DEF

A specification of an n-type transistor.

PTRAN_DEF

A specification of a p-type transistor.

NAND_DEF

A specification of a nand gate

NAND_IMP_DEF

An implementation of a nand gate in CMOS.

NAND_IMP_THM

A theorem stating the correctness of your nand gate implementation.

AND_DEF

A specification of an and gate

AND_IMP_DEF

An implementation of an and gate using only your nand gate implementation and connections to power and ground.

AND_IMP_THM

A theorem stating the correctness of your and gate implementation.

You program should also bind identifiers to specifications, implementations, and correctness theorems for or gates, nor gates, xor gates and not gates. Your implementations for these gates should use only connections to power and ground, nand gates, or other gates your have already implemented using nand gates.

Your program should be commented to explain the role of any tactics your define and the general proof strategies you use.

Submit your solution by mailing it to me.