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 *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 set "baseuri" "cic:/matita/freescale/memory_bits/".
29 (*include "/media/VIRTUOSO/freescale/memory_trees.ma".*)
30 include "freescale/memory_trees.ma".
32 (* ********************* *)
33 (* MEMORIA E DESCRITTORE *)
34 (* ********************* *)
36 (* tutta la memoria non installata *)
37 definition mb_out_of_bound_memory ≝
38 let base ≝ array_8T memory_type MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
39 MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND in
40 let lev4 ≝ array_16T ?
41 base base base base base base base base
42 base base base base base base base base
44 let lev3 ≝ array_16T ?
45 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
46 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
48 let lev2 ≝ array_16T ?
49 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
50 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
52 let lev1 ≝ array_16T ?
53 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
54 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
58 (* tutta la memoria a 0 *)
59 definition mb_zero_memory ≝
60 let base ≝ array_8T bool false false false false false false false false in
61 let lev4 ≝ array_16T ?
62 base base base base base base base base
63 base base base base base base base base
65 let lev3 ≝ array_16T ?
66 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
67 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
69 let lev2 ≝ array_16T ?
70 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
71 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
73 let lev1 ≝ array_16T ?
74 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
75 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
79 (* scrivi bit controllando il tipo di memoria *)
80 definition mb_mem_update_bit ≝
81 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
82 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
83 λaddr:word16.λsub:oct.λv:bool.
84 match getn_array8T sub memory_type (mt_visit (Prod8T memory_type) chk addr) with
85 (* ROM? ok, ma il valore viene perso *)
86 [ MEM_READ_ONLY ⇒ Some ? mem
88 | MEM_READ_WRITE ⇒ Some ? (mt_update (Prod8T bool) mem addr (setn_array8T sub bool (mt_visit (Prod8T bool) mem addr) v))
89 (* NON INSTALLATA? no *)
90 | MEM_OUT_OF_BOUND ⇒ None ? ].
92 (* scrivi tipo di bit *)
93 definition mb_chk_update_bit ≝
94 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
95 λaddr:word16.λsub:oct.λv:memory_type.
96 mt_update (Prod8T memory_type) chk addr (setn_array8T sub memory_type (mt_visit (Prod8T memory_type) chk addr) v).
98 (* leggi bit controllando il tipo di memoria *)
99 definition mb_mem_read_bit ≝
100 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
101 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
102 λaddr:word16.λsub:oct.
103 match getn_array8T sub memory_type (mt_visit (Prod8T memory_type) chk addr) with
104 (* ROM? ok, ma il valore viene perso *)
105 [ MEM_READ_ONLY ⇒ Some ? (getn_array8T sub bool (mt_visit (Prod8T bool) mem addr))
107 | MEM_READ_WRITE ⇒ Some ? (getn_array8T sub bool (mt_visit (Prod8T bool) mem addr))
108 (* NON INSTALLATA? no *)
109 | MEM_OUT_OF_BOUND ⇒ None ? ].
111 (* scrivi controllando il tipo di memoria *)
112 (* NB: devono esistere tutti i bit *)
113 definition mb_mem_update ≝
114 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
115 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
116 λaddr:word16.λv:byte8.
117 let bit_types ≝ mt_visit (Prod8T memory_type) chk addr in
118 let old_value ≝ mt_visit (Prod8T bool) mem addr in
119 let new_value ≝ bits_of_byte8 v in
120 let newbit0 ≝ match getn_array8T o0 memory_type bit_types 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 bit_types 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 bit_types 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 bit_types 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 bit_types 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 bit_types 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 bit_types 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 bit_types 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 (Prod8T 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 definition mb_mem_read ≝
165 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
166 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
168 let bit_types ≝ mt_visit (Prod8T memory_type) chk addr in
169 let value ≝ mt_visit (Prod8T 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 let rec mb_load_from_source_at (old_mem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))))
218 (source:list byte8) (addr:word16) on source ≝
220 (* fine di source: carica da old_mem *)
222 | cons hd tl ⇒ match lt_w16 addr 〈〈xF,xF〉:〈xF,xF〉〉 with
223 (* non supera 0xFFFF, ricorsione *)
224 [ true ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16nc addr 〈〈x0,x0〉:〈x0,x1〉〉)
225 (* supera 0xFFFF, niente ricorsione *)
226 | false ⇒ mt_update ? old_mem addr (bits_of_byte8 hd)