README
1% ===================================================================== %
2% TAMARACK 2 - Register-Transfer Level Implementation %
3
4Jeff Joyce, Cambridge University, 14 June 1989
5Thomas Tuerk, Ramana Kumar, port to modern HOL, 22 April 2018
6
7This directory contains the HOL sources for the formal specification and
8verification of a very simple microprocessor called "Tamarack-2". The
9file "writeup.tex" is the latex source for an introductory discussion
10on hardware verification based on the HOL sources in this directory
11(there are some minor differences in the write-up from the proofs).
12
13Tamarack-2 is a simplified version of the original version of Tamarack
14where the "idle cycle" aspect of the design has been eliminated. The
15instruction set is also slightly different: The HALT instruction from
16the old version of Tamarack is gone leaving a NOP instruction in its
17place (there are now two opcodes for a NOP operation). Different opcodes
18have been assigned to instructions than those used in Tamarack-1.
19
20These source were orignally written for an older version of HOL - some
21bits have been added to the start of most sources in this directory to
22make them compatible with HOL88 (all very simple things like turning on
23"sticky types" and stripping quantifiers off definitions).
24
25Otherwise, the sources in this directory are still in the state I left
26them in when I first did this example ... I still need to do alot of
27clean-up. Some things like the theory "wop" are no longer needed since
28they are built into HOL88. There is also a MOD function defined in HOL88
29but for the time being I have just kept my own theory of modular arithmetic
30so that I don't have to make changes to all the sources to use whatever
31theorems about MOD are now built into HOL88.
32
33In April 2018 this example was ported further to HOL 4. The original
34developments of arithmetic theories especially developments about DIV and
35MOD were not ported.
36