[257] | 1 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 2 | (* Interpret.ma: Operational semantics for the 8051/8052 processor. *) |
---|
| 3 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 4 | |
---|
[314] | 5 | include "ASM.ma". |
---|
[259] | 6 | include "Arithmetic.ma". |
---|
[257] | 7 | include "BitVectorTrie.ma". |
---|
| 8 | |
---|
[276] | 9 | ndefinition Time ≝ Nat. |
---|
| 10 | |
---|
| 11 | ninductive SerialBufferType: Type[0] ≝ |
---|
| 12 | Eight: Byte → SerialBufferType |
---|
| 13 | | Nine: Bit → Byte → SerialBufferType. |
---|
| 14 | |
---|
| 15 | ninductive LineType: Type[0] ≝ |
---|
| 16 | P1: Byte → LineType |
---|
| 17 | | P3: Byte → LineType |
---|
| 18 | | SerialBuffer: SerialBufferType → LineType. |
---|
| 19 | |
---|
| 20 | (* What is a continuation, now? *) |
---|
| 21 | |
---|
[257] | 22 | ninductive SFR8051: Type[0] ≝ |
---|
| 23 | SFR_SP: SFR8051 |
---|
| 24 | | SFR_DPL: SFR8051 |
---|
| 25 | | SFR_DPH: SFR8051 |
---|
| 26 | | SFR_PCON: SFR8051 |
---|
| 27 | | SFR_TCON: SFR8051 |
---|
| 28 | | SFR_TMOD: SFR8051 |
---|
| 29 | | SFR_TL0: SFR8051 |
---|
| 30 | | SFR_TL1: SFR8051 |
---|
| 31 | | SFR_TH0: SFR8051 |
---|
| 32 | | SFR_TH1: SFR8051 |
---|
| 33 | | SFR_P1: SFR8051 |
---|
| 34 | | SFR_SCON: SFR8051 |
---|
| 35 | | SFR_SBUF: SFR8051 |
---|
| 36 | | SFR_IE: SFR8051 |
---|
| 37 | | SFR_P3: SFR8051 |
---|
| 38 | | SFR_IP: SFR8051 |
---|
| 39 | | SFR_PSW: SFR8051 |
---|
| 40 | | SFR_ACC_A: SFR8051 |
---|
| 41 | | SFR_ACC_B: SFR8051. |
---|
| 42 | |
---|
| 43 | ndefinition sfr_8051_index ≝ |
---|
| 44 | λs: SFR8051. |
---|
| 45 | match s with |
---|
| 46 | [ SFR_SP ⇒ Z |
---|
| 47 | | SFR_DPL ⇒ S Z |
---|
| 48 | | SFR_DPH ⇒ two |
---|
| 49 | | SFR_PCON ⇒ three |
---|
| 50 | | SFR_TCON ⇒ four |
---|
| 51 | | SFR_TMOD ⇒ five |
---|
| 52 | | SFR_TL0 ⇒ six |
---|
| 53 | | SFR_TL1 ⇒ seven |
---|
| 54 | | SFR_TH0 ⇒ eight |
---|
| 55 | | SFR_TH1 ⇒ nine |
---|
| 56 | | SFR_P1 ⇒ ten |
---|
| 57 | | SFR_SCON ⇒ eleven |
---|
| 58 | | SFR_SBUF ⇒ twelve |
---|
| 59 | | SFR_IE ⇒ thirteen |
---|
| 60 | | SFR_P3 ⇒ fourteen |
---|
| 61 | | SFR_IP ⇒ fifteen |
---|
| 62 | | SFR_PSW ⇒ sixteen |
---|
| 63 | | SFR_ACC_A ⇒ seventeen |
---|
| 64 | | SFR_ACC_B ⇒ eighteen |
---|
| 65 | ]. |
---|
| 66 | |
---|
| 67 | ninductive SFR8052: Type[0] ≝ |
---|
| 68 | SFR_T2CON: SFR8052 |
---|
| 69 | | SFR_RCAP2L: SFR8052 |
---|
| 70 | | SFR_RCAP2H: SFR8052 |
---|
| 71 | | SFR_TL2: SFR8052 |
---|
| 72 | | SFR_TH2: SFR8052. |
---|
| 73 | |
---|
| 74 | ndefinition sfr_8052_index ≝ |
---|
| 75 | λs: SFR8052. |
---|
| 76 | match s with |
---|
| 77 | [ SFR_T2CON ⇒ Z |
---|
| 78 | | SFR_RCAP2L ⇒ S Z |
---|
| 79 | | SFR_RCAP2H ⇒ two |
---|
| 80 | | SFR_TL2 ⇒ three |
---|
| 81 | | SFR_TH2 ⇒ four |
---|
| 82 | ]. |
---|
| 83 | |
---|
| 84 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 85 | (* Processor status. *) |
---|
| 86 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 87 | nrecord Status: Type[0] ≝ |
---|
| 88 | { |
---|
| 89 | code_memory: BitVectorTrie Byte sixteen; |
---|
| 90 | low_internal_ram: BitVectorTrie Byte seven; |
---|
| 91 | high_internal_ram: BitVectorTrie Byte seven; |
---|
| 92 | external_ram: BitVectorTrie Byte sixteen; |
---|
| 93 | |
---|
| 94 | program_counter: Word; |
---|
| 95 | |
---|
| 96 | special_function_registers_8051: Vector Byte nineteen; |
---|
[281] | 97 | special_function_registers_8052: Vector Byte five; |
---|
| 98 | |
---|
| 99 | p1_latch: Byte; |
---|
[329] | 100 | p3_latch: Byte; |
---|
| 101 | |
---|
| 102 | clock: Time |
---|
[257] | 103 | }. |
---|
| 104 | |
---|
[351] | 105 | nlemma sfr8051_index_nineteen: |
---|
[265] | 106 | ∀i: SFR8051. |
---|
| 107 | sfr_8051_index i < nineteen. |
---|
[351] | 108 | #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone); |
---|
| 109 | napply less_than_or_equal_zero. |
---|
| 110 | nqed. |
---|
[265] | 111 | |
---|
[351] | 112 | nlemma sfr8052_index_five: |
---|
[265] | 113 | ∀i: SFR8052. |
---|
| 114 | sfr_8052_index i < five. |
---|
[351] | 115 | #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone); |
---|
| 116 | napply less_than_or_equal_zero. |
---|
| 117 | nqed. |
---|
[285] | 118 | |
---|
[329] | 119 | ndefinition set_clock ≝ |
---|
| 120 | λs: Status. |
---|
| 121 | λt: Time. |
---|
| 122 | let old_code_memory ≝ code_memory s in |
---|
| 123 | let old_low_internal_ram ≝ low_internal_ram s in |
---|
| 124 | let old_high_internal_ram ≝ high_internal_ram s in |
---|
| 125 | let old_external_ram ≝ external_ram s in |
---|
| 126 | let old_program_counter ≝ program_counter s in |
---|
| 127 | let old_special_function_registers_8051 ≝ special_function_registers_8051 s in |
---|
| 128 | let old_special_function_registers_8052 ≝ special_function_registers_8052 s in |
---|
| 129 | let old_p1_latch ≝ p1_latch s in |
---|
| 130 | let old_p3_latch ≝ p3_latch s in |
---|
| 131 | mk_Status old_code_memory |
---|
| 132 | old_low_internal_ram |
---|
| 133 | old_high_internal_ram |
---|
| 134 | old_external_ram |
---|
| 135 | old_program_counter |
---|
| 136 | old_special_function_registers_8051 |
---|
| 137 | old_special_function_registers_8052 |
---|
| 138 | old_p1_latch |
---|
| 139 | old_p3_latch |
---|
| 140 | t. |
---|
| 141 | |
---|
[285] | 142 | ndefinition set_p1_latch ≝ |
---|
| 143 | λs: Status. |
---|
| 144 | λb: Byte. |
---|
| 145 | let old_code_memory ≝ code_memory s in |
---|
| 146 | let old_low_internal_ram ≝ low_internal_ram s in |
---|
| 147 | let old_high_internal_ram ≝ high_internal_ram s in |
---|
| 148 | let old_external_ram ≝ external_ram s in |
---|
| 149 | let old_program_counter ≝ program_counter s in |
---|
| 150 | let old_special_function_registers_8051 ≝ special_function_registers_8051 s in |
---|
| 151 | let old_special_function_registers_8052 ≝ special_function_registers_8052 s in |
---|
| 152 | let old_p3_latch ≝ p3_latch s in |
---|
[329] | 153 | let old_clock ≝ clock s in |
---|
[285] | 154 | mk_Status old_code_memory |
---|
| 155 | old_low_internal_ram |
---|
| 156 | old_high_internal_ram |
---|
| 157 | old_external_ram |
---|
| 158 | old_program_counter |
---|
| 159 | old_special_function_registers_8051 |
---|
| 160 | old_special_function_registers_8052 |
---|
| 161 | b |
---|
[329] | 162 | old_p3_latch |
---|
| 163 | old_clock. |
---|
[265] | 164 | |
---|
[285] | 165 | ndefinition set_p3_latch ≝ |
---|
| 166 | λs: Status. |
---|
| 167 | λb: Byte. |
---|
| 168 | let old_code_memory ≝ code_memory s in |
---|
| 169 | let old_low_internal_ram ≝ low_internal_ram s in |
---|
| 170 | let old_high_internal_ram ≝ high_internal_ram s in |
---|
| 171 | let old_external_ram ≝ external_ram s in |
---|
| 172 | let old_program_counter ≝ program_counter s in |
---|
| 173 | let old_special_function_registers_8051 ≝ special_function_registers_8051 s in |
---|
| 174 | let old_special_function_registers_8052 ≝ special_function_registers_8052 s in |
---|
| 175 | let old_p1_latch ≝ p1_latch s in |
---|
[329] | 176 | let old_clock ≝ clock s in |
---|
[285] | 177 | mk_Status old_code_memory |
---|
| 178 | old_low_internal_ram |
---|
| 179 | old_high_internal_ram |
---|
| 180 | old_external_ram |
---|
| 181 | old_program_counter |
---|
| 182 | old_special_function_registers_8051 |
---|
| 183 | old_special_function_registers_8052 |
---|
| 184 | old_p1_latch |
---|
[329] | 185 | b |
---|
| 186 | old_clock. |
---|
[285] | 187 | |
---|
[265] | 188 | ndefinition get_8051_sfr ≝ |
---|
| 189 | λs: Status. |
---|
| 190 | λi: SFR8051. |
---|
| 191 | let sfr ≝ special_function_registers_8051 s in |
---|
| 192 | let index ≝ sfr_8051_index i in |
---|
[351] | 193 | get_index ?? sfr index ?. |
---|
[265] | 194 | napply (sfr8051_index_nineteen i). |
---|
| 195 | nqed. |
---|
| 196 | |
---|
| 197 | ndefinition get_8052_sfr ≝ |
---|
| 198 | λs: Status. |
---|
| 199 | λi: SFR8052. |
---|
| 200 | let sfr ≝ special_function_registers_8052 s in |
---|
| 201 | let index ≝ sfr_8052_index i in |
---|
[351] | 202 | get_index ?? sfr index ?. |
---|
[265] | 203 | napply (sfr8052_index_five i). |
---|
| 204 | nqed. |
---|
| 205 | |
---|
[259] | 206 | ndefinition set_8051_sfr ≝ |
---|
| 207 | λs: Status. |
---|
| 208 | λi: SFR8051. |
---|
| 209 | λb: Byte. |
---|
[265] | 210 | let index ≝ sfr_8051_index i in |
---|
| 211 | let old_code_memory ≝ code_memory s in |
---|
| 212 | let old_low_internal_ram ≝ low_internal_ram s in |
---|
| 213 | let old_high_internal_ram ≝ high_internal_ram s in |
---|
| 214 | let old_external_ram ≝ external_ram s in |
---|
| 215 | let old_program_counter ≝ program_counter s in |
---|
| 216 | let old_special_function_registers_8051 ≝ special_function_registers_8051 s in |
---|
| 217 | let old_special_function_registers_8052 ≝ special_function_registers_8052 s in |
---|
| 218 | let new_special_function_registers_8051 ≝ |
---|
[351] | 219 | set_index Byte nineteen old_special_function_registers_8051 index b ? in |
---|
[285] | 220 | let old_p1_latch ≝ p1_latch s in |
---|
| 221 | let old_p3_latch ≝ p3_latch s in |
---|
[329] | 222 | let old_clock ≝ clock s in |
---|
[265] | 223 | mk_Status old_code_memory |
---|
| 224 | old_low_internal_ram |
---|
| 225 | old_high_internal_ram |
---|
| 226 | old_external_ram |
---|
| 227 | old_program_counter |
---|
| 228 | new_special_function_registers_8051 |
---|
[285] | 229 | old_special_function_registers_8052 |
---|
| 230 | old_p1_latch |
---|
[329] | 231 | old_p3_latch |
---|
| 232 | old_clock. |
---|
[265] | 233 | napply (sfr8051_index_nineteen i). |
---|
| 234 | nqed. |
---|
[258] | 235 | |
---|
[265] | 236 | ndefinition set_8052_sfr ≝ |
---|
| 237 | λs: Status. |
---|
| 238 | λi: SFR8052. |
---|
| 239 | λb: Byte. |
---|
| 240 | let index ≝ sfr_8052_index i in |
---|
| 241 | let old_code_memory ≝ code_memory s in |
---|
| 242 | let old_low_internal_ram ≝ low_internal_ram s in |
---|
| 243 | let old_high_internal_ram ≝ high_internal_ram s in |
---|
| 244 | let old_external_ram ≝ external_ram s in |
---|
| 245 | let old_program_counter ≝ program_counter s in |
---|
| 246 | let old_special_function_registers_8051 ≝ special_function_registers_8051 s in |
---|
| 247 | let old_special_function_registers_8052 ≝ special_function_registers_8052 s in |
---|
| 248 | let new_special_function_registers_8052 ≝ |
---|
[351] | 249 | set_index Byte five old_special_function_registers_8052 index b ? in |
---|
[285] | 250 | let old_p1_latch ≝ p1_latch s in |
---|
| 251 | let old_p3_latch ≝ p3_latch s in |
---|
[329] | 252 | let old_clock ≝ clock s in |
---|
[265] | 253 | mk_Status old_code_memory |
---|
| 254 | old_low_internal_ram |
---|
| 255 | old_high_internal_ram |
---|
| 256 | old_external_ram |
---|
| 257 | old_program_counter |
---|
| 258 | old_special_function_registers_8051 |
---|
[285] | 259 | new_special_function_registers_8052 |
---|
| 260 | old_p1_latch |
---|
[329] | 261 | old_p3_latch |
---|
| 262 | old_clock. |
---|
[265] | 263 | napply (sfr8052_index_five i). |
---|
| 264 | nqed. |
---|
| 265 | |
---|
| 266 | ndefinition set_program_counter ≝ |
---|
| 267 | λs: Status. |
---|
| 268 | λw: Word. |
---|
| 269 | let old_code_memory ≝ code_memory s in |
---|
| 270 | let old_low_internal_ram ≝ low_internal_ram s in |
---|
| 271 | let old_high_internal_ram ≝ high_internal_ram s in |
---|
| 272 | let old_external_ram ≝ external_ram s in |
---|
| 273 | let old_special_function_registers_8051 ≝ special_function_registers_8051 s in |
---|
| 274 | let old_special_function_registers_8052 ≝ special_function_registers_8052 s in |
---|
[285] | 275 | let old_p1_latch ≝ p1_latch s in |
---|
| 276 | let old_p3_latch ≝ p3_latch s in |
---|
[329] | 277 | let old_clock ≝ clock s in |
---|
[265] | 278 | mk_Status old_code_memory |
---|
| 279 | old_low_internal_ram |
---|
| 280 | old_high_internal_ram |
---|
| 281 | old_external_ram |
---|
| 282 | w |
---|
| 283 | old_special_function_registers_8051 |
---|
[285] | 284 | old_special_function_registers_8052 |
---|
| 285 | old_p1_latch |
---|
[329] | 286 | old_p3_latch |
---|
| 287 | old_clock. |
---|
[265] | 288 | |
---|
| 289 | ndefinition set_code_memory ≝ |
---|
| 290 | λs: Status. |
---|
| 291 | λr: BitVectorTrie Byte sixteen. |
---|
| 292 | let old_low_internal_ram ≝ low_internal_ram s in |
---|
| 293 | let old_high_internal_ram ≝ high_internal_ram s in |
---|
| 294 | let old_external_ram ≝ external_ram s in |
---|
| 295 | let old_program_counter ≝ program_counter s in |
---|
| 296 | let old_special_function_registers_8051 ≝ special_function_registers_8051 s in |
---|
| 297 | let old_special_function_registers_8052 ≝ special_function_registers_8052 s in |
---|
[285] | 298 | let old_p1_latch ≝ p1_latch s in |
---|
| 299 | let old_p3_latch ≝ p3_latch s in |
---|
[329] | 300 | let old_clock ≝ clock s in |
---|
[265] | 301 | mk_Status r |
---|
| 302 | old_low_internal_ram |
---|
| 303 | old_high_internal_ram |
---|
| 304 | old_external_ram |
---|
| 305 | old_program_counter |
---|
| 306 | old_special_function_registers_8051 |
---|
[285] | 307 | old_special_function_registers_8052 |
---|
| 308 | old_p1_latch |
---|
[329] | 309 | old_p3_latch |
---|
| 310 | old_clock. |
---|
[265] | 311 | |
---|
| 312 | ndefinition set_low_internal_ram ≝ |
---|
| 313 | λs: Status. |
---|
| 314 | λr: BitVectorTrie Byte seven. |
---|
| 315 | let old_code_memory ≝ code_memory s in |
---|
| 316 | let old_high_internal_ram ≝ high_internal_ram s in |
---|
| 317 | let old_external_ram ≝ external_ram s in |
---|
| 318 | let old_program_counter ≝ program_counter s in |
---|
| 319 | let old_special_function_registers_8051 ≝ special_function_registers_8051 s in |
---|
| 320 | let old_special_function_registers_8052 ≝ special_function_registers_8052 s in |
---|
[285] | 321 | let old_p1_latch ≝ p1_latch s in |
---|
| 322 | let old_p3_latch ≝ p3_latch s in |
---|
[329] | 323 | let old_clock ≝ clock s in |
---|
[265] | 324 | mk_Status old_code_memory |
---|
| 325 | r |
---|
| 326 | old_high_internal_ram |
---|
| 327 | old_external_ram |
---|
| 328 | old_program_counter |
---|
| 329 | old_special_function_registers_8051 |
---|
[285] | 330 | old_special_function_registers_8052 |
---|
| 331 | old_p1_latch |
---|
[329] | 332 | old_p3_latch |
---|
| 333 | old_clock. |
---|
[265] | 334 | |
---|
[285] | 335 | ndefinition set_high_internal_ram ≝ |
---|
| 336 | λs: Status. |
---|
| 337 | λr: BitVectorTrie Byte seven. |
---|
| 338 | let old_code_memory ≝ code_memory s in |
---|
| 339 | let old_low_internal_ram ≝ low_internal_ram s in |
---|
| 340 | let old_high_internal_ram ≝ high_internal_ram s in |
---|
| 341 | let old_external_ram ≝ external_ram s in |
---|
| 342 | let old_program_counter ≝ program_counter s in |
---|
| 343 | let old_special_function_registers_8051 ≝ special_function_registers_8051 s in |
---|
| 344 | let old_special_function_registers_8052 ≝ special_function_registers_8052 s in |
---|
| 345 | let old_p1_latch ≝ p1_latch s in |
---|
| 346 | let old_p3_latch ≝ p3_latch s in |
---|
[329] | 347 | let old_clock ≝ clock s in |
---|
[285] | 348 | mk_Status old_code_memory |
---|
| 349 | old_low_internal_ram |
---|
| 350 | r |
---|
| 351 | old_external_ram |
---|
| 352 | old_program_counter |
---|
| 353 | old_special_function_registers_8051 |
---|
| 354 | old_special_function_registers_8052 |
---|
| 355 | old_p1_latch |
---|
[329] | 356 | old_p3_latch |
---|
| 357 | old_clock. |
---|
[285] | 358 | |
---|
[313] | 359 | ndefinition set_external_ram ≝ |
---|
| 360 | λs: Status. |
---|
| 361 | λr: BitVectorTrie Byte sixteen. |
---|
| 362 | let old_code_memory ≝ code_memory s in |
---|
| 363 | let old_low_internal_ram ≝ low_internal_ram s in |
---|
| 364 | let old_high_internal_ram ≝ high_internal_ram s in |
---|
| 365 | let old_program_counter ≝ program_counter s in |
---|
| 366 | let old_special_function_registers_8051 ≝ special_function_registers_8051 s in |
---|
| 367 | let old_special_function_registers_8052 ≝ special_function_registers_8052 s in |
---|
| 368 | let old_p1_latch ≝ p1_latch s in |
---|
| 369 | let old_p3_latch ≝ p3_latch s in |
---|
[329] | 370 | let old_clock ≝ clock s in |
---|
[313] | 371 | mk_Status old_code_memory |
---|
| 372 | old_low_internal_ram |
---|
| 373 | old_high_internal_ram |
---|
| 374 | r |
---|
| 375 | old_program_counter |
---|
| 376 | old_special_function_registers_8051 |
---|
| 377 | old_special_function_registers_8052 |
---|
| 378 | old_p1_latch |
---|
[329] | 379 | old_p3_latch |
---|
| 380 | old_clock. |
---|
[313] | 381 | |
---|
[265] | 382 | ndefinition get_cy_flag ≝ |
---|
| 383 | λs: Status. |
---|
| 384 | let sfr ≝ special_function_registers_8051 s in |
---|
[267] | 385 | let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 386 | get_index Bool eight psw Z ?. |
---|
| 387 | nnormalize. |
---|
| 388 | napply (less_than_or_equal_monotone ? ?). |
---|
| 389 | napply (less_than_or_equal_zero). |
---|
| 390 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 391 | napply (less_than_or_equal_zero). |
---|
| 392 | nqed. |
---|
| 393 | |
---|
| 394 | ndefinition get_ac_flag ≝ |
---|
| 395 | λs: Status. |
---|
| 396 | let sfr ≝ special_function_registers_8051 s in |
---|
| 397 | let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 398 | get_index Bool eight psw (S Z) ?. |
---|
| 399 | nnormalize. |
---|
| 400 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 401 | napply (less_than_or_equal_zero). |
---|
| 402 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 403 | napply (less_than_or_equal_zero). |
---|
| 404 | nqed. |
---|
| 405 | |
---|
| 406 | ndefinition get_fo_flag ≝ |
---|
| 407 | λs: Status. |
---|
| 408 | let sfr ≝ special_function_registers_8051 s in |
---|
| 409 | let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 410 | get_index Bool eight psw two ?. |
---|
| 411 | nnormalize. |
---|
| 412 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 413 | napply (less_than_or_equal_zero). |
---|
| 414 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 415 | napply (less_than_or_equal_zero). |
---|
| 416 | nqed. |
---|
| 417 | |
---|
| 418 | ndefinition get_rs1_flag ≝ |
---|
| 419 | λs: Status. |
---|
| 420 | let sfr ≝ special_function_registers_8051 s in |
---|
| 421 | let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 422 | get_index Bool eight psw three ?. |
---|
| 423 | nnormalize. |
---|
| 424 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 425 | napply (less_than_or_equal_zero). |
---|
| 426 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 427 | napply (less_than_or_equal_zero). |
---|
| 428 | nqed. |
---|
| 429 | |
---|
| 430 | ndefinition get_rs0_flag ≝ |
---|
| 431 | λs: Status. |
---|
| 432 | let sfr ≝ special_function_registers_8051 s in |
---|
| 433 | let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 434 | get_index Bool eight psw four ?. |
---|
| 435 | nnormalize. |
---|
| 436 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 437 | napply (less_than_or_equal_zero). |
---|
| 438 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 439 | napply (less_than_or_equal_zero). |
---|
| 440 | nqed. |
---|
| 441 | |
---|
| 442 | ndefinition get_ov_flag ≝ |
---|
| 443 | λs: Status. |
---|
| 444 | let sfr ≝ special_function_registers_8051 s in |
---|
| 445 | let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 446 | get_index Bool eight psw five ?. |
---|
| 447 | nnormalize. |
---|
| 448 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 449 | napply (less_than_or_equal_zero). |
---|
| 450 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 451 | napply (less_than_or_equal_zero). |
---|
| 452 | nqed. |
---|
| 453 | |
---|
| 454 | ndefinition get_ud_flag ≝ |
---|
| 455 | λs: Status. |
---|
| 456 | let sfr ≝ special_function_registers_8051 s in |
---|
| 457 | let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 458 | get_index Bool eight psw six ?. |
---|
| 459 | nnormalize. |
---|
| 460 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 461 | napply (less_than_or_equal_zero). |
---|
| 462 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 463 | napply (less_than_or_equal_zero). |
---|
| 464 | nqed. |
---|
| 465 | |
---|
| 466 | ndefinition get_p_flag ≝ |
---|
| 467 | λs: Status. |
---|
| 468 | let sfr ≝ special_function_registers_8051 s in |
---|
| 469 | let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in |
---|
| 470 | get_index Bool eight psw seven ?. |
---|
| 471 | nnormalize. |
---|
| 472 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 473 | napply (less_than_or_equal_zero). |
---|
| 474 | nrepeat (napply (less_than_or_equal_monotone ? ?)). |
---|
| 475 | napply (less_than_or_equal_zero). |
---|
| 476 | nqed. |
---|
[265] | 477 | |
---|
[290] | 478 | ndefinition set_flags ≝ |
---|
| 479 | λs: Status. |
---|
| 480 | λcy: Bit. |
---|
| 481 | λac: Maybe Bit. |
---|
| 482 | λov: Bit. |
---|
| 483 | let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in |
---|
| 484 | let old_cy ≝ get_index … nu Z ? in |
---|
| 485 | let old_ac ≝ get_index … nu one ? in |
---|
| 486 | let old_fo ≝ get_index … nu two ? in |
---|
| 487 | let old_rs1 ≝ get_index … nu three ? in |
---|
| 488 | let old_rs0 ≝ get_index … nl Z ? in |
---|
| 489 | let old_ov ≝ get_index … nl one ? in |
---|
| 490 | let old_ud ≝ get_index … nl two ? in |
---|
| 491 | let old_p ≝ get_index … nl three ? in |
---|
| 492 | let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in |
---|
| 493 | let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ; |
---|
| 494 | old_rs0 ; old_ov ; old_ud ; old_p ]] in |
---|
| 495 | set_8051_sfr s SFR_PSW new_psw. |
---|
| 496 | ##[##1,2,3,4,5,6,7,8: |
---|
| 497 | nnormalize; |
---|
| 498 | nrepeat (napply less_than_or_equal_monotone); |
---|
| 499 | napply (less_than_or_equal_zero); |
---|
| 500 | ##] |
---|
| 501 | nqed. |
---|
| 502 | |
---|
[257] | 503 | ndefinition initialise_status ≝ |
---|
[285] | 504 | let status ≝ mk_Status (Stub Byte sixteen) (* Code mem. *) |
---|
| 505 | (Stub Byte seven) (* Low mem. *) |
---|
| 506 | (Stub Byte seven) (* High mem. *) |
---|
| 507 | (Stub Byte sixteen) (* Ext mem. *) |
---|
| 508 | (zero sixteen) (* PC. *) |
---|
| 509 | (replicate Byte nineteen (zero eight)) (* 8051 SFR. *) |
---|
| 510 | (replicate Byte five (zero eight)) (* 8052 SFR. *) |
---|
| 511 | (zero eight) (* P1 latch. *) |
---|
[329] | 512 | (zero eight) (* P3 latch. *) |
---|
| 513 | Z (* Clock. *) |
---|
| 514 | in |
---|
| 515 | set_program_counter status (bitvector_of_nat sixteen seven). |
---|
[281] | 516 | |
---|
| 517 | naxiom not_implemented: False. |
---|
| 518 | |
---|
| 519 | include "Arithmetic.ma". |
---|
| 520 | |
---|
| 521 | ndefinition get_bit_addressable_sfr ≝ |
---|
| 522 | λs: Status. |
---|
| 523 | λn: Nat. |
---|
| 524 | λb: BitVector n. |
---|
| 525 | λl: Bool. |
---|
| 526 | let address ≝ nat_of_bitvector … b in |
---|
[350] | 527 | if (eq_n address one_hundred_and_twenty_eight) then |
---|
[281] | 528 | ? |
---|
[350] | 529 | else if (eq_n address one_hundred_and_forty_four) then |
---|
[281] | 530 | if l then |
---|
| 531 | (p1_latch s) |
---|
| 532 | else |
---|
| 533 | (get_8051_sfr s SFR_P1) |
---|
[350] | 534 | else if (eq_n address one_hundred_and_sixty) then |
---|
[281] | 535 | ? |
---|
[350] | 536 | else if (eq_n address one_hundred_and_seventy_six) then |
---|
[281] | 537 | if l then |
---|
| 538 | (p3_latch s) |
---|
| 539 | else |
---|
| 540 | (get_8051_sfr s SFR_P3) |
---|
[350] | 541 | else if (eq_n address one_hundred_and_fifty_three) then |
---|
[281] | 542 | get_8051_sfr s SFR_SBUF |
---|
[350] | 543 | else if (eq_n address one_hundred_and_thirty_eight) then |
---|
[281] | 544 | get_8051_sfr s SFR_TL0 |
---|
[350] | 545 | else if (eq_n address one_hundred_and_thirty_nine) then |
---|
[281] | 546 | get_8051_sfr s SFR_TL1 |
---|
[350] | 547 | else if (eq_n address one_hundred_and_forty) then |
---|
[281] | 548 | get_8051_sfr s SFR_TH0 |
---|
[350] | 549 | else if (eq_n address one_hundred_and_forty_one) then |
---|
[281] | 550 | get_8051_sfr s SFR_TH1 |
---|
[350] | 551 | else if (eq_n address two_hundred) then |
---|
[281] | 552 | get_8052_sfr s SFR_T2CON |
---|
[350] | 553 | else if (eq_n address two_hundred_and_two) then |
---|
[281] | 554 | get_8052_sfr s SFR_RCAP2L |
---|
[350] | 555 | else if (eq_n address two_hundred_and_three) then |
---|
[281] | 556 | get_8052_sfr s SFR_RCAP2H |
---|
[350] | 557 | else if (eq_n address two_hundred_and_four) then |
---|
[281] | 558 | get_8052_sfr s SFR_TL2 |
---|
[350] | 559 | else if (eq_n address two_hundred_and_five) then |
---|
[281] | 560 | get_8052_sfr s SFR_TH2 |
---|
[350] | 561 | else if (eq_n address one_hundred_and_thirty_five) then |
---|
[281] | 562 | get_8051_sfr s SFR_PCON |
---|
[350] | 563 | else if (eq_n address one_hundred_and_thirty_six) then |
---|
[281] | 564 | get_8051_sfr s SFR_TCON |
---|
[350] | 565 | else if (eq_n address one_hundred_and_thirty_seven) then |
---|
[281] | 566 | get_8051_sfr s SFR_TMOD |
---|
[350] | 567 | else if (eq_n address one_hundred_and_fifty_two) then |
---|
[281] | 568 | get_8051_sfr s SFR_SCON |
---|
[350] | 569 | else if (eq_n address one_hundred_and_sixty_eight) then |
---|
[281] | 570 | get_8051_sfr s SFR_IE |
---|
[350] | 571 | else if (eq_n address one_hundred_and_eighty_four) then |
---|
[281] | 572 | get_8051_sfr s SFR_IP |
---|
[350] | 573 | else if (eq_n address one_hundred_and_twenty_nine) then |
---|
[281] | 574 | get_8051_sfr s SFR_SP |
---|
[350] | 575 | else if (eq_n address one_hundred_and_thirty) then |
---|
[281] | 576 | get_8051_sfr s SFR_DPL |
---|
[350] | 577 | else if (eq_n address one_hundred_and_thirty_one) then |
---|
[281] | 578 | get_8051_sfr s SFR_DPH |
---|
[350] | 579 | else if (eq_n address two_hundred_and_eight) then |
---|
[281] | 580 | get_8051_sfr s SFR_PSW |
---|
[350] | 581 | else if (eq_n address two_hundred_and_twenty_four) then |
---|
[281] | 582 | get_8051_sfr s SFR_ACC_A |
---|
[350] | 583 | else if (eq_n address two_hundred_and_forty) then |
---|
[281] | 584 | get_8051_sfr s SFR_ACC_B |
---|
| 585 | else |
---|
| 586 | ?. |
---|
| 587 | ncases not_implemented. |
---|
[285] | 588 | nqed. |
---|
| 589 | |
---|
| 590 | ndefinition set_bit_addressable_sfr ≝ |
---|
| 591 | λs: Status. |
---|
| 592 | λb: Byte. |
---|
[313] | 593 | λv: Byte. |
---|
[285] | 594 | let address ≝ nat_of_bitvector … b in |
---|
[350] | 595 | if (eq_n address one_hundred_and_twenty_eight) then |
---|
[285] | 596 | ? |
---|
[350] | 597 | else if (eq_n address one_hundred_and_forty_four) then |
---|
[313] | 598 | let status_1 ≝ set_8051_sfr s SFR_P1 v in |
---|
| 599 | let status_2 ≝ set_p1_latch s v in |
---|
[285] | 600 | status_2 |
---|
[350] | 601 | else if (eq_n address one_hundred_and_sixty) then |
---|
[285] | 602 | ? |
---|
[350] | 603 | else if (eq_n address one_hundred_and_seventy_six) then |
---|
[313] | 604 | let status_1 ≝ set_8051_sfr s SFR_P3 v in |
---|
| 605 | let status_2 ≝ set_p3_latch s v in |
---|
[285] | 606 | status_2 |
---|
[350] | 607 | else if (eq_n address one_hundred_and_fifty_three) then |
---|
[313] | 608 | set_8051_sfr s SFR_SBUF v |
---|
[350] | 609 | else if (eq_n address one_hundred_and_thirty_eight) then |
---|
[313] | 610 | set_8051_sfr s SFR_TL0 v |
---|
[350] | 611 | else if (eq_n address one_hundred_and_thirty_nine) then |
---|
[313] | 612 | set_8051_sfr s SFR_TL1 v |
---|
[350] | 613 | else if (eq_n address one_hundred_and_forty) then |
---|
[313] | 614 | set_8051_sfr s SFR_TH0 v |
---|
[350] | 615 | else if (eq_n address one_hundred_and_forty_one) then |
---|
[313] | 616 | set_8051_sfr s SFR_TH1 v |
---|
[350] | 617 | else if (eq_n address two_hundred) then |
---|
[313] | 618 | set_8052_sfr s SFR_T2CON v |
---|
[350] | 619 | else if (eq_n address two_hundred_and_two) then |
---|
[313] | 620 | set_8052_sfr s SFR_RCAP2L v |
---|
[350] | 621 | else if (eq_n address two_hundred_and_three) then |
---|
[313] | 622 | set_8052_sfr s SFR_RCAP2H v |
---|
[350] | 623 | else if (eq_n address two_hundred_and_four) then |
---|
[313] | 624 | set_8052_sfr s SFR_TL2 v |
---|
[350] | 625 | else if (eq_n address two_hundred_and_five) then |
---|
[313] | 626 | set_8052_sfr s SFR_TH2 v |
---|
[350] | 627 | else if (eq_n address one_hundred_and_thirty_five) then |
---|
[313] | 628 | set_8051_sfr s SFR_PCON v |
---|
[350] | 629 | else if (eq_n address one_hundred_and_thirty_six) then |
---|
[313] | 630 | set_8051_sfr s SFR_TCON v |
---|
[350] | 631 | else if (eq_n address one_hundred_and_thirty_seven) then |
---|
[313] | 632 | set_8051_sfr s SFR_TMOD v |
---|
[350] | 633 | else if (eq_n address one_hundred_and_fifty_two) then |
---|
[313] | 634 | set_8051_sfr s SFR_SCON v |
---|
[350] | 635 | else if (eq_n address one_hundred_and_sixty_eight) then |
---|
[313] | 636 | set_8051_sfr s SFR_IE v |
---|
[350] | 637 | else if (eq_n address one_hundred_and_eighty_four) then |
---|
[313] | 638 | set_8051_sfr s SFR_IP v |
---|
[350] | 639 | else if (eq_n address one_hundred_and_twenty_nine) then |
---|
[313] | 640 | set_8051_sfr s SFR_SP v |
---|
[350] | 641 | else if (eq_n address one_hundred_and_thirty) then |
---|
[313] | 642 | set_8051_sfr s SFR_DPL v |
---|
[350] | 643 | else if (eq_n address one_hundred_and_thirty_one) then |
---|
[313] | 644 | set_8051_sfr s SFR_DPH v |
---|
[350] | 645 | else if (eq_n address two_hundred_and_eight) then |
---|
[313] | 646 | set_8051_sfr s SFR_PSW v |
---|
[350] | 647 | else if (eq_n address two_hundred_and_twenty_four) then |
---|
[313] | 648 | set_8051_sfr s SFR_ACC_A v |
---|
[350] | 649 | else if (eq_n address two_hundred_and_forty) then |
---|
[313] | 650 | set_8051_sfr s SFR_ACC_B v |
---|
[285] | 651 | else |
---|
| 652 | ?. |
---|
| 653 | ncases not_implemented. |
---|
[286] | 654 | nqed. |
---|
| 655 | |
---|
| 656 | ndefinition bit_address_of_register ≝ |
---|
| 657 | λs: Status. |
---|
[317] | 658 | λr: BitVector three. |
---|
[337] | 659 | let b ≝ get_index_bv ? r Z ? in |
---|
| 660 | let c ≝ get_index_bv ? r one ? in |
---|
| 661 | let d ≝ get_index_bv ? r two ? in |
---|
[286] | 662 | let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in |
---|
[337] | 663 | let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_bv four un two ?) (get_index_bv four un three ?) in |
---|
[286] | 664 | let offset ≝ |
---|
| 665 | if conjunction (negation r1) (negation r0) then |
---|
| 666 | Z |
---|
| 667 | else if conjunction (negation r1) r0 then |
---|
| 668 | eight |
---|
| 669 | else if conjunction r1 r0 then |
---|
| 670 | twenty_four |
---|
| 671 | else |
---|
| 672 | sixteen |
---|
| 673 | in |
---|
| 674 | bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])). |
---|
[317] | 675 | ##[##1,2,3,4,5: |
---|
| 676 | nnormalize; |
---|
| 677 | nrepeat (napply less_than_or_equal_monotone); |
---|
| 678 | napply less_than_or_equal_zero; |
---|
| 679 | ##] |
---|
[287] | 680 | nqed. |
---|
| 681 | |
---|
| 682 | ndefinition get_register ≝ |
---|
| 683 | λs: Status. |
---|
[317] | 684 | λr: BitVector three. |
---|
| 685 | let address ≝ bit_address_of_register s r in |
---|
[287] | 686 | lookup … address (low_internal_ram s) (zero eight). |
---|
| 687 | |
---|
| 688 | ndefinition set_register ≝ |
---|
| 689 | λs: Status. |
---|
[317] | 690 | λr: BitVector three. |
---|
[287] | 691 | λv: Byte. |
---|
[317] | 692 | let address ≝ bit_address_of_register s r in |
---|
[287] | 693 | let old_low_internal_ram ≝ low_internal_ram s in |
---|
| 694 | let new_low_internal_ram ≝ insert … address v old_low_internal_ram in |
---|
| 695 | set_low_internal_ram s new_low_internal_ram. |
---|
| 696 | |
---|
| 697 | ndefinition read_at_stack_pointer ≝ |
---|
| 698 | λs: Status. |
---|
| 699 | let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in |
---|
[343] | 700 | let m ≝ get_index_bv … nu Z ? in |
---|
| 701 | let r1 ≝ get_index_bv … nu one ? in |
---|
| 702 | let r2 ≝ get_index_bv … nu two ? in |
---|
| 703 | let r3 ≝ get_index_bv … nu three ? in |
---|
[287] | 704 | let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in |
---|
| 705 | let memory ≝ |
---|
| 706 | if m then |
---|
| 707 | (low_internal_ram s) |
---|
| 708 | else |
---|
| 709 | (high_internal_ram s) |
---|
| 710 | in |
---|
| 711 | lookup … address memory (zero eight). |
---|
| 712 | ##[##1,2,3,4: |
---|
| 713 | nnormalize; |
---|
| 714 | nrepeat (napply less_than_or_equal_monotone); |
---|
| 715 | napply less_than_or_equal_zero; |
---|
| 716 | ##] |
---|
[288] | 717 | nqed. |
---|
| 718 | |
---|
[289] | 719 | ndefinition write_at_stack_pointer ≝ |
---|
[288] | 720 | λs: Status. |
---|
| 721 | λv: Byte. |
---|
[289] | 722 | let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in |
---|
| 723 | let bit_zero ≝ get_index … nu Z ? in |
---|
| 724 | let bit_one ≝ get_index … nu one ? in |
---|
| 725 | let bit_two ≝ get_index … nu two ? in |
---|
| 726 | let bit_three ≝ get_index … nu three ? in |
---|
| 727 | if bit_zero then |
---|
| 728 | let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl) |
---|
| 729 | v (low_internal_ram s) in |
---|
| 730 | set_low_internal_ram s memory |
---|
| 731 | else |
---|
| 732 | let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl) |
---|
| 733 | v (high_internal_ram s) in |
---|
| 734 | set_high_internal_ram s memory. |
---|
| 735 | ##[##1,2,3,4: |
---|
| 736 | nnormalize; |
---|
| 737 | nrepeat (napply less_than_or_equal_monotone); |
---|
| 738 | napply less_than_or_equal_zero; |
---|
| 739 | ##] |
---|
[294] | 740 | nqed. |
---|
| 741 | |
---|
| 742 | ndefinition set_arg_16: Status → Word → [[ dptr ]] → Status ≝ |
---|
| 743 | λs,v,a. |
---|
| 744 | match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with |
---|
| 745 | [ DPTR ⇒ λ_:True. |
---|
| 746 | let 〈 bu, bl 〉 ≝ split … eight eight v in |
---|
| 747 | let status ≝ set_8051_sfr s SFR_DPH bu in |
---|
| 748 | let status ≝ set_8051_sfr status SFR_DPL bl in |
---|
| 749 | status |
---|
| 750 | | _ ⇒ λK. |
---|
| 751 | match K in False with |
---|
| 752 | [ |
---|
| 753 | ] |
---|
| 754 | ] (subaddressing_modein … a). |
---|
| 755 | |
---|
| 756 | ndefinition get_arg_16: Status → [[ data16 ]] → Word ≝ |
---|
| 757 | λs, a. |
---|
| 758 | match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with |
---|
| 759 | [ DATA16 d ⇒ λ_:True. d |
---|
| 760 | | _ ⇒ λK. |
---|
| 761 | match K in False with |
---|
| 762 | [ |
---|
| 763 | ] |
---|
[310] | 764 | ] (subaddressing_modein … a). |
---|
| 765 | |
---|
| 766 | ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ; |
---|
| 767 | acc_a ; acc_b ; data ; acc_dptr ; |
---|
| 768 | acc_pc ; ext_indirect ; |
---|
| 769 | ext_indirect_dptr ]] → Byte ≝ |
---|
| 770 | λs, l, a. |
---|
| 771 | match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ; |
---|
| 772 | acc_a ; acc_b ; data ; acc_dptr ; |
---|
| 773 | acc_pc ; ext_indirect ; |
---|
| 774 | ext_indirect_dptr ]] x) → ? with |
---|
[311] | 775 | [ ACC_A ⇒ λacc_a: True. get_8051_sfr s SFR_ACC_A |
---|
| 776 | | ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B |
---|
| 777 | | DATA d ⇒ λdata: True. d |
---|
[316] | 778 | | REGISTER r ⇒ λregister: True. get_register s r |
---|
[310] | 779 | | EXT_INDIRECT_DPTR ⇒ |
---|
[311] | 780 | λext_indirect_dptr: True. |
---|
[310] | 781 | let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in |
---|
| 782 | lookup … sixteen address (external_ram s) (zero eight) |
---|
| 783 | | EXT_INDIRECT e ⇒ |
---|
[311] | 784 | λext_indirect: True. |
---|
[317] | 785 | let address ≝ get_register s [[ false; false; e ]] in |
---|
[310] | 786 | let padded_address ≝ pad eight eight address in |
---|
[311] | 787 | lookup … sixteen padded_address (external_ram s) (zero eight) |
---|
[310] | 788 | | ACC_DPTR ⇒ |
---|
[311] | 789 | λacc_dptr: True. |
---|
[310] | 790 | let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in |
---|
| 791 | let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in |
---|
[313] | 792 | let 〈 carry, address 〉 ≝ half_add sixteen dptr padded_acc in |
---|
[310] | 793 | lookup … sixteen address (external_ram s) (zero eight) |
---|
| 794 | | ACC_PC ⇒ |
---|
[311] | 795 | λacc_pc: True. |
---|
[310] | 796 | let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in |
---|
[313] | 797 | let 〈 carry, address 〉 ≝ half_add sixteen (program_counter s) padded_acc in |
---|
[310] | 798 | lookup … sixteen address (external_ram s) (zero eight) |
---|
| 799 | | DIRECT d ⇒ |
---|
[311] | 800 | λdirect: True. |
---|
| 801 | let 〈 nu, nl 〉 ≝ split … four four d in |
---|
[343] | 802 | let bit_one ≝ get_index_bv … nu one ? in |
---|
[311] | 803 | match bit_one with |
---|
| 804 | [ true ⇒ |
---|
| 805 | let 〈 bit_one, three_bits 〉 ≝ split ? one three nu in |
---|
| 806 | let address ≝ three_bits @@ nl in |
---|
| 807 | lookup ? seven address (low_internal_ram s) (zero eight) |
---|
| 808 | | false ⇒ get_bit_addressable_sfr s eight d l |
---|
| 809 | ] |
---|
[310] | 810 | | INDIRECT i ⇒ |
---|
[311] | 811 | λindirect: True. |
---|
[317] | 812 | let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in |
---|
[311] | 813 | let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in |
---|
[343] | 814 | let bit_one ≝ get_index_bv … bit_one_v Z ? in |
---|
[311] | 815 | match bit_one with |
---|
| 816 | [ true ⇒ |
---|
| 817 | lookup ? seven (three_bits @@ nl) (low_internal_ram s) (zero eight) |
---|
| 818 | | false ⇒ |
---|
| 819 | lookup ? seven (three_bits @@ nl) (high_internal_ram s) (zero eight) |
---|
| 820 | ] |
---|
| 821 | | _ ⇒ λother. |
---|
| 822 | match other in False with [ ] |
---|
[310] | 823 | ] (subaddressing_modein … a). |
---|
[311] | 824 | ##[##1,2: |
---|
| 825 | nnormalize; |
---|
| 826 | nrepeat (napply less_than_or_equal_monotone); |
---|
| 827 | napply less_than_or_equal_zero; |
---|
| 828 | ##] |
---|
| 829 | nqed. |
---|
[313] | 830 | |
---|
[314] | 831 | ndefinition set_arg_8: Status → [[ direct ; indirect ; register ; |
---|
| 832 | acc_a ; acc_b ; ext_indirect ; |
---|
| 833 | ext_indirect_dptr ]] → Byte → Status ≝ |
---|
| 834 | λs, a, v. |
---|
| 835 | match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ; |
---|
| 836 | acc_a ; acc_b ; ext_indirect ; |
---|
| 837 | ext_indirect_dptr ]] x) → ? with |
---|
| 838 | [ DIRECT d ⇒ |
---|
| 839 | λdirect: True. |
---|
| 840 | let 〈 nu, nl 〉 ≝ split … four four d in |
---|
[343] | 841 | let bit_one ≝ get_index_bv … nu one ? in |
---|
[314] | 842 | let 〈 ignore, three_bits 〉 ≝ split ? one three nu in |
---|
| 843 | match bit_one with |
---|
| 844 | [ true ⇒ set_bit_addressable_sfr s d v |
---|
| 845 | | false ⇒ |
---|
| 846 | let memory ≝ insert ? seven (three_bits @@ nl) v (low_internal_ram s) in |
---|
| 847 | set_low_internal_ram s memory |
---|
| 848 | ] |
---|
| 849 | | INDIRECT i ⇒ |
---|
| 850 | λindirect: True. |
---|
[317] | 851 | let register ≝ get_register s [[ false; false; i ]] in |
---|
[314] | 852 | let 〈 nu, nl 〉 ≝ split ? four four register in |
---|
[343] | 853 | let bit_one ≝ get_index_bv ? nu one ? in |
---|
[314] | 854 | let 〈 ignore, three_bits 〉 ≝ split ? one three nu in |
---|
| 855 | match bit_one with |
---|
| 856 | [ true ⇒ |
---|
| 857 | let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in |
---|
| 858 | set_low_internal_ram s memory |
---|
| 859 | | false ⇒ |
---|
| 860 | let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in |
---|
| 861 | set_high_internal_ram s memory |
---|
| 862 | ] |
---|
[317] | 863 | | REGISTER r ⇒ λregister: True. set_register s r v |
---|
[314] | 864 | | ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v |
---|
| 865 | | ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v |
---|
| 866 | | EXT_INDIRECT e ⇒ |
---|
| 867 | λext_indirect: True. |
---|
[317] | 868 | let address ≝ get_register s [[ false; false; e ]] in |
---|
[314] | 869 | let padded_address ≝ pad eight eight address in |
---|
| 870 | let memory ≝ insert ? sixteen padded_address v (external_ram s) in |
---|
| 871 | set_external_ram s memory |
---|
| 872 | | EXT_INDIRECT_DPTR ⇒ |
---|
| 873 | λext_indirect_dptr: True. |
---|
| 874 | let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in |
---|
| 875 | let memory ≝ insert ? sixteen address v (external_ram s) in |
---|
| 876 | set_external_ram s memory |
---|
| 877 | | _ ⇒ |
---|
| 878 | λother: False. |
---|
| 879 | match other in False with [ ] |
---|
| 880 | ] (subaddressing_modein … a). |
---|
| 881 | ##[##1,2: |
---|
| 882 | nnormalize; |
---|
| 883 | nrepeat (napply less_than_or_equal_monotone); |
---|
| 884 | napply less_than_or_equal_zero |
---|
| 885 | ##] |
---|
| 886 | nqed. |
---|
| 887 | |
---|
[351] | 888 | ntheorem modulus_less_than: |
---|
| 889 | ∀m,n: Nat. (m mod (S n)) < S n. |
---|
| 890 | #n m; nnormalize; napply less_than_or_equal_monotone; |
---|
| 891 | nlapply (ltoe_refl n); |
---|
| 892 | ngeneralize in ⊢ (?%? → ?(??%?)?); |
---|
| 893 | nelim n in ⊢ (∀_:?. ??% → ?(?%??)?) |
---|
| 894 | [ nnormalize; #n; napply (less_than_or_equal_b_elim n m); nnormalize |
---|
[352] | 895 | [ // | #H K; ninversion K [ #H1; nrewrite < H1; // | #x H1 H2 H3; ndestruct ]##] |
---|
[351] | 896 | ##| nnormalize; #y H1 n H2; napply (less_than_or_equal_b_elim n m); nnormalize |
---|
| 897 | [ // | #K; napply H1; ncut (n ≤ S y → n - S m ≤ y); /2/; |
---|
| 898 | ncases n; nnormalize; //; |
---|
| 899 | #x K1; nlapply (less_than_or_equal_injective … K1); ngeneralize in match m; |
---|
| 900 | nelim x; nnormalize; //; #w1 H m; ncases m; nnormalize; //; |
---|
| 901 | #q K2; napply H; /3/] |
---|
| 902 | nqed. |
---|
[314] | 903 | |
---|
[313] | 904 | ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] → |
---|
| 905 | Bool → Bool ≝ |
---|
| 906 | λs, a, l. |
---|
| 907 | match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; |
---|
| 908 | n_bit_addr ; |
---|
| 909 | carry ]] x) → ? with |
---|
| 910 | [ BIT_ADDR b ⇒ |
---|
| 911 | λbit_addr: True. |
---|
| 912 | let 〈 nu, nl 〉 ≝ split … four four b in |
---|
[343] | 913 | let bit_one ≝ get_index_bv … nu one ? in |
---|
[313] | 914 | let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in |
---|
| 915 | match bit_one with |
---|
| 916 | [ true ⇒ |
---|
| 917 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
| 918 | let d ≝ address ÷ eight in |
---|
| 919 | let m ≝ address mod eight in |
---|
[314] | 920 | let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in |
---|
[313] | 921 | let sfr ≝ get_bit_addressable_sfr s ? trans l in |
---|
[343] | 922 | get_index_bv ? sfr m ? |
---|
[313] | 923 | | false ⇒ |
---|
| 924 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
[314] | 925 | let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in |
---|
[313] | 926 | let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in |
---|
[343] | 927 | get_index_bv ? t (modulus address eight) ? |
---|
[313] | 928 | ] |
---|
| 929 | | N_BIT_ADDR n ⇒ |
---|
| 930 | λn_bit_addr: True. |
---|
| 931 | let 〈 nu, nl 〉 ≝ split … four four n in |
---|
[343] | 932 | let bit_one ≝ get_index_bv … nu one ? in |
---|
[313] | 933 | let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in |
---|
| 934 | match bit_one with |
---|
| 935 | [ true ⇒ |
---|
| 936 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
| 937 | let d ≝ address ÷ eight in |
---|
| 938 | let m ≝ address mod eight in |
---|
[314] | 939 | let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in |
---|
[313] | 940 | let sfr ≝ get_bit_addressable_sfr s ? trans l in |
---|
[343] | 941 | negation (get_index_bv ? sfr m ?) |
---|
[313] | 942 | | false ⇒ |
---|
| 943 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
[314] | 944 | let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in |
---|
[313] | 945 | let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in |
---|
[343] | 946 | negation (get_index_bv ? trans (modulus address eight) ?) |
---|
[313] | 947 | ] |
---|
| 948 | | CARRY ⇒ λcarry: True. get_cy_flag s |
---|
| 949 | | _ ⇒ λother. |
---|
| 950 | match other in False with [ ] |
---|
[314] | 951 | ] (subaddressing_modein … a). |
---|
| 952 | ##[##3,6: |
---|
| 953 | nnormalize; |
---|
| 954 | nrepeat (napply less_than_or_equal_monotone); |
---|
| 955 | napply less_than_or_equal_zero; |
---|
| 956 | ##|##1,2,4,5: |
---|
| 957 | napply modulus_less_than; |
---|
| 958 | ##] |
---|
| 959 | nqed. |
---|
| 960 | |
---|
| 961 | ndefinition set_arg_1: Status → [[ bit_addr ; carry ]] → |
---|
| 962 | Bit → Status ≝ |
---|
[313] | 963 | λs, a, v. |
---|
[314] | 964 | match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with |
---|
| 965 | [ BIT_ADDR b ⇒ λbit_addr: True. |
---|
| 966 | let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in |
---|
[343] | 967 | let bit_one ≝ get_index_bv ? nu one ? in |
---|
[313] | 968 | let 〈 ignore, three_bits 〉 ≝ split ? one three nu in |
---|
[314] | 969 | match bit_one with |
---|
| 970 | [ true ⇒ |
---|
| 971 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
| 972 | let d ≝ address ÷ eight in |
---|
| 973 | let m ≝ address mod eight in |
---|
| 974 | let t ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in |
---|
| 975 | let sfr ≝ get_bit_addressable_sfr s ? t true in |
---|
| 976 | let new_sfr ≝ set_index … sfr m v ? in |
---|
| 977 | set_bit_addressable_sfr s new_sfr t |
---|
| 978 | | false ⇒ |
---|
| 979 | let address ≝ nat_of_bitvector … (three_bits @@ nl) in |
---|
| 980 | let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in |
---|
| 981 | let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in |
---|
| 982 | let n_bit ≝ set_index … t (modulus address eight) v ? in |
---|
| 983 | let memory ≝ insert ? seven address' n_bit (low_internal_ram s) in |
---|
[313] | 984 | set_low_internal_ram s memory |
---|
[314] | 985 | ] |
---|
| 986 | | CARRY ⇒ |
---|
| 987 | λcarry: True. |
---|
| 988 | let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in |
---|
| 989 | let bit_one ≝ get_index … nu one ? in |
---|
| 990 | let bit_two ≝ get_index … nu two ? in |
---|
| 991 | let bit_three ≝ get_index … nu three ? in |
---|
| 992 | let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in |
---|
| 993 | set_8051_sfr s SFR_PSW new_psw |
---|
[313] | 994 | | _ ⇒ |
---|
| 995 | λother: False. |
---|
[314] | 996 | match other in False with |
---|
| 997 | [ ] |
---|
| 998 | ] (subaddressing_modein … a). |
---|
| 999 | ##[##1,2,3,6: |
---|
| 1000 | nnormalize; |
---|
| 1001 | nrepeat (napply less_than_or_equal_monotone); |
---|
| 1002 | napply less_than_or_equal_zero; |
---|
| 1003 | ##|##4,5: |
---|
[351] | 1004 | napply modulus_less_than; |
---|
[314] | 1005 | ##] |
---|
[345] | 1006 | nqed. |
---|
| 1007 | |
---|
| 1008 | ndefinition load_code_memory ≝ |
---|
[350] | 1009 | fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen). |
---|
[345] | 1010 | |
---|
| 1011 | ndefinition load ≝ |
---|
[351] | 1012 | λl,status. set_code_memory status (load_code_memory l). |
---|