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

Last change on this file since 347 was 347, checked in by mulligan, 10 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.