NameDateSize

..25-Jul-201935

arith.mlH A D25-Jul-20198.1 KiB

da.mlH A D25-Jul-20192.2 KiB

div.mlH A D25-Jul-20194.3 KiB

flowgraph.texH A D25-Jul-20195.6 KiB

MakeProofH A D25-Jul-2019426

mod.mlH A D25-Jul-20196.8 KiB

proof1.mlH A D25-Jul-201910.7 KiB

proof2.mlH A D25-Jul-20199.4 KiB

proof3.mlH A D25-Jul-20195.6 KiB

READMEH A D25-Jul-20191.7 KiB

tamarack.mlH A D25-Jul-20198.2 KiB

wop.mlH A D25-Jul-20191.4 KiB

writeup.texH A D25-Jul-2019122.5 KiB

README

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