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

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

A simple version of assembly (no labels) implemented.

File size: 14.7 KB
RevLine 
[334]1include "Status.ma".
[341]2include "Fetch.ma".
[329]3include "Cartesian.ma".
4include "Arithmetic.ma".
5include "List.ma".
6
[334]7alias id "inclusive_disjunction" = "cic:/matita/ng/Bool/inclusive_disjunction.fix(0,0,1)".
8
[338]9ndefinition sign_extension: Byte → Word ≝
10  λb.
11    zero eight @@ b.
12
[329]13ndefinition execute_1: Status → Status ≝
14  λs.
15    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
16    let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in
17    let s ≝ set_clock s (clock s + ticks) in
18    let s ≝ set_program_counter s pc in
19    let s ≝
20      match instr with
21        [ ADD addr1 addr2 ⇒
[333]22            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
23                                                   (get_arg_8 s false addr2) false in
24            let cy_flag ≝ get_index … flags Z ? in
25            let ac_flag ≝ get_index … flags one ? in
26            let ov_flag ≝ get_index … flags two ? in
27            let s ≝ set_arg_8 s ACC_A result in
28              set_flags s cy_flag (Just Bit ac_flag) ov_flag
[331]29        | ADDC addr1 addr2 ⇒
30            let old_cy_flag ≝ get_cy_flag s in
[333]31            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
32                                                   (get_arg_8 s false addr2) old_cy_flag in
33            let cy_flag ≝ get_index … flags Z ? in
34            let ac_flag ≝ get_index … flags one ? in
35            let ov_flag ≝ get_index … flags two ? in
36            let s ≝ set_arg_8 s ACC_A result in
37              set_flags s cy_flag (Just Bit ac_flag) ov_flag
38        | SUBB addr1 addr2 ⇒
39            let old_cy_flag ≝ get_cy_flag s in
40            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
41                                                   (get_arg_8 s false addr2) old_cy_flag in
42            let cy_flag ≝ get_index … flags Z ? in
43            let ac_flag ≝ get_index … flags one ? in
44            let ov_flag ≝ get_index … flags two ? in
45            let s ≝ set_arg_8 s ACC_A result in
46              set_flags s cy_flag (Just Bit ac_flag) ov_flag
47        | INC addr ⇒
48            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
49                                                           register;
50                                                           direct;
51                                                           indirect;
52                                                           dptr ]] x) → ? with
[331]53              [ ACC_A ⇒ λacc_a: True.
[333]54                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat eight one) in
55                  set_arg_8 s ACC_A result
56              | REGISTER r ⇒ λregister: True.
57                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat eight one) in
58                  set_arg_8 s (REGISTER r) result
59              | DIRECT d ⇒ λdirect: True.
60                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat eight one) in
61                  set_arg_8 s (DIRECT d) result
62              | INDIRECT i ⇒ λindirect: True.
63                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat eight one) in
64                  set_arg_8 s (INDIRECT i) result
65              | DPTR ⇒ λdptr: True.
66                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat eight one) in
67                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero eight) carry in
68                let s ≝ set_8051_sfr s SFR_DPL bl in
69                  set_8051_sfr s SFR_DPH bu
70              | _ ⇒ λother: False. ?
71              ] (subaddressing_modein … addr)
72       | DEC addr ⇒
73           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat eight one) false in
74             set_arg_8 s addr result
75        | MUL addr1 addr2 ⇒
76           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
77           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
78           let product ≝ acc_a_nat * acc_b_nat in
79           let ov_flag ≝ product ≥ two_hundred_and_fifty_six in
80           let low ≝ bitvector_of_nat eight (product mod two_hundred_and_fifty_six) in
81           let high ≝ bitvector_of_nat eight (product ÷ two_hundred_and_fifty_six) in
82           let s ≝ set_8051_sfr s SFR_ACC_A low in
83             set_8051_sfr s SFR_ACC_B high
84        | DIV addr1 addr2 ⇒
85           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
86           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
87             match acc_b_nat with
88               [ Z ⇒ set_flags s false (Nothing Bit) true
89               | S o ⇒
90                 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in
91                 let r ≝ bitvector_of_nat eight (acc_a_nat mod two_hundred_and_fifty_six) in
92                 let s ≝ set_8051_sfr s SFR_ACC_A q in
93                 let s ≝ set_8051_sfr s SFR_ACC_B r in
94                   set_flags s false (Nothing Bit) false
95               ]
[334]96        | DA addr ⇒
97            let 〈 acc_nu, acc_nl 〉 ≝ split ? four four (get_8051_sfr s SFR_ACC_A) in
98              if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then
99                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in
100                let cy_flag ≝ get_index ? flags Z ? in
101                let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in
102                  if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then
103                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat four six) in
104                    let new_acc ≝ nu @@ acc_nl' in
105                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
106                      set_flags s cy_flag (Just ? (get_ac_flag s)) (get_ov_flag s)
107                  else
108                    s
109              else
110                s
[337]111        | CLR addr ⇒
112          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
113            [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero eight)
114            | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
115            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
[334]116            | _ ⇒ λother: False. ?
[337]117            ] (subaddressing_modein … addr)
118        | CPL addr ⇒
119          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
120            [ ACC_A ⇒ λacc_a: True.
121                let old_acc ≝ get_8051_sfr s SFR_ACC_A in
122                let new_acc ≝ negation_bv ? old_acc in
123                  set_8051_sfr s SFR_ACC_A new_acc
124            | CARRY ⇒ λcarry: True.
125                let old_cy_flag ≝ get_arg_1 s CARRY true in
126                let new_cy_flag ≝ negation old_cy_flag in
127                  set_arg_1 s CARRY new_cy_flag
128            | BIT_ADDR b ⇒ λbit_addr: True.
129                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
130                let new_bit ≝ negation old_bit in
131                  set_arg_1 s (BIT_ADDR b) new_bit
132            | _ ⇒ λother: False. ?
133            ] (subaddressing_modein … addr)
134        | SETB b ⇒ set_arg_1 s b false
135        | RL _ ⇒ (* DPM: always ACC_A *)
136            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
137            let new_acc ≝ rotate_left_bv ? one old_acc in
138              set_8051_sfr s SFR_ACC_A new_acc
139        | RR _ ⇒ (* DPM: always ACC_A *)
140            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
141            let new_acc ≝ rotate_right_bv ? one old_acc in
142              set_8051_sfr s SFR_ACC_A new_acc
143        | RLC _ ⇒ (* DPM: always ACC_A *)
144            let old_cy_flag ≝ get_cy_flag s in
145            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
146            let new_cy_flag ≝ get_index_bv ? old_acc Z ? in
147            let new_acc ≝ shift_left_bv eight one old_acc old_cy_flag in
148            let s ≝ set_arg_1 s CARRY new_cy_flag in
149              set_8051_sfr s SFR_ACC_A new_acc
150        | RRC _ ⇒ (* DPM: always ACC_A *)
151            let old_cy_flag ≝ get_cy_flag s in
152            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
153            let new_cy_flag ≝ get_index_bv ? old_acc seven ? in
154            let new_acc ≝ shift_right_bv eight one old_acc old_cy_flag in
155            let s ≝ set_arg_1 s CARRY new_cy_flag in
156              set_8051_sfr s SFR_ACC_A new_acc
157        | SWAP _ ⇒ (* DPM: always ACC_A *)
158            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
159            let 〈nu,nl〉 ≝ split ? four four old_acc in
160            let new_acc ≝ nl @@ nu in
161              set_8051_sfr s SFR_ACC_A new_acc
162        | PUSH addr ⇒
163            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
164              [ DIRECT d ⇒ λdirect: True.
165                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
166                let s ≝ set_8051_sfr s SFR_SP new_sp in
167                  write_at_stack_pointer s d
168              | _ ⇒ λother: False. ?
169              ] (subaddressing_modein … addr)
170        | POP addr ⇒
171            let contents ≝ read_at_stack_pointer s in
172            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
173            let s ≝ set_8051_sfr s SFR_SP new_sp in
174              set_arg_8 s addr contents
175        | XCH addr1 addr2 ⇒
176            let old_addr ≝ get_arg_8 s false addr2 in
177            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
178            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
179              set_arg_8 s addr2 old_acc
[338]180        | XCHD addr1 addr2 ⇒
181            let 〈acc_nu, acc_nl〉 ≝ split … four four (get_8051_sfr s SFR_ACC_A) in
182            let 〈arg_nu, arg_nl〉 ≝ split … four four (get_arg_8 s false addr2) in
183            let new_acc ≝ acc_nu @@ arg_nl in
184            let new_arg ≝ arg_nu @@ acc_nl in
185            let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
186              set_arg_8 s addr2 new_arg
187        | Jump j ⇒
188          match j with
189            [ JC addr ⇒
190              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
191                [ RELATIVE r ⇒ λrel: True.
192                  if get_cy_flag s then
193                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
194                      set_program_counter s new_pc
195                  else
196                    s
197                | _ ⇒ λother: False. ?
198                ] (subaddressing_modein … addr)
199            | JNC addr ⇒
200              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
201                [ RELATIVE r ⇒ λrel: True.
202                  if negation (get_cy_flag s) then
203                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
204                      set_program_counter s new_pc
205                  else
206                    s
207                | _ ⇒ λother: False. ?
208                ] (subaddressing_modein … addr)
209            | JB addr1 addr2 ⇒
210              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
211                [ RELATIVE r ⇒ λrel: True.
212                  if get_arg_1 s addr1 false then
213                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
214                      set_program_counter s new_pc
215                  else
216                    s
217                | _ ⇒ λother: False. ?
218                ] (subaddressing_modein … addr2)
219            | JNB addr1 addr2 ⇒
220              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
221                [ RELATIVE r ⇒ λrel: True.
222                  if negation (get_arg_1 s addr1 false) then
223                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
224                      set_program_counter s new_pc
225                  else
226                    s
227                | _ ⇒ λother: False. ?
228                ] (subaddressing_modein … addr2)
229            | JBC addr1 addr2 ⇒
230              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
231                [ RELATIVE r ⇒ λrel: True.
232                  let s ≝ set_arg_1 s addr1 false in
233                    if get_arg_1 s addr1 false then
234                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
235                        set_program_counter s new_pc
236                    else
237                      s
238                | _ ⇒ λother: False. ?
239                ] (subaddressing_modein … addr2)
240            | JZ addr ⇒
241              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
242                [ RELATIVE r ⇒ λrel: True.
243                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight) then
244                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
245                        set_program_counter s new_pc
246                    else
247                      s
248                | _ ⇒ λother: False. ?
249                ] (subaddressing_modein … addr)
250            | JNZ addr ⇒
251              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
252                [ RELATIVE r ⇒ λrel: True.
253                    if negation (eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight)) then
254                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
255                        set_program_counter s new_pc
256                    else
257                      s
258                | _ ⇒ λother: False. ?
259                ] (subaddressing_modein … addr)
260            | CJNE addr1 addr2 ⇒ ?
261              match addr1 with
262                [ Left l ⇒ ?
263                | Right r ⇒ ?
264                ]
265            | DJNZ addr1 addr2 ⇒
266              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
267                [ RELATIVE r ⇒ λrel: True.
268                    let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat eight one) false in
269                    let s ≝ set_arg_8 s addr1 result in
270                      if negation (eq_bv ? result (zero eight)) then
271                        let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
272                          set_program_counter s new_pc
273                      else
274                        s
275                | _ ⇒ λother: False. ?
276                ] (subaddressing_modein … addr2)
277            ]
[337]278        | NOP ⇒ s
[329]279        | _ ⇒ s
280        ]
281    in
[337]282      s.
Note: See TracBrowser for help on using the repository browser.