source: src/ASM/Interpret.ma @ 757

Last change on this file since 757 was 757, checked in by mulligan, 10 years ago

Lots more fixing to get both front and backends using same conventions and types.

File size: 28.1 KB
Line 
1include "ASM/Status.ma".
2include "ASM/Fetch.ma".
3
4definition sign_extension: Byte → Word ≝
5  λc.
6    let b ≝ get_index_v ? 8 c 1 ? in
7      [[ b; b; b; b; b; b; b; b ]] @@ c.
8  normalize;
9  repeat (@ (le_S_S ?));
10  @ (le_O_n);
11qed.
12   
13lemma inclusive_disjunction_true:
14  ∀b, c: bool.
15    (orb b c) = true → b = true ∨ c = true.
16  # b
17  # c
18  elim b
19  [ normalize
20    # H
21    @ or_introl
22    %
23  | normalize
24    /2/
25  ]
26qed.
27
28lemma conjunction_true:
29  ∀b, c: bool.
30    andb b c = true → b = true ∧ c = true.
31  # b
32  # c
33  elim b
34  normalize
35  [ /2/
36  | # K
37    destruct
38  ]
39qed.
40
41lemma eq_true_false: false=true → False.
42 # K
43 destruct
44qed.
45
46lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
47 # a
48 # b
49 cases a
50 cases b
51 normalize
52 //
53 # K
54 cases (eq_true_false K)
55qed.
56
57lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
58 # b
59 cases b
60 %
61qed.
62
63lemma is_a_to_mem_to_is_in:
64 ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
65 # he
66 # a
67 # m
68 # q
69 elim q
70 [ normalize
71   # _
72   # K
73   assumption
74 | # m'
75   # t
76   # q'
77   # II
78   # H1
79   # H2
80   normalize
81   change in H2: (??%?) with (orb ??)
82   cases (inclusive_disjunction_true … H2)
83   [ # K
84     < (eq_a_to_eq … K)
85     > H1
86     %
87   | # K
88     > II
89     try assumption
90     cases (is_a t a)
91     normalize
92     %
93   ]
94 ]
95qed.
96
97lemma execute_1_technical:
98  ∀n, m: nat.
99  ∀v: Vector addressing_mode_tag (S n).
100  ∀q: Vector addressing_mode_tag (S m).
101  ∀a: addressing_mode.
102    bool_to_Prop (is_in ? v a) →
103    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
104    bool_to_Prop (is_in ? q a).
105 # n
106 # m
107 # v
108 # q
109 # a
110 elim v
111 [ normalize
112   # K
113   cases K
114 | # n'
115   # he
116   # tl
117   # II
118   whd in ⊢ (% → ? → ?)
119   lapply (refl … (is_in … (he:::tl) a))
120   cases (is_in … (he:::tl) a) in ⊢ (???% → %)
121   [ # K
122     # _
123     normalize in K;
124     whd in ⊢ (% → ?)
125     lapply (refl … (subvector_with … eq_a (he:::tl) q))
126     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
127     [ # K1
128       # _
129       change in K1 with ((andb ? (subvector_with …)) = true)
130       cases (conjunction_true … K1)
131       # K3
132       # K4
133       cases (inclusive_disjunction_true … K)
134       # K2
135       [ > (is_a_to_mem_to_is_in … K2 K3)
136         %
137       | @ II
138         [ > K2
139           %
140         | > K4
141           %
142         ]
143       ]
144     | # K1
145       # K2
146       (normalize in K2)
147       cases K2;
148     ]
149   | # K1
150     # K2
151     normalize in K2;
152     cases K2
153   ]
154 ]
155qed.
156
157include alias "arithmetics/nat.ma".
158include alias "ASM/BitVectorTrie.ma".
159
160definition execute_1: Status → Status ≝
161  λs: Status.
162    let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counter s) in
163    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
164    let s ≝ set_clock s (clock s + ticks) in
165    let s ≝ set_program_counter s pc in
166    let s ≝
167      match instr with
168        [ ADD addr1 addr2 ⇒
169            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
170                                                   (get_arg_8 s false addr2) false in
171            let cy_flag ≝ get_index' ? O  ? flags in
172            let ac_flag ≝ get_index' ? 1 ? flags in
173            let ov_flag ≝ get_index' ? 2 ? flags in
174            let s ≝ set_arg_8 s ACC_A result in
175              set_flags s cy_flag (Some Bit ac_flag) ov_flag
176        | ADDC addr1 addr2 ⇒
177            let old_cy_flag ≝ get_cy_flag s in
178            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
179                                                   (get_arg_8 s false addr2) old_cy_flag in
180            let cy_flag ≝ get_index' ? O ? flags in
181            let ac_flag ≝ get_index' ? 1 ? flags in
182            let ov_flag ≝ get_index' ? 2 ? flags in
183            let s ≝ set_arg_8 s ACC_A result in
184              set_flags s cy_flag (Some Bit ac_flag) ov_flag
185        | SUBB addr1 addr2 ⇒
186            let old_cy_flag ≝ get_cy_flag s in
187            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
188                                                   (get_arg_8 s false addr2) old_cy_flag in
189            let cy_flag ≝ get_index' ? O ? flags in
190            let ac_flag ≝ get_index' ? 1 ? flags in
191            let ov_flag ≝ get_index' ? 2 ? flags in
192            let s ≝ set_arg_8 s ACC_A result in
193              set_flags s cy_flag (Some Bit ac_flag) ov_flag
194        | ANL addr ⇒
195          match addr with
196            [ inl l ⇒
197              match l with
198                [ inl l' ⇒
199                  let 〈addr1, addr2〉 ≝ l' in
200                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
201                    set_arg_8 s addr1 and_val
202                | inr r ⇒
203                  let 〈addr1, addr2〉 ≝ r in
204                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
205                    set_arg_8 s addr1 and_val
206                ]
207            | inr r ⇒
208              let 〈addr1, addr2〉 ≝ r in
209              let and_val ≝ (get_cy_flag s) ∧ (get_arg_1 s addr2 true) in
210                set_flags s and_val (None ?) (get_ov_flag s)
211            ]
212        | ORL addr ⇒
213          match addr with
214            [ inl l ⇒
215              match l with
216                [ inl l' ⇒
217                  let 〈addr1, addr2〉 ≝ l' in
218                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
219                    set_arg_8 s addr1 or_val
220                | inr r ⇒
221                  let 〈addr1, addr2〉 ≝ r in
222                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
223                    set_arg_8 s addr1 or_val
224                ]
225            | inr r ⇒
226              let 〈addr1, addr2〉 ≝ r in
227              let or_val ≝ (get_cy_flag s) ∨ (get_arg_1 s addr2 true) in
228                set_flags s or_val (None ?) (get_ov_flag s)
229            ]
230        | XRL addr ⇒
231          match addr with
232            [ inl l' ⇒
233              let 〈addr1, addr2〉 ≝ l' in
234              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
235                set_arg_8 s addr1 xor_val
236            | inr r ⇒
237              let 〈addr1, addr2〉 ≝ r in
238              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
239                set_arg_8 s addr1 xor_val
240            ]
241        | INC addr ⇒
242            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
243                                                           registr;
244                                                           direct;
245                                                           indirect;
246                                                           dptr ]] x) → ? with
247              [ ACC_A ⇒ λacc_a: True.
248                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat 8 1) in
249                  set_arg_8 s ACC_A result
250              | REGISTER r ⇒ λregister: True.
251                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat 8 1) in
252                  set_arg_8 s (REGISTER r) result
253              | DIRECT d ⇒ λdirect: True.
254                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat 8 1) in
255                  set_arg_8 s (DIRECT d) result
256              | INDIRECT i ⇒ λindirect: True.
257                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat 8 1) in
258                  set_arg_8 s (INDIRECT i) result
259              | DPTR ⇒ λdptr: True.
260                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat 8 1) in
261                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero 8) carry in
262                let s ≝ set_8051_sfr s SFR_DPL bl in
263                  set_8051_sfr s SFR_DPH bu
264              | _ ⇒ λother: False. ⊥
265              ] (subaddressing_modein … addr)
266        | DEC addr ⇒
267           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat 8 1) false in
268             set_arg_8 s addr result
269        | MUL addr1 addr2 ⇒
270           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
271           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
272           let product ≝ acc_a_nat * acc_b_nat in
273           let ov_flag ≝ product ≥ 256 in
274           let low ≝ bitvector_of_nat 8 (product mod 256) in
275           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
276           let s ≝ set_8051_sfr s SFR_ACC_A low in
277             set_8051_sfr s SFR_ACC_B high
278        | DIV addr1 addr2 ⇒
279           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
280           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
281             match acc_b_nat with
282               [ O ⇒ set_flags s false (None Bit) true
283               | S o ⇒
284                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
285                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
286                 let s ≝ set_8051_sfr s SFR_ACC_A q in
287                 let s ≝ set_8051_sfr s SFR_ACC_B r in
288                   set_flags s false (None Bit) false
289               ]
290        | DA addr ⇒
291            let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_ACC_A) in
292              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag s) then
293                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat 8 6) false in
294                let cy_flag ≝ get_index' ? O ? flags in
295                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
296                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
297                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
298                    let new_acc ≝ nu @@ acc_nl' in
299                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
300                      set_flags s cy_flag (Some ? (get_ac_flag s)) (get_ov_flag s)
301                  else
302                    s
303              else
304                s
305        | CLR addr ⇒
306          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
307            [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero 8)
308            | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
309            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
310            | _ ⇒ λother: False. ⊥
311            ] (subaddressing_modein … addr)
312        | CPL addr ⇒
313          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
314            [ ACC_A ⇒ λacc_a: True.
315                let old_acc ≝ get_8051_sfr s SFR_ACC_A in
316                let new_acc ≝ negation_bv ? old_acc in
317                  set_8051_sfr s SFR_ACC_A new_acc
318            | CARRY ⇒ λcarry: True.
319                let old_cy_flag ≝ get_arg_1 s CARRY true in
320                let new_cy_flag ≝ ¬old_cy_flag in
321                  set_arg_1 s CARRY new_cy_flag
322            | BIT_ADDR b ⇒ λbit_addr: True.
323                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
324                let new_bit ≝ ¬old_bit in
325                  set_arg_1 s (BIT_ADDR b) new_bit
326            | _ ⇒ λother: False. ?
327            ] (subaddressing_modein … addr)
328        | SETB b ⇒ set_arg_1 s b false
329        | RL _ ⇒ (* DPM: always ACC_A *)
330            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
331            let new_acc ≝ rotate_left … 1 old_acc in
332              set_8051_sfr s SFR_ACC_A new_acc
333        | RR _ ⇒ (* DPM: always ACC_A *)
334            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
335            let new_acc ≝ rotate_right … 1 old_acc in
336              set_8051_sfr s SFR_ACC_A new_acc
337        | RLC _ ⇒ (* DPM: always ACC_A *)
338            let old_cy_flag ≝ get_cy_flag s in
339            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
340            let new_cy_flag ≝ get_index' ? O ? old_acc in
341            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
342            let s ≝ set_arg_1 s CARRY new_cy_flag in
343              set_8051_sfr s SFR_ACC_A new_acc
344        | RRC _ ⇒ (* DPM: always ACC_A *)
345            let old_cy_flag ≝ get_cy_flag s in
346            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
347            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
348            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
349            let s ≝ set_arg_1 s CARRY new_cy_flag in
350              set_8051_sfr s SFR_ACC_A new_acc
351        | SWAP _ ⇒ (* DPM: always ACC_A *)
352            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
353            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
354            let new_acc ≝ nl @@ nu in
355              set_8051_sfr s SFR_ACC_A new_acc
356        | PUSH addr ⇒
357            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
358              [ DIRECT d ⇒ λdirect: True.
359                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
360                let s ≝ set_8051_sfr s SFR_SP new_sp in
361                  write_at_stack_pointer s d
362              | _ ⇒ λother: False. ⊥
363              ] (subaddressing_modein … addr)
364        | POP addr ⇒
365            let contents ≝ read_at_stack_pointer s in
366            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
367            let s ≝ set_8051_sfr s SFR_SP new_sp in
368              set_arg_8 s addr contents
369        | XCH addr1 addr2 ⇒
370            let old_addr ≝ get_arg_8 s false addr2 in
371            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
372            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
373              set_arg_8 s addr2 old_acc
374        | XCHD addr1 addr2 ⇒
375            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr s SFR_ACC_A) in
376            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 s false addr2) in
377            let new_acc ≝ acc_nu @@ arg_nl in
378            let new_arg ≝ arg_nu @@ acc_nl in
379            let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
380              set_arg_8 s addr2 new_arg
381        | RET ⇒
382            let high_bits ≝ read_at_stack_pointer s in
383            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
384            let s ≝ set_8051_sfr s SFR_SP new_sp in
385            let low_bits ≝ read_at_stack_pointer s in
386            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
387            let s ≝ set_8051_sfr s SFR_SP new_sp in
388            let new_pc ≝ high_bits @@ low_bits in
389              set_program_counter s new_pc
390        | RETI ⇒
391            let high_bits ≝ read_at_stack_pointer s in
392            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
393            let s ≝ set_8051_sfr s SFR_SP new_sp in
394            let low_bits ≝ read_at_stack_pointer s in
395            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
396            let s ≝ set_8051_sfr s SFR_SP new_sp in
397            let new_pc ≝ high_bits @@ low_bits in
398              set_program_counter s new_pc
399        | JMP _ ⇒ (* DPM: always indirect_dptr *)
400          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
401          let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
402          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
403          let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
404            set_program_counter s new_pc
405        | LJMP addr ⇒
406          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
407            [ ADDR16 a ⇒ λaddr16: True.
408                set_program_counter s a
409            | _ ⇒ λother: False. ⊥
410            ] (subaddressing_modein … addr)
411        | SJMP addr ⇒
412          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
413            [ RELATIVE r ⇒ λrelative: True.
414                let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
415                  set_program_counter s new_pc
416            | _ ⇒ λother: False. ⊥
417            ] (subaddressing_modein … addr)
418        | AJMP addr ⇒
419          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
420            [ ADDR11 a ⇒ λaddr11: True.
421              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
422              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
423              let bit ≝ get_index' ? O ? nl in
424              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
425              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
426              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
427                set_program_counter s new_pc
428            | _ ⇒ λother: False. ⊥
429            ] (subaddressing_modein … addr)
430        | MOVX addr ⇒
431          (* DPM: only copies --- doesn't affect I/O *)
432          match addr with
433            [ inl l ⇒
434              let 〈addr1, addr2〉 ≝ l in
435                set_arg_8 s addr1 (get_arg_8 s false addr2)
436            | inr r ⇒
437              let 〈addr1, addr2〉 ≝ r in
438                set_arg_8 s addr1 (get_arg_8 s false addr2)
439            ]
440        | MOV addr ⇒
441          match addr with
442            [ inl l ⇒
443              match l with
444                [ inl l' ⇒
445                  match l' with
446                    [ inl l'' ⇒
447                      match l'' with
448                        [ inl l''' ⇒
449                          match l''' with
450                            [ inl l'''' ⇒
451                              let 〈addr1, addr2〉 ≝ l'''' in
452                                set_arg_8 s addr1 (get_arg_8 s false addr2)
453                            | inr r'''' ⇒
454                              let 〈addr1, addr2〉 ≝ r'''' in
455                                set_arg_8 s addr1 (get_arg_8 s false addr2)
456                            ]
457                        | inr r''' ⇒
458                          let 〈addr1, addr2〉 ≝ r''' in
459                            set_arg_8 s addr1 (get_arg_8 s false addr2)
460                        ]
461                    | inr r'' ⇒
462                      let 〈addr1, addr2〉 ≝ r'' in
463                        set_arg_16 s (get_arg_16 s addr2) addr1
464                    ]
465                | inr r ⇒
466                  let 〈addr1, addr2〉 ≝ r in
467                    set_arg_1 s addr1 (get_arg_1 s addr2 false)
468                ]
469            | inr r ⇒
470              let 〈addr1, addr2〉 ≝ r in
471                set_arg_1 s addr1 (get_arg_1 s addr2 false)
472            ]
473        | LCALL addr ⇒
474          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
475            [ ADDR16 a ⇒ λaddr16: True.
476              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
477              let s ≝ set_8051_sfr s SFR_SP new_sp in
478              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (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 8 1) 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                set_program_counter s a
484            | _ ⇒ λother: False. ⊥
485            ] (subaddressing_modein … addr)
486        | ACALL addr ⇒
487          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
488            [ ADDR11 a ⇒ λaddr11: True.
489              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
490              let s ≝ set_8051_sfr s SFR_SP new_sp in
491              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
492              let s ≝ write_at_stack_pointer s pc_bl in
493              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
494              let s ≝ set_8051_sfr s SFR_SP new_sp in
495              let s ≝ write_at_stack_pointer s pc_bu in
496              let 〈thr, eig〉 ≝ split ? 3 8 a in
497              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
498              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
499                set_program_counter s new_addr
500            | _ ⇒ λother: False. ⊥
501            ] (subaddressing_modein … addr)
502        | Jump j ⇒
503          match j with
504            [ JC addr ⇒
505              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
506                [ RELATIVE r ⇒ λrel: True.
507                  if get_cy_flag s then
508                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
509                      set_program_counter s new_pc
510                  else
511                    s
512                | _ ⇒ λother: False. ⊥
513                ] (subaddressing_modein … addr)
514            | JNC addr ⇒
515              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
516                [ RELATIVE r ⇒ λrel: True.
517                  if ¬(get_cy_flag s) then
518                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
519                      set_program_counter s new_pc
520                  else
521                    s
522                | _ ⇒ λother: False. ⊥
523                ] (subaddressing_modein … addr)
524            | JB addr1 addr2 ⇒
525              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
526                [ RELATIVE r ⇒ λrel: True.
527                  if get_arg_1 s addr1 false then
528                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
529                      set_program_counter s new_pc
530                  else
531                    s
532                | _ ⇒ λother: False. ⊥
533                ] (subaddressing_modein … addr2)
534            | JNB addr1 addr2 ⇒
535              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
536                [ RELATIVE r ⇒ λrel: True.
537                  if ¬(get_arg_1 s addr1 false) then
538                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
539                      set_program_counter s new_pc
540                  else
541                    s
542                | _ ⇒ λother: False. ⊥
543                ] (subaddressing_modein … addr2)
544            | JBC addr1 addr2 ⇒
545              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
546                [ RELATIVE r ⇒ λrel: True.
547                  let s ≝ set_arg_1 s addr1 false in
548                    if get_arg_1 s addr1 false then
549                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
550                        set_program_counter s new_pc
551                    else
552                      s
553                | _ ⇒ λother: False. ⊥
554                ] (subaddressing_modein … addr2)
555            | JZ addr ⇒
556              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
557                [ RELATIVE r ⇒ λrel: True.
558                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then
559                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
560                        set_program_counter s new_pc
561                    else
562                      s
563                | _ ⇒ λother: False. ⊥
564                ] (subaddressing_modein … addr)
565            | JNZ addr ⇒
566              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
567                [ RELATIVE r ⇒ λrel: True.
568                    if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
569                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
570                        set_program_counter s new_pc
571                    else
572                      s
573                | _ ⇒ λother: False. ⊥
574                ] (subaddressing_modein … addr)
575            | CJNE addr1 addr2 ⇒
576              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
577                [ RELATIVE r ⇒ λrelative: True.
578                  match addr1 with
579                    [ inl l ⇒
580                        let 〈addr1, addr2〉 ≝ l in
581                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
582                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
583                          if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
584                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
585                            let s ≝ set_program_counter s new_pc in
586                              set_flags s new_cy (None ?) (get_ov_flag s)
587                          else
588                            (set_flags s new_cy (None ?) (get_ov_flag s))
589                    | inr r' ⇒
590                        let 〈addr1, addr2〉 ≝ r' in
591                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
592                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
593                          if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
594                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
595                            let s ≝ set_program_counter s new_pc in
596                              set_flags s new_cy (None ?) (get_ov_flag s)
597                          else
598                            (set_flags s new_cy (None ?) (get_ov_flag s))
599                    ]
600                | _ ⇒ λother: False. ⊥
601                ] (subaddressing_modein … addr2)
602            | DJNZ addr1 addr2 ⇒
603              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
604                [ RELATIVE r ⇒ λrel: True.
605                    let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
606                    let s ≝ set_arg_8 s addr1 result in
607                      if ¬(eq_bv ? result (zero 8)) then
608                        let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
609                          set_program_counter s new_pc
610                      else
611                        s
612                | _ ⇒ λother: False. ⊥
613                ] (subaddressing_modein … addr2)
614            ]
615        | MOVC addr1 addr2 ⇒
616          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
617            [ ACC_DPTR ⇒ λacc_dptr: True.
618              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
619              let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
620              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
621              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
622                set_8051_sfr s SFR_ACC_A result
623            | ACC_PC ⇒ λacc_pc: True.
624              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
625              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in
626              (* DPM: Under specified: does the carry from PC incrementation affect the *)
627              (*      addition of the PC with the DPTR? At the moment, no.              *)
628              let s ≝ set_program_counter s inc_pc in
629              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
630              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
631                set_8051_sfr s SFR_ACC_A result
632            | _ ⇒ λother: False. ⊥
633            ] (subaddressing_modein … addr2)
634        | NOP ⇒ s
635        ]
636    in
637      s.
638    try assumption
639    try (
640      normalize
641      repeat (@ (le_S_S))
642      @ (le_O_n)
643    )
644    try (
645      @ (execute_1_technical … (subaddressing_modein …))
646      @ I
647    )
648    try (
649      normalize
650      @ I
651    )     
652qed.
653
654let rec execute (n: nat) (s: Status) on n: Status ≝
655  match n with
656    [ O ⇒ s
657    | S o ⇒ execute o (execute_1 s)
658    ].
Note: See TracBrowser for help on using the repository browser.