CSE482/CIS582: Project
Goal of the project
You will design a simple n-bit ALU and verify its correctness
in the PVS verification system.
Administrivia
- What to submit: The file "your.name-cse482-project.pvs" containing
the design and the file "your.name-cse482-project.prf"
containing the proofs.
- When: Tuesday, November 29th, 2005.
- How: Email the files to Pavol Cerny.
PVS
PVS is a verification system: that is, a specification language integrated
with support tools and a theorem prover.
You can get the system as well as the documentation and various tutorials
from the PVS homepage.
PVS is installed on Eniac. You can run it by typing
~cse482/pvs/pvs.
A tutorial on PVS will be given in class on Tuesday, November 15th.
Slides 10-101 (except for the part on arithmetic (82-93))
from a
tutorial by Dr. N. Shankar will be used.
Tasks
You will construct a simple n-bit ALU. It will perform only one arithmetic
operation (addition) and one logic operation (bitwise and).
The basic building blocks we will use in this project are the
p-transistor and the n-transistor.
The definitions of the p-transistor and the n-transistor are provided,
as well as the implementation of the NOT and NAND gates
together with the proofs of their correctness.
Your tasks will be:
- Implement NOR gate using the p-transistor and n-transistor
and prove the correctness of your implementation
using the propositional simplification (e.g.: rule
bddsimp, ground),
quantifier rules (e.g.:
inst, skosimp)
and the rule expand
to expand the definitions.
- Prove the correctness of the (simple) implementation
of the OR, AND, XOR gates and of the multiplexer.
The implementation is provided.
- Implement 1-bit ALU using the OR, AND, XOR gates
and prove the correctness of your implementation.
- Implement n-bit ALU using the 1-bit ALU
and prove its correctness by induction.
Download
- PVS file containing initial definitions.
- PVS proof file
containing proofs of correctness for the NOT and NAND gates.
Background
- For a good review of how to build combinational circuits,
see the following lecture notes by Charles C. Lin:
- For basic information on transistors and on building logic gates,
you can read this Wikipedia article.