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/read_write/Freescale_load_write.ma".
24 include "emulator/read_write/IP2022_load_write.ma".
26 (* ************************************** *)
27 (* raccordo di tutte le possibili letture *)
28 (* ************************************** *)
30 ndefinition multi_mode_loadb ≝
32 return λm.Πt.any_status m t → word16 → aux_im_type m →
33 option (Prod3T (any_status m t) byte8 word16)
35 [ HC05 ⇒ Freescale_multi_mode_load_auxb HC05
36 | HC08 ⇒ Freescale_multi_mode_load_auxb HC08
37 | HCS08 ⇒ Freescale_multi_mode_load_auxb HCS08
38 | RS08 ⇒ Freescale_multi_mode_load_auxb RS08
39 | IP2022 ⇒ IP2022_multi_mode_load_auxb
42 ndefinition multi_mode_loadw ≝
44 return λm.Πt.any_status m t → word16 → aux_im_type m →
45 option (Prod3T (any_status m t) word16 word16)
47 [ HC05 ⇒ Freescale_multi_mode_load_auxw HC05
48 | HC08 ⇒ Freescale_multi_mode_load_auxw HC08
49 | HCS08 ⇒ Freescale_multi_mode_load_auxw HCS08
50 | RS08 ⇒ Freescale_multi_mode_load_auxw RS08
51 | IP2022 ⇒ IP2022_multi_mode_load_auxw
54 (* tutte le modalita' di lettura: false=loadb true=loadw *)
56 (* **************************************** *)
57 (* raccordo di tutte le possibili scritture *)
58 (* **************************************** *)
60 ndefinition multi_mode_writeb ≝
62 return λm.Πt.any_status m t → word16 → aux_im_type m → byte8 →
63 option (ProdT (any_status m t) word16)
65 [ HC05 ⇒ Freescale_multi_mode_write_auxb HC05
66 | HC08 ⇒ Freescale_multi_mode_write_auxb HC08
67 | HCS08 ⇒ Freescale_multi_mode_write_auxb HCS08
68 | RS08 ⇒ Freescale_multi_mode_write_auxb RS08
69 | IP2022 ⇒ IP2022_multi_mode_write_auxb
72 ndefinition multi_mode_writew ≝
74 return λm.Πt.any_status m t → word16 → aux_im_type m → word16 →
75 option (ProdT (any_status m t) word16)
77 [ HC05 ⇒ Freescale_multi_mode_write_auxw HC05
78 | HC08 ⇒ Freescale_multi_mode_write_auxw HC08
79 | HCS08 ⇒ Freescale_multi_mode_write_auxw HCS08
80 | RS08 ⇒ Freescale_multi_mode_write_auxw RS08
81 | IP2022 ⇒ IP2022_multi_mode_write_auxw