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_addr_reg_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 ? (get_call_reg_IP2022 alu) ]
168 (* getter di IP, non esiste sempre *)
169 ndefinition get_ip_reg ≝
170 λm:mcu_type.λt:memory_impl.λs:any_status m t.
172 return aux_get_type (option word16) with
175 | HCS08 ⇒ λalu.None ?
177 | IP2022 ⇒ λalu.Some ? (ip_reg_IP2022 alu) ]
180 (* getter di DP, non esiste sempre *)
181 ndefinition get_dp_reg ≝
182 λm:mcu_type.λt:memory_impl.λs:any_status m t.
184 return aux_get_type (option word16) with
187 | HCS08 ⇒ λalu.None ?
189 | IP2022 ⇒ λalu.Some ? (dp_reg_IP2022 alu) ]
192 (* getter di DATA, non esiste sempre *)
193 ndefinition get_data_reg ≝
194 λm:mcu_type.λt:memory_impl.λs:any_status m t.
196 return aux_get_type (option word16) with
199 | HCS08 ⇒ λalu.None ?
201 | IP2022 ⇒ λalu.Some ? (data_reg_IP2022 alu) ]
204 (* getter di SPEED, non esiste sempre *)
205 ndefinition get_speed_reg ≝
206 λm:mcu_type.λt:memory_impl.λs:any_status m t.
208 return aux_get_type (option exadecim) with
211 | HCS08 ⇒ λalu.None ?
213 | IP2022 ⇒ λalu.Some ? (speed_reg_IP2022 alu) ]
216 (* getter di PAGE, non esiste sempre *)
217 ndefinition get_page_reg ≝
218 λm:mcu_type.λt:memory_impl.λs:any_status m t.
220 return aux_get_type (option oct) with
223 | HCS08 ⇒ λalu.None ?
225 | IP2022 ⇒ λalu.Some ? (page_reg_IP2022 alu) ]
228 (* REGISTRI SPECIALI *)
230 (* getter di memory mapped X, non esiste sempre *)
231 ndefinition get_x_map ≝
232 λm:mcu_type.λt:memory_impl.λs:any_status m t.
234 return aux_get_type (option byte8) with
237 | HCS08 ⇒ λalu.None ?
238 | RS08 ⇒ λalu.Some ? (x_map_RS08 alu)
239 | IP2022 ⇒ λalu.None ? ]
242 (* getter di memory mapped PS, non esiste sempre *)
243 ndefinition get_ps_map ≝
244 λm:mcu_type.λt:memory_impl.λs:any_status m t.
246 return aux_get_type (option byte8) with
249 | HCS08 ⇒ λalu.None ?
250 | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu)
251 | IP2022 ⇒ λalu.None ? ]
254 (* getter di skip mode, non esiste sempre *)
255 ndefinition get_skip_mode ≝
256 λm:mcu_type.λt:memory_impl.λs:any_status m t.
258 return aux_get_type (option bool) with
261 | HCS08 ⇒ λalu.None ?
263 | IP2022 ⇒ λalu.Some ? (skip_mode_IP2022 alu) ]
268 (* getter di V, non esiste sempre *)
269 ndefinition get_v_flag ≝
270 λm:mcu_type.λt:memory_impl.λs:any_status m t.
272 return aux_get_type (option bool) with
274 | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
275 | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
277 | IP2022 ⇒ λalu.None ? ]
280 (* getter di H, non esiste sempre *)
281 ndefinition get_h_flag ≝
282 λm:mcu_type.λt:memory_impl.λs:any_status m t.
284 return aux_get_type (option bool) with
285 [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
286 | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
287 | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
289 | IP2022 ⇒ λalu.Some ? (h_flag_IP2022 alu) ]
292 (* getter di I, non esiste sempre *)
293 ndefinition get_i_flag ≝
294 λm:mcu_type.λt:memory_impl.λs:any_status m t.
296 return aux_get_type (option bool) with
297 [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
298 | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
299 | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
301 | IP2022 ⇒ λalu.None ? ]
304 (* getter di N, non esiste sempre *)
305 ndefinition get_n_flag ≝
306 λm:mcu_type.λt:memory_impl.λs:any_status m t.
308 return aux_get_type (option bool) with
309 [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
310 | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
311 | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
313 | IP2022 ⇒ λalu.None ? ]
316 (* getter di Z, esiste sempre *)
317 ndefinition get_z_flag ≝
318 λm:mcu_type.λt:memory_impl.λs:any_status m t.
320 return aux_get_type bool with
323 | HCS08 ⇒ z_flag_HC08
325 | IP2022 ⇒ z_flag_IP2022 ]
328 (* getter di C, esiste sempre *)
329 ndefinition get_c_flag ≝
330 λm:mcu_type.λt:memory_impl.λs:any_status m t.
332 return aux_get_type bool with
335 | HCS08 ⇒ c_flag_HC08
337 | IP2022 ⇒ c_flag_IP2022 ]
340 (* getter di IRQ, non esiste sempre *)
341 ndefinition get_irq_flag ≝
342 λm:mcu_type.λt:memory_impl.λs:any_status m t.
344 return aux_get_type (option bool) with
345 [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
346 | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
347 | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
349 | IP2022 ⇒ λalu.None ? ]