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