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

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

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