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 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "freescale/memory_trees.ma".
25 (* ********************* *)
26 (* MEMORIA E DESCRITTORE *)
27 (* ********************* *)
29 (* tutta la memoria non installata *)
30 ndefinition mb_out_of_bound_memory ≝
31 let base ≝ array_8T memory_type MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
32 MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND in
33 let lev4 ≝ array_16T ?
34 base base base base base base base base
35 base base base base base base base base
37 let lev3 ≝ array_16T ?
38 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
39 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
41 let lev2 ≝ array_16T ?
42 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
43 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
45 let lev1 ≝ array_16T ?
46 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
47 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
51 (* tutta la memoria a 0 *)
52 ndefinition mb_zero_memory ≝
53 let base ≝ array_8T bool false false false false false false false false in
54 let lev4 ≝ array_16T ?
55 base base base base base base base base
56 base base base base base base base base
58 let lev3 ≝ array_16T ?
59 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
60 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
62 let lev2 ≝ array_16T ?
63 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
64 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
66 let lev1 ≝ array_16T ?
67 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
68 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
72 (* scrivi bit controllando il tipo di memoria *)
73 ndefinition mb_mem_update_bit ≝
74 λmem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))).
75 λchk:Array16T (Array16T (Array16T (Array16T (Array8T memory_type)))).
76 λaddr:word16.λsub:oct.λv:bool.
77 match getn_array8T sub memory_type (mt_visit (Array8T memory_type) chk addr) with
78 (* ROM? ok, ma il valore viene perso *)
79 [ MEM_READ_ONLY ⇒ Some ? mem
81 | MEM_READ_WRITE ⇒ Some ? (mt_update (Array8T bool) mem addr (setn_array8T sub bool (mt_visit (Array8T bool) mem addr) v))
82 (* NON INSTALLATA? no *)
83 | MEM_OUT_OF_BOUND ⇒ None ? ].
85 (* scrivi tipo di bit *)
86 ndefinition mb_chk_update_bit ≝
87 λchk:Array16T (Array16T (Array16T (Array16T (Array8T memory_type)))).
88 λaddr:word16.λsub:oct.λv:memory_type.
89 mt_update (Array8T memory_type) chk addr (setn_array8T sub memory_type (mt_visit (Array8T memory_type) chk addr) v).
91 (* leggi bit controllando il tipo di memoria *)
92 ndefinition mb_mem_read_bit ≝
93 λmem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))).
94 λchk:Array16T (Array16T (Array16T (Array16T (Array8T memory_type)))).
95 λaddr:word16.λsub:oct.
96 match getn_array8T sub memory_type (mt_visit (Array8T memory_type) chk addr) with
97 (* ROM? ok, ma il valore viene perso *)
98 [ MEM_READ_ONLY ⇒ Some ? (getn_array8T sub bool (mt_visit (Array8T bool) mem addr))
100 | MEM_READ_WRITE ⇒ Some ? (getn_array8T sub bool (mt_visit (Array8T bool) mem addr))
101 (* NON INSTALLATA? no *)
102 | MEM_OUT_OF_BOUND ⇒ None ? ].
104 ndefinition mb_chk_get ≝
105 λchk:Array16T (Array16T (Array16T (Array16T (Array8T memory_type)))).λaddr:word16.
106 let c ≝ mt_visit (Array8T memory_type) chk addr in
107 array_8T ? (getn_array8T o7 ? c) (getn_array8T o6 ? c)
108 (getn_array8T o5 ? c) (getn_array8T o4 ? c)
109 (getn_array8T o3 ? c) (getn_array8T o2 ? c)
110 (getn_array8T o1 ? c) (getn_array8T o0 ? c).
112 (* scrivi controllando il tipo di memoria *)
113 (* NB: devono esistere tutti i bit *)
114 ndefinition mb_mem_update ≝
115 λmem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))).
116 λchk:Array8T memory_type.
117 λaddr:word16.λv:byte8.
118 let old_value ≝ mt_visit (Array8T bool) mem addr in
119 let new_value ≝ bits_of_byte8 v in
120 let newbit0 ≝ match getn_array8T o0 memory_type chk with
121 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool old_value)
122 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool new_value)
123 | MEM_OUT_OF_BOUND ⇒ None bool ] in
124 let newbit1 ≝ match getn_array8T o1 memory_type chk with
125 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool old_value)
126 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool new_value)
127 | MEM_OUT_OF_BOUND ⇒ None bool ] in
128 let newbit2 ≝ match getn_array8T o2 memory_type chk with
129 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool old_value)
130 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool new_value)
131 | MEM_OUT_OF_BOUND ⇒ None bool ] in
132 let newbit3 ≝ match getn_array8T o3 memory_type chk with
133 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool old_value)
134 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool new_value)
135 | MEM_OUT_OF_BOUND ⇒ None bool ] in
136 let newbit4 ≝ match getn_array8T o4 memory_type chk with
137 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool old_value)
138 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool new_value)
139 | MEM_OUT_OF_BOUND ⇒ None bool ] in
140 let newbit5 ≝ match getn_array8T o5 memory_type chk with
141 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool old_value)
142 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool new_value)
143 | MEM_OUT_OF_BOUND ⇒ None bool ] in
144 let newbit6 ≝ match getn_array8T o6 memory_type chk with
145 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool old_value)
146 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool new_value)
147 | MEM_OUT_OF_BOUND ⇒ None bool ] in
148 let newbit7 ≝ match getn_array8T o7 memory_type chk with
149 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool old_value)
150 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool new_value)
151 | MEM_OUT_OF_BOUND ⇒ None bool ] in
153 (λnb0.opt_map … newbit1
154 (λnb1.opt_map … newbit2
155 (λnb2.opt_map … newbit3
156 (λnb3.opt_map … newbit4
157 (λnb4.opt_map … newbit5
158 (λnb5.opt_map … newbit6
159 (λnb6.opt_map … newbit7
160 (λnb7.Some ? (mt_update (Array8T bool) mem addr (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
162 (* leggi controllando il tipo di memoria *)
163 (* NB: devono esistere tutti i bit *)
164 ndefinition mb_mem_read ≝
165 λmem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))).
166 λchk:Array16T (Array16T (Array16T (Array16T (Array8T memory_type)))).
168 let bit_types ≝ mt_visit (Array8T memory_type) chk addr in
169 let value ≝ mt_visit (Array8T bool) mem addr in
170 let newbit0 ≝ match getn_array8T o0 memory_type bit_types with
171 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool value)
172 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool value)
173 | MEM_OUT_OF_BOUND ⇒ None bool ] in
174 let newbit1 ≝ match getn_array8T o1 memory_type bit_types with
175 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool value)
176 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool value)
177 | MEM_OUT_OF_BOUND ⇒ None bool ] in
178 let newbit2 ≝ match getn_array8T o2 memory_type bit_types with
179 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool value)
180 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool value)
181 | MEM_OUT_OF_BOUND ⇒ None bool ] in
182 let newbit3 ≝ match getn_array8T o3 memory_type bit_types with
183 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool value)
184 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool value)
185 | MEM_OUT_OF_BOUND ⇒ None bool ] in
186 let newbit4 ≝ match getn_array8T o4 memory_type bit_types with
187 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool value)
188 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool value)
189 | MEM_OUT_OF_BOUND ⇒ None bool ] in
190 let newbit5 ≝ match getn_array8T o5 memory_type bit_types with
191 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool value)
192 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool value)
193 | MEM_OUT_OF_BOUND ⇒ None bool ] in
194 let newbit6 ≝ match getn_array8T o6 memory_type bit_types with
195 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool value)
196 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool value)
197 | MEM_OUT_OF_BOUND ⇒ None bool ] in
198 let newbit7 ≝ match getn_array8T o7 memory_type bit_types with
199 [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool value)
200 | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool value)
201 | MEM_OUT_OF_BOUND ⇒ None bool ] in
203 (λnb0.opt_map … newbit1
204 (λnb1.opt_map … newbit2
205 (λnb2.opt_map … newbit3
206 (λnb3.opt_map … newbit4
207 (λnb4.opt_map … newbit5
208 (λnb5.opt_map … newbit6
209 (λnb6.opt_map … newbit7
210 (λnb7.Some ? (byte8_of_bits (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
212 (* ************************** *)
213 (* CARICAMENTO PROGRAMMA/DATI *)
214 (* ************************** *)
216 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
217 nlet rec mb_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))))
218 (src:list byte8) (addr:word16) on src ≝
220 (* fine di source: carica da old_mem *)
222 | cons hd tl ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)