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

Last change on this file since 362 was 362, checked in by sacerdot, 9 years ago

Less ambiguous definitions.

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