1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "emulator/status/status_setter.ma".
25 (* **************** *)
26 (* GETTER SPECIFICI *)
27 (* **************** *)
29 (* funzione ausiliaria per il tipaggio dei getter *)
30 ndefinition aux_get_type ≝ λx:Type.λm:mcu_type.match m with
31 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
32 | IP2022 ⇒ alu_IP2022 ] → x.
36 (* getter di A, esiste sempre *)
37 ndefinition get_acc_8_low_reg ≝
38 λm:mcu_type.λt:memory_impl.λs:any_status m t.
40 return aux_get_type byte8 with
41 [ HC05 ⇒ acc_low_reg_HC05
42 | HC08 ⇒ acc_low_reg_HC08
43 | HCS08 ⇒ acc_low_reg_HC08
44 | RS08 ⇒ acc_low_reg_RS08
45 | IP2022 ⇒ acc_low_reg_IP2022 ]
48 (* getter di X, non esiste sempre *)
49 ndefinition get_indX_8_low_reg ≝
50 λm:mcu_type.λt:memory_impl.λs:any_status m t.
52 return aux_get_type (option byte8) with
53 [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
54 | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
55 | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
57 | IP2022 ⇒ λalu.None ? ]
60 (* getter di H, non esiste sempre *)
61 ndefinition get_indX_8_high_reg ≝
62 λm:mcu_type.λt:memory_impl.λs:any_status m t.
64 return aux_get_type (option byte8) with
66 | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
67 | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
69 | IP2022 ⇒ λalu.None ? ]
72 (* getter di H:X, non esiste sempre *)
73 ndefinition get_indX_16_reg ≝
74 λm:mcu_type.λt:memory_impl.λs:any_status m t.
76 return aux_get_type (option word16) with
78 | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
79 | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
81 | IP2022 ⇒ λalu.None ? ]
84 (* getter di SP, non esiste sempre *)
85 ndefinition get_sp_reg ≝
86 λm:mcu_type.λt:memory_impl.λs:any_status m t.
88 return aux_get_type (option word16) with
89 [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
90 | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
91 | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
93 | IP2022 ⇒ λalu.Some ? (sp_reg_IP2022 alu) ]
96 (* getter di PC, esiste sempre *)
97 ndefinition get_pc_reg ≝
98 λm:mcu_type.λt:memory_impl.λs:any_status m t.
100 return aux_get_type word16 with
103 | HCS08 ⇒ pc_reg_HC08
105 | IP2022 ⇒ pc_reg_IP2022 ]
108 (* getter di SPC, non esiste sempre *)
109 ndefinition get_spc_reg ≝
110 λm:mcu_type.λt:memory_impl.λs:any_status m t.
112 return aux_get_type (option word16) with
115 | HCS08 ⇒ λalu.None ?
116 | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu)
117 | IP2022 ⇒ λalu.None ? ]
120 (* getter di MULH, non esiste sempre *)
121 ndefinition get_mulh_reg ≝
122 λm:mcu_type.λt:memory_impl.λs:any_status m t.
124 return aux_get_type (option byte8) with
127 | HCS08 ⇒ λalu.None ?
129 | IP2022 ⇒ λalu.Some ? (mulh_reg_IP2022 alu) ]
132 (* getter di ADDRSEL, non esiste sempre *)
133 ndefinition get_addrsel_reg ≝
134 λm:mcu_type.λt:memory_impl.λs:any_status m t.
136 return aux_get_type (option byte8) with
139 | HCS08 ⇒ λalu.None ?
141 | IP2022 ⇒ λalu.Some ? (addrsel_reg_IP2022 alu) ]
144 (* getter di ADDR, non esiste sempre *)
145 ndefinition get_addr_reg ≝
146 λm:mcu_type.λt:memory_impl.λs:any_status m t.
148 return aux_get_type (option word24) with
151 | HCS08 ⇒ λalu.None ?
153 | IP2022 ⇒ λalu.Some ? (get_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu)) ]
156 (* getter di CALL, non esiste sempre *)
157 ndefinition get_call_reg ≝
158 λm:mcu_type.λt:memory_impl.λs:any_status m t.
160 return aux_get_type (option word16) with
163 | HCS08 ⇒ λalu.None ?
165 | IP2022 ⇒ λalu.Some ? (getn_array16T x0 ? (call_stack_IP2022 alu)) ]
168 ndefinition pop_call_reg ≝
171 return λm.Πt.any_status m t → (option (ProdT word16 (any_status m t))) with
172 [ HC05 ⇒ λt:memory_impl.λs:any_status HC05 t.None ?
173 | HC08 ⇒ λt:memory_impl.λs:any_status HC08 t.None ?
174 | HCS08 ⇒ λt:memory_impl.λs:any_status HCS08 t.None ?
175 | RS08 ⇒ λt:memory_impl.λs:any_status RS08 t.None ?
176 | IP2022 ⇒ λt:memory_impl.λs:any_status IP2022 t.
177 match pop_callstack (call_stack_IP2022 (alu IP2022 t s)) with
178 [ pair val call' ⇒ Some ? (pair … val
181 (acc_low_reg_IP2022 (alu IP2022 t s))
182 (mulh_reg_IP2022 (alu IP2022 t s))
183 (addrsel_reg_IP2022 (alu IP2022 t s))
184 (addr_array_IP2022 (alu IP2022 t s))
186 (ip_reg_IP2022 (alu IP2022 t s))
187 (dp_reg_IP2022 (alu IP2022 t s))
188 (data_reg_IP2022 (alu IP2022 t s))
189 (sp_reg_IP2022 (alu IP2022 t s))
190 (pc_reg_IP2022 (alu IP2022 t s))
191 (speed_reg_IP2022 (alu IP2022 t s))
192 (page_reg_IP2022 (alu IP2022 t s))
193 (h_flag_IP2022 (alu IP2022 t s))
194 (z_flag_IP2022 (alu IP2022 t s))
195 (c_flag_IP2022 (alu IP2022 t s))
196 (skip_mode_IP2022 (alu IP2022 t s))))) ]].
198 (* getter di IP, non esiste sempre *)
199 ndefinition get_ip_reg ≝
200 λm:mcu_type.λt:memory_impl.λs:any_status m t.
202 return aux_get_type (option word16) with
205 | HCS08 ⇒ λalu.None ?
207 | IP2022 ⇒ λalu.Some ? (ip_reg_IP2022 alu) ]
210 (* getter di DP, non esiste sempre *)
211 ndefinition get_dp_reg ≝
212 λm:mcu_type.λt:memory_impl.λs:any_status m t.
214 return aux_get_type (option word16) with
217 | HCS08 ⇒ λalu.None ?
219 | IP2022 ⇒ λalu.Some ? (dp_reg_IP2022 alu) ]
222 (* getter di DATA, non esiste sempre *)
223 ndefinition get_data_reg ≝
224 λm:mcu_type.λt:memory_impl.λs:any_status m t.
226 return aux_get_type (option word16) with
229 | HCS08 ⇒ λalu.None ?
231 | IP2022 ⇒ λalu.Some ? (data_reg_IP2022 alu) ]
234 (* getter di SPEED, non esiste sempre *)
235 ndefinition get_speed_reg ≝
236 λm:mcu_type.λt:memory_impl.λs:any_status m t.
238 return aux_get_type (option exadecim) with
241 | HCS08 ⇒ λalu.None ?
243 | IP2022 ⇒ λalu.Some ? (speed_reg_IP2022 alu) ]
246 (* getter di PAGE, non esiste sempre *)
247 ndefinition get_page_reg ≝
248 λm:mcu_type.λt:memory_impl.λs:any_status m t.
250 return aux_get_type (option oct) with
253 | HCS08 ⇒ λalu.None ?
255 | IP2022 ⇒ λalu.Some ? (page_reg_IP2022 alu) ]
258 (* REGISTRI SPECIALI *)
260 (* getter di memory mapped X, non esiste sempre *)
261 ndefinition get_x_map ≝
262 λm:mcu_type.λt:memory_impl.λs:any_status m t.
264 return aux_get_type (option byte8) with
267 | HCS08 ⇒ λalu.None ?
268 | RS08 ⇒ λalu.Some ? (x_map_RS08 alu)
269 | IP2022 ⇒ λalu.None ? ]
272 (* getter di memory mapped PS, non esiste sempre *)
273 ndefinition get_ps_map ≝
274 λm:mcu_type.λt:memory_impl.λs:any_status m t.
276 return aux_get_type (option byte8) with
279 | HCS08 ⇒ λalu.None ?
280 | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu)
281 | IP2022 ⇒ λalu.None ? ]
284 (* getter di skip mode, non esiste sempre *)
285 ndefinition get_skip_mode ≝
286 λm:mcu_type.λt:memory_impl.λs:any_status m t.
288 return aux_get_type (option bool) with
291 | HCS08 ⇒ λalu.None ?
293 | IP2022 ⇒ λalu.Some ? (skip_mode_IP2022 alu) ]
298 (* getter di V, non esiste sempre *)
299 ndefinition get_v_flag ≝
300 λm:mcu_type.λt:memory_impl.λs:any_status m t.
302 return aux_get_type (option bool) with
304 | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
305 | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
307 | IP2022 ⇒ λalu.None ? ]
310 (* getter di H, non esiste sempre *)
311 ndefinition get_h_flag ≝
312 λm:mcu_type.λt:memory_impl.λs:any_status m t.
314 return aux_get_type (option bool) with
315 [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
316 | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
317 | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
319 | IP2022 ⇒ λalu.Some ? (h_flag_IP2022 alu) ]
322 (* getter di I, non esiste sempre *)
323 ndefinition get_i_flag ≝
324 λm:mcu_type.λt:memory_impl.λs:any_status m t.
326 return aux_get_type (option bool) with
327 [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
328 | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
329 | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
331 | IP2022 ⇒ λalu.None ? ]
334 (* getter di N, non esiste sempre *)
335 ndefinition get_n_flag ≝
336 λm:mcu_type.λt:memory_impl.λs:any_status m t.
338 return aux_get_type (option bool) with
339 [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
340 | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
341 | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
343 | IP2022 ⇒ λalu.None ? ]
346 (* getter di Z, esiste sempre *)
347 ndefinition get_z_flag ≝
348 λm:mcu_type.λt:memory_impl.λs:any_status m t.
350 return aux_get_type bool with
353 | HCS08 ⇒ z_flag_HC08
355 | IP2022 ⇒ z_flag_IP2022 ]
358 (* getter di C, esiste sempre *)
359 ndefinition get_c_flag ≝
360 λm:mcu_type.λt:memory_impl.λs:any_status m t.
362 return aux_get_type bool with
365 | HCS08 ⇒ c_flag_HC08
367 | IP2022 ⇒ c_flag_IP2022 ]
370 (* getter di IRQ, non esiste sempre *)
371 ndefinition get_irq_flag ≝
372 λm:mcu_type.λt:memory_impl.λs:any_status m t.
374 return aux_get_type (option bool) with
375 [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
376 | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
377 | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
379 | IP2022 ⇒ λalu.None ? ]