1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 set "baseuri" "cic:/matita/freescale/load_write/".
29 (*include "/media/VIRTUOSO/freescale/model.ma".*)
30 include "freescale/model.ma".
32 (* errori possibili nel fetch *)
33 inductive error_type : Type ≝
35 | ILL_FETCH_AD: error_type
36 | ILL_EX_AD: error_type.
38 (* un tipo opzione ad hoc
39 - errore: interessa solo l'errore
40 - ok: interessa info e il nuovo pc
42 inductive fetch_result (A:Type) : Type ≝
43 FetchERR : error_type → fetch_result A
44 | FetchOK : A → word16 → fetch_result A.
46 (* **************************** *)
47 (* FETCH E ACCESSO ALLA MEMORIA *)
48 (* **************************** *)
50 (* ausialiaria per RS08 read *)
51 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
52 memory mapped, quindi bisona intercettare la lettura.
53 NB: fare molta attenzione alle note sulle combinazioni possibili perche'
54 il comportamento della memoria nell'RS08 e' strano e ci sono
55 precise condizioni che impediscono una semantica circolare dell'accesso
56 (divergenza=assenza di definizione) *)
57 definition RS08_memory_filter_read_aux ≝
58 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
59 λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option T.
61 [ mk_any_status alu mem chk _ ⇒ match alu with
62 [ mk_alu_RS08 _ _ _ _ xm psm _ _ ⇒
64 possibili accessi al registro X
66 2) addr=000E (X =0F): indiretto
67 3) addr=00CF (PS=00): paging
69 [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
70 non si possono combinare due effetti contemporaneamente!
71 per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni
73 match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
74 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
75 (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
79 possibili accessi al registro PS
81 2) addr=000E (X =1F): indiretto
82 3) addr=00DF (PS=00): paging
84 match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
85 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
86 (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
90 accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
91 altrimenti sarebbero 2 indirezioni
93 match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
94 [ true ⇒ fMEM mem chk 〈〈x0,x0〉:xm〉
97 accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
99 match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
100 [ true ⇒ fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
101 (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉))
105 | false ⇒ fMEM mem chk addr ]]]]]].
107 (* lettura RS08 di un byte *)
108 definition RS08_memory_filter_read ≝
109 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
110 RS08_memory_filter_read_aux t s addr byte8
112 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read t m c a).
114 (* lettura RS08 di un bit *)
115 definition RS08_memory_filter_read_bit ≝
116 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.
117 RS08_memory_filter_read_aux t s addr bool
118 (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
119 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read_bit t m c a sub).
121 (* in caso di RS08 si dirotta sul filtro, altrimenti si legge direttamente *)
122 definition memory_filter_read ≝
123 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → option byte8 with
124 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.
125 mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
126 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.
127 mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
128 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.
129 mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
130 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.
131 RS08_memory_filter_read t s addr
134 definition memory_filter_read_bit ≝
135 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → oct → option bool with
136 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.
137 mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
138 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.
139 mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
140 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.
141 mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
142 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.
143 RS08_memory_filter_read_bit t s addr sub
146 (* ausialiaria per RS08 write *)
147 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
148 memory mapped, quindi bisona intercettare la scrittura.
149 NB: fare molta attenzione alle note sulle combinazioni possibili perche'
150 il comportamento della memoria nell'RS08 e' strano e ci sono
151 precise condizioni che impediscono una semantica circolare dell'accesso
152 (divergenza=assenza di definizione) *)
153 definition RS08_memory_filter_write_aux ≝
154 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
155 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option (aux_mem_type t).
157 [ mk_any_status alu mem chk clk ⇒ match alu with
158 [ mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl ⇒
160 possibili accessi al registro X
161 1) addr=000F: diretto
162 2) addr=000E (X =0F): indiretto
163 3) addr=00CF (PS=00): paging
165 [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
166 non si possono combinare due effetti contemporaneamente!
167 per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni
169 match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
170 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
171 (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
172 [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc (fREG xm) psm zfl cfl) mem chk clk)
175 possibili accessi al registro PS
176 1) addr=001F: diretto
177 2) addr=000E (X =1F): indiretto
178 3) addr=00DF (PS=00): paging
180 match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
181 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
182 (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
183 [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm (fREG psm) zfl cfl) mem chk clk)
186 accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
187 altrimenti sarebbero 2 indirezioni
189 match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
190 [ true ⇒ opt_map ?? (fMEM mem chk 〈〈x0,x0〉:xm〉)
191 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
195 accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
197 match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
198 [ true ⇒ opt_map ?? (fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
199 (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉)))
200 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
204 | false ⇒ opt_map ?? (fMEM mem chk addr)
205 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk)) ]]]]]].
207 (* scrittura RS08 di un byte *)
208 definition RS08_memory_filter_write ≝
209 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λval:byte8.
210 RS08_memory_filter_write_aux t s addr
212 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update t m c a val).
214 (* scrittura RS08 di un bit *)
215 definition RS08_memory_filter_write_bit ≝
216 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
217 RS08_memory_filter_write_aux t s addr
218 (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
219 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update_bit t m c a sub val).
221 (* in caso di RS08 si dirotta sul filtro, altrimenti si scrive direttamente *)
222 definition memory_filter_write ≝
223 λm:mcu_type.λt:memory_impl.match m
224 return λm:mcu_type.any_status m t → word16 → byte8 → option (any_status m t) with
225 [ HC05 ⇒ λs:any_status HC05 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 | HC08 ⇒ λs:any_status HC08 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 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λval:byte8.
232 opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
233 (λmem.Some ? (set_mem_desc ? t s mem))
234 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λval:byte8.
235 RS08_memory_filter_write t s addr val
238 definition memory_filter_write_bit ≝
239 λm:mcu_type.λt:memory_impl.match m
240 return λm:mcu_type.any_status m t → word16 → oct → bool → option (any_status m t) with
241 [ HC05 ⇒ λs:any_status HC05 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 | HC08 ⇒ λs:any_status HC08 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 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.λval:bool.
248 opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
249 (λmem.Some ? (set_mem_desc ? t s mem))
250 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
251 RS08_memory_filter_write_bit t s addr sub val
255 Da utilizzarsi solo per gli aggiornamenti di PC (per il fetch),
256 NON per il caricamento degli indiretti.
257 - il caricamento degli immediati spetta al fetcher
258 (incremento progressivo di PC ciclo per ciclo, e riempimento del prefetch
259 che a questo punto DEVE poter indirizzare qualsiasi locazione puntata da PC)
260 - il caricamento degli indiretti non spetta al fetcher
262 definition filtered_inc_w16 ≝
263 λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
264 get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
266 let rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
269 | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
272 errore1: non esiste traduzione ILL_OP
273 errore2: non e' riuscito a leggere ILL_FETCH_AD
274 altrimenti OK=info+new_pc
277 λm:mcu_type.λt:memory_impl.λs:any_status m t.
278 let pc ≝ get_pc_reg m t s in
279 let pc_next1 ≝ filtered_inc_w16 m t s pc in
280 let pc_next2 ≝ filtered_inc_w16 m t s pc_next1 in
281 match memory_filter_read m t s pc with
282 [ None ⇒ FetchERR ? ILL_FETCH_AD
283 | Some bh ⇒ match full_info_of_word16 m (Byte bh) with
284 (* non ha trovato una traduzione con 1 byte *)
285 [ None ⇒ match m with
286 (* HC05 non esistono op a 2 byte *)
287 [ HC05 ⇒ FetchERR ? ILL_OP
288 | HC08 ⇒ match eq_b8 bh 〈x9,xE〉 with
289 (* HC08 se il primo byte e' 0x9E il secondo puo' avere senso *)
290 [ true ⇒ match memory_filter_read m t s pc_next1 with
291 [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
292 [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
293 (* HC08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
294 | false ⇒ FetchERR ? ILL_OP
296 | HCS08 ⇒ match eq_b8 bh 〈x9,xE〉 with
297 (* HCS08 se il primo byte e' 0x9E il secondo puo' avere senso *)
298 [ true ⇒ match memory_filter_read m t s pc_next1 with
299 [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
300 [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
301 (* HCS08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
302 | false ⇒ FetchERR ? ILL_OP
304 (* RS08 non esistono op a 2 byte *)
305 | RS08 ⇒ FetchERR ? ILL_OP
307 (* ha trovato una traduzione con 1 byte *)
308 | Some info ⇒ FetchOK ? info pc_next1 ]].
310 (* ************************ *)
311 (* MODALITA' INDIRIZZAMENTO *)
312 (* ************************ *)
315 (* - incrementano l'indirizzo normalmente *)
316 (* - incrementano PC attraverso il filtro *)
318 (* lettura byte da addr *)
319 definition loadb_from ≝
320 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
321 opt_map ?? (memory_filter_read m t s addr)
322 (λb.Some ? (tripleT ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
324 (* lettura bit da addr *)
325 definition loadbit_from ≝
326 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.
327 opt_map ?? (memory_filter_read_bit m t s addr sub)
328 (λb.Some ? (tripleT ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
330 (* lettura word da addr *)
331 definition loadw_from ≝
332 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
333 opt_map ?? (memory_filter_read m t s addr)
334 (λbh.opt_map ?? (memory_filter_read m t s (succ_w16 addr))
335 (λbl.Some ? (tripleT ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc fetched)))).
337 (* scrittura byte su addr *)
338 definition writeb_to ≝
339 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwriteb:byte8.
340 opt_map ?? (memory_filter_write m t s addr writeb)
341 (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
343 (* scrittura bit su addr *)
344 definition writebit_to ≝
345 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.λwriteb:bool.
346 opt_map ?? (memory_filter_write_bit m t s addr sub writeb)
347 (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
349 (* scrittura word su addr *)
350 definition writew_to ≝
351 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
352 opt_map ?? (memory_filter_write m t s addr (w16h writew))
353 (λtmps.opt_map ?? (memory_filter_write m t s (succ_w16 addr) (w16l writew))
354 (λtmps'.Some ? (pair ?? tmps' (filtered_plus_w16 m t s cur_pc fetched)))).
356 (* ausiliari per definire i tipi e la lettura/scrittura *)
358 (* ausiliaria per definire il tipo di aux_load *)
359 definition aux_load_typing ≝
360 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
361 any_status m t → word16 → word16 → nat →
362 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
364 (* per non dover ramificare i vari load in byte/word *)
365 definition aux_load ≝
366 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
367 [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
369 (* ausiliaria per definire il tipo di aux_write *)
370 definition aux_write_typing ≝
371 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
372 any_status m t → word16 → word16 → nat →
373 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
374 option (Prod (any_status m t) word16).
376 (* per non dover ramificare i vari load in byte/word *)
377 definition aux_write ≝
378 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
379 [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
381 (* modalita' vere e proprie *)
383 (* lettura da [curpc]: IMM1 comportamento asimmetrico, quindi non si appoggia a loadb *)
384 definition mode_IMM1_load ≝
385 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
386 opt_map ?? (memory_filter_read m t s cur_pc)
387 (λb.Some ? (tripleT ??? s b (filtered_inc_w16 m t s cur_pc))).
389 (* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
390 definition mode_IMM2_load ≝
391 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
392 opt_map ?? (memory_filter_read m t s cur_pc)
393 (λbh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
394 (λbl.Some ? (tripleT ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc 2)))).
396 (* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
397 definition mode_DIR1_load ≝
398 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
399 opt_map ?? (memory_filter_read m t s cur_pc)
400 (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
402 (* lettura da [byte [curpc]]: loadbit *)
403 definition mode_DIR1n_load ≝
404 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
405 opt_map ?? (memory_filter_read m t s cur_pc)
406 (λaddr.loadbit_from m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
408 (* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
409 definition mode_DIR1_write ≝
410 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
411 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
412 opt_map ?? (memory_filter_read m t s cur_pc)
413 (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 writebw).
415 (* scrittura su [byte [curpc]]: writebit *)
416 definition mode_DIR1n_write ≝
417 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
418 opt_map ?? (memory_filter_read m t s cur_pc)
419 (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 writeb).
421 (* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
422 definition mode_DIR2_load ≝
423 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
424 opt_map ?? (memory_filter_read m t s cur_pc)
425 (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
426 (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc 2)).
428 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
429 definition mode_DIR2_write ≝
430 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
431 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
432 opt_map ?? (memory_filter_read m t s cur_pc)
433 (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
434 (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc 2 writebw)).
437 λm:mcu_type.λt:memory_impl.λs:any_status m t.
439 [ HC05 ⇒ opt_map ?? (get_indX_8_low_reg m t s) (λindx.Some ? 〈〈x0,x0〉:indx〉)
440 | HC08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
441 | HCS08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
444 (* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
445 definition mode_IX0_load ≝
446 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
447 opt_map ?? (get_IX m t s)
448 (λaddr.(aux_load m t byteflag) s addr cur_pc 0).
450 (* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
451 definition mode_IX0_write ≝
452 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
453 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
454 opt_map ?? (get_IX m t s)
455 (λaddr.(aux_write m t byteflag) s addr cur_pc 0 writebw).
457 (* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
458 definition mode_IX1_load ≝
459 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
460 opt_map ?? (get_IX m t s)
461 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
462 (λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
464 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
465 definition mode_IX1_write ≝
466 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
467 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
468 opt_map ?? (get_IX m t s)
469 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
470 (λoffs.(aux_write m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
472 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
473 definition mode_IX2_load ≝
474 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
475 opt_map ?? (get_IX m t s)
476 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
477 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
478 (λoffsl.(aux_load m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2))).
480 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
481 definition mode_IX2_write ≝
482 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
483 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
484 opt_map ?? (get_IX m t s)
485 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
486 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
487 (λoffsl.(aux_write m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2 writebw))).
489 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
490 definition mode_SP1_load ≝
491 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
492 opt_map ?? (get_sp_reg m t s)
493 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
494 (λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
496 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
497 definition mode_SP1_write ≝
498 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
499 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
500 opt_map ?? (get_sp_reg m t s)
501 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
502 (λoffs.(aux_write m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
504 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
505 definition mode_SP2_load ≝
506 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
507 opt_map ?? (get_sp_reg m t s)
508 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
509 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
510 (λoffsl.(aux_load m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2))).
512 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
513 definition mode_SP2_write ≝
514 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
515 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
516 opt_map ?? (get_sp_reg m t s)
517 (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
518 (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
519 (λoffsl.(aux_write m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2 writebw))).
521 (* ************************************** *)
522 (* raccordo di tutte le possibili letture *)
523 (* ************************************** *)
526 definition aux_inc_indX_16 ≝
527 λm:mcu_type.λt:memory_impl.λs:any_status m t.
528 opt_map ?? (get_indX_16_reg m t s)
529 (λX_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 X_op))
530 (λs_tmp.Some ? s_tmp)).
532 (* tutte le modalita' di lettura: false=loadb true=loadw *)
533 definition multi_mode_load ≝
534 λbyteflag:bool.λm:mcu_type.λt:memory_impl.
536 return λbyteflag:bool.any_status m t → word16 → instr_mode →
537 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
539 (* lettura di un byte *)
540 [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
541 (* NO: non ci sono indicazioni *)
544 | MODE_INHA ⇒ Some ? (tripleT ??? s (get_acc_8_low_reg m t s) cur_pc)
546 | MODE_INHX ⇒ opt_map ?? (get_indX_8_low_reg m t s)
547 (λindx.Some ? (tripleT ??? s indx cur_pc))
549 | MODE_INHH ⇒ opt_map ?? (get_indX_8_high_reg m t s)
550 (λindx.Some ? (tripleT ??? s indx cur_pc))
552 (* preleva 1 byte immediato *)
553 | MODE_IMM1 ⇒ mode_IMM1_load m t s cur_pc
554 (* NO: solo lettura word *)
556 (* preleva 1 byte da indirizzo diretto 1 byte *)
557 | MODE_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
558 (* preleva 1 byte da indirizzo diretto 1 word *)
559 | MODE_DIR2 ⇒ mode_DIR2_load true m t s cur_pc
560 (* preleva 1 byte da H:X *)
561 | MODE_IX0 ⇒ mode_IX0_load true m t s cur_pc
562 (* preleva 1 byte da H:X+1 byte offset *)
563 | MODE_IX1 ⇒ mode_IX1_load true m t s cur_pc
564 (* preleva 1 byte da H:X+1 word offset *)
565 | MODE_IX2 ⇒ mode_IX2_load true m t s cur_pc
566 (* preleva 1 byte da SP+1 byte offset *)
567 | MODE_SP1 ⇒ mode_SP1_load true m t s cur_pc
568 (* preleva 1 byte da SP+1 word offset *)
569 | MODE_SP2 ⇒ mode_SP2_load true m t s cur_pc
571 (* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
572 | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
573 (* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
574 | MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load m t s cur_pc
575 (* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
576 | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true m t s cur_pc
577 (* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
578 | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true m t s cur_pc
580 (* NO: solo lettura word/scrittura byte *)
581 | MODE_INHA_and_IMM1 ⇒ None ?
582 (* NO: solo lettura word/scrittura byte *)
583 | MODE_INHX_and_IMM1 ⇒ None ?
584 (* NO: solo lettura word *)
585 | MODE_IMM1_and_IMM1 ⇒ None ?
586 (* NO: solo lettura word/scrittura byte *)
587 | MODE_DIR1_and_IMM1 ⇒ None ?
588 (* NO: solo lettura word/scrittura byte *)
589 | MODE_IX0_and_IMM1 ⇒ None ?
590 (* NO: solo lettura word *)
591 | MODE_IX0p_and_IMM1 ⇒ None ?
592 (* NO: solo lettura word/scrittura byte *)
593 | MODE_IX1_and_IMM1 ⇒ None ?
594 (* NO: solo lettura word *)
595 | MODE_IX1p_and_IMM1 ⇒ None ?
596 (* NO: solo lettura word/scrittura byte *)
597 | MODE_SP1_and_IMM1 ⇒ None ?
599 (* NO: solo scrittura byte *)
600 | MODE_DIRn _ ⇒ None ?
601 (* NO: solo lettura word *)
602 | MODE_DIRn_and_IMM1 _ ⇒ None ?
603 (* preleva 1 byte da 0000 0000 0000 xxxxb *)
604 | MODE_TNY e ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
605 (λb.Some ? (tripleT ??? s b cur_pc))
606 (* preleva 1 byte da 0000 0000 000x xxxxb *)
607 | MODE_SRT e ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉)
608 (λb.Some ? (tripleT ??? s b cur_pc))
610 (* lettura di una word *)
611 | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
612 (* NO: non ci sono indicazioni *)
614 (* NO: solo lettura/scrittura byte *)
616 (* NO: solo lettura/scrittura byte *)
618 (* NO: solo lettura/scrittura byte *)
621 (* NO: solo lettura byte *)
623 (* preleva 1 word immediato *)
624 | MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
625 (* preleva 1 word da indirizzo diretto 1 byte *)
626 | MODE_DIR1 ⇒ mode_DIR1_load false m t s cur_pc
627 (* preleva 1 word da indirizzo diretto 1 word *)
628 | MODE_DIR2 ⇒ mode_DIR2_load false m t s cur_pc
629 (* preleva 1 word da H:X *)
630 | MODE_IX0 ⇒ mode_IX0_load false m t s cur_pc
631 (* preleva 1 word da H:X+1 byte offset *)
632 | MODE_IX1 ⇒ mode_IX1_load false m t s cur_pc
633 (* preleva 1 word da H:X+1 word offset *)
634 | MODE_IX2 ⇒ mode_IX2_load false m t s cur_pc
635 (* preleva 1 word da SP+1 byte offset *)
636 | MODE_SP1 ⇒ mode_SP1_load false m t s cur_pc
637 (* preleva 1 word da SP+1 word offset *)
638 | MODE_SP2 ⇒ mode_SP2_load false m t s cur_pc
640 (* NO: solo lettura/scrittura byte *)
641 | MODE_DIR1_to_DIR1 ⇒ None ?
642 (* NO: solo lettura/scrittura byte *)
643 | MODE_IMM1_to_DIR1 ⇒ None ?
644 (* NO: solo lettura/scrittura byte *)
645 | MODE_IX0p_to_DIR1 ⇒ None ?
646 (* NO: solo lettura/scrittura byte *)
647 | MODE_DIR1_to_IX0p ⇒ None ?
649 (* preleva 2 byte, possibilita' modificare Io argomento *)
650 | MODE_INHA_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
651 (λS_immb_and_PC.match S_immb_and_PC with
652 [ tripleT _ immb cur_pc' ⇒
653 Some ? (tripleT ??? s 〈(get_acc_8_low_reg m t s):immb〉 cur_pc')])
654 (* preleva 2 byte, possibilita' modificare Io argomento *)
655 | MODE_INHX_and_IMM1 ⇒ opt_map ?? (get_indX_8_low_reg m t s)
656 (λX_op.opt_map ?? (mode_IMM1_load m t s cur_pc)
657 (λS_immb_and_PC.match S_immb_and_PC with
658 [ tripleT _ immb cur_pc' ⇒
659 Some ? (tripleT ??? s 〈X_op:immb〉 cur_pc')]))
660 (* preleva 2 byte, NO possibilita' modificare Io argomento *)
661 | MODE_IMM1_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
662 (λS_immb1_and_PC.match S_immb1_and_PC with
663 [ tripleT _ immb1 cur_pc' ⇒
664 opt_map ?? (mode_IMM1_load m t s cur_pc')
665 (λS_immb2_and_PC.match S_immb2_and_PC with
666 [ tripleT _ immb2 cur_pc'' ⇒
667 Some ? (tripleT ??? s 〈immb1:immb2〉 cur_pc'')])])
668 (* preleva 2 byte, possibilita' modificare Io argomento *)
669 | MODE_DIR1_and_IMM1 ⇒ opt_map ?? (mode_DIR1_load true m t s cur_pc)
670 (λS_dirb_and_PC.match S_dirb_and_PC with
671 [ tripleT _ dirb cur_pc' ⇒
672 opt_map ?? (mode_IMM1_load m t s cur_pc')
673 (λS_immb_and_PC.match S_immb_and_PC with
674 [ tripleT _ immb cur_pc'' ⇒
675 Some ? (tripleT ??? s 〈dirb:immb〉 cur_pc'')])])
676 (* preleva 2 byte, possibilita' modificare Io argomento *)
677 | MODE_IX0_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
678 (λS_ixb_and_PC.match S_ixb_and_PC with
679 [ tripleT _ ixb cur_pc' ⇒
680 opt_map ?? (mode_IMM1_load m t s cur_pc')
681 (λS_immb_and_PC.match S_immb_and_PC with
682 [ tripleT _ immb cur_pc'' ⇒
683 Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
684 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
685 | MODE_IX0p_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
686 (λS_ixb_and_PC.match S_ixb_and_PC with
687 [ tripleT _ ixb cur_pc' ⇒
688 opt_map ?? (mode_IMM1_load m t s cur_pc')
689 (λS_immb_and_PC.match S_immb_and_PC with
690 [ tripleT _ immb cur_pc'' ⇒
692 opt_map ?? (aux_inc_indX_16 m t s)
693 (λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
694 (* preleva 2 byte, possibilita' modificare Io argomento *)
695 | MODE_IX1_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
696 (λS_ixb_and_PC.match S_ixb_and_PC with
697 [ tripleT _ ixb cur_pc' ⇒
698 opt_map ?? (mode_IMM1_load m t s cur_pc')
699 (λS_immb_and_PC.match S_immb_and_PC with
700 [ tripleT _ immb cur_pc'' ⇒
701 Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
702 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
703 | MODE_IX1p_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
704 (λS_ixb_and_PC.match S_ixb_and_PC with
705 [ tripleT _ ixb cur_pc' ⇒
706 opt_map ?? (mode_IMM1_load m t s cur_pc')
707 (λS_immb_and_PC.match S_immb_and_PC with
708 [ tripleT _ immb cur_pc'' ⇒
710 opt_map ?? (aux_inc_indX_16 m t s)
711 (λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
712 (* preleva 2 byte, possibilita' modificare Io argomento *)
713 | MODE_SP1_and_IMM1 ⇒ opt_map ?? (mode_SP1_load true m t s cur_pc)
714 (λS_spb_and_PC.match S_spb_and_PC with
715 [ tripleT _ spb cur_pc' ⇒
716 opt_map ?? (mode_IMM1_load m t s cur_pc')
717 (λS_immb_and_PC.match S_immb_and_PC with
718 [ tripleT _ immb cur_pc'' ⇒
719 Some ? (tripleT ??? s 〈spb:immb〉 cur_pc'')])])
721 (* NO: solo scrittura byte *)
722 | MODE_DIRn _ ⇒ None ?
723 (* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
724 | MODE_DIRn_and_IMM1 msk ⇒ opt_map ?? (mode_DIR1n_load m t s cur_pc msk)
725 (λS_dirbn_and_PC.match S_dirbn_and_PC with
726 [ tripleT _ dirbn cur_pc' ⇒
727 opt_map ?? (mode_IMM1_load m t s cur_pc')
728 (λS_immb_and_PC.match S_immb_and_PC with
729 [ tripleT _ immb cur_pc'' ⇒
730 Some ? (tripleT ??? s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
731 (* NO: solo lettura/scrittura byte *)
732 | MODE_TNY _ ⇒ None ?
733 (* NO: solo lettura/scrittura byte *)
734 | MODE_SRT _ ⇒ None ?
738 (* **************************************** *)
739 (* raccordo di tutte le possibili scritture *)
740 (* **************************************** *)
742 (* tutte le modalita' di scrittura: true=writeb, false=writew *)
743 definition multi_mode_write ≝
744 λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
745 return λbyteflag:bool.any_status m t → word16 → instr_mode →
746 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
747 option (Prod (any_status m t) word16) with
748 (* scrittura di un byte *)
749 [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwriteb:byte8.match i with
750 (* NO: non ci sono indicazioni *)
753 | MODE_INHA ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
755 | MODE_INHX ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
756 (λtmps.Some ? (pair ?? tmps cur_pc))
758 | MODE_INHH ⇒ opt_map ?? (set_indX_8_high_reg m t s writeb)
759 (λtmps.Some ? (pair ?? tmps cur_pc))
761 (* NO: solo lettura byte *)
763 (* NO: solo lettura word *)
765 (* scrive 1 byte su indirizzo diretto 1 byte *)
766 | MODE_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
767 (* scrive 1 byte su indirizzo diretto 1 word *)
768 | MODE_DIR2 ⇒ mode_DIR2_write true m t s cur_pc writeb
769 (* scrive 1 byte su H:X *)
770 | MODE_IX0 ⇒ mode_IX0_write true m t s cur_pc writeb
771 (* scrive 1 byte su H:X+1 byte offset *)
772 | MODE_IX1 ⇒ mode_IX1_write true m t s cur_pc writeb
773 (* scrive 1 byte su H:X+1 word offset *)
774 | MODE_IX2 ⇒ mode_IX2_write true m t s cur_pc writeb
775 (* scrive 1 byte su SP+1 byte offset *)
776 | MODE_SP1 ⇒ mode_SP1_write true m t s cur_pc writeb
777 (* scrive 1 byte su SP+1 word offset *)
778 | MODE_SP2 ⇒ mode_SP2_write true m t s cur_pc writeb
780 (* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
781 | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
782 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
783 | MODE_IMM1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
784 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
785 | MODE_IX0p_to_DIR1 ⇒ opt_map ?? (mode_DIR1_write true m t s cur_pc writeb)
786 (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
788 opt_map ?? (aux_inc_indX_16 m t S_op)
789 (λS_op'.Some ? (pair ?? S_op' PC_op))])
790 (* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
791 | MODE_DIR1_to_IX0p ⇒ opt_map ?? (mode_IX0_write true m t s cur_pc writeb)
792 (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
794 opt_map ?? (aux_inc_indX_16 m t S_op)
795 (λS_op'.Some ? (pair ?? S_op' PC_op))])
797 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
798 | MODE_INHA_and_IMM1 ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
799 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)
800 | MODE_INHX_and_IMM1 ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
801 (λtmps.Some ? (pair ?? tmps cur_pc))
802 (* NO: solo lettura word *)
803 | MODE_IMM1_and_IMM1 ⇒ None ?
804 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
805 | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write true m t s cur_pc writeb
806 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
807 | MODE_IX0_and_IMM1 ⇒ mode_IX0_write true m t s cur_pc writeb
808 (* NO: solo lettura word *)
809 | MODE_IX0p_and_IMM1 ⇒ None ?
810 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
811 | MODE_IX1_and_IMM1 ⇒ mode_IX1_write true m t s cur_pc writeb
812 (* NO: solo lettura word *)
813 | MODE_IX1p_and_IMM1 ⇒ None ?
814 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
815 | MODE_SP1_and_IMM1 ⇒ mode_SP1_write true m t s cur_pc writeb
817 (* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
818 | MODE_DIRn msk ⇒ mode_DIR1n_write m t s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))
819 (* NO: solo lettura word *)
820 | MODE_DIRn_and_IMM1 _ ⇒ None ?
821 (* scrive 1 byte su 0000 0000 0000 xxxxb *)
822 | MODE_TNY e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
823 (λtmps.Some ? (pair ?? tmps cur_pc))
824 (* scrive 1 byte su 0000 0000 000x xxxxb *)
825 | MODE_SRT e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉 writeb)
826 (λtmps.Some ? (pair ?? tmps cur_pc)) ]
827 (* scrittura di una word *)
828 | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwritew:word16.match i with
829 (* NO: non ci sono indicazioni *)
831 (* NO: solo lettura/scrittura byte *)
833 (* NO: solo lettura/scrittura byte *)
835 (* NO: solo lettura/scrittura byte *)
838 (* NO: solo lettura byte *)
840 (* NO: solo lettura word *)
842 (* scrive 1 word su indirizzo diretto 1 byte *)
843 | MODE_DIR1 ⇒ mode_DIR1_write false m t s cur_pc writew
844 (* scrive 1 word su indirizzo diretto 1 word *)
845 | MODE_DIR2 ⇒ mode_DIR2_write false m t s cur_pc writew
846 (* scrive 1 word su H:X *)
847 | MODE_IX0 ⇒ mode_IX0_write false m t s cur_pc writew
848 (* scrive 1 word su H:X+1 byte offset *)
849 | MODE_IX1 ⇒ mode_IX1_write false m t s cur_pc writew
850 (* scrive 1 word su H:X+1 word offset *)
851 | MODE_IX2 ⇒ mode_IX2_write false m t s cur_pc writew
852 (* scrive 1 word su SP+1 byte offset *)
853 | MODE_SP1 ⇒ mode_SP1_write false m t s cur_pc writew
854 (* scrive 1 word su SP+1 word offset *)
855 | MODE_SP2 ⇒ mode_SP2_write false m t s cur_pc writew
857 (* NO: solo lettura/scrittura byte *)
858 | MODE_DIR1_to_DIR1 ⇒ None ?
859 (* NO: solo lettura/scrittura byte *)
860 | MODE_IMM1_to_DIR1 ⇒ None ?
861 (* NO: solo lettura/scrittura byte *)
862 | MODE_IX0p_to_DIR1 ⇒ None ?
863 (* NO: solo lettura/scrittura byte *)
864 | MODE_DIR1_to_IX0p ⇒ None ?
866 (* NO: solo lettura word/scrittura byte *)
867 | MODE_INHA_and_IMM1 ⇒ None ?
868 (* NO: solo lettura word/scrittura byte *)
869 | MODE_INHX_and_IMM1 ⇒ None ?
870 (* NO: solo lettura word *)
871 | MODE_IMM1_and_IMM1 ⇒ None ?
872 (* NO: solo lettura word/scrittura byte *)
873 | MODE_DIR1_and_IMM1 ⇒ None ?
874 (* NO: solo lettura word/scrittura byte *)
875 | MODE_IX0_and_IMM1 ⇒ None ?
876 (* NO: solo lettura word *)
877 | MODE_IX0p_and_IMM1 ⇒ None ?
878 (* NO: solo lettura word/scrittura byte *)
879 | MODE_IX1_and_IMM1 ⇒ None ?
880 (* NO: solo lettura word *)
881 | MODE_IX1p_and_IMM1 ⇒ None ?
882 (* NO: solo lettura word/scrittura byte *)
883 | MODE_SP1_and_IMM1 ⇒ None ?
885 (* NO: solo scrittura byte *)
886 | MODE_DIRn _ ⇒ None ?
887 (* NO: solo lettura word *)
888 | MODE_DIRn_and_IMM1 _ ⇒ None ?
889 (* NO: solo lettura/scrittura byte *)
890 | MODE_TNY _ ⇒ None ?
891 (* NO: solo lettura/scrittura byte *)
892 | MODE_SRT _ ⇒ None ?