1% MICROCODED COMPUTER PROOF : HOL % 2% % 3% 'proof2.ml' % 4% % 5% Description % 6% % 7% This theory results in a theorem about each of the fifteen % 8% possible execution cycles. There are five possible cycles for % 9% the idling case, four when the button is pressed depending on the % 10% value of knob, and one possible cycle when the button is not % 11% pressed. The remaining ten possible execution cycles are cases % 12% of when the computer is running. There is one possible execution % 13% cycle for each of the eight opcode except for the conditional jump % 14% for which there are two possible execution cycles depending on % 15% whether the accumulator is zero or non-zero. Finally, there is % 16% is the execution cycle which results when the machine is running % 17% and the button is pressed. The idling case is mpc t1 = #00000" % 18% and the running case is "mpc t1 = #00101". % 19% The theorems are derived for each case by simulating the exec- % 20% ution cycle. Instead of data, the 'values' are assertions about % 21% data in terms of the state at the start of the execution cycle. % 22% This is the major step in the proof. The rest of the proof is % 23% mostly 'stitching' together results of this step. % 24% % 25% Author: Jeff Joyce % 26% Date: August 4, 1985 % 27 28new_theory `proof2`;; 29 30new_parent `proof1`;; 31 32let CUT_PAD = axiom `values` `CUT_PAD`;; 33let CUT_INC_PAD = axiom `values` `CUT_INC_PAD`;; 34 35let arith_lemmas = 36 [ 37 (theorem `arith` `plus_0_2`); 38 (theorem `arith` `plus_1_2`); 39 (theorem `arith` `plus_2_2`); 40 (theorem `arith` `plus_3_2`); 41 (theorem `arith` `plus_0_10`); 42 (theorem `arith` `plus_1_10`); 43 (theorem `arith` `plus_2_10`); 44 (theorem `arith` `plus_3_10`); 45 (theorem `arith` `plus_4_10`); 46 (theorem `arith` `plus_5_10`); 47 (theorem `arith` `plus_6_10`); 48 (theorem `arith` `plus_7_10`) 49 ];; 50 51let microcode = 52[ 53 WORD_RULE (axiom `microcode` `MICROCODE0`); 54 WORD_RULE (axiom `microcode` `MICROCODE1`); 55 WORD_RULE (axiom `microcode` `MICROCODE2`); 56 WORD_RULE (axiom `microcode` `MICROCODE3`); 57 WORD_RULE (axiom `microcode` `MICROCODE4`); 58 WORD_RULE (axiom `microcode` `MICROCODE5`); 59 WORD_RULE (axiom `microcode` `MICROCODE6`); 60 WORD_RULE (axiom `microcode` `MICROCODE7`); 61 WORD_RULE (axiom `microcode` `MICROCODE8`); 62 WORD_RULE (axiom `microcode` `MICROCODE9`); 63 WORD_RULE (axiom `microcode` `MICROCODE10`); 64 WORD_RULE (axiom `microcode` `MICROCODE11`); 65 WORD_RULE (axiom `microcode` `MICROCODE12`); 66 WORD_RULE (axiom `microcode` `MICROCODE13`); 67 WORD_RULE (axiom `microcode` `MICROCODE14`); 68 WORD_RULE (axiom `microcode` `MICROCODE15`); 69 WORD_RULE (axiom `microcode` `MICROCODE16`); 70 WORD_RULE (axiom `microcode` `MICROCODE17`); 71 WORD_RULE (axiom `microcode` `MICROCODE18`); 72 WORD_RULE (axiom `microcode` `MICROCODE19`); 73 WORD_RULE (axiom `microcode` `MICROCODE20`); 74 WORD_RULE (axiom `microcode` `MICROCODE21`); 75 WORD_RULE (axiom `microcode` `MICROCODE22`); 76 WORD_RULE (axiom `microcode` `MICROCODE23`); 77 WORD_RULE (axiom `microcode` `MICROCODE24`); 78 WORD_RULE (axiom `microcode` `MICROCODE25`) 79];; 80 81let COMPUTER_IMP_EXP_ASM = theorem `computer_imp` `COMPUTER_IMP_EXP_ASM`;; 82 83letrec nth_CONJUNCT n thm = 84 if n = 0 then thm else (nth_CONJUNCT (n - 1) (CONJUNCT2 thm));; 85 86let COMPUTER_IMP_buf = CONJUNCT1 (nth_CONJUNCT 0 COMPUTER_IMP_EXP_ASM);; 87let COMPUTER_IMP_m = CONJUNCT1 (nth_CONJUNCT 1 COMPUTER_IMP_EXP_ASM);; 88let COMPUTER_IMP_mar = CONJUNCT1 (nth_CONJUNCT 2 COMPUTER_IMP_EXP_ASM);; 89let COMPUTER_IMP_pc = CONJUNCT1 (nth_CONJUNCT 3 COMPUTER_IMP_EXP_ASM);; 90let COMPUTER_IMP_acc = CONJUNCT1 (nth_CONJUNCT 4 COMPUTER_IMP_EXP_ASM);; 91let COMPUTER_IMP_ir = CONJUNCT1 (nth_CONJUNCT 5 COMPUTER_IMP_EXP_ASM);; 92let COMPUTER_IMP_arg = CONJUNCT1 (nth_CONJUNCT 6 COMPUTER_IMP_EXP_ASM);; 93let COMPUTER_IMP_mpc = CONJUNCT1 (nth_CONJUNCT 7 COMPUTER_IMP_EXP_ASM);; 94let COMPUTER_IMP_ready = CONJUNCT1 (nth_CONJUNCT 8 COMPUTER_IMP_EXP_ASM);; 95let COMPUTER_IMP_idle = CONJUNCT2 (nth_CONJUNCT 8 COMPUTER_IMP_EXP_ASM);; 96 97letrec tm n = if n = 0 then "t1:num" else "(^(tm (n - 1))) + 1";; 98 99let arith_rule thm = WORD_RULE (SUBS arith_lemmas thm);; 100 101let evaluate_rule = 102 BITS_RULE thenf 103 EL_RULE thenf 104 COND_RULE thenf 105 SEG_RULE thenf 106 V_RULE thenf 107 WORD_RULE thenf 108 VAL_RULE thenf 109 EQ_RULE thenf 110 COND_RULE thenf 111 U_RULE thenf 112 TRI_RULE thenf 113 bool_RULE thenf 114 COND_RULE;; 115 116let reduce_rule assumptions thm = 117 REWRITE_RULE [CUT_PAD;CUT_INC_PAD] 118 (arith_rule 119 (SUBS assumptions 120 (evaluate_rule 121 (SUBS microcode 122 (SUBS assumptions thm)))));; 123 124let first_state assumptions = 125 ( 126 (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_buf)), 127 (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_m)), 128 (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_mar)), 129 (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_pc)), 130 (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_acc)), 131 (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_ir)), 132 (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_arg)), 133 (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_mpc)), 134 (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_ready)) 135 );; 136 137% The state at time t1 + i is obtained by specifying COMPUTER_IMP_buf, % 138% COMPUTER_IMP_m, ..., COMPUTER_IMP_ready for the term (tm (i - 1)) and % 139% 'reducing' these assertions. Reduction involves substitution with % 140% assertions about the state at time t1 + (i - 1) as well as substi- % 141% tution with the microcode and assumptions for the the particular % 142% case followed by an evaluation. The evalution uses BITS_RULE, % 143% EL_RULE, WORD_RULE, etc. (see 'evaluate_rule'). % 144 145letrec iterate_state 146 i n assumptions (buf,m,mar,pc,acc,ir,arg,mpc,ready) = 147 if i > n 148 then (buf,m,mar,pc,acc,ir,arg,mpc,ready) 149 else 150 let update_rule thm = 151 (reduce_rule 152 ([buf;m;mar;pc;acc;ir;arg;mpc] @ assumptions) 153 (SPEC (tm (i - 1)) thm) 154 ) in 155 iterate_state 156 (i + 1) 157 n 158 assumptions 159 ( 160 (update_rule COMPUTER_IMP_buf), 161 (update_rule COMPUTER_IMP_m), 162 (update_rule COMPUTER_IMP_mar), 163 (update_rule COMPUTER_IMP_pc), 164 (update_rule COMPUTER_IMP_acc), 165 (update_rule COMPUTER_IMP_ir), 166 (update_rule COMPUTER_IMP_arg), 167 (update_rule COMPUTER_IMP_mpc), 168 (LIST_CONJ [(update_rule COMPUTER_IMP_ready);ready]) 169 );; 170 171let simulate ncycles assumptions = 172 let (buf,m,mar,pc,acc,ir,arg,mpc,readylist) = 173 iterate_state 2 ncycles assumptions (first_state assumptions) in 174 let idle = reduce_rule [mpc] (SPEC (tm ncycles) COMPUTER_IMP_idle) in 175 let ready = reduce_rule [mpc] (SPEC (tm ncycles) COMPUTER_IMP_ready) in 176 LIST_CONJ [m;pc;acc;idle;ready;readylist];; 177 178% ===================================================================== % 179% Case: mpc = 0, button = T, knob = 0 ================================= % 180 181let assumptions = 182[ 183 ASSUME "(mpc (t1:num)) = #00000"; 184 ASSUME "(button (t1:num)) = T"; 185 ASSUME "(VAL2 (knob ((t1:num) + 1))) = 0" 186];; 187 188let COMPUTER_IMP_mpc_0_button_T_knob_0 = 189 save_thm (`COMPUTER_IMP_mpc_0_button_T_knob_0`,(simulate 3 assumptions));; 190 191% ===================================================================== % 192% Case: mpc = 0, button = T, knob = 1 ================================= % 193 194let assumptions = 195[ 196 ASSUME "(mpc (t1:num)) = #00000"; 197 ASSUME "(button (t1:num)) = T"; 198 ASSUME "(VAL2 (knob ((t1:num) + 1))) = 1" 199];; 200 201let COMPUTER_IMP_mpc_0_button_T_knob_1 = 202 save_thm (`COMPUTER_IMP_mpc_0_button_T_knob_1`,(simulate 3 assumptions));; 203 204% ===================================================================== % 205% Case: mpc = 0, button = T, knob = 2 ================================= % 206 207let assumptions = 208[ 209 ASSUME "(mpc (t1:num)) = #00000"; 210 ASSUME "(button (t1:num)) = T"; 211 ASSUME "(VAL2 (knob ((t1:num) + 1))) = 2" 212];; 213 214let COMPUTER_IMP_mpc_0_button_T_knob_2 = 215 save_thm (`COMPUTER_IMP_mpc_0_button_T_knob_2`,(simulate 4 assumptions));; 216 217% ===================================================================== % 218% Case: mpc = 0, button = T, knob = 3 ================================= % 219 220let assumptions = 221[ 222 ASSUME "(mpc (t1:num)) = #00000"; 223 ASSUME "(button (t1:num)) = T"; 224 ASSUME "(VAL2 (knob ((t1:num) + 1))) = 3" 225];; 226 227let COMPUTER_IMP_mpc_0_button_T_knob_3 = 228 save_thm (`COMPUTER_IMP_mpc_0_button_T_knob_3`,(simulate 2 assumptions));; 229 230% ===================================================================== % 231% Case: mpc = 0, button = F =========================================== % 232 233let assumptions = 234[ 235 ASSUME "(mpc (t1:num)) = #00000"; 236 ASSUME "(button (t1:num)) = F"; 237];; 238 239let COMPUTER_IMP_mpc_0_button_F = 240 save_thm (`COMPUTER_IMP_mpc_0_button_F`,(simulate 1 assumptions));; 241 242% ===================================================================== % 243% Case: mpc = 5, button = T =========================================== % 244 245let assumptions = 246[ 247 ASSUME "(mpc (t1:num)) = #00101"; 248 ASSUME "(button (t1:num)) = T"; 249];; 250 251let COMPUTER_IMP_mpc_5_button_T = 252 save_thm (`COMPUTER_IMP_mpc_5_button_T`,(simulate 1 assumptions));; 253 254% ===================================================================== % 255% Case: mpc = 5, button = F, opcode is 0 (HALT) ======================= % 256 257let assumptions = 258[ 259 ASSUME "(mpc (t1:num)) = #00101"; 260 ASSUME "(button (t1:num)) = F"; 261 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 0" 262];; 263 264let COMPUTER_IMP_mpc_5_button_F_opcode_0 = 265 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_0`,(simulate 5 assumptions));; 266 267% ===================================================================== % 268% Case: mpc = 5, button = F, opcode is 1 (JMP) ======================== % 269 270let assumptions = 271[ 272 ASSUME "(mpc (t1:num)) = #00101"; 273 ASSUME "(button (t1:num)) = F"; 274 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 1" 275];; 276 277let COMPUTER_IMP_mpc_5_button_F_opcode_1 = 278 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_1`,(simulate 5 assumptions));; 279 280% ===================================================================== % 281% Case: mpc = 5, button = F, zero, opcode is 2 (JZR) ================== % 282 283let assumptions = 284[ 285 ASSUME "(mpc (t1:num)) = #00101"; 286 ASSUME "(button (t1:num)) = F"; 287 ASSUME "((VAL16(acc (t1:num))) = 0) = T"; 288 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 2" 289];; 290 291let COMPUTER_IMP_mpc_5_button_F_zero_opcode_2 = 292 save_thm (`COMPUTER_IMP_mpc_5_button_F_zero_opcode_2`,(simulate 6 assumptions));; 293 294% ===================================================================== % 295% Case: mpc = 5, button = F, nonzero, opcode is 2 (JZR) =============== % 296 297let assumptions = 298[ 299 ASSUME "(mpc (t1:num)) = #00101"; 300 ASSUME "(button (t1:num)) = F"; 301 ASSUME "((VAL16(acc (t1:num))) = 0) = F"; 302 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 2" 303];; 304 305let COMPUTER_IMP_mpc_5_button_F_nonzero_opcode_2 = 306 save_thm (`COMPUTER_IMP_mpc_5_button_F_nonzero_opcode_2`,(simulate 7 assumptions));; 307 308% ===================================================================== % 309% Case: mpc = 5, button = F, opcode is 3 (ADD) ======================== % 310 311let assumptions = 312[ 313 ASSUME "(mpc (t1:num)) = #00101"; 314 ASSUME "(button (t1:num)) = F"; 315 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 3" 316];; 317 318let COMPUTER_IMP_mpc_5_button_F_opcode_3 = 319 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_3`,(simulate 10 assumptions));; 320 321% ===================================================================== % 322% Case: mpc = 5, button = F, opcode is 4 (SUB) ======================== % 323 324let assumptions = 325[ 326 ASSUME "(mpc (t1:num)) = #00101"; 327 ASSUME "(button (t1:num)) = F"; 328 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 4" 329];; 330 331let COMPUTER_IMP_mpc_5_button_F_opcode_4 = 332 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_4`,(simulate 10 assumptions));; 333 334% ===================================================================== % 335% Case: mpc = 5, button = F, opcode is 5 (LD) ========================= % 336 337let assumptions = 338[ 339 ASSUME "(mpc (t1:num)) = #00101"; 340 ASSUME "(button (t1:num)) = F"; 341 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 5" 342];; 343 344let COMPUTER_IMP_mpc_5_button_F_opcode_5 = 345 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_5`,(simulate 8 assumptions));; 346 347% ===================================================================== % 348% Case: mpc = 5, button = F, opcode is 6 (ST) ========================= % 349 350let assumptions = 351[ 352 ASSUME "(mpc (t1:num)) = #00101"; 353 ASSUME "(button (t1:num)) = F"; 354 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 6" 355];; 356 357let COMPUTER_IMP_mpc_5_button_F_opcode_6 = 358 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_6`,(simulate 8 assumptions));; 359 360% ===================================================================== % 361% Case: mpc = 5, button = F, opcode is 7 (SKIP) ======================= % 362 363let assumptions = 364[ 365 ASSUME "(mpc (t1:num)) = #00101"; 366 ASSUME "(button (t1:num)) = F"; 367 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 7" 368];; 369 370let COMPUTER_IMP_mpc_5_button_F_opcode_7 = 371 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_7`,(simulate 6 assumptions));; 372 373close_theory ();; 374