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

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

Work on execute_1 function.

File size: 5.3 KB
Line 
1include "Status.ma".
2include "Fetch.ma".
3include "Cartesian.ma".
4include "Arithmetic.ma".
5include "List.ma".
6
7ndefinition execute_1: Status → Status ≝
8  λs.
9    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
10    let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in
11    let s ≝ set_clock s (clock s + ticks) in
12    let s ≝ set_program_counter s pc in
13    let s ≝
14      match instr with
15        [ ADD addr1 addr2 ⇒
16            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
17                                                   (get_arg_8 s false addr2) false in
18            let cy_flag ≝ get_index … flags Z ? in
19            let ac_flag ≝ get_index … flags one ? in
20            let ov_flag ≝ get_index … flags two ? in
21            let s ≝ set_arg_8 s ACC_A result in
22              set_flags s cy_flag (Just Bit ac_flag) ov_flag
23        | ADDC addr1 addr2 ⇒
24            let old_cy_flag ≝ get_cy_flag s in
25            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
26                                                   (get_arg_8 s false addr2) old_cy_flag in
27            let cy_flag ≝ get_index … flags Z ? in
28            let ac_flag ≝ get_index … flags one ? in
29            let ov_flag ≝ get_index … flags two ? in
30            let s ≝ set_arg_8 s ACC_A result in
31              set_flags s cy_flag (Just Bit ac_flag) ov_flag
32        | SUBB addr1 addr2 ⇒
33            let old_cy_flag ≝ get_cy_flag s in
34            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
35                                                   (get_arg_8 s false addr2) old_cy_flag in
36            let cy_flag ≝ get_index … flags Z ? in
37            let ac_flag ≝ get_index … flags one ? in
38            let ov_flag ≝ get_index … flags two ? in
39            let s ≝ set_arg_8 s ACC_A result in
40              set_flags s cy_flag (Just Bit ac_flag) ov_flag
41        | INC addr ⇒
42            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
43                                                           register;
44                                                           direct;
45                                                           indirect;
46                                                           dptr ]] x) → ? with
47              [ ACC_A ⇒ λacc_a: True.
48                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat eight one) in
49                  set_arg_8 s ACC_A result
50              | REGISTER r ⇒ λregister: True.
51                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat eight one) in
52                  set_arg_8 s (REGISTER r) result
53              | DIRECT d ⇒ λdirect: True.
54                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat eight one) in
55                  set_arg_8 s (DIRECT d) result
56              | INDIRECT i ⇒ λindirect: True.
57                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat eight one) in
58                  set_arg_8 s (INDIRECT i) result
59              | DPTR ⇒ λdptr: True.
60                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat eight one) in
61                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero eight) carry in
62                let s ≝ set_8051_sfr s SFR_DPL bl in
63                  set_8051_sfr s SFR_DPH bu
64              | _ ⇒ λother: False. ?
65              ] (subaddressing_modein … addr)
66       | DEC addr ⇒
67           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat eight one) false in
68             set_arg_8 s addr result
69        | MUL addr1 addr2 ⇒
70           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
71           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
72           let product ≝ acc_a_nat * acc_b_nat in
73           let ov_flag ≝ product ≥ two_hundred_and_fifty_six in
74           let low ≝ bitvector_of_nat eight (product mod two_hundred_and_fifty_six) in
75           let high ≝ bitvector_of_nat eight (product ÷ two_hundred_and_fifty_six) in
76           let s ≝ set_8051_sfr s SFR_ACC_A low in
77             set_8051_sfr s SFR_ACC_B high
78        | DIV addr1 addr2 ⇒
79           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
80           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
81             match acc_b_nat with
82               [ Z ⇒ set_flags s false (Nothing Bit) true
83               | S o ⇒
84                 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in
85                 let r ≝ bitvector_of_nat eight (acc_a_nat mod two_hundred_and_fifty_six) in
86                 let s ≝ set_8051_sfr s SFR_ACC_A q in
87                 let s ≝ set_8051_sfr s SFR_ACC_B r in
88                   set_flags s false (Nothing Bit) false
89               ]
90(*
91         DA addr ⇒
92            match addr return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with
93              [ ACC_A ⇒ λacc_a: True.
94                let 〈 acc_nu, acc_nl 〉 ≝
95              | _ ⇒ λother: False. ?
96              ] (subaddressing_modein … addr) *)
97        | _ ⇒ s
98        ]
99    in
100      s.
101   
102   
Note: See TracBrowser for help on using the repository browser.