1% MICROCODED COMPUTER PROOF : HOL % 2% % 3% 'computer_imp.ml' % 4% % 5% Description % 6% % 7% This theory is the specification of the register-transfer level % 8% implementation of the computer. This specification is the HOL % 9% equivalent to the specification in Mike Gordon's technical report % 10% with a minor modification in the decode unit (see the definition % 11% of DECODE). % 12% % 13% Author: Jeff Joyce % 14% Date: August 4, 1985 % 15 16new_theory `computer_imp`;; 17 18new_parent `values`;; 19 20% Define macros for the types ":num->word13", ":num->word16", % 21% ":num->bool" and ":num->tri_word16". % 22 23let sig13 = ":num->word13";; 24let sig16 = ":num->word16";; 25let sigbool = ":num->bool";; 26let sigtri16 = ":num->tri_word16";; 27 28let REG16 = new_definition 29( 30 `REG16`, 31 "REG16 (input:^sig16,load:^sigbool,output:^sig16) = 32 !t:num. output(t+1) = ((load t) => input t | output t)" 33);; 34 35let REG13 = new_definition 36( 37 `REG13`, 38 "REG13 (input:^sig16,load:^sigbool,output:^sig13) = 39 !t:num. output(t+1) = (load t => CUT16_13(input t) | output t)" 40);; 41 42let IR = new_definition (`IR`,"IR = REG16");; 43let PC = new_definition (`PC`,"PC = REG13");; 44let ACC = new_definition (`ACC`,"ACC = REG16");; 45let ARG = new_definition (`ARG`,"ARG = REG16");; 46let MAR = new_definition (`MAR`,"MAR = REG13");; 47 48let BUF = new_definition 49( 50 `BUF`, 51 "BUF (input:^sig16,output:^sig16) = !t:num. output(t+1) = input t" 52);; 53 54let GATE16 = new_definition 55( 56 `GATE16`, 57 "GATE16 (input:^sig16,control:^sigbool,output:^sigtri16) = 58 !t:num. output t = (control t => MK_TRI16(input t) | FLOAT16)" 59);; 60 61let GATE13 = new_definition 62( 63 `GATE13`, 64 "GATE13 (input:^sig13,control:^sigbool,output:^sigtri16) = 65 !t:num. output t = (control t => MK_TRI16(PAD13_16 (input t)) | FLOAT16)" 66);; 67 68let G0 = new_definition (`G0`,"G0 = GATE16");; 69let G1 = new_definition (`G1`,"G1 = GATE13");; 70let G2 = new_definition (`G2`,"G2 = GATE16");; 71let G3 = new_definition (`G3`,"G3 = GATE16");; 72let G4 = new_definition (`G4`,"G4 = GATE16");; 73 74let MEM = new_definition 75( 76 `MEM`, 77 "MEM 78 (memory:num->mem13_16, 79 mar:^sig13,bus:^sig16,memcntl:num->word2,memout:^sigtri16) = 80 !t:num. 81 (memout t = 82 ((VAL2(memcntl t) = 1) => 83 MK_TRI16(FETCH13(memory t)(mar t)) | FLOAT16)) /\ 84 (memory(t+1) = 85 ((VAL2(memcntl t) = 2) => 86 STORE13(mar t)(bus t)(memory t) | memory t))" 87);; 88 89let ALU = new_definition 90( 91 `ALU`, 92 "ALU 93 (arg:^sig16,bus:^sig16,alucntl:num->word2,alu:^sig16) = 94 !t:num. 95 (alu t = 96 ((VAL2(alucntl t) = 0) => bus t | 97 (VAL2(alucntl t) = 1) => INC16(bus t) | 98 (VAL2(alucntl t) = 2) => ADD16(arg t)(bus t) | SUB16(arg t)(bus t)))" 99);; 100 101let BUS = new_definition 102( 103 `BUS`, 104 "BUS 105 (memout:^sigtri16,g0:^sigtri16,g1:^sigtri16, 106 g2:^sigtri16,g3:^sigtri16,g4:^sigtri16,bus:^sig16) = 107 !t:num. 108 bus t = 109 DEST_TRI16 (memout t U16 g0 t U16 g1 t U16 g2 t U16 g3 t U16 g4 t)" 110);; 111 112let DATA = new_definition 113( 114 `DATA`, 115 "DATA 116 (memory,mar,pc,acc,ir,arg,buf,switches,rsw,wmar,memcntl, 117 wpc,rpc,wacc,racc,wir,rir,warg,alucntl,rbuf) = 118 ?g0 g1 g2 g3 g4 memout alu bus. 119 MEM(memory,mar,bus,memcntl,memout) /\ 120 MAR(bus,wmar,mar) /\ 121 PC(bus,wpc,pc) /\ 122 ACC(bus,wacc,acc) /\ 123 IR(bus,wir,ir) /\ 124 ARG(bus,warg,arg) /\ 125 BUF(alu,buf) /\ 126 G0(switches,rsw,g0) /\ 127 G1(pc,rpc,g1) /\ 128 G2(acc,racc,g2) /\ 129 G3(ir,rir,g3) /\ 130 G4(buf,rbuf,g4) /\ 131 ALU(arg,bus,alucntl,alu) /\ 132 BUS(memout,g0,g1,g2,g3,g4,bus)" 133);; 134 135let ROM = new_definition 136( 137 `ROM`, 138 "ROM (microcode:mem5_30) (mpc,rom) = !t:num. rom t = FETCH5 microcode (mpc t)" 139);; 140 141let MPC = new_definition 142( 143 `MPC`, 144 "MPC(nextaddress,mpc:num->word5) = !t:num. mpc(t+1) = nextaddress t" 145);; 146 147let CNTL_BIT = new_definition 148( 149 `CNTL_BIT`,"CNTL_BIT n w = EL n (BITS30 w)" 150);; 151 152let CNTL_FIELD = new_definition 153( 154 `CNTL_FIELD`,"CNTL_FIELD (m,n) w = WORD2(V(SEG(m,n)(BITS30 w)))" 155);; 156 157let B_ADDR = new_definition 158( 159 `B_ADDR`,"B_ADDR w = WORD5(V(SEG(3,7)(BITS30 w)))" 160);; 161 162let A_ADDR = new_definition 163( 164 `A_ADDR`,"A_ADDR w = WORD5(V(SEG(8,12)(BITS30 w)))" 165);; 166 167let TEST = new_definition 168( 169 `TEST`,"TEST w = V(SEG(0,2)(BITS30 w))" 170);; 171 172% Modification % 173% % 174% The decode unit has been modified slightly from the specification % 175% in Mike Gordon's technical report. The decode unit does not add 1 % 176% to the 'A_ADDR' to obtain the next microinstruction address when the % 177% test field is 3 (ie. 'jump_knob'). This results in a change in the % 178% microcode such that the 'A_ADDR' field of word 1 is 2 instead of 1. % 179 180let DECODE = new_definition 181( 182 `DECODE`, 183 "DECODE 184 (rom,knob,button,acc,ir,nextaddress,rsw,wmar,memcntl, 185 wpc,rpc,wacc,racc,wir,rir,warg,alucntl,rbuf,ready,idle) = 186 !t:num. 187 (nextaddress t = 188 (((TEST(rom t) = 1) /\ (button t)) => B_ADDR(rom t) | 189 ((TEST(rom t) = 2) /\ (VAL16(acc t) = 0)) => B_ADDR(rom t) | 190 (TEST(rom t) = 3) => WORD5(VAL2(knob t) + VAL5(A_ADDR(rom t))) | 191 (TEST(rom t) = 4) => WORD5(VAL3(OPCODE(ir t)) + VAL5(A_ADDR(rom t))) | 192 A_ADDR(rom t))) /\ 193 (rsw t = CNTL_BIT 28 (rom t)) /\ 194 (wmar t = CNTL_BIT 27 (rom t)) /\ 195 (memcntl t = CNTL_FIELD (25,26) (rom t)) /\ 196 (wpc t = CNTL_BIT 24 (rom t)) /\ 197 (rpc t = CNTL_BIT 23 (rom t)) /\ 198 (wacc t = CNTL_BIT 22 (rom t)) /\ 199 (racc t = CNTL_BIT 21 (rom t)) /\ 200 (wir t = CNTL_BIT 20 (rom t)) /\ 201 (rir t = CNTL_BIT 19 (rom t)) /\ 202 (warg t = CNTL_BIT 18 (rom t)) /\ 203 (alucntl t = CNTL_FIELD (16,17) (rom t)) /\ 204 (rbuf t = CNTL_BIT 15 (rom t)) /\ 205 (ready t = CNTL_BIT 14 (rom t)) /\ 206 (idle t = CNTL_BIT 13 (rom t))" 207);; 208 209new_constant(`MICROCODE`,":mem5_30");; 210 211let CONTROL = new_definition 212( 213 `CONTROL`, 214 "CONTROL 215 microcode 216 (mpc,knob,button,acc,ir,rsw,wmar,memcntl, 217 wpc,rpc,wacc,racc,wir,rir,warg,alucntl,rbuf,ready,idle) = 218 ?rom nextaddress. 219 ROM microcode (mpc,rom) /\ 220 MPC(nextaddress,mpc) /\ 221 DECODE 222 (rom,knob,button,acc,ir,nextaddress,rsw,wmar,memcntl, 223 wpc,rpc,wacc,racc,wir,rir,warg,alucntl,rbuf,ready,idle)" 224);; 225 226let COMPUTER_IMP = new_definition 227( 228 `COMPUTER_IMP`, 229 "COMPUTER_IMP 230 (mpc,mar,ir,arg,buf) 231 (memory,knob,button,switches,pc,acc,idle,ready) = 232 ?rsw wmar memcntl wpc rpc wacc racc wir rir warg alucntl rbuf. 233 CONTROL 234 MICROCODE 235 (mpc,knob,button,acc,ir,rsw,wmar,memcntl, 236 wpc,rpc,wacc,racc,wir,rir,warg,alucntl,rbuf,ready,idle) /\ 237 DATA 238 (memory,mar,pc,acc,ir,arg,buf,switches,rsw,wmar,memcntl, 239 wpc,rpc,wacc,racc,wir,rir,warg,alucntl,rbuf)" 240);; 241 242let CONTROL_prims = [ROM;MPC;DECODE];; 243 244let CONTROL_EXP = EXPANDF CONTROL_prims CONTROL;; 245 246let DATA_prims = 247 [MEM;ALU;BUS;BUF] @ 248 [ 249 SUBS [SYM PC] REG13; 250 SUBS [SYM IR] REG16; 251 SUBS [SYM MAR] REG13; 252 SUBS [SYM ACC] REG16; 253 SUBS [SYM ARG] REG16; 254 SUBS [SYM G0] GATE16; 255 SUBS [SYM G1] GATE13; 256 SUBS [SYM G2] GATE16; 257 SUBS [SYM G3] GATE16; 258 SUBS [SYM G4] GATE16];; 259 260let DATA_EXP = EXPANDF DATA_prims DATA;; 261 262let COMPUTER_IMP_EXP = EXPANDF [CONTROL_EXP;DATA_EXP] COMPUTER_IMP;; 263 264let COMPUTER_IMP_EXP_ASM = 265 PURE_REWRITE_RULE [TEST;A_ADDR;B_ADDR;CNTL_BIT;CNTL_FIELD] 266 (SUBS [COMPUTER_IMP_EXP] 267 (ASSUME 268 "COMPUTER_IMP 269 (mpc,mar,ir,arg,buf) 270 (memory,knob,button,switches,pc,acc,idle,ready)"));; 271 272save_thm (`COMPUTER_IMP_EXP_ASM`,COMPUTER_IMP_EXP_ASM);; 273 274close_theory ();; 275