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 include "freescale/model.ma".
29 (* errori possibili nel fetch *)
30 inductive error_type : Type ≝
32 | ILL_FETCH_AD: error_type
33 | ILL_EX_AD: error_type.
35 (* un tipo opzione ad hoc
36 - errore: interessa solo l'errore
37 - ok: interessa info e il nuovo pc
39 inductive fetch_result (A:Type) : Type ≝
40 FetchERR : error_type → fetch_result A
41 | FetchOK : A → word16 → fetch_result A.
43 (* **************************** *)
44 (* FETCH E ACCESSO ALLA MEMORIA *)
45 (* **************************** *)
47 (* ausialiaria per RS08 read *)
48 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
49 memory mapped, quindi bisona intercettare la lettura.
50 NB: fare molta attenzione alle note sulle combinazioni possibili perche'
51 il comportamento della memoria nell'RS08 e' strano e ci sono
52 precise condizioni che impediscono una semantica circolare dell'accesso
53 (divergenza=assenza di definizione) *)
54 definition RS08_memory_filter_read_aux ≝
55 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
56 λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option T.
58 [ mk_any_status alu mem chk _ ⇒ match alu with
59 [ mk_alu_RS08 _ _ _ _ xm psm _ _ ⇒
61 possibili accessi al registro X
63 2) addr=000E (X =0F): indiretto
64 3) addr=00CF (PS=00): paging
66 [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
67 non si possono combinare due effetti contemporaneamente!
68 per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni
70 match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
71 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
72 (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
76 possibili accessi al registro PS
78 2) addr=000E (X =1F): indiretto
79 3) addr=00DF (PS=00): paging
81 match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
82 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
83 (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
87 accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
88 altrimenti sarebbero 2 indirezioni
90 match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
91 [ true ⇒ fMEM mem chk 〈〈x0,x0〉:xm〉
94 accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
96 match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
97 [ true ⇒ fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
98 (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉))
102 | false ⇒ fMEM mem chk addr ]]]]]].
104 (* lettura RS08 di un byte *)
105 definition RS08_memory_filter_read ≝
106 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
107 RS08_memory_filter_read_aux t s addr byte8
109 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read t m c a).
111 (* lettura RS08 di un bit *)
112 definition RS08_memory_filter_read_bit ≝
113 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.
114 RS08_memory_filter_read_aux t s addr bool
115 (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
116 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read_bit t m c a sub).
118 (* in caso di RS08 si dirotta sul filtro, altrimenti si legge direttamente *)
119 definition memory_filter_read ≝
120 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → option byte8 with
121 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.
122 mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
123 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.
124 mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
125 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.
126 mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
127 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.
128 RS08_memory_filter_read t s addr
131 definition memory_filter_read_bit ≝
132 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → oct → option bool with
133 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.
134 mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
135 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.
136 mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
137 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.
138 mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
139 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.
140 RS08_memory_filter_read_bit t s addr sub
143 (* ausialiaria per RS08 write *)
144 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
145 memory mapped, quindi bisona intercettare la scrittura.
146 NB: fare molta attenzione alle note sulle combinazioni possibili perche'
147 il comportamento della memoria nell'RS08 e' strano e ci sono
148 precise condizioni che impediscono una semantica circolare dell'accesso
149 (divergenza=assenza di definizione) *)
150 definition RS08_memory_filter_write_aux ≝
151 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
152 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option (aux_mem_type t).
154 [ mk_any_status alu mem chk clk ⇒ match alu with
155 [ mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl ⇒
157 possibili accessi al registro X
158 1) addr=000F: diretto
159 2) addr=000E (X =0F): indiretto
160 3) addr=00CF (PS=00): paging
162 [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
163 non si possono combinare due effetti contemporaneamente!
164 per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni
166 match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
167 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
168 (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
169 [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc (fREG xm) psm zfl cfl) mem chk clk)
172 possibili accessi al registro PS
173 1) addr=001F: diretto
174 2) addr=000E (X =1F): indiretto
175 3) addr=00DF (PS=00): paging
177 match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
178 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
179 (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
180 [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm (fREG psm) zfl cfl) mem chk clk)
183 accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
184 altrimenti sarebbero 2 indirezioni
186 match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
187 [ true ⇒ opt_map ?? (fMEM mem chk 〈〈x0,x0〉:xm〉)
188 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
192 accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
194 match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
195 [ true ⇒ opt_map ?? (fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
196 (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉)))
197 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
201 | false ⇒ opt_map ?? (fMEM mem chk addr)
202 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk)) ]]]]]].
204 (* scrittura RS08 di un byte *)
205 definition RS08_memory_filter_write ≝
206 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λval:byte8.
207 RS08_memory_filter_write_aux t s addr
209 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update t m c a val).
211 (* scrittura RS08 di un bit *)
212 definition RS08_memory_filter_write_bit ≝
213 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
214 RS08_memory_filter_write_aux t s addr
215 (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
216 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update_bit t m c a sub val).
218 (* in caso di RS08 si dirotta sul filtro, altrimenti si scrive direttamente *)
219 definition memory_filter_write ≝
220 λm:mcu_type.λt:memory_impl.match m
221 return λm:mcu_type.any_status m t → word16 → byte8 → option (any_status m t) with
222 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λval:byte8.
223 opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
224 (λmem.Some ? (set_mem_desc ? t s mem))
225 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λval:byte8.
226 opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
227 (λmem.Some ? (set_mem_desc ? t s mem))
228 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λval:byte8.
229 opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
230 (λmem.Some ? (set_mem_desc ? t s mem))
231 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λval:byte8.
232 RS08_memory_filter_write t s addr val
235 definition memory_filter_write_bit ≝
236 λm:mcu_type.λt:memory_impl.match m
237 return λm:mcu_type.any_status m t → word16 → oct → bool → option (any_status m t) with
238 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.λval:bool.
239 opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
240 (λmem.Some ? (set_mem_desc ? t s mem))
241 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.λval:bool.
242 opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
243 (λmem.Some ? (set_mem_desc ? t s mem))
244 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.λval:bool.
245 opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
246 (λmem.Some ? (set_mem_desc ? t s mem))
247 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
248 RS08_memory_filter_write_bit t s addr sub val
252 Da utilizzarsi solo per gli aggiornamenti di PC (per il fetch),
253 NON per il caricamento degli indiretti.
254 - il caricamento degli immediati spetta al fetcher
255 (incremento progressivo di PC ciclo per ciclo, e riempimento del prefetch
256 che a questo punto DEVE poter indirizzare qualsiasi locazione puntata da PC)
257 - il caricamento degli indiretti non spetta al fetcher
259 definition filtered_inc_w16 ≝
260 λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
261 get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
263 let rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
266 | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
269 errore1: non esiste traduzione ILL_OP
270 errore2: non e' riuscito a leggere ILL_FETCH_AD
271 altrimenti OK=info+new_pc
274 λm:mcu_type.λt:memory_impl.λs:any_status m t.
275 let pc ≝ get_pc_reg m t s in
276 let pc_next1 ≝ filtered_inc_w16 m t s pc in
277 let pc_next2 ≝ filtered_inc_w16 m t s pc_next1 in
278 match memory_filter_read m t s pc with
279 [ None ⇒ FetchERR ? ILL_FETCH_AD
280 | Some bh ⇒ match full_info_of_word16 m (Byte bh) with
281 (* non ha trovato una traduzione con 1 byte *)
282 [ None ⇒ match m with
283 (* HC05 non esistono op a 2 byte *)
284 [ HC05 ⇒ FetchERR ? ILL_OP
285 | HC08 ⇒ match eq_b8 bh 〈x9,xE〉 with
286 (* HC08 se il primo byte e' 0x9E il secondo puo' avere senso *)
287 [ true ⇒ match memory_filter_read m t s pc_next1 with
288 [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
289 [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
290 (* HC08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
291 | false ⇒ FetchERR ? ILL_OP
293 | HCS08 ⇒ match eq_b8 bh 〈x9,xE〉 with
294 (* HCS08 se il primo byte e' 0x9E il secondo puo' avere senso *)
295 [ true ⇒ match memory_filter_read m t s pc_next1 with
296 [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
297 [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
298 (* HCS08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
299 | false ⇒ FetchERR ? ILL_OP
301 (* RS08 non esistono op a 2 byte *)
302 | RS08 ⇒ FetchERR ? ILL_OP
304 (* ha trovato una traduzione con 1 byte *)
305 | Some info ⇒ FetchOK ? info pc_next1 ]].
307 (* ************************ *)
308 (* MODALITA' INDIRIZZAMENTO *)
309 (* ************************ *)
312 (* - incrementano l'indirizzo normalmente *)
313 (* - incrementano PC attraverso il filtro *)
315 (* lettura byte da addr *)
316 definition loadb_from ≝
317 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
318 opt_map ?? (memory_filter_read m t s addr)
319 (λb.Some ? (tripleT ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
321 (* lettura bit da addr *)
322 definition loadbit_from ≝
323 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.
324 opt_map ?? (memory_filter_read_bit m t s addr sub)
325 (λb.Some ? (tripleT ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
327 (* lettura word da addr *)
328 definition loadw_from ≝
329 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
330 opt_map ?? (memory_filter_read m t s addr)
331 (λbh.opt_map ?? (memory_filter_read m t s (succ_w16 addr))
332 (λbl.Some ? (tripleT ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc fetched)))).
334 (* scrittura byte su addr *)
335 definition writeb_to ≝
336 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwriteb:byte8.
337 opt_map ?? (memory_filter_write m t s addr writeb)
338 (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
340 (* scrittura bit su addr *)
341 definition writebit_to ≝
342 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.λwriteb:bool.
343 opt_map ?? (memory_filter_write_bit m t s addr sub writeb)
344 (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
346 (* scrittura word su addr *)
347 definition writew_to ≝
348 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
349 opt_map ?? (memory_filter_write m t s addr (w16h writew))
350 (λtmps1.opt_map ?? (memory_filter_write m t tmps1 (succ_w16 addr) (w16l writew))
351 (λtmps2.Some ? (pair ?? tmps2 (filtered_plus_w16 m t tmps2 cur_pc fetched)))).
353 (* ausiliari per definire i tipi e la lettura/scrittura *)
355 (* ausiliaria per definire il tipo di aux_load *)
356 definition aux_load_typing ≝
357 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
358 any_status m t → word16 → word16 → nat →
359 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
361 (* per non dover ramificare i vari load in byte/word *)
362 definition aux_load ≝
363 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
364 [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
366 (* ausiliaria per definire il tipo di aux_write *)
367 definition aux_write_typing ≝
368 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
369 any_status m t → word16 → word16 → nat →
370 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
371 option (ProdT (any_status m t) word16).
373 (* per non dover ramificare i vari load in byte/word *)
374 definition aux_write ≝
375 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
376 [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
378 (* modalita' vere e proprie *)
380 (* lettura da [curpc]: IMM1 comportamento asimmetrico, quindi non si appoggia a loadb *)
381 definition mode_IMM1_load ≝
382 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
383 opt_map ?? (memory_filter_read m t s cur_pc)
384 (λb.Some ? (tripleT ??? s b (filtered_inc_w16 m t s cur_pc))).
386 (* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
387 definition mode_IMM2_load ≝
388 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
389 opt_map ?? (memory_filter_read m t s cur_pc)
390 (λbh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
391 (λbl.Some ? (tripleT ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc 2)))).
393 (* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
394 definition mode_DIR1_load ≝
395 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
396 opt_map ?? (memory_filter_read m t s cur_pc)
397 (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
399 (* lettura da [byte [curpc]]: loadbit *)
400 definition mode_DIR1n_load ≝
401 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
402 opt_map ?? (memory_filter_read m t s cur_pc)
403 (λaddr.loadbit_from m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
405 (* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
406 definition mode_DIR1_write ≝
407 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
408 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
409 opt_map ?? (memory_filter_read m t s cur_pc)
410 (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 writebw).
412 (* scrittura su [byte [curpc]]: writebit *)
413 definition mode_DIR1n_write ≝
414 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
415 opt_map ?? (memory_filter_read m t s cur_pc)
416 (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 writeb).
418 (* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
419 definition mode_DIR2_load ≝
420 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
421 opt_map ?? (memory_filter_read m t s cur_pc)
422 (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
423 (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc 2)).
425 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
426 definition mode_DIR2_write ≝
427 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
428 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
429 opt_map ?? (memory_filter_read m t s cur_pc)
430 (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
431 (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc 2 writebw)).
434 λm:mcu_type.λt:memory_impl.λs:any_status m t.
436 [ HC05 ⇒ opt_map ?? (get_indX_8_low_reg m t s) (λindx.Some ? 〈〈x0,x0〉:indx〉)
437 | HC08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
438 | HCS08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
441 (* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
442 definition mode_IX0_load ≝
443 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
444 opt_map ?? (get_IX m t s)
445 (λaddr.(aux_load m t byteflag) s addr cur_pc 0).
447 (* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
448 definition mode_IX0_write ≝
449 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
450 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
451 opt_map ?? (get_IX m t s)
452 (λaddr.(aux_write m t byteflag) s addr cur_pc 0 writebw).
454 (* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
455 definition mode_IX1_load ≝
456 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
457 opt_map ?? (get_IX m t s)
458 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
459 (λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
461 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
462 definition mode_IX1_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 ?? (get_IX m t s)
466 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
467 (λoffs.(aux_write m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
469 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
470 definition mode_IX2_load ≝
471 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
472 opt_map ?? (get_IX m t s)
473 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
474 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
475 (λoffsl.(aux_load m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2))).
477 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
478 definition mode_IX2_write ≝
479 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
480 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
481 opt_map ?? (get_IX m t s)
482 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
483 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
484 (λoffsl.(aux_write m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2 writebw))).
486 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
487 definition mode_SP1_load ≝
488 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
489 opt_map ?? (get_sp_reg m t s)
490 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
491 (λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
493 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
494 definition mode_SP1_write ≝
495 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
496 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
497 opt_map ?? (get_sp_reg m t s)
498 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
499 (λoffs.(aux_write m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
501 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
502 definition mode_SP2_load ≝
503 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
504 opt_map ?? (get_sp_reg m t s)
505 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
506 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
507 (λoffsl.(aux_load m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2))).
509 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
510 definition mode_SP2_write ≝
511 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
512 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
513 opt_map ?? (get_sp_reg m t s)
514 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
515 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
516 (λoffsl.(aux_write m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2 writebw))).
518 (* ************************************** *)
519 (* raccordo di tutte le possibili letture *)
520 (* ************************************** *)
523 definition aux_inc_indX_16 ≝
524 λm:mcu_type.λt:memory_impl.λs:any_status m t.
525 opt_map ?? (get_indX_16_reg m t s)
526 (λX_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 X_op))
527 (λs_tmp.Some ? s_tmp)).
529 (* tutte le modalita' di lettura: false=loadb true=loadw *)
530 definition multi_mode_load ≝
531 λbyteflag:bool.λm:mcu_type.λt:memory_impl.
533 return λbyteflag:bool.any_status m t → word16 → instr_mode →
534 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
536 (* lettura di un byte *)
537 [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
538 (* NO: non ci sono indicazioni *)
541 | MODE_INHA ⇒ Some ? (tripleT ??? s (get_acc_8_low_reg m t s) cur_pc)
543 | MODE_INHX ⇒ opt_map ?? (get_indX_8_low_reg m t s)
544 (λindx.Some ? (tripleT ??? s indx cur_pc))
546 | MODE_INHH ⇒ opt_map ?? (get_indX_8_high_reg m t s)
547 (λindx.Some ? (tripleT ??? s indx cur_pc))
549 (* preleva 1 byte immediato *)
550 | MODE_IMM1 ⇒ mode_IMM1_load m t s cur_pc
551 (* NO: solo lettura word *)
553 (* preleva 1 byte da indirizzo diretto 1 byte *)
554 | MODE_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
555 (* preleva 1 byte da indirizzo diretto 1 word *)
556 | MODE_DIR2 ⇒ mode_DIR2_load true m t s cur_pc
557 (* preleva 1 byte da H:X *)
558 | MODE_IX0 ⇒ mode_IX0_load true m t s cur_pc
559 (* preleva 1 byte da H:X+1 byte offset *)
560 | MODE_IX1 ⇒ mode_IX1_load true m t s cur_pc
561 (* preleva 1 byte da H:X+1 word offset *)
562 | MODE_IX2 ⇒ mode_IX2_load true m t s cur_pc
563 (* preleva 1 byte da SP+1 byte offset *)
564 | MODE_SP1 ⇒ mode_SP1_load true m t s cur_pc
565 (* preleva 1 byte da SP+1 word offset *)
566 | MODE_SP2 ⇒ mode_SP2_load true m t s cur_pc
568 (* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
569 | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
570 (* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
571 | MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load m t s cur_pc
572 (* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
573 | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true m t s cur_pc
574 (* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
575 | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true m t s cur_pc
577 (* NO: solo lettura word/scrittura byte *)
578 | MODE_INHA_and_IMM1 ⇒ None ?
579 (* NO: solo lettura word/scrittura byte *)
580 | MODE_INHX_and_IMM1 ⇒ None ?
581 (* NO: solo lettura word *)
582 | MODE_IMM1_and_IMM1 ⇒ None ?
583 (* NO: solo lettura word/scrittura byte *)
584 | MODE_DIR1_and_IMM1 ⇒ None ?
585 (* NO: solo lettura word/scrittura byte *)
586 | MODE_IX0_and_IMM1 ⇒ None ?
587 (* NO: solo lettura word *)
588 | MODE_IX0p_and_IMM1 ⇒ None ?
589 (* NO: solo lettura word/scrittura byte *)
590 | MODE_IX1_and_IMM1 ⇒ None ?
591 (* NO: solo lettura word *)
592 | MODE_IX1p_and_IMM1 ⇒ None ?
593 (* NO: solo lettura word/scrittura byte *)
594 | MODE_SP1_and_IMM1 ⇒ None ?
596 (* NO: solo scrittura byte *)
597 | MODE_DIRn _ ⇒ None ?
598 (* NO: solo lettura word *)
599 | MODE_DIRn_and_IMM1 _ ⇒ None ?
600 (* preleva 1 byte da 0000 0000 0000 xxxxb *)
601 | MODE_TNY e ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
602 (λb.Some ? (tripleT ??? s b cur_pc))
603 (* preleva 1 byte da 0000 0000 000x xxxxb *)
604 | MODE_SRT e ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉)
605 (λb.Some ? (tripleT ??? s b cur_pc))
607 (* lettura di una word *)
608 | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
609 (* NO: non ci sono indicazioni *)
611 (* NO: solo lettura/scrittura byte *)
613 (* NO: solo lettura/scrittura byte *)
615 (* NO: solo lettura/scrittura byte *)
618 (* NO: solo lettura byte *)
620 (* preleva 1 word immediato *)
621 | MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
622 (* preleva 1 word da indirizzo diretto 1 byte *)
623 | MODE_DIR1 ⇒ mode_DIR1_load false m t s cur_pc
624 (* preleva 1 word da indirizzo diretto 1 word *)
625 | MODE_DIR2 ⇒ mode_DIR2_load false m t s cur_pc
626 (* preleva 1 word da H:X *)
627 | MODE_IX0 ⇒ mode_IX0_load false m t s cur_pc
628 (* preleva 1 word da H:X+1 byte offset *)
629 | MODE_IX1 ⇒ mode_IX1_load false m t s cur_pc
630 (* preleva 1 word da H:X+1 word offset *)
631 | MODE_IX2 ⇒ mode_IX2_load false m t s cur_pc
632 (* preleva 1 word da SP+1 byte offset *)
633 | MODE_SP1 ⇒ mode_SP1_load false m t s cur_pc
634 (* preleva 1 word da SP+1 word offset *)
635 | MODE_SP2 ⇒ mode_SP2_load false m t s cur_pc
637 (* NO: solo lettura/scrittura byte *)
638 | MODE_DIR1_to_DIR1 ⇒ None ?
639 (* NO: solo lettura/scrittura byte *)
640 | MODE_IMM1_to_DIR1 ⇒ None ?
641 (* NO: solo lettura/scrittura byte *)
642 | MODE_IX0p_to_DIR1 ⇒ None ?
643 (* NO: solo lettura/scrittura byte *)
644 | MODE_DIR1_to_IX0p ⇒ None ?
646 (* preleva 2 byte, possibilita' modificare Io argomento *)
647 | MODE_INHA_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
648 (λS_immb_and_PC.match S_immb_and_PC with
649 [ tripleT _ immb cur_pc' ⇒
650 Some ? (tripleT ??? s 〈(get_acc_8_low_reg m t s):immb〉 cur_pc')])
651 (* preleva 2 byte, possibilita' modificare Io argomento *)
652 | MODE_INHX_and_IMM1 ⇒ opt_map ?? (get_indX_8_low_reg m t s)
653 (λX_op.opt_map ?? (mode_IMM1_load m t s cur_pc)
654 (λS_immb_and_PC.match S_immb_and_PC with
655 [ tripleT _ immb cur_pc' ⇒
656 Some ? (tripleT ??? s 〈X_op:immb〉 cur_pc')]))
657 (* preleva 2 byte, NO possibilita' modificare Io argomento *)
658 | MODE_IMM1_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
659 (λS_immb1_and_PC.match S_immb1_and_PC with
660 [ tripleT _ immb1 cur_pc' ⇒
661 opt_map ?? (mode_IMM1_load m t s cur_pc')
662 (λS_immb2_and_PC.match S_immb2_and_PC with
663 [ tripleT _ immb2 cur_pc'' ⇒
664 Some ? (tripleT ??? s 〈immb1:immb2〉 cur_pc'')])])
665 (* preleva 2 byte, possibilita' modificare Io argomento *)
666 | MODE_DIR1_and_IMM1 ⇒ opt_map ?? (mode_DIR1_load true m t s cur_pc)
667 (λS_dirb_and_PC.match S_dirb_and_PC with
668 [ tripleT _ dirb cur_pc' ⇒
669 opt_map ?? (mode_IMM1_load m t s cur_pc')
670 (λS_immb_and_PC.match S_immb_and_PC with
671 [ tripleT _ immb cur_pc'' ⇒
672 Some ? (tripleT ??? s 〈dirb:immb〉 cur_pc'')])])
673 (* preleva 2 byte, possibilita' modificare Io argomento *)
674 | MODE_IX0_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
675 (λS_ixb_and_PC.match S_ixb_and_PC with
676 [ tripleT _ ixb cur_pc' ⇒
677 opt_map ?? (mode_IMM1_load m t s cur_pc')
678 (λS_immb_and_PC.match S_immb_and_PC with
679 [ tripleT _ immb cur_pc'' ⇒
680 Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
681 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
682 | MODE_IX0p_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
683 (λS_ixb_and_PC.match S_ixb_and_PC with
684 [ tripleT _ ixb cur_pc' ⇒
685 opt_map ?? (mode_IMM1_load m t s cur_pc')
686 (λS_immb_and_PC.match S_immb_and_PC with
687 [ tripleT _ immb cur_pc'' ⇒
689 opt_map ?? (aux_inc_indX_16 m t s)
690 (λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
691 (* preleva 2 byte, possibilita' modificare Io argomento *)
692 | MODE_IX1_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
693 (λS_ixb_and_PC.match S_ixb_and_PC with
694 [ tripleT _ ixb cur_pc' ⇒
695 opt_map ?? (mode_IMM1_load m t s cur_pc')
696 (λS_immb_and_PC.match S_immb_and_PC with
697 [ tripleT _ immb cur_pc'' ⇒
698 Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
699 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
700 | MODE_IX1p_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
701 (λS_ixb_and_PC.match S_ixb_and_PC with
702 [ tripleT _ ixb cur_pc' ⇒
703 opt_map ?? (mode_IMM1_load m t s cur_pc')
704 (λS_immb_and_PC.match S_immb_and_PC with
705 [ tripleT _ immb cur_pc'' ⇒
707 opt_map ?? (aux_inc_indX_16 m t s)
708 (λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
709 (* preleva 2 byte, possibilita' modificare Io argomento *)
710 | MODE_SP1_and_IMM1 ⇒ opt_map ?? (mode_SP1_load true m t s cur_pc)
711 (λS_spb_and_PC.match S_spb_and_PC with
712 [ tripleT _ spb cur_pc' ⇒
713 opt_map ?? (mode_IMM1_load m t s cur_pc')
714 (λS_immb_and_PC.match S_immb_and_PC with
715 [ tripleT _ immb cur_pc'' ⇒
716 Some ? (tripleT ??? s 〈spb:immb〉 cur_pc'')])])
718 (* NO: solo scrittura byte *)
719 | MODE_DIRn _ ⇒ None ?
720 (* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
721 | MODE_DIRn_and_IMM1 msk ⇒ opt_map ?? (mode_DIR1n_load m t s cur_pc msk)
722 (λS_dirbn_and_PC.match S_dirbn_and_PC with
723 [ tripleT _ dirbn cur_pc' ⇒
724 opt_map ?? (mode_IMM1_load m t s cur_pc')
725 (λS_immb_and_PC.match S_immb_and_PC with
726 [ tripleT _ immb cur_pc'' ⇒
727 Some ? (tripleT ??? s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
728 (* NO: solo lettura/scrittura byte *)
729 | MODE_TNY _ ⇒ None ?
730 (* NO: solo lettura/scrittura byte *)
731 | MODE_SRT _ ⇒ None ?
735 (* **************************************** *)
736 (* raccordo di tutte le possibili scritture *)
737 (* **************************************** *)
739 (* tutte le modalita' di scrittura: true=writeb, false=writew *)
740 definition multi_mode_write ≝
741 λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
742 return λbyteflag:bool.any_status m t → word16 → instr_mode →
743 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
744 option (ProdT (any_status m t) word16) with
745 (* scrittura di un byte *)
746 [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwriteb:byte8.match i with
747 (* NO: non ci sono indicazioni *)
750 | MODE_INHA ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
752 | MODE_INHX ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
753 (λtmps.Some ? (pair ?? tmps cur_pc))
755 | MODE_INHH ⇒ opt_map ?? (set_indX_8_high_reg m t s writeb)
756 (λtmps.Some ? (pair ?? tmps cur_pc))
758 (* NO: solo lettura byte *)
760 (* NO: solo lettura word *)
762 (* scrive 1 byte su indirizzo diretto 1 byte *)
763 | MODE_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
764 (* scrive 1 byte su indirizzo diretto 1 word *)
765 | MODE_DIR2 ⇒ mode_DIR2_write true m t s cur_pc writeb
766 (* scrive 1 byte su H:X *)
767 | MODE_IX0 ⇒ mode_IX0_write true m t s cur_pc writeb
768 (* scrive 1 byte su H:X+1 byte offset *)
769 | MODE_IX1 ⇒ mode_IX1_write true m t s cur_pc writeb
770 (* scrive 1 byte su H:X+1 word offset *)
771 | MODE_IX2 ⇒ mode_IX2_write true m t s cur_pc writeb
772 (* scrive 1 byte su SP+1 byte offset *)
773 | MODE_SP1 ⇒ mode_SP1_write true m t s cur_pc writeb
774 (* scrive 1 byte su SP+1 word offset *)
775 | MODE_SP2 ⇒ mode_SP2_write true m t s cur_pc writeb
777 (* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
778 | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
779 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
780 | MODE_IMM1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
781 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
782 | MODE_IX0p_to_DIR1 ⇒ opt_map ?? (mode_DIR1_write true m t s cur_pc writeb)
783 (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
785 opt_map ?? (aux_inc_indX_16 m t S_op)
786 (λS_op'.Some ? (pair ?? S_op' PC_op))])
787 (* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
788 | MODE_DIR1_to_IX0p ⇒ opt_map ?? (mode_IX0_write true m t s cur_pc writeb)
789 (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
791 opt_map ?? (aux_inc_indX_16 m t S_op)
792 (λS_op'.Some ? (pair ?? S_op' PC_op))])
794 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
795 | MODE_INHA_and_IMM1 ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
796 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)
797 | MODE_INHX_and_IMM1 ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
798 (λtmps.Some ? (pair ?? tmps cur_pc))
799 (* NO: solo lettura word *)
800 | MODE_IMM1_and_IMM1 ⇒ None ?
801 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
802 | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write true m t s cur_pc writeb
803 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
804 | MODE_IX0_and_IMM1 ⇒ mode_IX0_write true m t s cur_pc writeb
805 (* NO: solo lettura word *)
806 | MODE_IX0p_and_IMM1 ⇒ None ?
807 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
808 | MODE_IX1_and_IMM1 ⇒ mode_IX1_write true m t s cur_pc writeb
809 (* NO: solo lettura word *)
810 | MODE_IX1p_and_IMM1 ⇒ None ?
811 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
812 | MODE_SP1_and_IMM1 ⇒ mode_SP1_write true m t s cur_pc writeb
814 (* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
815 | MODE_DIRn msk ⇒ mode_DIR1n_write m t s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))
816 (* NO: solo lettura word *)
817 | MODE_DIRn_and_IMM1 _ ⇒ None ?
818 (* scrive 1 byte su 0000 0000 0000 xxxxb *)
819 | MODE_TNY e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
820 (λtmps.Some ? (pair ?? tmps cur_pc))
821 (* scrive 1 byte su 0000 0000 000x xxxxb *)
822 | MODE_SRT e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉 writeb)
823 (λtmps.Some ? (pair ?? tmps cur_pc)) ]
824 (* scrittura di una word *)
825 | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwritew:word16.match i with
826 (* NO: non ci sono indicazioni *)
828 (* NO: solo lettura/scrittura byte *)
830 (* NO: solo lettura/scrittura byte *)
832 (* NO: solo lettura/scrittura byte *)
835 (* NO: solo lettura byte *)
837 (* NO: solo lettura word *)
839 (* scrive 1 word su indirizzo diretto 1 byte *)
840 | MODE_DIR1 ⇒ mode_DIR1_write false m t s cur_pc writew
841 (* scrive 1 word su indirizzo diretto 1 word *)
842 | MODE_DIR2 ⇒ mode_DIR2_write false m t s cur_pc writew
843 (* scrive 1 word su H:X *)
844 | MODE_IX0 ⇒ mode_IX0_write false m t s cur_pc writew
845 (* scrive 1 word su H:X+1 byte offset *)
846 | MODE_IX1 ⇒ mode_IX1_write false m t s cur_pc writew
847 (* scrive 1 word su H:X+1 word offset *)
848 | MODE_IX2 ⇒ mode_IX2_write false m t s cur_pc writew
849 (* scrive 1 word su SP+1 byte offset *)
850 | MODE_SP1 ⇒ mode_SP1_write false m t s cur_pc writew
851 (* scrive 1 word su SP+1 word offset *)
852 | MODE_SP2 ⇒ mode_SP2_write false m t s cur_pc writew
854 (* NO: solo lettura/scrittura byte *)
855 | MODE_DIR1_to_DIR1 ⇒ None ?
856 (* NO: solo lettura/scrittura byte *)
857 | MODE_IMM1_to_DIR1 ⇒ None ?
858 (* NO: solo lettura/scrittura byte *)
859 | MODE_IX0p_to_DIR1 ⇒ None ?
860 (* NO: solo lettura/scrittura byte *)
861 | MODE_DIR1_to_IX0p ⇒ None ?
863 (* NO: solo lettura word/scrittura byte *)
864 | MODE_INHA_and_IMM1 ⇒ None ?
865 (* NO: solo lettura word/scrittura byte *)
866 | MODE_INHX_and_IMM1 ⇒ None ?
867 (* NO: solo lettura word *)
868 | MODE_IMM1_and_IMM1 ⇒ None ?
869 (* NO: solo lettura word/scrittura byte *)
870 | MODE_DIR1_and_IMM1 ⇒ None ?
871 (* NO: solo lettura word/scrittura byte *)
872 | MODE_IX0_and_IMM1 ⇒ None ?
873 (* NO: solo lettura word *)
874 | MODE_IX0p_and_IMM1 ⇒ None ?
875 (* NO: solo lettura word/scrittura byte *)
876 | MODE_IX1_and_IMM1 ⇒ None ?
877 (* NO: solo lettura word *)
878 | MODE_IX1p_and_IMM1 ⇒ None ?
879 (* NO: solo lettura word/scrittura byte *)
880 | MODE_SP1_and_IMM1 ⇒ None ?
882 (* NO: solo scrittura byte *)
883 | MODE_DIRn _ ⇒ None ?
884 (* NO: solo lettura word *)
885 | MODE_DIRn_and_IMM1 _ ⇒ None ?
886 (* NO: solo lettura/scrittura byte *)
887 | MODE_TNY _ ⇒ None ?
888 (* NO: solo lettura/scrittura byte *)
889 | MODE_SRT _ ⇒ None ?