source: src/ASM/Interpret.ma @ 757

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

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

File size: 28.1 KB
RevLine 
[698]1include "ASM/Status.ma".
2include "ASM/Fetch.ma".
[475]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.
[712]156
157include alias "arithmetics/nat.ma".
[757]158include alias "ASM/BitVectorTrie.ma".
[712]159
[475]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
[757]175              set_flags s cy_flag (Some Bit ac_flag) ov_flag
[475]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;
[757]243                                                           registr;
[475]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)
[712]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            ]
[757]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)
[475]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.