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: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/model.ma".
24 include "freescale/translation.ma".
26 (* errori possibili nel fetch *)
27 ninductive error_type : Type ≝
29 | ILL_FETCH_AD: error_type
30 | ILL_EX_AD: error_type.
32 ndefinition error_type_ind : ΠP:error_type → Prop.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
33 λP:error_type → Prop.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
34 match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
36 ndefinition error_type_rec : ΠP:error_type → Set.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
37 λP:error_type → Set.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
38 match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
40 ndefinition error_type_rect : ΠP:error_type → Type.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
41 λP:error_type → Type.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
42 match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
44 (* un tipo opzione ad hoc
45 - errore: interessa solo l'errore
46 - ok: interessa info e il nuovo pc
48 ninductive fetch_result (A:Type) : Type ≝
49 FetchERR : error_type → fetch_result A
50 | FetchOK : A → word16 → fetch_result A.
52 ndefinition fetch_result_ind
53 : ΠA:Type.ΠP:fetch_result A → Prop.(Πn:error_type.P (FetchERR A n)) →
54 (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
55 λA:Type.λP:fetch_result A → Prop.λf:Πn:error_type.P (FetchERR A n).
56 λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
57 match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
59 ndefinition fetch_result_rec
60 : ΠA:Type.ΠP:fetch_result A → Set.(Πn:error_type.P (FetchERR A n)) →
61 (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
62 λA:Type.λP:fetch_result A → Set.λf:Πn:error_type.P (FetchERR A n).
63 λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
64 match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
66 ndefinition fetch_result_rect
67 : ΠA:Type.ΠP:fetch_result A → Type.(Πn:error_type.P (FetchERR A n)) →
68 (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
69 λA:Type.λP:fetch_result A → Type.λf:Πn:error_type.P (FetchERR A n).
70 λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
71 match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
73 (* **************************** *)
74 (* FETCH E ACCESSO ALLA MEMORIA *)
75 (* **************************** *)
77 (* ausialiaria per RS08 read *)
78 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
79 memory mapped, quindi bisona intercettare la lettura.
80 NB: fare molta attenzione alle note sulle combinazioni possibili perche'
81 il comportamento della memoria nell'RS08 e' strano e ci sono
82 precise condizioni che impediscono una semantica circolare dell'accesso
83 (divergenza=assenza di definizione) *)
84 ndefinition RS08_memory_filter_read_aux ≝
85 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
86 λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option T.
88 [ mk_any_status alu mem chk _ ⇒ match alu with
89 [ mk_alu_RS08 _ _ _ _ xm psm _ _ ⇒
91 possibili accessi al registro X
93 2) addr=000E (X =0F): indiretto
94 3) addr=00CF (PS=00): paging
96 [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
97 non si possono combinare due effetti contemporaneamente!
98 per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni
100 match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
101 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
102 (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
106 possibili accessi al registro PS
107 1) addr=001F: diretto
108 2) addr=000E (X =1F): indiretto
109 3) addr=00DF (PS=00): paging
111 match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
112 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
113 (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
117 accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
118 altrimenti sarebbero 2 indirezioni
120 match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
121 [ true ⇒ fMEM mem chk 〈〈x0,x0〉:xm〉
124 accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
126 match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
127 [ true ⇒ fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
128 (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉))
132 | false ⇒ fMEM mem chk addr ]]]]]].
134 (* lettura RS08 di un byte *)
135 ndefinition RS08_memory_filter_read ≝
136 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
137 RS08_memory_filter_read_aux t s addr byte8
139 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read t m c a).
141 (* lettura RS08 di un bit *)
142 ndefinition RS08_memory_filter_read_bit ≝
143 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.
144 RS08_memory_filter_read_aux t s addr bool
145 (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
146 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read_bit t m c a sub).
148 (* in caso di RS08 si dirotta sul filtro, altrimenti si legge direttamente *)
149 ndefinition memory_filter_read ≝
150 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → option byte8 with
151 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.
152 mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
153 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.
154 mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
155 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.
156 mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
157 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.
158 RS08_memory_filter_read t s addr
161 ndefinition memory_filter_read_bit ≝
162 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → oct → option bool with
163 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.
164 mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
165 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.
166 mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
167 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.
168 mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
169 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.
170 RS08_memory_filter_read_bit t s addr sub
173 (* ausialiaria per RS08 write *)
174 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
175 memory mapped, quindi bisona intercettare la scrittura.
176 NB: fare molta attenzione alle note sulle combinazioni possibili perche'
177 il comportamento della memoria nell'RS08 e' strano e ci sono
178 precise condizioni che impediscono una semantica circolare dell'accesso
179 (divergenza=assenza di definizione) *)
180 ndefinition RS08_memory_filter_write_aux ≝
181 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
182 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option (aux_mem_type t).
184 [ mk_any_status alu mem chk clk ⇒ match alu with
185 [ mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl ⇒
187 possibili accessi al registro X
188 1) addr=000F: diretto
189 2) addr=000E (X =0F): indiretto
190 3) addr=00CF (PS=00): paging
192 [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
193 non si possono combinare due effetti contemporaneamente!
194 per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni
196 match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
197 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
198 (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
199 [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc (fREG xm) psm zfl cfl) mem chk clk)
202 possibili accessi al registro PS
203 1) addr=001F: diretto
204 2) addr=000E (X =1F): indiretto
205 3) addr=00DF (PS=00): paging
207 match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
208 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
209 (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
210 [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm (fREG psm) zfl cfl) mem chk clk)
213 accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
214 altrimenti sarebbero 2 indirezioni
216 match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
217 [ true ⇒ opt_map ?? (fMEM mem chk 〈〈x0,x0〉:xm〉)
218 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
222 accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
224 match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
225 [ true ⇒ opt_map ?? (fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
226 (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉)))
227 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
231 | false ⇒ opt_map ?? (fMEM mem chk addr)
232 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk)) ]]]]]].
234 (* scrittura RS08 di un byte *)
235 ndefinition RS08_memory_filter_write ≝
236 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λval:byte8.
237 RS08_memory_filter_write_aux t s addr
239 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update t m c a val).
241 (* scrittura RS08 di un bit *)
242 ndefinition RS08_memory_filter_write_bit ≝
243 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
244 RS08_memory_filter_write_aux t s addr
245 (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
246 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update_bit t m c a sub val).
248 (* in caso di RS08 si dirotta sul filtro, altrimenti si scrive direttamente *)
249 ndefinition memory_filter_write ≝
250 λm:mcu_type.λt:memory_impl.match m
251 return λm:mcu_type.any_status m t → word16 → byte8 → option (any_status m t) with
252 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λval:byte8.
253 opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
254 (λmem.Some ? (set_mem_desc ? t s mem))
255 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λval:byte8.
256 opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
257 (λmem.Some ? (set_mem_desc ? t s mem))
258 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λval:byte8.
259 opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
260 (λmem.Some ? (set_mem_desc ? t s mem))
261 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λval:byte8.
262 RS08_memory_filter_write t s addr val
265 ndefinition memory_filter_write_bit ≝
266 λm:mcu_type.λt:memory_impl.match m
267 return λm:mcu_type.any_status m t → word16 → oct → bool → option (any_status m t) with
268 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.λval:bool.
269 opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
270 (λmem.Some ? (set_mem_desc ? t s mem))
271 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.λval:bool.
272 opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
273 (λmem.Some ? (set_mem_desc ? t s mem))
274 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.λval:bool.
275 opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
276 (λmem.Some ? (set_mem_desc ? t s mem))
277 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
278 RS08_memory_filter_write_bit t s addr sub val
282 Da utilizzarsi solo per gli aggiornamenti di PC (per il fetch),
283 NON per il caricamento degli indiretti.
284 - il caricamento degli immediati spetta al fetcher
285 (incremento progressivo di PC ciclo per ciclo, e riempimento del prefetch
286 che a questo punto DEVE poter indirizzare qualsiasi locazione puntata da PC)
287 - il caricamento degli indiretti non spetta al fetcher
289 ndefinition filtered_inc_w16 ≝
290 λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
291 get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
293 nlet rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
296 | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
299 errore1: non esiste traduzione ILL_OP
300 errore2: non e' riuscito a leggere ILL_FETCH_AD
301 altrimenti OK=info+new_pc
304 λm:mcu_type.λt:memory_impl.λs:any_status m t.
305 let pc ≝ get_pc_reg m t s in
306 let pc_next1 ≝ filtered_inc_w16 m t s pc in
307 let pc_next2 ≝ filtered_inc_w16 m t s pc_next1 in
308 match memory_filter_read m t s pc with
309 [ None ⇒ FetchERR ? ILL_FETCH_AD
310 | Some bh ⇒ match full_info_of_word16 m (Byte bh) with
311 (* non ha trovato una traduzione con 1 byte *)
312 [ None ⇒ match m with
313 (* HC05 non esistono op a 2 byte *)
314 [ HC05 ⇒ FetchERR ? ILL_OP
315 | HC08 ⇒ match eq_b8 bh 〈x9,xE〉 with
316 (* HC08 se il primo byte e' 0x9E il secondo puo' avere senso *)
317 [ true ⇒ match memory_filter_read m t s pc_next1 with
318 [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
319 [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
320 (* HC08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
321 | false ⇒ FetchERR ? ILL_OP
323 | HCS08 ⇒ match eq_b8 bh 〈x9,xE〉 with
324 (* HCS08 se il primo byte e' 0x9E il secondo puo' avere senso *)
325 [ true ⇒ match memory_filter_read m t s pc_next1 with
326 [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
327 [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
328 (* HCS08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
329 | false ⇒ FetchERR ? ILL_OP
331 (* RS08 non esistono op a 2 byte *)
332 | RS08 ⇒ FetchERR ? ILL_OP
334 (* ha trovato una traduzione con 1 byte *)
335 | Some info ⇒ FetchOK ? info pc_next1 ]].
337 (* ************************ *)
338 (* MODALITA' INDIRIZZAMENTO *)
339 (* ************************ *)
342 (* - incrementano l'indirizzo normalmente *)
343 (* - incrementano PC attraverso il filtro *)
345 (* lettura byte da addr *)
346 ndefinition loadb_from ≝
347 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
348 opt_map ?? (memory_filter_read m t s addr)
349 (λb.Some ? (triple ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
351 (* lettura bit da addr *)
352 ndefinition loadbit_from ≝
353 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.
354 opt_map ?? (memory_filter_read_bit m t s addr sub)
355 (λb.Some ? (triple ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
357 (* lettura word da addr *)
358 ndefinition loadw_from ≝
359 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
360 opt_map ?? (memory_filter_read m t s addr)
361 (λbh.opt_map ?? (memory_filter_read m t s (succ_w16 addr))
362 (λbl.Some ? (triple ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc fetched)))).
364 (* scrittura byte su addr *)
365 ndefinition writeb_to ≝
366 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwriteb:byte8.
367 opt_map ?? (memory_filter_write m t s addr writeb)
368 (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
370 (* scrittura bit su addr *)
371 ndefinition writebit_to ≝
372 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.λwriteb:bool.
373 opt_map ?? (memory_filter_write_bit m t s addr sub writeb)
374 (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
376 (* scrittura word su addr *)
377 ndefinition writew_to ≝
378 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
379 opt_map ?? (memory_filter_write m t s addr (w16h writew))
380 (λtmps1.opt_map ?? (memory_filter_write m t tmps1 (succ_w16 addr) (w16l writew))
381 (λtmps2.Some ? (pair ?? tmps2 (filtered_plus_w16 m t tmps2 cur_pc fetched)))).
383 (* ausiliari per definire i tipi e la lettura/scrittura *)
385 (* ausiliaria per definire il tipo di aux_load *)
386 ndefinition aux_load_typing ≝
387 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
388 any_status m t → word16 → word16 → nat →
389 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
391 (* per non dover ramificare i vari load in byte/word *)
392 ndefinition aux_load ≝
393 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
394 [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
396 (* ausiliaria per definire il tipo di aux_write *)
397 ndefinition aux_write_typing ≝
398 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
399 any_status m t → word16 → word16 → nat →
400 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
401 option (ProdT (any_status m t) word16).
403 (* per non dover ramificare i vari load in byte/word *)
404 ndefinition aux_write ≝
405 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
406 [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
408 (* modalita' vere e proprie *)
410 (* lettura da [curpc]: IMM1 comportamento asimmetrico, quindi non si appoggia a loadb *)
411 ndefinition mode_IMM1_load ≝
412 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
413 opt_map ?? (memory_filter_read m t s cur_pc)
414 (λb.Some ? (triple ??? s b (filtered_inc_w16 m t s cur_pc))).
416 (* lettura da [curpc]: IMM1 + estensione a word *)
417 ndefinition mode_IMM1EXT_load ≝
418 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
419 opt_map ?? (memory_filter_read m t s cur_pc)
420 (λb.Some ? (triple ??? s 〈〈x0,x0〉:b〉 (filtered_inc_w16 m t s cur_pc))).
422 (* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
423 ndefinition mode_IMM2_load ≝
424 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
425 opt_map ?? (memory_filter_read m t s cur_pc)
426 (λbh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
427 (λbl.Some ? (triple ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc 2)))).
429 (* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
430 ndefinition mode_DIR1_load ≝
431 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
432 opt_map ?? (memory_filter_read m t s cur_pc)
433 (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
435 (* lettura da [byte [curpc]]: loadbit *)
436 ndefinition mode_DIR1n_load ≝
437 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
438 opt_map ?? (memory_filter_read m t s cur_pc)
439 (λaddr.loadbit_from m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
441 (* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
442 ndefinition mode_DIR1_write ≝
443 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
444 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
445 opt_map ?? (memory_filter_read m t s cur_pc)
446 (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 writebw).
448 (* scrittura su [byte [curpc]]: writebit *)
449 ndefinition mode_DIR1n_write ≝
450 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
451 opt_map ?? (memory_filter_read m t s cur_pc)
452 (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 writeb).
454 (* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
455 ndefinition mode_DIR2_load ≝
456 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
457 opt_map ?? (memory_filter_read m t s cur_pc)
458 (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
459 (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc 2)).
461 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
462 ndefinition mode_DIR2_write ≝
463 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
464 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
465 opt_map ?? (memory_filter_read m t s cur_pc)
466 (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
467 (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc 2 writebw)).
470 λm:mcu_type.λt:memory_impl.λs:any_status m t.
472 [ HC05 ⇒ opt_map ?? (get_indX_8_low_reg m t s) (λindx.Some ? 〈〈x0,x0〉:indx〉)
473 | HC08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
474 | HCS08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
477 (* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
478 ndefinition mode_IX0_load ≝
479 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
480 opt_map ?? (get_IX m t s)
481 (λaddr.(aux_load m t byteflag) s addr cur_pc 0).
483 (* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
484 ndefinition mode_IX0_write ≝
485 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
486 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
487 opt_map ?? (get_IX m t s)
488 (λaddr.(aux_write m t byteflag) s addr cur_pc 0 writebw).
490 (* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
491 ndefinition mode_IX1_load ≝
492 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
493 opt_map ?? (get_IX m t s)
494 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
495 (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
497 (* lettura da X+[byte curpc] *)
498 ndefinition mode_IX1ADD_load ≝
499 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
500 opt_map ?? (memory_filter_read m t s cur_pc)
501 (λb.opt_map ?? (get_IX m t s)
502 (λaddr.Some ? (triple ??? s (plus_w16_d_d addr 〈〈x0,x0〉:b〉) (filtered_inc_w16 m t s cur_pc)))).
504 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
505 ndefinition mode_IX1_write ≝
506 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
507 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
508 opt_map ?? (get_IX m t s)
509 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
510 (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
512 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
513 ndefinition mode_IX2_load ≝
514 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
515 opt_map ?? (get_IX m t s)
516 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
517 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
518 (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
520 (* lettura da X+[word curpc] *)
521 ndefinition mode_IX2ADD_load ≝
522 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
523 opt_map ?? (memory_filter_read m t s cur_pc)
524 (λbh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
525 (λbl.opt_map ?? (get_IX m t s)
526 (λaddr.Some ? (triple ??? s (plus_w16_d_d addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
528 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
529 ndefinition mode_IX2_write ≝
530 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
531 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
532 opt_map ?? (get_IX m t s)
533 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
534 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
535 (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
537 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
538 ndefinition mode_SP1_load ≝
539 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
540 opt_map ?? (get_sp_reg m t s)
541 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
542 (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
544 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
545 ndefinition mode_SP1_write ≝
546 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
547 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
548 opt_map ?? (get_sp_reg m t s)
549 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
550 (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
552 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
553 ndefinition mode_SP2_load ≝
554 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
555 opt_map ?? (get_sp_reg m t s)
556 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
557 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
558 (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
560 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
561 ndefinition mode_SP2_write ≝
562 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
563 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
564 opt_map ?? (get_sp_reg m t s)
565 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
566 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
567 (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
569 (* ************************************** *)
570 (* raccordo di tutte le possibili letture *)
571 (* ************************************** *)
574 ndefinition aux_inc_indX_16 ≝
575 λm:mcu_type.λt:memory_impl.λs:any_status m t.
576 opt_map ?? (get_indX_16_reg m t s)
577 (λX_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 X_op))
578 (λs_tmp.Some ? s_tmp)).
580 (* tutte le modalita' di lettura: false=loadb true=loadw *)
581 ndefinition multi_mode_load ≝
582 λbyteflag:bool.λm:mcu_type.λt:memory_impl.
584 return λbyteflag:bool.any_status m t → word16 → instr_mode →
585 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
587 (* lettura di un byte *)
588 [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
589 (* NO: non ci sono indicazioni *)
592 | MODE_INHA ⇒ Some ? (triple ??? s (get_acc_8_low_reg m t s) cur_pc)
594 | MODE_INHX ⇒ opt_map ?? (get_indX_8_low_reg m t s)
595 (λindx.Some ? (triple ??? s indx cur_pc))
597 | MODE_INHH ⇒ opt_map ?? (get_indX_8_high_reg m t s)
598 (λindx.Some ? (triple ??? s indx cur_pc))
600 (* NO: solo lettura word *)
601 | MODE_INHX0ADD ⇒ None ?
602 (* NO: solo lettura word *)
603 | MODE_INHX1ADD ⇒ None ?
604 (* NO: solo lettura word *)
605 | MODE_INHX2ADD ⇒ None ?
607 (* preleva 1 byte immediato *)
608 | MODE_IMM1 ⇒ mode_IMM1_load m t s cur_pc
609 (* NO: solo lettura word *)
610 | MODE_IMM1EXT ⇒ None ?
611 (* NO: solo lettura word *)
613 (* preleva 1 byte da indirizzo diretto 1 byte *)
614 | MODE_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
615 (* preleva 1 byte da indirizzo diretto 1 word *)
616 | MODE_DIR2 ⇒ mode_DIR2_load true m t s cur_pc
617 (* preleva 1 byte da H:X *)
618 | MODE_IX0 ⇒ mode_IX0_load true m t s cur_pc
619 (* preleva 1 byte da H:X+1 byte offset *)
620 | MODE_IX1 ⇒ mode_IX1_load true m t s cur_pc
621 (* preleva 1 byte da H:X+1 word offset *)
622 | MODE_IX2 ⇒ mode_IX2_load true m t s cur_pc
623 (* preleva 1 byte da SP+1 byte offset *)
624 | MODE_SP1 ⇒ mode_SP1_load true m t s cur_pc
625 (* preleva 1 byte da SP+1 word offset *)
626 | MODE_SP2 ⇒ mode_SP2_load true m t s cur_pc
628 (* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
629 | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
630 (* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
631 | MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load m t s cur_pc
632 (* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
633 | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true m t s cur_pc
634 (* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
635 | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true m t s cur_pc
637 (* NO: solo lettura word/scrittura byte *)
638 | MODE_INHA_and_IMM1 ⇒ None ?
639 (* NO: solo lettura word/scrittura byte *)
640 | MODE_INHX_and_IMM1 ⇒ None ?
641 (* NO: solo lettura word *)
642 | MODE_IMM1_and_IMM1 ⇒ None ?
643 (* NO: solo lettura word/scrittura byte *)
644 | MODE_DIR1_and_IMM1 ⇒ None ?
645 (* NO: solo lettura word/scrittura byte *)
646 | MODE_IX0_and_IMM1 ⇒ None ?
647 (* NO: solo lettura word *)
648 | MODE_IX0p_and_IMM1 ⇒ None ?
649 (* NO: solo lettura word/scrittura byte *)
650 | MODE_IX1_and_IMM1 ⇒ None ?
651 (* NO: solo lettura word *)
652 | MODE_IX1p_and_IMM1 ⇒ None ?
653 (* NO: solo lettura word/scrittura byte *)
654 | MODE_SP1_and_IMM1 ⇒ None ?
656 (* NO: solo scrittura byte *)
657 | MODE_DIRn _ ⇒ None ?
658 (* NO: solo lettura word *)
659 | MODE_DIRn_and_IMM1 _ ⇒ None ?
660 (* preleva 1 byte da 0000 0000 0000 xxxxb *)
661 | MODE_TNY e ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
662 (λb.Some ? (triple ??? s b cur_pc))
663 (* preleva 1 byte da 0000 0000 000x xxxxb *)
664 | MODE_SRT e ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉)
665 (λb.Some ? (triple ??? s b cur_pc))
667 (* lettura di una word *)
668 | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
669 (* NO: non ci sono indicazioni *)
671 (* NO: solo lettura/scrittura byte *)
673 (* NO: solo lettura/scrittura byte *)
675 (* NO: solo lettura/scrittura byte *)
678 (* preleva 1 word immediato *)
679 | MODE_INHX0ADD ⇒ opt_map ?? (get_IX m t s)
680 (λw.Some ? (triple ??? s w cur_pc))
681 (* preleva 1 word immediato *)
682 | MODE_INHX1ADD ⇒ mode_IX1ADD_load m t s cur_pc
683 (* preleva 1 word immediato *)
684 | MODE_INHX2ADD ⇒ mode_IX2ADD_load m t s cur_pc
686 (* NO: solo lettura byte *)
688 (* preleva 1 word immediato *)
689 | MODE_IMM1EXT ⇒ mode_IMM1EXT_load m t s cur_pc
690 (* preleva 1 word immediato *)
691 | MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
692 (* preleva 1 word da indirizzo diretto 1 byte *)
693 | MODE_DIR1 ⇒ mode_DIR1_load false m t s cur_pc
694 (* preleva 1 word da indirizzo diretto 1 word *)
695 | MODE_DIR2 ⇒ mode_DIR2_load false m t s cur_pc
696 (* preleva 1 word da H:X *)
697 | MODE_IX0 ⇒ mode_IX0_load false m t s cur_pc
698 (* preleva 1 word da H:X+1 byte offset *)
699 | MODE_IX1 ⇒ mode_IX1_load false m t s cur_pc
700 (* preleva 1 word da H:X+1 word offset *)
701 | MODE_IX2 ⇒ mode_IX2_load false m t s cur_pc
702 (* preleva 1 word da SP+1 byte offset *)
703 | MODE_SP1 ⇒ mode_SP1_load false m t s cur_pc
704 (* preleva 1 word da SP+1 word offset *)
705 | MODE_SP2 ⇒ mode_SP2_load false m t s cur_pc
707 (* NO: solo lettura/scrittura byte *)
708 | MODE_DIR1_to_DIR1 ⇒ None ?
709 (* NO: solo lettura/scrittura byte *)
710 | MODE_IMM1_to_DIR1 ⇒ None ?
711 (* NO: solo lettura/scrittura byte *)
712 | MODE_IX0p_to_DIR1 ⇒ None ?
713 (* NO: solo lettura/scrittura byte *)
714 | MODE_DIR1_to_IX0p ⇒ None ?
716 (* preleva 2 byte, possibilita' modificare Io argomento *)
717 | MODE_INHA_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
718 (λS_immb_and_PC.match S_immb_and_PC with
719 [ triple _ immb cur_pc' ⇒
720 Some ? (triple ??? s 〈(get_acc_8_low_reg m t s):immb〉 cur_pc')])
721 (* preleva 2 byte, possibilita' modificare Io argomento *)
722 | MODE_INHX_and_IMM1 ⇒ opt_map ?? (get_indX_8_low_reg m t s)
723 (λX_op.opt_map ?? (mode_IMM1_load m t s cur_pc)
724 (λS_immb_and_PC.match S_immb_and_PC with
725 [ triple _ immb cur_pc' ⇒
726 Some ? (triple ??? s 〈X_op:immb〉 cur_pc')]))
727 (* preleva 2 byte, NO possibilita' modificare Io argomento *)
728 | MODE_IMM1_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
729 (λS_immb1_and_PC.match S_immb1_and_PC with
730 [ triple _ immb1 cur_pc' ⇒
731 opt_map ?? (mode_IMM1_load m t s cur_pc')
732 (λS_immb2_and_PC.match S_immb2_and_PC with
733 [ triple _ immb2 cur_pc'' ⇒
734 Some ? (triple ??? s 〈immb1:immb2〉 cur_pc'')])])
735 (* preleva 2 byte, possibilita' modificare Io argomento *)
736 | MODE_DIR1_and_IMM1 ⇒ opt_map ?? (mode_DIR1_load true m t s cur_pc)
737 (λS_dirb_and_PC.match S_dirb_and_PC with
738 [ triple _ dirb cur_pc' ⇒
739 opt_map ?? (mode_IMM1_load m t s cur_pc')
740 (λS_immb_and_PC.match S_immb_and_PC with
741 [ triple _ immb cur_pc'' ⇒
742 Some ? (triple ??? s 〈dirb:immb〉 cur_pc'')])])
743 (* preleva 2 byte, possibilita' modificare Io argomento *)
744 | MODE_IX0_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
745 (λS_ixb_and_PC.match S_ixb_and_PC with
746 [ triple _ ixb cur_pc' ⇒
747 opt_map ?? (mode_IMM1_load m t s cur_pc')
748 (λS_immb_and_PC.match S_immb_and_PC with
749 [ triple _ immb cur_pc'' ⇒
750 Some ? (triple ??? s 〈ixb:immb〉 cur_pc'')])])
751 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
752 | MODE_IX0p_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
753 (λS_ixb_and_PC.match S_ixb_and_PC with
754 [ triple _ ixb cur_pc' ⇒
755 opt_map ?? (mode_IMM1_load m t s cur_pc')
756 (λS_immb_and_PC.match S_immb_and_PC with
757 [ triple _ immb cur_pc'' ⇒
759 opt_map ?? (aux_inc_indX_16 m t s)
760 (λs'.Some ? (triple ??? s' 〈ixb:immb〉 cur_pc''))])])
761 (* preleva 2 byte, possibilita' modificare Io argomento *)
762 | MODE_IX1_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
763 (λS_ixb_and_PC.match S_ixb_and_PC with
764 [ triple _ ixb cur_pc' ⇒
765 opt_map ?? (mode_IMM1_load m t s cur_pc')
766 (λS_immb_and_PC.match S_immb_and_PC with
767 [ triple _ immb cur_pc'' ⇒
768 Some ? (triple ??? s 〈ixb:immb〉 cur_pc'')])])
769 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
770 | MODE_IX1p_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
771 (λS_ixb_and_PC.match S_ixb_and_PC with
772 [ triple _ ixb cur_pc' ⇒
773 opt_map ?? (mode_IMM1_load m t s cur_pc')
774 (λS_immb_and_PC.match S_immb_and_PC with
775 [ triple _ immb cur_pc'' ⇒
777 opt_map ?? (aux_inc_indX_16 m t s)
778 (λs'.Some ? (triple ??? s' 〈ixb:immb〉 cur_pc''))])])
779 (* preleva 2 byte, possibilita' modificare Io argomento *)
780 | MODE_SP1_and_IMM1 ⇒ opt_map ?? (mode_SP1_load true m t s cur_pc)
781 (λS_spb_and_PC.match S_spb_and_PC with
782 [ triple _ spb cur_pc' ⇒
783 opt_map ?? (mode_IMM1_load m t s cur_pc')
784 (λS_immb_and_PC.match S_immb_and_PC with
785 [ triple _ immb cur_pc'' ⇒
786 Some ? (triple ??? s 〈spb:immb〉 cur_pc'')])])
788 (* NO: solo scrittura byte *)
789 | MODE_DIRn _ ⇒ None ?
790 (* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
791 | MODE_DIRn_and_IMM1 msk ⇒ opt_map ?? (mode_DIR1n_load m t s cur_pc msk)
792 (λS_dirbn_and_PC.match S_dirbn_and_PC with
793 [ triple _ dirbn cur_pc' ⇒
794 opt_map ?? (mode_IMM1_load m t s cur_pc')
795 (λS_immb_and_PC.match S_immb_and_PC with
796 [ triple _ immb cur_pc'' ⇒
797 Some ? (triple ??? s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
798 (* NO: solo lettura/scrittura byte *)
799 | MODE_TNY _ ⇒ None ?
800 (* NO: solo lettura/scrittura byte *)
801 | MODE_SRT _ ⇒ None ?
805 (* **************************************** *)
806 (* raccordo di tutte le possibili scritture *)
807 (* **************************************** *)
809 (* tutte le modalita' di scrittura: true=writeb, false=writew *)
810 ndefinition multi_mode_write ≝
811 λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
812 return λbyteflag:bool.any_status m t → word16 → instr_mode →
813 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
814 option (ProdT (any_status m t) word16) with
815 (* scrittura di un byte *)
816 [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwriteb:byte8.match i with
817 (* NO: non ci sono indicazioni *)
820 | MODE_INHA ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
822 | MODE_INHX ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
823 (λtmps.Some ? (pair ?? tmps cur_pc))
825 | MODE_INHH ⇒ opt_map ?? (set_indX_8_high_reg m t s writeb)
826 (λtmps.Some ? (pair ?? tmps cur_pc))
828 (* NO: solo lettura word *)
829 | MODE_INHX0ADD ⇒ None ?
830 (* NO: solo lettura word *)
831 | MODE_INHX1ADD ⇒ None ?
832 (* NO: solo lettura word *)
833 | MODE_INHX2ADD ⇒ None ?
835 (* NO: solo lettura byte *)
837 (* NO: solo lettura word *)
838 | MODE_IMM1EXT ⇒ None ?
839 (* NO: solo lettura word *)
841 (* scrive 1 byte su indirizzo diretto 1 byte *)
842 | MODE_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
843 (* scrive 1 byte su indirizzo diretto 1 word *)
844 | MODE_DIR2 ⇒ mode_DIR2_write true m t s cur_pc writeb
845 (* scrive 1 byte su H:X *)
846 | MODE_IX0 ⇒ mode_IX0_write true m t s cur_pc writeb
847 (* scrive 1 byte su H:X+1 byte offset *)
848 | MODE_IX1 ⇒ mode_IX1_write true m t s cur_pc writeb
849 (* scrive 1 byte su H:X+1 word offset *)
850 | MODE_IX2 ⇒ mode_IX2_write true m t s cur_pc writeb
851 (* scrive 1 byte su SP+1 byte offset *)
852 | MODE_SP1 ⇒ mode_SP1_write true m t s cur_pc writeb
853 (* scrive 1 byte su SP+1 word offset *)
854 | MODE_SP2 ⇒ mode_SP2_write true m t s cur_pc writeb
856 (* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
857 | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
858 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
859 | MODE_IMM1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
860 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
861 | MODE_IX0p_to_DIR1 ⇒ opt_map ?? (mode_DIR1_write true m t s cur_pc writeb)
862 (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
864 opt_map ?? (aux_inc_indX_16 m t S_op)
865 (λS_op'.Some ? (pair ?? S_op' PC_op))])
866 (* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
867 | MODE_DIR1_to_IX0p ⇒ opt_map ?? (mode_IX0_write true m t s cur_pc writeb)
868 (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
870 opt_map ?? (aux_inc_indX_16 m t S_op)
871 (λS_op'.Some ? (pair ?? S_op' PC_op))])
873 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
874 | MODE_INHA_and_IMM1 ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
875 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)
876 | MODE_INHX_and_IMM1 ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
877 (λtmps.Some ? (pair ?? tmps cur_pc))
878 (* NO: solo lettura word *)
879 | MODE_IMM1_and_IMM1 ⇒ None ?
880 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
881 | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write true m t s cur_pc writeb
882 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
883 | MODE_IX0_and_IMM1 ⇒ mode_IX0_write true m t s cur_pc writeb
884 (* NO: solo lettura word *)
885 | MODE_IX0p_and_IMM1 ⇒ None ?
886 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
887 | MODE_IX1_and_IMM1 ⇒ mode_IX1_write true m t s cur_pc writeb
888 (* NO: solo lettura word *)
889 | MODE_IX1p_and_IMM1 ⇒ None ?
890 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
891 | MODE_SP1_and_IMM1 ⇒ mode_SP1_write true m t s cur_pc writeb
893 (* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
894 | MODE_DIRn msk ⇒ mode_DIR1n_write m t s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))
895 (* NO: solo lettura word *)
896 | MODE_DIRn_and_IMM1 _ ⇒ None ?
897 (* scrive 1 byte su 0000 0000 0000 xxxxb *)
898 | MODE_TNY e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
899 (λtmps.Some ? (pair ?? tmps cur_pc))
900 (* scrive 1 byte su 0000 0000 000x xxxxb *)
901 | MODE_SRT e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉 writeb)
902 (λtmps.Some ? (pair ?? tmps cur_pc)) ]
903 (* scrittura di una word *)
904 | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwritew:word16.match i with
905 (* NO: non ci sono indicazioni *)
907 (* NO: solo lettura/scrittura byte *)
909 (* NO: solo lettura/scrittura byte *)
911 (* NO: solo lettura/scrittura byte *)
914 (* NO: solo lettura word *)
915 | MODE_INHX0ADD ⇒ None ?
916 (* NO: solo lettura word *)
917 | MODE_INHX1ADD ⇒ None ?
918 (* NO: solo lettura word *)
919 | MODE_INHX2ADD ⇒ None ?
921 (* NO: solo lettura byte *)
923 (* NO: solo lettura word *)
924 | MODE_IMM1EXT ⇒ None ?
925 (* NO: solo lettura word *)
927 (* scrive 1 word su indirizzo diretto 1 byte *)
928 | MODE_DIR1 ⇒ mode_DIR1_write false m t s cur_pc writew
929 (* scrive 1 word su indirizzo diretto 1 word *)
930 | MODE_DIR2 ⇒ mode_DIR2_write false m t s cur_pc writew
931 (* scrive 1 word su H:X *)
932 | MODE_IX0 ⇒ mode_IX0_write false m t s cur_pc writew
933 (* scrive 1 word su H:X+1 byte offset *)
934 | MODE_IX1 ⇒ mode_IX1_write false m t s cur_pc writew
935 (* scrive 1 word su H:X+1 word offset *)
936 | MODE_IX2 ⇒ mode_IX2_write false m t s cur_pc writew
937 (* scrive 1 word su SP+1 byte offset *)
938 | MODE_SP1 ⇒ mode_SP1_write false m t s cur_pc writew
939 (* scrive 1 word su SP+1 word offset *)
940 | MODE_SP2 ⇒ mode_SP2_write false m t s cur_pc writew
942 (* NO: solo lettura/scrittura byte *)
943 | MODE_DIR1_to_DIR1 ⇒ None ?
944 (* NO: solo lettura/scrittura byte *)
945 | MODE_IMM1_to_DIR1 ⇒ None ?
946 (* NO: solo lettura/scrittura byte *)
947 | MODE_IX0p_to_DIR1 ⇒ None ?
948 (* NO: solo lettura/scrittura byte *)
949 | MODE_DIR1_to_IX0p ⇒ None ?
951 (* NO: solo lettura word/scrittura byte *)
952 | MODE_INHA_and_IMM1 ⇒ None ?
953 (* NO: solo lettura word/scrittura byte *)
954 | MODE_INHX_and_IMM1 ⇒ None ?
955 (* NO: solo lettura word *)
956 | MODE_IMM1_and_IMM1 ⇒ None ?
957 (* NO: solo lettura word/scrittura byte *)
958 | MODE_DIR1_and_IMM1 ⇒ None ?
959 (* NO: solo lettura word/scrittura byte *)
960 | MODE_IX0_and_IMM1 ⇒ None ?
961 (* NO: solo lettura word *)
962 | MODE_IX0p_and_IMM1 ⇒ None ?
963 (* NO: solo lettura word/scrittura byte *)
964 | MODE_IX1_and_IMM1 ⇒ None ?
965 (* NO: solo lettura word *)
966 | MODE_IX1p_and_IMM1 ⇒ None ?
967 (* NO: solo lettura word/scrittura byte *)
968 | MODE_SP1_and_IMM1 ⇒ None ?
970 (* NO: solo scrittura byte *)
971 | MODE_DIRn _ ⇒ None ?
972 (* NO: solo lettura word *)
973 | MODE_DIRn_and_IMM1 _ ⇒ None ?
974 (* NO: solo lettura/scrittura byte *)
975 | MODE_TNY _ ⇒ None ?
976 (* NO: solo lettura/scrittura byte *)
977 | MODE_SRT _ ⇒ None ?