1%  MICROCODED COMPUTER PROOF : HOL                                      %
2%                                                                       %
3%  'computer.ml'                                                        %
4%                                                                       %
5%  Description                                                          % 
6%                                                                       %
7%     This theory is the target level specification of the computer.    %
8%  The definition of EXECUTE evaluates to the next state of the         %
9%  computer which results from the execution of a single target level   %
10%  instruction.  COMPUTER is an overall specification of the computer   %
11%  including its behaviour when it is idling as well as when it is      %
12%  running.  COMPUTER expresses the intended behaviour of the computer  %
13%  from a register-transfer point of view.  It is used in the first     %
14%  part of the verification procedure.  The final version of the        %
15%  correctness statement uses the specification given by COMPUTER_abs.  %
16%  COMPUTER_abs expresses the intended behaviour of the computer from   %
17%  target level point of view.                                          %
18%                                                                       %
19%  Author:  Jeff Joyce                                                  %
20%  Date:    July 26, 1985                                               %
21
22new_theory `computer`;;
23
24new_parent `values`;;
25
26%  'memory_val', 'pc_val', 'acc_val' are values of signals at           %
27%  a single point in time.                                              %
28%                                                                       %
29%       memory_val  : mem13_16                                          %
30%       pc_val      : word13                                            %
31%       acc_val     : word16                                            %
32
33new_definition
34(
35 `EXECUTE`,
36  "EXECUTE (memory_val,pc_val,acc_val) =
37   let op   = VAL3(OPCODE(FETCH13 memory_val pc_val)) in
38   let addr = CUT16_13(FETCH13 memory_val pc_val)     in
39   ((op=0) =>
40     (memory_val, pc_val, acc_val, T) |
41    (op=1) =>
42     (memory_val, addr, acc_val, F) |
43    (op=2) =>
44     ((VAL16 acc_val = 0) =>
45      (memory_val, addr, acc_val, F) |
46      (memory_val, INC13 pc_val, acc_val, F)) |
47    (op=3) =>
48     (memory_val, INC13 pc_val, ADD16 acc_val (FETCH13 memory_val addr), F) |
49    (op=4) =>
50     (memory_val, INC13 pc_val, SUB16 acc_val (FETCH13 memory_val addr), F) |
51    (op=5) =>
52     (memory_val, INC13 pc_val, FETCH13 memory_val addr, F) |
53    (op=6) =>
54     (STORE13 addr acc_val memory_val, INC13 pc_val, acc_val, F) |
55     (memory_val, INC13 pc_val, acc_val, F))"
56);;
57
58%  'memory', 'knob', 'button', 'switches', 'pc', 'acc', and 'idle' are  %
59%  signals which map points in time to values.                          %
60%                                                                       %
61%       memory    : num->mem13_16                                       %
62%       knob      : num->word2                                          %
63%       button    : num->bool                                           %
64%       switches  : num->word16                                         %
65%       pc        : num->word13                                         %
66%       acc       : num->word16                                         %
67%       idle      : num->bool                                           %
68
69new_definition
70(
71  `COMPUTER`,
72  "COMPUTER
73    (t1:num,t2:num)
74    (memory,knob,button,switches,pc,acc,idle) =
75   (memory t2,pc t2,acc t2,idle t2) =
76    (idle t1 => 
77     (button t1 => 
78      ((VAL2(knob t1) = 0) =>
79        (memory t1, CUT16_13(switches t1), acc t1, T) |
80       (VAL2(knob t1) = 1) =>
81        (memory t1, pc t1, switches t1, T) |
82       (VAL2(knob t1) = 2) =>
83        (STORE13(pc t1)(acc t1)(memory t1), pc t1, acc t1, T) |
84        (memory t1, pc t1, acc t1, F)) |
85      (memory t1, pc t1, acc t1, T)) |
86     (button t1 =>
87      (memory t1, pc t1, acc t1, T) |
88      EXECUTE(memory t1, pc t1, acc t1)))"
89);;
90
91let COMPUTER_abs = new_definition
92(
93 `COMPUTER_abs`,
94  "COMPUTER_abs
95    (memory_abs,knob_abs,button_abs,switches_abs,pc_abs,acc_abs,idle_abs) =
96   !t:num.
97    (memory_abs (t+1),pc_abs (t+1),acc_abs (t+1),idle_abs (t+1)) =
98     (idle_abs t => 
99      (button_abs t => 
100       ((VAL2(knob_abs t) = 0) =>
101         (memory_abs t, CUT16_13(switches_abs t), acc_abs t, T) |
102        (VAL2(knob_abs t) = 1) =>
103         (memory_abs t, pc_abs t, switches_abs t, T) |
104        (VAL2(knob_abs t) = 2) =>
105         (STORE13(pc_abs t)(acc_abs t)(memory_abs t), pc_abs t, acc_abs t, T) |
106         (memory_abs t, pc_abs t, acc_abs t, F)) |
107       (memory_abs t, pc_abs t, acc_abs t, T)) |
108      (button_abs t =>
109       (memory_abs t, pc_abs t, acc_abs t, T) |
110       EXECUTE(memory_abs t, pc_abs t, acc_abs t)))"
111);;
112
113close_theory ();;
114