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 *)
28 (* - letture filtrate, quindi da segmento 0 *)
30 (* lettura byte da addr *)
31 ndefinition loadb_from ≝
32 λm:mcu_type.λt:memory_impl.λs:any_status m t.
33 λaddr:word16.λcur_pc:word16.λfetched:exadecim.
34 opt_map … (memory_filter_read … s addr)
35 (λb.Some ? (triple … s b (plusc_d_d ? cur_pc (extu2_w16 fetched)))).
37 (* lettura bit da addr *)
38 ndefinition loadbit_from ≝
39 λm:mcu_type.λt:memory_impl.λs:any_status m t.
40 λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:exadecim.
41 opt_map … (memory_filter_read_bit … s addr sub)
42 (λb.Some ? (triple … s b (plusc_d_d ? cur_pc (extu2_w16 fetched)))).
44 (* lettura word da addr *)
45 ndefinition loadw_from ≝
46 λm:mcu_type.λt:memory_impl.λs:any_status m t.
47 λaddr:word16.λcur_pc:word16.λfetched:exadecim.
48 opt_map … (memory_filter_read … s addr)
49 (λbh.opt_map … (memory_filter_read … s (succc ? addr))
50 (λbl.Some ? (triple … s 〈bh:bl〉 (plusc_d_d ? cur_pc (extu2_w16 fetched))))).
52 (* scrittura byte su addr *)
53 ndefinition writeb_to ≝
54 λm:mcu_type.λt:memory_impl.λs:any_status m t.
55 λaddr:word16.λflag:aux_mod_type.λcur_pc:word16.λfetched:exadecim.λwriteb:byte8.
56 opt_map … (memory_filter_write … s addr flag writeb)
57 (λtmps.Some ? (pair … tmps (plusc_d_d ? cur_pc (extu2_w16 fetched)))).
59 (* scrittura bit su addr *)
60 ndefinition writebit_to ≝
61 λm:mcu_type.λt:memory_impl.λs:any_status m t.
62 λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:exadecim.λwriteb:bool.
63 opt_map … (memory_filter_write_bit … s addr sub writeb)
64 (λtmps.Some ? (pair … tmps (plusc_d_d ? cur_pc (extu2_w16 fetched)))).
66 (* scrittura word su addr *)
67 ndefinition writew_to ≝
68 λm:mcu_type.λt:memory_impl.λs:any_status m t.
69 λaddr:word16.λflag:aux_mod_type.λcur_pc:word16.λfetched:exadecim.λwritew:word16.
70 opt_map … (memory_filter_write … s addr auxMode_ok (cnH ? writew))
71 (λtmps1.opt_map … (memory_filter_write … tmps1 (succc ? addr) auxMode_ok (cnL ? writew))
72 (λtmps2.Some ? (pair … tmps2 (plusc_d_d ? cur_pc (extu2_w16 fetched))))).
74 (* ausiliari per definire i tipi e la lettura/scrittura *)
76 (* ausiliaria per definire il tipo di aux_load *)
77 ndefinition aux_load_typing ≝
78 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
79 any_status m t → word16 → word16 → exadecim →
80 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
82 (* per non dover ramificare i vari load in byte/word *)
83 ndefinition aux_load ≝
84 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
85 [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
87 (* ausiliaria per definire il tipo di aux_write *)
88 ndefinition aux_write_typing ≝
89 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
90 any_status m t → word16 → aux_mod_type → word16 → exadecim →
91 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
92 option (ProdT (any_status m t) word16).
94 (* per non dover ramificare i vari load in byte/word *)
95 ndefinition aux_write ≝
96 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
97 [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
99 ndefinition mem_read_s ≝
100 λm,t.λs:any_status m t.mem_read t (mem_desc … s) (chk_desc … s).
102 ndefinition mem_read_bit_s ≝
103 λm,t.λs:any_status m t.mem_read_bit t (mem_desc … s) (chk_desc … s).
105 ndefinition mem_write_s ≝
106 λm,t.λs:any_status m t.λseg,a,val.
107 opt_map … (mem_update t (mem_desc … s) (chk_desc … s) seg a val)
108 (λmem'.Some ? (set_mem_desc … s mem')).
110 ndefinition mem_write_bit_s ≝
111 λm,t.λs:any_status m t.λseg,a,sub,val.
112 opt_map … (mem_update_bit t (mem_desc … s) (chk_desc … s) seg a sub val)
113 (λmem'.Some ? (set_mem_desc … s mem')).