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/read_write.ma".
25 (* ************************ *)
26 (* MODALITA' INDIRIZZAMENTO *)
27 (* ************************ *)
30 (* - incrementano l'indirizzo normalmente *)
31 (* - incrementano PC attraverso il filtro *)
33 (* lettura byte da addr *)
34 ndefinition loadb_from ≝
35 λm:mcu_type.λt:memory_impl.λs:any_status m t.
36 λaddr:word32.λcur_pc:word16.λfetched:exadecim.
37 opt_map … (memory_filter_read … s addr)
38 (λb.Some ? (triple … s b (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
40 (* lettura bit da addr *)
41 ndefinition loadbit_from ≝
42 λm:mcu_type.λt:memory_impl.λs:any_status m t.
43 λaddr:word32.λsub:oct.λcur_pc:word16.λfetched:exadecim.
44 opt_map … (memory_filter_read_bit … s addr sub)
45 (λb.Some ? (triple … s b (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
47 (* lettura word da addr *)
48 ndefinition loadw_from ≝
49 λm:mcu_type.λt:memory_impl.λs:any_status m t.
50 λaddr:word32.λcur_pc:word16.λfetched:exadecim.
51 opt_map … (memory_filter_read … s addr)
52 (λbh.opt_map … (memory_filter_read … s (succ_w32 addr))
53 (λbl.Some ? (triple … s 〈bh:bl〉 (plus_w16_d_d cur_pc (extu2_w16 fetched))))).
55 (* scrittura byte su addr *)
56 ndefinition writeb_to ≝
57 λm:mcu_type.λt:memory_impl.λs:any_status m t.
58 λaddr:word32.λflag:aux_mod_type.λcur_pc:word16.λfetched:exadecim.λwriteb:byte8.
59 opt_map … (memory_filter_write … s addr flag writeb)
60 (λtmps.Some ? (pair … tmps (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
62 (* scrittura bit su addr *)
63 ndefinition writebit_to ≝
64 λm:mcu_type.λt:memory_impl.λs:any_status m t.
65 λaddr:word32.λsub:oct.λcur_pc:word16.λfetched:exadecim.λwriteb:bool.
66 opt_map … (memory_filter_write_bit … s addr sub writeb)
67 (λtmps.Some ? (pair … tmps (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
69 (* scrittura word su addr *)
70 ndefinition writew_to ≝
71 λm:mcu_type.λt:memory_impl.λs:any_status m t.
72 λaddr:word32.λflag:aux_mod_type.λcur_pc:word16.λfetched:exadecim.λwritew:word16.
73 opt_map … (memory_filter_write … s addr auxMode_ok (cnH ? writew))
74 (λtmps1.opt_map … (memory_filter_write … tmps1 (succ_w32 addr) auxMode_ok (cnL ? writew))
75 (λtmps2.Some ? (pair … tmps2 (plus_w16_d_d cur_pc (extu2_w16 fetched))))).
77 (* ausiliari per definire i tipi e la lettura/scrittura *)
79 (* ausiliaria per definire il tipo di aux_load *)
80 ndefinition aux_load_typing ≝
81 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
82 any_status m t → word32 → word16 → exadecim →
83 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
85 (* per non dover ramificare i vari load in byte/word *)
86 ndefinition aux_load ≝
87 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
88 [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
90 (* ausiliaria per definire il tipo di aux_write *)
91 ndefinition aux_write_typing ≝
92 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
93 any_status m t → word32 → aux_mod_type → word16 → exadecim →
94 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
95 option (ProdT (any_status m t) word16).
97 (* per non dover ramificare i vari load in byte/word *)
98 ndefinition aux_write ≝
99 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
100 [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
102 ndefinition mem_read_s ≝
103 λm,t.λs:any_status m t.mem_read t (mem_desc … s) (chk_desc … s).
105 ndefinition mem_read_bit_s ≝
106 λm,t.λs:any_status m t.mem_read_bit t (mem_desc … s) (chk_desc … s).