source: Deliverables/D4.1/Matita/Interpret.ma @ 367

Last change on this file since 367 was 367, checked in by mulligan, 9 years ago

Added decidable equality for addressing_mode_tags.

File size: 27.0 KB
Line 
1include "Status.ma".
2include "Fetch.ma".
3
4ndefinition sign_extension: Byte → Word ≝
5  λb.
6    zero eight @@ b.
7   
8naxiom eq_a: addressing_mode_tag → addressing_mode_tag → Bool.
9   
10naxiom execute_1_technical:
11  ∀n,m: Nat.
12  ∀v: Vector addressing_mode_tag (S n).
13  ∀q: Vector addressing_mode_tag (S m).
14  ∀a: addressing_mode.
15    bool_to_Prop (is_in ? v a) →
16    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
17    bool_to_Prop (is_in ? q a).
18   
19ndefinition execute_1: Status → Status ≝
20  λs.
21    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
22    let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in
23    let s ≝ set_clock s (clock s + ticks) in
24    let s ≝ set_program_counter s pc in
25    let s ≝
26      match instr with
27        [ ADD addr1 addr2 ⇒
28            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
29                                                   (get_arg_8 s false addr2) false in
30            let cy_flag ≝ get_index' ? Z  ? flags in
31            let ac_flag ≝ get_index' ? one ? flags in
32            let ov_flag ≝ get_index' ? two ? flags in
33            let s ≝ set_arg_8 s ACC_A result in
34              set_flags s cy_flag (Just Bit ac_flag) ov_flag
35        | ADDC addr1 addr2 ⇒
36            let old_cy_flag ≝ get_cy_flag s in
37            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
38                                                   (get_arg_8 s false addr2) old_cy_flag in
39            let cy_flag ≝ get_index' ? Z ? flags in
40            let ac_flag ≝ get_index' ? one ? flags in
41            let ov_flag ≝ get_index' ? two ? flags in
42            let s ≝ set_arg_8 s ACC_A result in
43              set_flags s cy_flag (Just Bit ac_flag) ov_flag
44        | SUBB addr1 addr2 ⇒
45            let old_cy_flag ≝ get_cy_flag s in
46            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
47                                                   (get_arg_8 s false addr2) old_cy_flag in
48            let cy_flag ≝ get_index' ? Z ? flags in
49            let ac_flag ≝ get_index' ? one ? flags in
50            let ov_flag ≝ get_index' ? two ? flags in
51            let s ≝ set_arg_8 s ACC_A result in
52              set_flags s cy_flag (Just Bit ac_flag) ov_flag
53        | ANL addr ⇒
54          match addr with
55            [ Left l ⇒
56              match l with
57                [ Left l' ⇒
58                  let 〈addr1, addr2〉 ≝ l' in
59                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
60                    set_arg_8 s addr1 and_val
61                | Right r ⇒
62                  let 〈addr1, addr2〉 ≝ r in
63                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
64                    set_arg_8 s addr1 and_val
65                ]
66            | Right r ⇒
67              let 〈addr1, addr2〉 ≝ r in
68              let and_val ≝ conjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
69                set_flags s and_val (Nothing ?) (get_ov_flag s)
70            ]
71        | ORL addr ⇒
72          match addr with
73            [ Left l ⇒
74              match l with
75                [ Left l' ⇒
76                  let 〈addr1, addr2〉 ≝ l' in
77                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
78                    set_arg_8 s addr1 or_val
79                | Right r ⇒
80                  let 〈addr1, addr2〉 ≝ r in
81                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
82                    set_arg_8 s addr1 or_val
83                ]
84            | Right r ⇒
85              let 〈addr1, addr2〉 ≝ r in
86              let or_val ≝ inclusive_disjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
87                set_flags s or_val (Nothing ?) (get_ov_flag s)
88            ]
89        | XRL addr ⇒
90          match addr with
91            [ Left l' ⇒
92              let 〈addr1, addr2〉 ≝ l' in
93              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
94                set_arg_8 s addr1 xor_val
95            | Right r ⇒
96              let 〈addr1, addr2〉 ≝ r in
97              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
98                set_arg_8 s addr1 xor_val
99            ]
100        | INC addr ⇒
101            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
102                                                           register;
103                                                           direct;
104                                                           indirect;
105                                                           dptr ]] x) → ? with
106              [ ACC_A ⇒ λacc_a: True.
107                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat eight one) in
108                  set_arg_8 s ACC_A result
109              | REGISTER r ⇒ λregister: True.
110                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat eight one) in
111                  set_arg_8 s (REGISTER r) result
112              | DIRECT d ⇒ λdirect: True.
113                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat eight one) in
114                  set_arg_8 s (DIRECT d) result
115              | INDIRECT i ⇒ λindirect: True.
116                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat eight one) in
117                  set_arg_8 s (INDIRECT i) result
118              | DPTR ⇒ λdptr: True.
119                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat eight one) in
120                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero eight) carry in
121                let s ≝ set_8051_sfr s SFR_DPL bl in
122                  set_8051_sfr s SFR_DPH bu
123              | _ ⇒ λother: False. ⊥
124              ] (subaddressing_modein … addr)
125       | DEC addr ⇒
126           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat eight one) false in
127             set_arg_8 s addr result
128        | MUL addr1 addr2 ⇒
129           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
130           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
131           let product ≝ acc_a_nat * acc_b_nat in
132           let ov_flag ≝ product ≥ two_hundred_and_fifty_six in
133           let low ≝ bitvector_of_nat eight (product mod two_hundred_and_fifty_six) in
134           let high ≝ bitvector_of_nat eight (product ÷ two_hundred_and_fifty_six) in
135           let s ≝ set_8051_sfr s SFR_ACC_A low in
136             set_8051_sfr s SFR_ACC_B high
137        | DIV addr1 addr2 ⇒
138           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
139           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
140             match acc_b_nat with
141               [ Z ⇒ set_flags s false (Nothing Bit) true
142               | S o ⇒
143                 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in
144                 let r ≝ bitvector_of_nat eight (acc_a_nat mod two_hundred_and_fifty_six) in
145                 let s ≝ set_8051_sfr s SFR_ACC_A q in
146                 let s ≝ set_8051_sfr s SFR_ACC_B r in
147                   set_flags s false (Nothing Bit) false
148               ]
149        | DA addr ⇒
150            let 〈 acc_nu, acc_nl 〉 ≝ split ? four four (get_8051_sfr s SFR_ACC_A) in
151              if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then
152                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in
153                let cy_flag ≝ get_index' ? Z ? flags in
154                let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in
155                  if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then
156                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat four six) in
157                    let new_acc ≝ nu @@ acc_nl' in
158                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
159                      set_flags s cy_flag (Just ? (get_ac_flag s)) (get_ov_flag s)
160                  else
161                    s
162              else
163                s
164        | CLR addr ⇒
165          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
166            [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero eight)
167            | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
168            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
169            | _ ⇒ λother: False. ⊥
170            ] (subaddressing_modein … addr)
171        | CPL addr ⇒
172          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
173            [ ACC_A ⇒ λacc_a: True.
174                let old_acc ≝ get_8051_sfr s SFR_ACC_A in
175                let new_acc ≝ negation_bv ? old_acc in
176                  set_8051_sfr s SFR_ACC_A new_acc
177            | CARRY ⇒ λcarry: True.
178                let old_cy_flag ≝ get_arg_1 s CARRY true in
179                let new_cy_flag ≝ negation old_cy_flag in
180                  set_arg_1 s CARRY new_cy_flag
181            | BIT_ADDR b ⇒ λbit_addr: True.
182                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
183                let new_bit ≝ negation old_bit in
184                  set_arg_1 s (BIT_ADDR b) new_bit
185            | _ ⇒ λother: False. ?
186            ] (subaddressing_modein … addr)
187        | SETB b ⇒ set_arg_1 s b false
188        | RL _ ⇒ (* DPM: always ACC_A *)
189            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
190            let new_acc ≝ rotate_left … one old_acc in
191              set_8051_sfr s SFR_ACC_A new_acc
192        | RR _ ⇒ (* DPM: always ACC_A *)
193            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
194            let new_acc ≝ rotate_right … one old_acc in
195              set_8051_sfr s SFR_ACC_A new_acc
196        | RLC _ ⇒ (* DPM: always ACC_A *)
197            let old_cy_flag ≝ get_cy_flag s in
198            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
199            let new_cy_flag ≝ get_index' ? Z ? old_acc in
200            let new_acc ≝ shift_left ? eight one old_acc old_cy_flag in
201            let s ≝ set_arg_1 s CARRY new_cy_flag in
202              set_8051_sfr s SFR_ACC_A new_acc
203        | RRC _ ⇒ (* DPM: always ACC_A *)
204            let old_cy_flag ≝ get_cy_flag s in
205            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
206            let new_cy_flag ≝ get_index' ? seven ? old_acc in
207            let new_acc ≝ shift_right ? eight one old_acc old_cy_flag in
208            let s ≝ set_arg_1 s CARRY new_cy_flag in
209              set_8051_sfr s SFR_ACC_A new_acc
210        | SWAP _ ⇒ (* DPM: always ACC_A *)
211            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
212            let 〈nu,nl〉 ≝ split ? four four old_acc in
213            let new_acc ≝ nl @@ nu in
214              set_8051_sfr s SFR_ACC_A new_acc
215        | PUSH addr ⇒
216            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
217              [ DIRECT d ⇒ λdirect: True.
218                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
219                let s ≝ set_8051_sfr s SFR_SP new_sp in
220                  write_at_stack_pointer s d
221              | _ ⇒ λother: False. ⊥
222              ] (subaddressing_modein … addr)
223        | POP addr ⇒
224            let contents ≝ read_at_stack_pointer s in
225            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
226            let s ≝ set_8051_sfr s SFR_SP new_sp in
227              set_arg_8 s addr contents
228        | XCH addr1 addr2 ⇒
229            let old_addr ≝ get_arg_8 s false addr2 in
230            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
231            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
232              set_arg_8 s addr2 old_acc
233        | XCHD addr1 addr2 ⇒
234            let 〈acc_nu, acc_nl〉 ≝ split … four four (get_8051_sfr s SFR_ACC_A) in
235            let 〈arg_nu, arg_nl〉 ≝ split … four four (get_arg_8 s false addr2) in
236            let new_acc ≝ acc_nu @@ arg_nl in
237            let new_arg ≝ arg_nu @@ acc_nl in
238            let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
239              set_arg_8 s addr2 new_arg
240        | RET ⇒
241            let high_bits ≝ read_at_stack_pointer s in
242            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
243            let s ≝ set_8051_sfr s SFR_SP new_sp in
244            let low_bits ≝ read_at_stack_pointer s in
245            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
246            let s ≝ set_8051_sfr s SFR_SP new_sp in
247            let new_pc ≝ high_bits @@ low_bits in
248              set_program_counter s new_pc
249        | RETI ⇒
250            let high_bits ≝ read_at_stack_pointer s in
251            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
252            let s ≝ set_8051_sfr s SFR_SP new_sp in
253            let low_bits ≝ read_at_stack_pointer s in
254            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
255            let s ≝ set_8051_sfr s SFR_SP new_sp in
256            let new_pc ≝ high_bits @@ low_bits in
257              set_program_counter s new_pc
258        | Jump j ⇒
259          match j with
260            [ JC addr ⇒
261              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
262                [ RELATIVE r ⇒ λrel: True.
263                  if get_cy_flag s then
264                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
265                      set_program_counter s new_pc
266                  else
267                    s
268                | _ ⇒ λother: False. ⊥
269                ] (subaddressing_modein … addr)
270            | JNC addr ⇒
271              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
272                [ RELATIVE r ⇒ λrel: True.
273                  if negation (get_cy_flag s) then
274                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
275                      set_program_counter s new_pc
276                  else
277                    s
278                | _ ⇒ λother: False. ⊥
279                ] (subaddressing_modein … addr)
280            | JB addr1 addr2 ⇒
281              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
282                [ RELATIVE r ⇒ λrel: True.
283                  if get_arg_1 s addr1 false then
284                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
285                      set_program_counter s new_pc
286                  else
287                    s
288                | _ ⇒ λother: False. ⊥
289                ] (subaddressing_modein … addr2)
290            | JNB addr1 addr2 ⇒
291              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
292                [ RELATIVE r ⇒ λrel: True.
293                  if negation (get_arg_1 s addr1 false) then
294                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
295                      set_program_counter s new_pc
296                  else
297                    s
298                | _ ⇒ λother: False. ⊥
299                ] (subaddressing_modein … addr2)
300            | JBC addr1 addr2 ⇒
301              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
302                [ RELATIVE r ⇒ λrel: True.
303                  let s ≝ set_arg_1 s addr1 false in
304                    if get_arg_1 s addr1 false then
305                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
306                        set_program_counter s new_pc
307                    else
308                      s
309                | _ ⇒ λother: False. ⊥
310                ] (subaddressing_modein … addr2)
311            | JZ addr ⇒
312              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
313                [ RELATIVE r ⇒ λrel: True.
314                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight) then
315                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
316                        set_program_counter s new_pc
317                    else
318                      s
319                | _ ⇒ λother: False. ⊥
320                ] (subaddressing_modein … addr)
321            | JNZ addr ⇒
322              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
323                [ RELATIVE r ⇒ λrel: True.
324                    if negation (eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight)) then
325                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
326                        set_program_counter s new_pc
327                    else
328                      s
329                | _ ⇒ λother: False. ⊥
330                ] (subaddressing_modein … addr)
331            | CJNE addr1 addr2 ⇒
332              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
333                [ RELATIVE r ⇒ λrelative: True.
334                  match addr1 with
335                    [ Left l ⇒
336                        let 〈addr1, addr2〉 ≝ l in
337                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
338                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
339                          if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
340                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
341                            let s ≝ set_program_counter s new_pc in
342                              set_flags s new_cy (Nothing ?) (get_ov_flag s)
343                          else
344                            (set_flags s new_cy (Nothing ?) (get_ov_flag s))
345                    | Right r' ⇒
346                        let 〈addr1, addr2〉 ≝ r' in
347                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
348                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
349                          if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
350                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
351                            let s ≝ set_program_counter s new_pc in
352                              set_flags s new_cy (Nothing ?) (get_ov_flag s)
353                          else
354                            (set_flags s new_cy (Nothing ?) (get_ov_flag s))
355                    ]
356                | _ ⇒ λother: False. ⊥
357                ] (subaddressing_modein … addr2)
358            | DJNZ addr1 addr2 ⇒
359              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
360                [ RELATIVE r ⇒ λrel: True.
361                    let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat eight one) false in
362                    let s ≝ set_arg_8 s addr1 result in
363                      if negation (eq_bv ? result (zero eight)) then
364                        let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
365                          set_program_counter s new_pc
366                      else
367                        s
368                | _ ⇒ λother: False. ⊥
369                ] (subaddressing_modein … addr2)
370            ]
371        | JMP _ ⇒ (* DPM: always indirect_dptr *)
372          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
373          let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
374          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
375          let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
376            set_program_counter s new_pc
377        | LJMP addr ⇒
378          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
379            [ ADDR16 a ⇒ λaddr16: True.
380                set_program_counter s a
381            | _ ⇒ λother: False. ⊥
382            ] (subaddressing_modein … addr)
383        | SJMP addr ⇒
384          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
385            [ RELATIVE r ⇒ λrelative: True.
386                let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
387                  set_program_counter s new_pc
388            | _ ⇒ λother: False. ⊥
389            ] (subaddressing_modein … addr)
390        | AJMP addr ⇒
391          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
392            [ ADDR11 a ⇒ λaddr11: True.
393              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
394              let 〈nu, nl〉 ≝ split ? four four pc_bu in
395              let bit ≝ get_index' ? Z ? nl in
396              let 〈relevant1, relevant2〉 ≝ split ? three eight a in
397              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
398              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
399                set_program_counter s new_pc
400            | _ ⇒ λother: False. ⊥
401            ] (subaddressing_modein … addr)
402        | MOVC addr1 addr2 ⇒
403          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
404            [ ACC_DPTR ⇒ λacc_dptr: True.
405              let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
406              let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
407              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
408              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
409                set_8051_sfr s SFR_ACC_A result
410            | ACC_PC ⇒ λacc_pc: True.
411              let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
412              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat sixteen one) in
413              (* DPM: Under specified: does the carry from PC incrementation affect the *)
414              (*      addition of the PC with the DPTR? At the moment, no.              *)
415              let s ≝ set_program_counter s inc_pc in
416              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
417              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
418                set_8051_sfr s SFR_ACC_A result
419            | _ ⇒ λother: False. ⊥
420            ] (subaddressing_modein … addr2)
421        | MOVX addr ⇒
422          (* DPM: only copies --- doesn't affect I/O *)
423          match addr with
424            [ Left l ⇒
425              let 〈addr1, addr2〉 ≝ l in
426                set_arg_8 s addr1 (get_arg_8 s false addr2)
427            | Right r ⇒
428              let 〈addr1, addr2〉 ≝ r in
429                set_arg_8 s addr1 (get_arg_8 s false addr2)
430            ]
431        | MOV addr ⇒
432          match addr with
433            [ Left l ⇒
434              match l with
435                [ Left l' ⇒
436                  match l' with
437                    [ Left l'' ⇒
438                      match l'' with
439                        [ Left l''' ⇒
440                          match l''' with
441                            [ Left l'''' ⇒
442                              let 〈addr1, addr2〉 ≝ l'''' in
443                                set_arg_8 s addr1 (get_arg_8 s false addr2)
444                            | Right r'''' ⇒
445                              let 〈addr1, addr2〉 ≝ r'''' in
446                                set_arg_8 s addr1 (get_arg_8 s false addr2)
447                            ]
448                        | Right r''' ⇒
449                          let 〈addr1, addr2〉 ≝ r''' in
450                            set_arg_8 s addr1 (get_arg_8 s false addr2)
451                        ]
452                    | Right r'' ⇒
453                      let 〈addr1, addr2〉 ≝ r'' in
454                        set_arg_16 s (get_arg_16 s addr2) addr1
455                    ]
456                | Right r ⇒
457                  let 〈addr1, addr2〉 ≝ r in
458                    set_arg_1 s addr1 (get_arg_1 s addr2 false)
459                ]
460            | Right r ⇒
461              let 〈addr1, addr2〉 ≝ r in
462                set_arg_1 s addr1 (get_arg_1 s addr2 false)
463            ]
464        | LCALL addr ⇒
465          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
466            [ ADDR16 a ⇒ λaddr16: True.
467              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
468              let s ≝ set_8051_sfr s SFR_SP new_sp in
469              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
470              let s ≝ write_at_stack_pointer s pc_bl in
471              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
472              let s ≝ set_8051_sfr s SFR_SP new_sp in
473              let s ≝ write_at_stack_pointer s pc_bu in
474                set_program_counter s a
475            | _ ⇒ λother: False. ⊥
476            ] (subaddressing_modein … addr)
477        | ACALL addr ⇒
478          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
479            [ ADDR11 a ⇒ λaddr11: True.
480              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
481              let s ≝ set_8051_sfr s SFR_SP new_sp in
482              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
483              let s ≝ write_at_stack_pointer s pc_bl in
484              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
485              let s ≝ set_8051_sfr s SFR_SP new_sp in
486              let s ≝ write_at_stack_pointer s pc_bu in
487              let 〈thr, eig〉 ≝ split ? three eight a in
488              let 〈fiv, thr'〉 ≝ split ? five three pc_bu in
489              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
490                set_program_counter s new_addr
491            | _ ⇒ λother: False. ⊥
492            ] (subaddressing_modein … addr)
493        | NOP ⇒ s
494        ]
495    in
496      s.
497    ##[ ntry
498          nassumption;
499    ##| ntry (
500          nnormalize
501          nrepeat (napply (less_than_or_equal_monotone))
502          napply (less_than_or_equal_zero)
503        );
504    ##| ntry (
505          nnormalize
506          //
507        );
508    ##| ntry (
509          nnormalize
510          //);
511    ##| napply (execute_1_technical ? ? [[ acc_a ]]
512                                        [[ direct; indirect; register;
513                                           acc_a; acc_b; data; acc_dptr;
514                                           acc_pc; ext_indirect;
515                                           ext_indirect_dptr ]] ACC_A).
516nqed.
517
518nlet rec execute (n: Nat) (s: Status) on n: Status ≝
519  match n with
520    [ Z ⇒ s
521    | S o ⇒ execute o (execute_1 s)
522    ].
Note: See TracBrowser for help on using the repository browser.