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.ma".
25 (* ***************************** *)
26 (* SETTER SPECIFICI FORTI/DEBOLI *)
27 (* ***************************** *)
29 (* funzione ausiliaria per il tipaggio dei setter forti *)
30 ndefinition aux_set_type ≝ λx:Type.λm:mcu_type.
31 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
32 | IP2022 ⇒ alu_IP2022 ]
34 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
35 | IP2022 ⇒ alu_IP2022 ].
37 (* funzione ausiliaria per il tipaggio dei setter deboli *)
38 ndefinition aux_set_type_opt ≝ λx:Type.λm:mcu_type.option
39 (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
40 | IP2022 ⇒ alu_IP2022 ]
42 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
43 | IP2022 ⇒ alu_IP2022 ]).
45 (* DESCRITTORI ESTERNI ALLA ALU *)
47 (* setter forte della ALU *)
49 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
50 mk_any_status m t alu' (mem_desc m t s) (chk_desc m t s) (clk_desc m t s).
52 (* setter forte della memoria *)
53 ndefinition set_mem_desc ≝
54 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
55 mk_any_status m t (alu m t s) mem' (chk_desc m t s) (clk_desc m t s).
57 (* setter forte del descrittore *)
58 ndefinition set_chk_desc ≝
59 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
60 mk_any_status m t (alu m t s) (mem_desc m t s) chk' (clk_desc m t s).
62 (* setter forte del clik *)
63 ndefinition set_clk_desc ≝
64 λm:mcu_type.λt:memory_impl.λs:any_status m t.
65 λclk':option (aux_clk_type m).
66 mk_any_status m t (alu m t s) (mem_desc m t s) (chk_desc m t s) clk'.
70 (* setter forte di A *)
71 ndefinition set_acc_8_low_reg ≝
72 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
74 (match m return aux_set_type byte8 with
75 [ HC05 ⇒ set_acc_8_low_reg_HC05
76 | HC08 ⇒ set_acc_8_low_reg_HC08
77 | HCS08 ⇒ set_acc_8_low_reg_HC08
78 | RS08 ⇒ set_acc_8_low_reg_RS08
79 | IP2022 ⇒ set_acc_8_low_reg_IP2022
80 ] (alu m t s) acclow').
84 (* setter forte di X *)
85 ndefinition set_indX_8_low_reg ≝
86 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
87 opt_map … (match m return aux_set_type_opt byte8 with
88 [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
89 | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
90 | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
93 (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
95 (* setter debole di X *)
96 ndefinition setweak_indX_8_low_reg ≝
97 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
98 match set_indX_8_low_reg m t s indxlow' with
99 [ None ⇒ s | Some s' ⇒ s' ].
103 (* setter forte di H *)
104 ndefinition set_indX_8_high_reg ≝
105 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
106 opt_map … (match m return aux_set_type_opt byte8 with
108 | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
109 | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
112 (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
114 (* setter debole di H *)
115 ndefinition setweak_indX_8_high_reg ≝
116 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
117 match set_indX_8_high_reg m t s indxhigh' with
118 [ None ⇒ s | Some s' ⇒ s' ].
122 (* setter forte di H:X *)
123 ndefinition set_indX_16_reg ≝
124 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
125 opt_map … (match m return aux_set_type_opt word16 with
127 | HC08 ⇒ Some ? set_indX_16_reg_HC08
128 | HCS08 ⇒ Some ? set_indX_16_reg_HC08
131 (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
133 (* setter debole di H:X *)
134 ndefinition setweak_indX_16_reg ≝
135 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
136 match set_indX_16_reg m t s indx16 with
137 [ None ⇒ s | Some s' ⇒ s' ].
141 (* setter forte di SP *)
142 ndefinition set_sp_reg ≝
143 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
144 opt_map … (match m return aux_set_type_opt word16 with
145 [ HC05 ⇒ Some ? set_sp_reg_HC05
146 | HC08 ⇒ Some ? set_sp_reg_HC08
147 | HCS08 ⇒ Some ? set_sp_reg_HC08
149 | IP2022 ⇒ Some ? set_sp_reg_IP2022 ])
150 (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
152 (* setter debole di SP *)
153 ndefinition setweak_sp_reg ≝
154 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
155 match set_sp_reg m t s sp' with
156 [ None ⇒ s | Some s' ⇒ s' ].
160 (* setter forte di PC *)
161 ndefinition set_pc_reg ≝
162 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
164 (match m return aux_set_type word16 with
165 [ HC05 ⇒ set_pc_reg_HC05
166 | HC08 ⇒ set_pc_reg_HC08
167 | HCS08 ⇒ set_pc_reg_HC08
168 | RS08 ⇒ set_pc_reg_RS08
169 | IP2022 ⇒ set_pc_reg_IP2022
174 (* setter forte di SPC *)
175 ndefinition set_spc_reg ≝
176 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
177 opt_map … (match m return aux_set_type_opt word16 with
181 | RS08 ⇒ Some ? set_spc_reg_RS08
183 (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
185 (* setter debole di SPC *)
186 ndefinition setweak_spc_reg ≝
187 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
188 match set_spc_reg m t s spc' with
189 [ None ⇒ s | Some s' ⇒ s' ].
193 (* setter forte di MULH *)
194 ndefinition set_mulh_reg ≝
195 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmulh':byte8.
196 opt_map … (match m return aux_set_type_opt byte8 with
201 | IP2022 ⇒ Some ? set_mulh_reg_IP2022 ])
202 (λf.Some ? (set_alu m t s (f (alu m t s) mulh'))).
204 (* setter debole di MULH *)
205 ndefinition setweak_mulh_reg ≝
206 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmulh':byte8.
207 match set_mulh_reg m t s mulh' with
208 [ None ⇒ s | Some s' ⇒ s' ].
210 (* REGISTRO ADDRSEL *)
212 (* setter forte di ADDRSEL *)
213 ndefinition set_addrsel_reg ≝
214 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddrsel':byte8.
215 opt_map … (match m return aux_set_type_opt byte8 with
220 | IP2022 ⇒ Some ? set_addrsel_reg_IP2022 ])
221 (λf.Some ? (set_alu m t s (f (alu m t s) addrsel'))).
223 (* setter debole di ADDRSEL *)
224 ndefinition setweak_addrsel_reg ≝
225 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddrsel':byte8.
226 match set_addrsel_reg m t s addrsel' with
227 [ None ⇒ s | Some s' ⇒ s' ].
231 (* setter forte di ADDR *)
232 ndefinition set_addr_reg ≝
233 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr':word24.
234 opt_map … (match m return aux_set_type_opt word24 with
239 | IP2022 ⇒ Some ? set_addr_reg_IP2022 ])
240 (λf.Some ? (set_alu m t s (f (alu m t s) addr'))).
242 (* setter debole di ADDR *)
243 ndefinition setweak_addr_reg ≝
244 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr':word24.
245 match set_addr_reg m t s addr' with
246 [ None ⇒ s | Some s' ⇒ s' ].
250 (* setter forte di CALL *)
251 ndefinition set_call_reg ≝
252 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
253 opt_map … (match m return aux_set_type_opt word16 with
258 | IP2022 ⇒ Some ? set_call_reg_IP2022 ])
259 (λf.Some ? (set_alu m t s (f (alu m t s) call'))).
261 (* setter debole di CALL *)
262 ndefinition setweak_call_reg ≝
263 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
264 match set_call_reg m t s call' with
265 [ None ⇒ s | Some s' ⇒ s' ].
267 (* push forte di CALL *)
268 ndefinition push_call_reg ≝
269 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
270 opt_map … (match m return aux_set_type_opt word16 with
275 | IP2022 ⇒ Some ? push_call_reg_IP2022 ])
276 (λf.Some ? (set_alu m t s (f (alu m t s) call'))).
278 (* push debole di CALL *)
279 ndefinition pushweak_call_reg ≝
280 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
281 match push_call_reg m t s call' with
282 [ None ⇒ s | Some s' ⇒ s' ].
286 (* setter forte di IP *)
287 ndefinition set_ip_reg ≝
288 λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
289 opt_map … (match m return aux_set_type_opt word16 with
294 | IP2022 ⇒ Some ? set_ip_reg_IP2022 ])
295 (λf.Some ? (set_alu m t s (f (alu m t s) ip'))).
297 (* setter debole di IP *)
298 ndefinition setweak_ip_reg ≝
299 λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
300 match set_ip_reg m t s ip' with
301 [ None ⇒ s | Some s' ⇒ s' ].
305 (* setter forte di DP *)
306 ndefinition set_dp_reg ≝
307 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
308 opt_map … (match m return aux_set_type_opt word16 with
313 | IP2022 ⇒ Some ? set_dp_reg_IP2022 ])
314 (λf.Some ? (set_alu m t s (f (alu m t s) dp'))).
316 (* setter debole di DP *)
317 ndefinition setweak_dp_reg ≝
318 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
319 match set_dp_reg m t s dp' with
320 [ None ⇒ s | Some s' ⇒ s' ].
324 (* setter forte di DATA *)
325 ndefinition set_data_reg ≝
326 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
327 opt_map … (match m return aux_set_type_opt word16 with
332 | IP2022 ⇒ Some ? set_data_reg_IP2022 ])
333 (λf.Some ? (set_alu m t s (f (alu m t s) data'))).
335 (* setter debole di DATA *)
336 ndefinition setweak_data_reg ≝
337 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
338 match set_data_reg m t s data' with
339 [ None ⇒ s | Some s' ⇒ s' ].
343 (* setter forte di SPEED *)
344 ndefinition set_speed_reg ≝
345 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
346 opt_map … (match m return aux_set_type_opt exadecim with
351 | IP2022 ⇒ Some ? set_speed_reg_IP2022 ])
352 (λf.Some ? (set_alu m t s (f (alu m t s) speed'))).
354 (* setter debole di SPEED *)
355 ndefinition setweak_speed_reg ≝
356 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
357 match set_speed_reg m t s speed' with
358 [ None ⇒ s | Some s' ⇒ s' ].
362 (* setter forte di PAGE *)
363 ndefinition set_page_reg ≝
364 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
365 opt_map … (match m return aux_set_type_opt oct with
370 | IP2022 ⇒ Some ? set_page_reg_IP2022 ])
371 (λf.Some ? (set_alu m t s (f (alu m t s) page'))).
373 (* setter debole di PAGE *)
374 ndefinition setweak_page_reg ≝
375 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
376 match set_page_reg m t s page' with
377 [ None ⇒ s | Some s' ⇒ s' ].
379 (* REGISTRO MEMORY MAPPED X *)
381 (* setter forte di memory mapped X *)
382 ndefinition set_x_map ≝
383 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
384 opt_map … (match m return aux_set_type_opt byte8 with
388 | RS08 ⇒ Some ? set_x_map_RS08
390 (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
392 (* setter debole di memory mapped X *)
393 ndefinition setweak_x_map ≝
394 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
395 match set_x_map m t s xm' with
396 [ None ⇒ s | Some s' ⇒ s' ].
398 (* REGISTRO MEMORY MAPPED PS *)
400 (* setter forte di memory mapped PS *)
401 ndefinition set_ps_map ≝
402 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
403 opt_map … (match m return aux_set_type_opt byte8 with
407 | RS08 ⇒ Some ? set_ps_map_RS08
409 (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
411 (* setter debole di memory mapped PS *)
412 ndefinition setweak_ps_map ≝
413 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
414 match set_ps_map m t s psm' with
415 [ None ⇒ s | Some s' ⇒ s' ].
419 (* setter forte di SKIP *)
420 ndefinition set_skip_mode ≝
421 λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
422 opt_map … (match m return aux_set_type_opt bool with
427 | IP2022 ⇒ Some ? set_skip_mode_IP2022 ])
428 (λf.Some ? (set_alu m t s (f (alu m t s) skipmode'))).
430 (* setter debole di SKIP *)
431 ndefinition setweak_skip_mode ≝
432 λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
433 match set_skip_mode m t s skipmode' with
434 [ None ⇒ s | Some s' ⇒ s' ].
438 (* setter forte di V *)
439 ndefinition set_v_flag ≝
440 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
441 opt_map … (match m return aux_set_type_opt bool with
443 | HC08 ⇒ Some ? set_v_flag_HC08
444 | HCS08 ⇒ Some ? set_v_flag_HC08
447 (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
449 (* setter debole di V *)
450 ndefinition setweak_v_flag ≝
451 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
452 match set_v_flag m t s vfl' with
453 [ None ⇒ s | Some s' ⇒ s' ].
457 (* setter forte di H *)
458 ndefinition set_h_flag ≝
459 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
460 opt_map … (match m return aux_set_type_opt bool with
461 [ HC05 ⇒ Some ? set_h_flag_HC05
462 | HC08 ⇒ Some ? set_h_flag_HC08
463 | HCS08 ⇒ Some ? set_h_flag_HC08
465 | IP2022 ⇒ Some ? set_h_flag_IP2022 ])
466 (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
468 (* setter debole di H *)
469 ndefinition setweak_h_flag ≝
470 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
471 match set_h_flag m t s hfl' with
472 [ None ⇒ s | Some s' ⇒ s' ].
476 (* setter forte di I *)
477 ndefinition set_i_flag ≝
478 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
479 opt_map … (match m return aux_set_type_opt bool with
480 [ HC05 ⇒ Some ? set_i_flag_HC05
481 | HC08 ⇒ Some ? set_i_flag_HC08
482 | HCS08 ⇒ Some ? set_i_flag_HC08
485 (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
487 (* setter debole di I *)
488 ndefinition setweak_i_flag ≝
489 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
490 match set_i_flag m t s ifl' with
491 [ None ⇒ s | Some s' ⇒ s' ].
495 (* setter forte di N *)
496 ndefinition set_n_flag ≝
497 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
498 opt_map … (match m return aux_set_type_opt bool with
499 [ HC05 ⇒ Some ? set_n_flag_HC05
500 | HC08 ⇒ Some ? set_n_flag_HC08
501 | HCS08 ⇒ Some ? set_n_flag_HC08
504 (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
506 (* setter debole di N *)
507 ndefinition setweak_n_flag ≝
508 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
509 match set_n_flag m t s nfl' with
510 [ None ⇒ s | Some s' ⇒ s' ].
514 (* setter forte di Z *)
515 ndefinition set_z_flag ≝
516 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
518 (match m return aux_set_type bool with
519 [ HC05 ⇒ set_z_flag_HC05
520 | HC08 ⇒ set_z_flag_HC08
521 | HCS08 ⇒ set_z_flag_HC08
522 | RS08 ⇒ set_z_flag_RS08
523 | IP2022 ⇒ set_z_flag_IP2022
528 (* setter forte di C *)
529 ndefinition set_c_flag ≝
530 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
532 (match m return aux_set_type bool with
533 [ HC05 ⇒ set_c_flag_HC05
534 | HC08 ⇒ set_c_flag_HC08
535 | HCS08 ⇒ set_c_flag_HC08
536 | RS08 ⇒ set_c_flag_RS08
537 | IP2022 ⇒ set_c_flag_IP2022
542 (* setter forte di IRQ *)
543 ndefinition set_irq_flag ≝
544 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
545 opt_map … (match m return aux_set_type_opt bool with
546 [ HC05 ⇒ Some ? set_irq_flag_HC05
547 | HC08 ⇒ Some ? set_irq_flag_HC08
548 | HCS08 ⇒ Some ? set_irq_flag_HC08
551 (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
553 (* setter debole di IRQ *)
554 ndefinition setweak_irq_flag ≝
555 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
556 match set_irq_flag m t s irqfl' with
557 [ None ⇒ s | Some s' ⇒ s' ].