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

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

Work on main execution loop. All cases covered. Need to close open proof states and remove computational axioms.

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