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 ≝ λT:Type.λm:mcu_type.aux_alu_type m → T.
34 (* getter di A, esiste sempre *)
35 ndefinition get_acc_8_low_reg ≝
36 λm:mcu_type.λt:memory_impl.λs:any_status m t.
38 return aux_get_type byte8 with
39 [ HC05 ⇒ acc_low_reg_HC05
40 | HC08 ⇒ acc_low_reg_HC08
41 | HCS08 ⇒ acc_low_reg_HC08
42 | RS08 ⇒ acc_low_reg_RS08
43 | IP2022 ⇒ acc_low_reg_IP2022 ]
46 (* getter di X, non esiste sempre *)
47 ndefinition get_indX_8_low_reg ≝
48 λm:mcu_type.λt:memory_impl.λs:any_status m t.
50 return aux_get_type (option byte8) with
51 [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
52 | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
53 | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
55 | IP2022 ⇒ λalu.None ? ]
58 (* getter di H, non esiste sempre *)
59 ndefinition get_indX_8_high_reg ≝
60 λm:mcu_type.λt:memory_impl.λs:any_status m t.
62 return aux_get_type (option byte8) with
64 | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
65 | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
67 | IP2022 ⇒ λalu.None ? ]
70 (* getter di H:X, non esiste sempre *)
71 ndefinition get_indX_16_reg ≝
72 λm:mcu_type.λt:memory_impl.λs:any_status m t.
74 return aux_get_type (option word16) with
76 | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
77 | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
79 | IP2022 ⇒ λalu.None ? ]
82 (* getter di SP, non esiste sempre *)
83 ndefinition get_sp_reg ≝
84 λm:mcu_type.λt:memory_impl.λs:any_status m t.
86 return aux_get_type (option word16) with
87 [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
88 | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
89 | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
91 | IP2022 ⇒ λalu.Some ? (sp_reg_IP2022 alu) ]
94 (* getter di PC, esiste sempre *)
95 ndefinition get_pc_reg ≝
96 λm:mcu_type.λt:memory_impl.λs:any_status m t.
98 return aux_get_type word16 with
101 | HCS08 ⇒ pc_reg_HC08
103 | IP2022 ⇒ pc_reg_IP2022 ]
106 (* getter di SPC, non esiste sempre *)
107 ndefinition get_spc_reg ≝
108 λm:mcu_type.λt:memory_impl.λs:any_status m t.
110 return aux_get_type (option word16) with
113 | HCS08 ⇒ λalu.None ?
114 | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu)
115 | IP2022 ⇒ λalu.None ? ]
118 (* getter di MULH, non esiste sempre *)
119 ndefinition get_mulh_reg ≝
120 λm:mcu_type.λt:memory_impl.λs:any_status m t.
122 return aux_get_type (option byte8) with
125 | HCS08 ⇒ λalu.None ?
127 | IP2022 ⇒ λalu.Some ? (mulh_reg_IP2022 alu) ]
130 (* getter di ADDRSEL, non esiste sempre *)
131 ndefinition get_addrsel_reg ≝
132 λm:mcu_type.λt:memory_impl.λs:any_status m t.
134 return aux_get_type (option byte8) with
137 | HCS08 ⇒ λalu.None ?
139 | IP2022 ⇒ λalu.Some ? (addrsel_reg_IP2022 alu) ]
142 (* getter di ADDR, non esiste sempre *)
143 ndefinition get_addr_reg ≝
144 λm:mcu_type.λt:memory_impl.λs:any_status m t.
146 return aux_get_type (option word24) with
149 | HCS08 ⇒ λalu.None ?
151 | IP2022 ⇒ λalu.Some ? (get_addr_reg_IP2022 alu) ]
154 (* getter di CALL, non esiste sempre *)
155 ndefinition get_call_reg ≝
156 λm:mcu_type.λt:memory_impl.λs:any_status m t.
158 return aux_get_type (option word16) with
161 | HCS08 ⇒ λalu.None ?
163 | IP2022 ⇒ λalu.Some ? (get_call_reg_IP2022 alu) ]
166 (* getter di IP, non esiste sempre *)
167 ndefinition get_ip_reg ≝
168 λm:mcu_type.λt:memory_impl.λs:any_status m t.
170 return aux_get_type (option word16) with
173 | HCS08 ⇒ λalu.None ?
175 | IP2022 ⇒ λalu.Some ? (ip_reg_IP2022 alu) ]
178 (* getter di DP, non esiste sempre *)
179 ndefinition get_dp_reg ≝
180 λm:mcu_type.λt:memory_impl.λs:any_status m t.
182 return aux_get_type (option word16) with
185 | HCS08 ⇒ λalu.None ?
187 | IP2022 ⇒ λalu.Some ? (dp_reg_IP2022 alu) ]
190 (* getter di DATA, non esiste sempre *)
191 ndefinition get_data_reg ≝
192 λm:mcu_type.λt:memory_impl.λs:any_status m t.
194 return aux_get_type (option word16) with
197 | HCS08 ⇒ λalu.None ?
199 | IP2022 ⇒ λalu.Some ? (data_reg_IP2022 alu) ]
202 (* getter di SPEED, non esiste sempre *)
203 ndefinition get_speed_reg ≝
204 λm:mcu_type.λt:memory_impl.λs:any_status m t.
206 return aux_get_type (option exadecim) with
209 | HCS08 ⇒ λalu.None ?
211 | IP2022 ⇒ λalu.Some ? (speed_reg_IP2022 alu) ]
214 (* getter di PAGE, non esiste sempre *)
215 ndefinition get_page_reg ≝
216 λm:mcu_type.λt:memory_impl.λs:any_status m t.
218 return aux_get_type (option oct) with
221 | HCS08 ⇒ λalu.None ?
223 | IP2022 ⇒ λalu.Some ? (page_reg_IP2022 alu) ]
226 (* REGISTRI SPECIALI *)
228 (* getter di memory mapped X, non esiste sempre *)
229 ndefinition get_x_map ≝
230 λm:mcu_type.λt:memory_impl.λs:any_status m t.
232 return aux_get_type (option byte8) with
235 | HCS08 ⇒ λalu.None ?
236 | RS08 ⇒ λalu.Some ? (x_map_RS08 alu)
237 | IP2022 ⇒ λalu.None ? ]
240 (* getter di memory mapped PS, non esiste sempre *)
241 ndefinition get_ps_map ≝
242 λm:mcu_type.λt:memory_impl.λs:any_status m t.
244 return aux_get_type (option byte8) with
247 | HCS08 ⇒ λalu.None ?
248 | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu)
249 | IP2022 ⇒ λalu.None ? ]
252 (* getter di skip mode, non esiste sempre *)
253 ndefinition get_skip_mode ≝
254 λm:mcu_type.λt:memory_impl.λs:any_status m t.
256 return aux_get_type (option bool) with
259 | HCS08 ⇒ λalu.None ?
261 | IP2022 ⇒ λalu.Some ? (skip_mode_IP2022 alu) ]
266 (* getter di V, non esiste sempre *)
267 ndefinition get_v_flag ≝
268 λm:mcu_type.λt:memory_impl.λs:any_status m t.
270 return aux_get_type (option bool) with
272 | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
273 | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
275 | IP2022 ⇒ λalu.None ? ]
278 (* getter di H, non esiste sempre *)
279 ndefinition get_h_flag ≝
280 λm:mcu_type.λt:memory_impl.λs:any_status m t.
282 return aux_get_type (option bool) with
283 [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
284 | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
285 | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
287 | IP2022 ⇒ λalu.Some ? (h_flag_IP2022 alu) ]
290 (* getter di I, non esiste sempre *)
291 ndefinition get_i_flag ≝
292 λm:mcu_type.λt:memory_impl.λs:any_status m t.
294 return aux_get_type (option bool) with
295 [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
296 | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
297 | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
299 | IP2022 ⇒ λalu.None ? ]
302 (* getter di N, non esiste sempre *)
303 ndefinition get_n_flag ≝
304 λm:mcu_type.λt:memory_impl.λs:any_status m t.
306 return aux_get_type (option bool) with
307 [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
308 | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
309 | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
311 | IP2022 ⇒ λalu.None ? ]
314 (* getter di Z, esiste sempre *)
315 ndefinition get_z_flag ≝
316 λm:mcu_type.λt:memory_impl.λs:any_status m t.
318 return aux_get_type bool with
321 | HCS08 ⇒ z_flag_HC08
323 | IP2022 ⇒ z_flag_IP2022 ]
326 (* getter di C, esiste sempre *)
327 ndefinition get_c_flag ≝
328 λm:mcu_type.λt:memory_impl.λs:any_status m t.
330 return aux_get_type bool with
333 | HCS08 ⇒ c_flag_HC08
335 | IP2022 ⇒ c_flag_IP2022 ]
338 (* getter di IRQ, non esiste sempre *)
339 ndefinition get_irq_flag ≝
340 λm:mcu_type.λt:memory_impl.λs:any_status m t.
342 return aux_get_type (option bool) with
343 [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
344 | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
345 | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
347 | IP2022 ⇒ λalu.None ? ]