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 (* pop forte di CALL *)
279 ndefinition pop_call_reg ≝
282 return λm.Πt.any_status m t → option (ProdT word16 (any_status m t))
284 [ HC05 ⇒ λt:memory_impl.λs:any_status HC05 t.None ?
285 | HC08 ⇒ λt:memory_impl.λs:any_status HC08 t.None ?
286 | HCS08 ⇒ λt:memory_impl.λs:any_status HCS08 t.None ?
287 | RS08 ⇒ λt:memory_impl.λs:any_status RS08 t.None ?
288 | IP2022 ⇒ λt:memory_impl.λs:any_status IP2022 t.
289 match pop_call_reg_IP2022 (alu … s) with
290 [ pair val alu' ⇒ Some ? (pair … val (set_alu … s alu')) ]
295 (* setter forte di IP *)
296 ndefinition set_ip_reg ≝
297 λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
298 opt_map … (match m return aux_set_type_opt word16 with
303 | IP2022 ⇒ Some ? set_ip_reg_IP2022 ])
304 (λf.Some ? (set_alu m t s (f (alu m t s) ip'))).
306 (* setter debole di IP *)
307 ndefinition setweak_ip_reg ≝
308 λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
309 match set_ip_reg m t s ip' with
310 [ None ⇒ s | Some s' ⇒ s' ].
314 (* setter forte di DP *)
315 ndefinition set_dp_reg ≝
316 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
317 opt_map … (match m return aux_set_type_opt word16 with
322 | IP2022 ⇒ Some ? set_dp_reg_IP2022 ])
323 (λf.Some ? (set_alu m t s (f (alu m t s) dp'))).
325 (* setter debole di DP *)
326 ndefinition setweak_dp_reg ≝
327 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
328 match set_dp_reg m t s dp' with
329 [ None ⇒ s | Some s' ⇒ s' ].
333 (* setter forte di DATA *)
334 ndefinition set_data_reg ≝
335 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
336 opt_map … (match m return aux_set_type_opt word16 with
341 | IP2022 ⇒ Some ? set_data_reg_IP2022 ])
342 (λf.Some ? (set_alu m t s (f (alu m t s) data'))).
344 (* setter debole di DATA *)
345 ndefinition setweak_data_reg ≝
346 λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
347 match set_data_reg m t s data' with
348 [ None ⇒ s | Some s' ⇒ s' ].
352 (* setter forte di SPEED *)
353 ndefinition set_speed_reg ≝
354 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
355 opt_map … (match m return aux_set_type_opt exadecim with
360 | IP2022 ⇒ Some ? set_speed_reg_IP2022 ])
361 (λf.Some ? (set_alu m t s (f (alu m t s) speed'))).
363 (* setter debole di SPEED *)
364 ndefinition setweak_speed_reg ≝
365 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
366 match set_speed_reg m t s speed' with
367 [ None ⇒ s | Some s' ⇒ s' ].
371 (* setter forte di PAGE *)
372 ndefinition set_page_reg ≝
373 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
374 opt_map … (match m return aux_set_type_opt oct with
379 | IP2022 ⇒ Some ? set_page_reg_IP2022 ])
380 (λf.Some ? (set_alu m t s (f (alu m t s) page'))).
382 (* setter debole di PAGE *)
383 ndefinition setweak_page_reg ≝
384 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
385 match set_page_reg m t s page' with
386 [ None ⇒ s | Some s' ⇒ s' ].
388 (* REGISTRO MEMORY MAPPED X *)
390 (* setter forte di memory mapped X *)
391 ndefinition set_x_map ≝
392 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
393 opt_map … (match m return aux_set_type_opt byte8 with
397 | RS08 ⇒ Some ? set_x_map_RS08
399 (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
401 (* setter debole di memory mapped X *)
402 ndefinition setweak_x_map ≝
403 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
404 match set_x_map m t s xm' with
405 [ None ⇒ s | Some s' ⇒ s' ].
407 (* REGISTRO MEMORY MAPPED PS *)
409 (* setter forte di memory mapped PS *)
410 ndefinition set_ps_map ≝
411 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
412 opt_map … (match m return aux_set_type_opt byte8 with
416 | RS08 ⇒ Some ? set_ps_map_RS08
418 (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
420 (* setter debole di memory mapped PS *)
421 ndefinition setweak_ps_map ≝
422 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
423 match set_ps_map m t s psm' with
424 [ None ⇒ s | Some s' ⇒ s' ].
428 (* setter forte di SKIP *)
429 ndefinition set_skip_mode ≝
430 λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
431 opt_map … (match m return aux_set_type_opt bool with
436 | IP2022 ⇒ Some ? set_skip_mode_IP2022 ])
437 (λf.Some ? (set_alu m t s (f (alu m t s) skipmode'))).
439 (* setter debole di SKIP *)
440 ndefinition setweak_skip_mode ≝
441 λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
442 match set_skip_mode m t s skipmode' with
443 [ None ⇒ s | Some s' ⇒ s' ].
447 (* setter forte di V *)
448 ndefinition set_v_flag ≝
449 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
450 opt_map … (match m return aux_set_type_opt bool with
452 | HC08 ⇒ Some ? set_v_flag_HC08
453 | HCS08 ⇒ Some ? set_v_flag_HC08
456 (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
458 (* setter debole di V *)
459 ndefinition setweak_v_flag ≝
460 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
461 match set_v_flag m t s vfl' with
462 [ None ⇒ s | Some s' ⇒ s' ].
466 (* setter forte di H *)
467 ndefinition set_h_flag ≝
468 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
469 opt_map … (match m return aux_set_type_opt bool with
470 [ HC05 ⇒ Some ? set_h_flag_HC05
471 | HC08 ⇒ Some ? set_h_flag_HC08
472 | HCS08 ⇒ Some ? set_h_flag_HC08
474 | IP2022 ⇒ Some ? set_h_flag_IP2022 ])
475 (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
477 (* setter debole di H *)
478 ndefinition setweak_h_flag ≝
479 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
480 match set_h_flag m t s hfl' with
481 [ None ⇒ s | Some s' ⇒ s' ].
485 (* setter forte di I *)
486 ndefinition set_i_flag ≝
487 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
488 opt_map … (match m return aux_set_type_opt bool with
489 [ HC05 ⇒ Some ? set_i_flag_HC05
490 | HC08 ⇒ Some ? set_i_flag_HC08
491 | HCS08 ⇒ Some ? set_i_flag_HC08
494 (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
496 (* setter debole di I *)
497 ndefinition setweak_i_flag ≝
498 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
499 match set_i_flag m t s ifl' with
500 [ None ⇒ s | Some s' ⇒ s' ].
504 (* setter forte di N *)
505 ndefinition set_n_flag ≝
506 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
507 opt_map … (match m return aux_set_type_opt bool with
508 [ HC05 ⇒ Some ? set_n_flag_HC05
509 | HC08 ⇒ Some ? set_n_flag_HC08
510 | HCS08 ⇒ Some ? set_n_flag_HC08
513 (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
515 (* setter debole di N *)
516 ndefinition setweak_n_flag ≝
517 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
518 match set_n_flag m t s nfl' with
519 [ None ⇒ s | Some s' ⇒ s' ].
523 (* setter forte di Z *)
524 ndefinition set_z_flag ≝
525 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
527 (match m return aux_set_type bool with
528 [ HC05 ⇒ set_z_flag_HC05
529 | HC08 ⇒ set_z_flag_HC08
530 | HCS08 ⇒ set_z_flag_HC08
531 | RS08 ⇒ set_z_flag_RS08
532 | IP2022 ⇒ set_z_flag_IP2022
537 (* setter forte di C *)
538 ndefinition set_c_flag ≝
539 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
541 (match m return aux_set_type bool with
542 [ HC05 ⇒ set_c_flag_HC05
543 | HC08 ⇒ set_c_flag_HC08
544 | HCS08 ⇒ set_c_flag_HC08
545 | RS08 ⇒ set_c_flag_RS08
546 | IP2022 ⇒ set_c_flag_IP2022
551 (* setter forte di IRQ *)
552 ndefinition set_irq_flag ≝
553 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
554 opt_map … (match m return aux_set_type_opt bool with
555 [ HC05 ⇒ Some ? set_irq_flag_HC05
556 | HC08 ⇒ Some ? set_irq_flag_HC08
557 | HCS08 ⇒ Some ? set_irq_flag_HC08
560 (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
562 (* setter debole di IRQ *)
563 ndefinition setweak_irq_flag ≝
564 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
565 match set_irq_flag m t s irqfl' with
566 [ None ⇒ s | Some s' ⇒ s' ].