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 definition filtered_plus_w16 := \lambda m:mcu_type.
264 let rec filtered_plus_w16 (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
267 | S n' ⇒ filtered_plus_w16 t s (filtered_inc_w16 m t s w) n' ]
268 in filtered_plus_w16.
271 errore1: non esiste traduzione ILL_OP
272 errore2: non e' riuscito a leggere ILL_FETCH_AD
273 altrimenti OK=info+new_pc
276 λm:mcu_type.λt:memory_impl.λs:any_status m t.
277 let pc ≝ get_pc_reg m t s in
278 let pc_next1 ≝ filtered_inc_w16 m t s pc in
279 let pc_next2 ≝ filtered_inc_w16 m t s pc_next1 in
280 match memory_filter_read m t s pc with
281 [ None ⇒ FetchERR ? ILL_FETCH_AD
282 | Some bh ⇒ match full_info_of_word16 m (Byte bh) with
283 (* non ha trovato una traduzione con 1 byte *)
284 [ None ⇒ match m with
285 (* HC05 non esistono op a 2 byte *)
286 [ HC05 ⇒ FetchERR ? ILL_OP
287 | HC08 ⇒ match eq_b8 bh 〈x9,xE〉 with
288 (* HC08 se il primo byte e' 0x9E il secondo puo' avere senso *)
289 [ true ⇒ match memory_filter_read m t s pc_next1 with
290 [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
291 [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
292 (* HC08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
293 | false ⇒ FetchERR ? ILL_OP
295 | HCS08 ⇒ match eq_b8 bh 〈x9,xE〉 with
296 (* HCS08 se il primo byte e' 0x9E il secondo puo' avere senso *)
297 [ true ⇒ match memory_filter_read m t s pc_next1 with
298 [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
299 [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
300 (* HCS08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
301 | false ⇒ FetchERR ? ILL_OP
303 (* RS08 non esistono op a 2 byte *)
304 | RS08 ⇒ FetchERR ? ILL_OP
306 (* ha trovato una traduzione con 1 byte *)
307 | Some info ⇒ FetchOK ? info pc_next1 ]].
309 (* ************************ *)
310 (* MODALITA' INDIRIZZAMENTO *)
311 (* ************************ *)
314 (* - incrementano l'indirizzo normalmente *)
315 (* - incrementano PC attraverso il filtro *)
317 (* lettura byte da addr *)
318 definition loadb_from ≝
319 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
320 opt_map ?? (memory_filter_read m t s addr)
321 (λb.Some ? (tripleT ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
323 (* lettura bit da addr *)
324 definition loadbit_from ≝
325 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.
326 opt_map ?? (memory_filter_read_bit m t s addr sub)
327 (λb.Some ? (tripleT ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
329 (* lettura word da addr *)
330 definition loadw_from ≝
331 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
332 opt_map ?? (memory_filter_read m t s addr)
333 (λbh.opt_map ?? (memory_filter_read m t s (succ_w16 addr))
334 (λbl.Some ? (tripleT ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc fetched)))).
336 (* scrittura byte su addr *)
337 definition writeb_to ≝
338 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwriteb:byte8.
339 opt_map ?? (memory_filter_write m t s addr writeb)
340 (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
342 (* scrittura bit su addr *)
343 definition writebit_to ≝
344 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.λwriteb:bool.
345 opt_map ?? (memory_filter_write_bit m t s addr sub writeb)
346 (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
348 (* scrittura word su addr *)
349 definition writew_to ≝
350 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
351 opt_map ?? (memory_filter_write m t s addr (w16h writew))
352 (λtmps1.opt_map ?? (memory_filter_write m t tmps1 (succ_w16 addr) (w16l writew))
353 (λtmps2.Some ? (pair ?? tmps2 (filtered_plus_w16 m t tmps2 cur_pc fetched)))).
355 (* ausiliari per definire i tipi e la lettura/scrittura *)
357 (* ausiliaria per definire il tipo di aux_load *)
358 definition aux_load_typing ≝
359 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
360 any_status m t → word16 → word16 → nat →
361 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
363 (* per non dover ramificare i vari load in byte/word *)
364 definition aux_load ≝
365 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
366 [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
368 (* ausiliaria per definire il tipo di aux_write *)
369 definition aux_write_typing ≝
370 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
371 any_status m t → word16 → word16 → nat →
372 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
373 option (Prod (any_status m t) word16).
375 (* per non dover ramificare i vari load in byte/word *)
376 definition aux_write ≝
377 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
378 [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
380 (* modalita' vere e proprie *)
382 (* lettura da [curpc]: IMM1 comportamento asimmetrico, quindi non si appoggia a loadb *)
383 definition mode_IMM1_load ≝
384 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
385 opt_map ?? (memory_filter_read m t s cur_pc)
386 (λb.Some ? (tripleT ??? s b (filtered_inc_w16 m t s cur_pc))).
388 (* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
389 definition mode_IMM2_load ≝
390 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
391 opt_map ?? (memory_filter_read m t s cur_pc)
392 (λbh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
393 (λbl.Some ? (tripleT ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc 2)))).
395 (* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
396 definition mode_DIR1_load ≝
397 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
398 opt_map ?? (memory_filter_read m t s cur_pc)
399 (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
401 (* lettura da [byte [curpc]]: loadbit *)
402 definition mode_DIR1n_load ≝
403 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
404 opt_map ?? (memory_filter_read m t s cur_pc)
405 (λaddr.loadbit_from m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
407 (* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
408 definition mode_DIR1_write ≝
409 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
410 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
411 opt_map ?? (memory_filter_read m t s cur_pc)
412 (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 writebw).
414 (* scrittura su [byte [curpc]]: writebit *)
415 definition mode_DIR1n_write ≝
416 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
417 opt_map ?? (memory_filter_read m t s cur_pc)
418 (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 writeb).
420 (* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
421 definition mode_DIR2_load ≝
422 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
423 opt_map ?? (memory_filter_read m t s cur_pc)
424 (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
425 (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc 2)).
427 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
428 definition mode_DIR2_write ≝
429 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
430 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
431 opt_map ?? (memory_filter_read m t s cur_pc)
432 (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
433 (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc 2 writebw)).
436 λm:mcu_type.λt:memory_impl.λs:any_status m t.
438 [ HC05 ⇒ opt_map ?? (get_indX_8_low_reg m t s) (λindx.Some ? 〈〈x0,x0〉:indx〉)
439 | HC08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
440 | HCS08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
443 (* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
444 definition mode_IX0_load ≝
445 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
446 opt_map ?? (get_IX m t s)
447 (λaddr.(aux_load m t byteflag) s addr cur_pc 0).
449 (* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
450 definition mode_IX0_write ≝
451 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
452 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
453 opt_map ?? (get_IX m t s)
454 (λaddr.(aux_write m t byteflag) s addr cur_pc 0 writebw).
456 (* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
457 definition mode_IX1_load ≝
458 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
459 opt_map ?? (get_IX m t s)
460 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
461 (λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
463 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
464 definition mode_IX1_write ≝
465 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
466 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
467 opt_map ?? (get_IX m t s)
468 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
469 (λoffs.(aux_write m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
471 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
472 definition mode_IX2_load ≝
473 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
474 opt_map ?? (get_IX m t s)
475 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
476 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
477 (λoffsl.(aux_load m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2))).
479 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
480 definition mode_IX2_write ≝
481 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
482 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
483 opt_map ?? (get_IX m t s)
484 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
485 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
486 (λoffsl.(aux_write m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2 writebw))).
488 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
489 definition mode_SP1_load ≝
490 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
491 opt_map ?? (get_sp_reg m t s)
492 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
493 (λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
495 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
496 definition mode_SP1_write ≝
497 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
498 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
499 opt_map ?? (get_sp_reg m t s)
500 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
501 (λoffs.(aux_write m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
503 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
504 definition mode_SP2_load ≝
505 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
506 opt_map ?? (get_sp_reg m t s)
507 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
508 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
509 (λoffsl.(aux_load m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2))).
511 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
512 definition mode_SP2_write ≝
513 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
514 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
515 opt_map ?? (get_sp_reg 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_write m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2 writebw))).
520 (* ************************************** *)
521 (* raccordo di tutte le possibili letture *)
522 (* ************************************** *)
525 definition aux_inc_indX_16 ≝
526 λm:mcu_type.λt:memory_impl.λs:any_status m t.
527 opt_map ?? (get_indX_16_reg m t s)
528 (λX_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 X_op))
529 (λs_tmp.Some ? s_tmp)).
531 (* tutte le modalita' di lettura: false=loadb true=loadw *)
532 definition multi_mode_load ≝
533 λbyteflag:bool.λm:mcu_type.λt:memory_impl.
535 return λbyteflag:bool.any_status m t → word16 → instr_mode →
536 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
538 (* lettura di un byte *)
539 [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
540 (* NO: non ci sono indicazioni *)
543 | MODE_INHA ⇒ Some ? (tripleT ??? s (get_acc_8_low_reg m t s) cur_pc)
545 | MODE_INHX ⇒ opt_map ?? (get_indX_8_low_reg m t s)
546 (λindx.Some ? (tripleT ??? s indx cur_pc))
548 | MODE_INHH ⇒ opt_map ?? (get_indX_8_high_reg m t s)
549 (λindx.Some ? (tripleT ??? s indx cur_pc))
551 (* preleva 1 byte immediato *)
552 | MODE_IMM1 ⇒ mode_IMM1_load m t s cur_pc
553 (* NO: solo lettura word *)
555 (* preleva 1 byte da indirizzo diretto 1 byte *)
556 | MODE_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
557 (* preleva 1 byte da indirizzo diretto 1 word *)
558 | MODE_DIR2 ⇒ mode_DIR2_load true m t s cur_pc
559 (* preleva 1 byte da H:X *)
560 | MODE_IX0 ⇒ mode_IX0_load true m t s cur_pc
561 (* preleva 1 byte da H:X+1 byte offset *)
562 | MODE_IX1 ⇒ mode_IX1_load true m t s cur_pc
563 (* preleva 1 byte da H:X+1 word offset *)
564 | MODE_IX2 ⇒ mode_IX2_load true m t s cur_pc
565 (* preleva 1 byte da SP+1 byte offset *)
566 | MODE_SP1 ⇒ mode_SP1_load true m t s cur_pc
567 (* preleva 1 byte da SP+1 word offset *)
568 | MODE_SP2 ⇒ mode_SP2_load true m t s cur_pc
570 (* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
571 | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
572 (* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
573 | MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load m t s cur_pc
574 (* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
575 | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true m t s cur_pc
576 (* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
577 | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true m t s cur_pc
579 (* NO: solo lettura word/scrittura byte *)
580 | MODE_INHA_and_IMM1 ⇒ None ?
581 (* NO: solo lettura word/scrittura byte *)
582 | MODE_INHX_and_IMM1 ⇒ None ?
583 (* NO: solo lettura word *)
584 | MODE_IMM1_and_IMM1 ⇒ None ?
585 (* NO: solo lettura word/scrittura byte *)
586 | MODE_DIR1_and_IMM1 ⇒ None ?
587 (* NO: solo lettura word/scrittura byte *)
588 | MODE_IX0_and_IMM1 ⇒ None ?
589 (* NO: solo lettura word *)
590 | MODE_IX0p_and_IMM1 ⇒ None ?
591 (* NO: solo lettura word/scrittura byte *)
592 | MODE_IX1_and_IMM1 ⇒ None ?
593 (* NO: solo lettura word *)
594 | MODE_IX1p_and_IMM1 ⇒ None ?
595 (* NO: solo lettura word/scrittura byte *)
596 | MODE_SP1_and_IMM1 ⇒ None ?
598 (* NO: solo scrittura byte *)
599 | MODE_DIRn _ ⇒ None ?
600 (* NO: solo lettura word *)
601 | MODE_DIRn_and_IMM1 _ ⇒ None ?
602 (* preleva 1 byte da 0000 0000 0000 xxxxb *)
603 | MODE_TNY e ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
604 (λb.Some ? (tripleT ??? s b cur_pc))
605 (* preleva 1 byte da 0000 0000 000x xxxxb *)
606 | MODE_SRT e ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉)
607 (λb.Some ? (tripleT ??? s b cur_pc))
609 (* lettura di una word *)
610 | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
611 (* NO: non ci sono indicazioni *)
613 (* NO: solo lettura/scrittura byte *)
615 (* NO: solo lettura/scrittura byte *)
617 (* NO: solo lettura/scrittura byte *)
620 (* NO: solo lettura byte *)
622 (* preleva 1 word immediato *)
623 | MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
624 (* preleva 1 word da indirizzo diretto 1 byte *)
625 | MODE_DIR1 ⇒ mode_DIR1_load false m t s cur_pc
626 (* preleva 1 word da indirizzo diretto 1 word *)
627 | MODE_DIR2 ⇒ mode_DIR2_load false m t s cur_pc
628 (* preleva 1 word da H:X *)
629 | MODE_IX0 ⇒ mode_IX0_load false m t s cur_pc
630 (* preleva 1 word da H:X+1 byte offset *)
631 | MODE_IX1 ⇒ mode_IX1_load false m t s cur_pc
632 (* preleva 1 word da H:X+1 word offset *)
633 | MODE_IX2 ⇒ mode_IX2_load false m t s cur_pc
634 (* preleva 1 word da SP+1 byte offset *)
635 | MODE_SP1 ⇒ mode_SP1_load false m t s cur_pc
636 (* preleva 1 word da SP+1 word offset *)
637 | MODE_SP2 ⇒ mode_SP2_load false m t s cur_pc
639 (* NO: solo lettura/scrittura byte *)
640 | MODE_DIR1_to_DIR1 ⇒ None ?
641 (* NO: solo lettura/scrittura byte *)
642 | MODE_IMM1_to_DIR1 ⇒ None ?
643 (* NO: solo lettura/scrittura byte *)
644 | MODE_IX0p_to_DIR1 ⇒ None ?
645 (* NO: solo lettura/scrittura byte *)
646 | MODE_DIR1_to_IX0p ⇒ None ?
648 (* preleva 2 byte, possibilita' modificare Io argomento *)
649 | MODE_INHA_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
650 (λS_immb_and_PC.match S_immb_and_PC with
651 [ tripleT _ immb cur_pc' ⇒
652 Some ? (tripleT ??? s 〈(get_acc_8_low_reg m t s):immb〉 cur_pc')])
653 (* preleva 2 byte, possibilita' modificare Io argomento *)
654 | MODE_INHX_and_IMM1 ⇒ opt_map ?? (get_indX_8_low_reg m t s)
655 (λX_op.opt_map ?? (mode_IMM1_load m t s cur_pc)
656 (λS_immb_and_PC.match S_immb_and_PC with
657 [ tripleT _ immb cur_pc' ⇒
658 Some ? (tripleT ??? s 〈X_op:immb〉 cur_pc')]))
659 (* preleva 2 byte, NO possibilita' modificare Io argomento *)
660 | MODE_IMM1_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
661 (λS_immb1_and_PC.match S_immb1_and_PC with
662 [ tripleT _ immb1 cur_pc' ⇒
663 opt_map ?? (mode_IMM1_load m t s cur_pc')
664 (λS_immb2_and_PC.match S_immb2_and_PC with
665 [ tripleT _ immb2 cur_pc'' ⇒
666 Some ? (tripleT ??? s 〈immb1:immb2〉 cur_pc'')])])
667 (* preleva 2 byte, possibilita' modificare Io argomento *)
668 | MODE_DIR1_and_IMM1 ⇒ opt_map ?? (mode_DIR1_load true m t s cur_pc)
669 (λS_dirb_and_PC.match S_dirb_and_PC with
670 [ tripleT _ dirb cur_pc' ⇒
671 opt_map ?? (mode_IMM1_load m t s cur_pc')
672 (λS_immb_and_PC.match S_immb_and_PC with
673 [ tripleT _ immb cur_pc'' ⇒
674 Some ? (tripleT ??? s 〈dirb:immb〉 cur_pc'')])])
675 (* preleva 2 byte, possibilita' modificare Io argomento *)
676 | MODE_IX0_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
677 (λS_ixb_and_PC.match S_ixb_and_PC with
678 [ tripleT _ ixb cur_pc' ⇒
679 opt_map ?? (mode_IMM1_load m t s cur_pc')
680 (λS_immb_and_PC.match S_immb_and_PC with
681 [ tripleT _ immb cur_pc'' ⇒
682 Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
683 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
684 | MODE_IX0p_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
685 (λS_ixb_and_PC.match S_ixb_and_PC with
686 [ tripleT _ ixb cur_pc' ⇒
687 opt_map ?? (mode_IMM1_load m t s cur_pc')
688 (λS_immb_and_PC.match S_immb_and_PC with
689 [ tripleT _ immb cur_pc'' ⇒
691 opt_map ?? (aux_inc_indX_16 m t s)
692 (λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
693 (* preleva 2 byte, possibilita' modificare Io argomento *)
694 | MODE_IX1_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
695 (λS_ixb_and_PC.match S_ixb_and_PC with
696 [ tripleT _ ixb cur_pc' ⇒
697 opt_map ?? (mode_IMM1_load m t s cur_pc')
698 (λS_immb_and_PC.match S_immb_and_PC with
699 [ tripleT _ immb cur_pc'' ⇒
700 Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
701 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
702 | MODE_IX1p_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
703 (λS_ixb_and_PC.match S_ixb_and_PC with
704 [ tripleT _ ixb cur_pc' ⇒
705 opt_map ?? (mode_IMM1_load m t s cur_pc')
706 (λS_immb_and_PC.match S_immb_and_PC with
707 [ tripleT _ immb cur_pc'' ⇒
709 opt_map ?? (aux_inc_indX_16 m t s)
710 (λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
711 (* preleva 2 byte, possibilita' modificare Io argomento *)
712 | MODE_SP1_and_IMM1 ⇒ opt_map ?? (mode_SP1_load true m t s cur_pc)
713 (λS_spb_and_PC.match S_spb_and_PC with
714 [ tripleT _ spb cur_pc' ⇒
715 opt_map ?? (mode_IMM1_load m t s cur_pc')
716 (λS_immb_and_PC.match S_immb_and_PC with
717 [ tripleT _ immb cur_pc'' ⇒
718 Some ? (tripleT ??? s 〈spb:immb〉 cur_pc'')])])
720 (* NO: solo scrittura byte *)
721 | MODE_DIRn _ ⇒ None ?
722 (* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
723 | MODE_DIRn_and_IMM1 msk ⇒ opt_map ?? (mode_DIR1n_load m t s cur_pc msk)
724 (λS_dirbn_and_PC.match S_dirbn_and_PC with
725 [ tripleT _ dirbn cur_pc' ⇒
726 opt_map ?? (mode_IMM1_load m t s cur_pc')
727 (λS_immb_and_PC.match S_immb_and_PC with
728 [ tripleT _ immb cur_pc'' ⇒
729 Some ? (tripleT ??? s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
730 (* NO: solo lettura/scrittura byte *)
731 | MODE_TNY _ ⇒ None ?
732 (* NO: solo lettura/scrittura byte *)
733 | MODE_SRT _ ⇒ None ?
737 (* **************************************** *)
738 (* raccordo di tutte le possibili scritture *)
739 (* **************************************** *)
741 (* tutte le modalita' di scrittura: true=writeb, false=writew *)
742 definition multi_mode_write ≝
743 λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
744 return λbyteflag:bool.any_status m t → word16 → instr_mode →
745 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
746 option (Prod (any_status m t) word16) with
747 (* scrittura di un byte *)
748 [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwriteb:byte8.match i with
749 (* NO: non ci sono indicazioni *)
752 | MODE_INHA ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
754 | MODE_INHX ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
755 (λtmps.Some ? (pair ?? tmps cur_pc))
757 | MODE_INHH ⇒ opt_map ?? (set_indX_8_high_reg m t s writeb)
758 (λtmps.Some ? (pair ?? tmps cur_pc))
760 (* NO: solo lettura byte *)
762 (* NO: solo lettura word *)
764 (* scrive 1 byte su indirizzo diretto 1 byte *)
765 | MODE_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
766 (* scrive 1 byte su indirizzo diretto 1 word *)
767 | MODE_DIR2 ⇒ mode_DIR2_write true m t s cur_pc writeb
768 (* scrive 1 byte su H:X *)
769 | MODE_IX0 ⇒ mode_IX0_write true m t s cur_pc writeb
770 (* scrive 1 byte su H:X+1 byte offset *)
771 | MODE_IX1 ⇒ mode_IX1_write true m t s cur_pc writeb
772 (* scrive 1 byte su H:X+1 word offset *)
773 | MODE_IX2 ⇒ mode_IX2_write true m t s cur_pc writeb
774 (* scrive 1 byte su SP+1 byte offset *)
775 | MODE_SP1 ⇒ mode_SP1_write true m t s cur_pc writeb
776 (* scrive 1 byte su SP+1 word offset *)
777 | MODE_SP2 ⇒ mode_SP2_write true m t s cur_pc writeb
779 (* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
780 | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
781 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
782 | MODE_IMM1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
783 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
784 | MODE_IX0p_to_DIR1 ⇒ opt_map ?? (mode_DIR1_write true m t s cur_pc writeb)
785 (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
787 opt_map ?? (aux_inc_indX_16 m t S_op)
788 (λS_op'.Some ? (pair ?? S_op' PC_op))])
789 (* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
790 | MODE_DIR1_to_IX0p ⇒ opt_map ?? (mode_IX0_write true m t s cur_pc writeb)
791 (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
793 opt_map ?? (aux_inc_indX_16 m t S_op)
794 (λS_op'.Some ? (pair ?? S_op' PC_op))])
796 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
797 | MODE_INHA_and_IMM1 ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
798 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)
799 | MODE_INHX_and_IMM1 ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
800 (λtmps.Some ? (pair ?? tmps cur_pc))
801 (* NO: solo lettura word *)
802 | MODE_IMM1_and_IMM1 ⇒ None ?
803 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
804 | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write true m t s cur_pc writeb
805 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
806 | MODE_IX0_and_IMM1 ⇒ mode_IX0_write true m t s cur_pc writeb
807 (* NO: solo lettura word *)
808 | MODE_IX0p_and_IMM1 ⇒ None ?
809 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
810 | MODE_IX1_and_IMM1 ⇒ mode_IX1_write true m t s cur_pc writeb
811 (* NO: solo lettura word *)
812 | MODE_IX1p_and_IMM1 ⇒ None ?
813 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
814 | MODE_SP1_and_IMM1 ⇒ mode_SP1_write true m t s cur_pc writeb
816 (* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
817 | MODE_DIRn msk ⇒ mode_DIR1n_write m t s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))
818 (* NO: solo lettura word *)
819 | MODE_DIRn_and_IMM1 _ ⇒ None ?
820 (* scrive 1 byte su 0000 0000 0000 xxxxb *)
821 | MODE_TNY e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
822 (λtmps.Some ? (pair ?? tmps cur_pc))
823 (* scrive 1 byte su 0000 0000 000x xxxxb *)
824 | MODE_SRT e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉 writeb)
825 (λtmps.Some ? (pair ?? tmps cur_pc)) ]
826 (* scrittura di una word *)
827 | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwritew:word16.match i with
828 (* NO: non ci sono indicazioni *)
830 (* NO: solo lettura/scrittura byte *)
832 (* NO: solo lettura/scrittura byte *)
834 (* NO: solo lettura/scrittura byte *)
837 (* NO: solo lettura byte *)
839 (* NO: solo lettura word *)
841 (* scrive 1 word su indirizzo diretto 1 byte *)
842 | MODE_DIR1 ⇒ mode_DIR1_write false m t s cur_pc writew
843 (* scrive 1 word su indirizzo diretto 1 word *)
844 | MODE_DIR2 ⇒ mode_DIR2_write false m t s cur_pc writew
845 (* scrive 1 word su H:X *)
846 | MODE_IX0 ⇒ mode_IX0_write false m t s cur_pc writew
847 (* scrive 1 word su H:X+1 byte offset *)
848 | MODE_IX1 ⇒ mode_IX1_write false m t s cur_pc writew
849 (* scrive 1 word su H:X+1 word offset *)
850 | MODE_IX2 ⇒ mode_IX2_write false m t s cur_pc writew
851 (* scrive 1 word su SP+1 byte offset *)
852 | MODE_SP1 ⇒ mode_SP1_write false m t s cur_pc writew
853 (* scrive 1 word su SP+1 word offset *)
854 | MODE_SP2 ⇒ mode_SP2_write false m t s cur_pc writew
856 (* NO: solo lettura/scrittura byte *)
857 | MODE_DIR1_to_DIR1 ⇒ None ?
858 (* NO: solo lettura/scrittura byte *)
859 | MODE_IMM1_to_DIR1 ⇒ None ?
860 (* NO: solo lettura/scrittura byte *)
861 | MODE_IX0p_to_DIR1 ⇒ None ?
862 (* NO: solo lettura/scrittura byte *)
863 | MODE_DIR1_to_IX0p ⇒ None ?
865 (* NO: solo lettura word/scrittura byte *)
866 | MODE_INHA_and_IMM1 ⇒ None ?
867 (* NO: solo lettura word/scrittura byte *)
868 | MODE_INHX_and_IMM1 ⇒ None ?
869 (* NO: solo lettura word *)
870 | MODE_IMM1_and_IMM1 ⇒ None ?
871 (* NO: solo lettura word/scrittura byte *)
872 | MODE_DIR1_and_IMM1 ⇒ None ?
873 (* NO: solo lettura word/scrittura byte *)
874 | MODE_IX0_and_IMM1 ⇒ None ?
875 (* NO: solo lettura word *)
876 | MODE_IX0p_and_IMM1 ⇒ None ?
877 (* NO: solo lettura word/scrittura byte *)
878 | MODE_IX1_and_IMM1 ⇒ None ?
879 (* NO: solo lettura word *)
880 | MODE_IX1p_and_IMM1 ⇒ None ?
881 (* NO: solo lettura word/scrittura byte *)
882 | MODE_SP1_and_IMM1 ⇒ None ?
884 (* NO: solo scrittura byte *)
885 | MODE_DIRn _ ⇒ None ?
886 (* NO: solo lettura word *)
887 | MODE_DIRn_and_IMM1 _ ⇒ None ?
888 (* NO: solo lettura/scrittura byte *)
889 | MODE_TNY _ ⇒ None ?
890 (* NO: solo lettura/scrittura byte *)
891 | MODE_SRT _ ⇒ None ?