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