1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/model.ma".
24 include "freescale/translation.ma".
26 (* errori possibili nel fetch *)
27 ninductive error_type : Type ≝
29 | ILL_FETCH_AD: error_type
30 | ILL_EX_AD: error_type.
32 (* un tipo opzione ad hoc
33 - errore: interessa solo l'errore
34 - ok: interessa info e il nuovo pc
36 ninductive fetch_result (A:Type) : Type ≝
37 FetchERR : error_type → fetch_result A
38 | FetchOK : A → word16 → fetch_result A.
40 (* **************************** *)
41 (* FETCH E ACCESSO ALLA MEMORIA *)
42 (* **************************** *)
44 (* ausialiaria per RS08 read *)
45 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
46 memory mapped, quindi bisona intercettare la lettura.
47 NB: fare molta attenzione alle note sulle combinazioni possibili perche'
48 il comportamento della memoria nell'RS08 e' strano e ci sono
49 precise condizioni che impediscono una semantica circolare dell'accesso
50 (divergenza=assenza di definizione) *)
51 ndefinition RS08_memory_filter_read_aux ≝
52 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
53 λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option T.
55 [ mk_any_status alu mem chk _ ⇒ match alu with
56 [ mk_alu_RS08 _ _ _ _ xm psm _ _ ⇒
58 possibili accessi al registro X
60 2) addr=000E (X =0F): indiretto
61 3) addr=00CF (PS=00): paging
63 [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
64 non si possono combinare due effetti contemporaneamente!
65 per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni
67 match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
68 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
69 (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
73 possibili accessi al registro PS
75 2) addr=000E (X =1F): indiretto
76 3) addr=00DF (PS=00): paging
78 match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
79 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
80 (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
84 accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
85 altrimenti sarebbero 2 indirezioni
87 match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
88 [ true ⇒ fMEM mem chk 〈〈x0,x0〉:xm〉
91 accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
93 match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
94 [ true ⇒ fMEM mem chk (or_w16 (fst … (shr_w16 (fst … (shr_w16 〈psm:〈x0,x0〉〉))))
95 (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉))
99 | false ⇒ fMEM mem chk addr ]]]]]].
101 (* lettura RS08 di un byte *)
102 ndefinition RS08_memory_filter_read ≝
103 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
104 RS08_memory_filter_read_aux t s addr byte8
106 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read t m c a).
108 (* lettura RS08 di un bit *)
109 ndefinition RS08_memory_filter_read_bit ≝
110 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.
111 RS08_memory_filter_read_aux t s addr bool
112 (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
113 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read_bit t m c a sub).
115 (* in caso di RS08 si dirotta sul filtro, altrimenti si legge direttamente *)
116 ndefinition memory_filter_read ≝
117 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → option byte8 with
118 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.
119 mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
120 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.
121 mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
122 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.
123 mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
124 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.
125 RS08_memory_filter_read t s addr
128 ndefinition memory_filter_read_bit ≝
129 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → oct → option bool with
130 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.
131 mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
132 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.
133 mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
134 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.
135 mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
136 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.
137 RS08_memory_filter_read_bit t s addr sub
140 (* ausialiaria per RS08 write *)
141 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
142 memory mapped, quindi bisona intercettare la scrittura.
143 NB: fare molta attenzione alle note sulle combinazioni possibili perche'
144 il comportamento della memoria nell'RS08 e' strano e ci sono
145 precise condizioni che impediscono una semantica circolare dell'accesso
146 (divergenza=assenza di definizione) *)
147 ndefinition RS08_memory_filter_write_aux ≝
148 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
149 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option (aux_mem_type t).
151 [ mk_any_status alu mem chk clk ⇒ match alu with
152 [ mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl ⇒
154 possibili accessi al registro X
155 1) addr=000F: diretto
156 2) addr=000E (X =0F): indiretto
157 3) addr=00CF (PS=00): paging
159 [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
160 non si possono combinare due effetti contemporaneamente!
161 per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni
163 match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
164 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
165 (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
166 [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc (fREG xm) psm zfl cfl) mem chk clk)
169 possibili accessi al registro PS
170 1) addr=001F: diretto
171 2) addr=000E (X =1F): indiretto
172 3) addr=00DF (PS=00): paging
174 match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
175 (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
176 (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
177 [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm (fREG psm) zfl cfl) mem chk clk)
180 accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
181 altrimenti sarebbero 2 indirezioni
183 match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
184 [ true ⇒ opt_map … (fMEM mem chk 〈〈x0,x0〉:xm〉)
185 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
189 accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
191 match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
192 [ true ⇒ opt_map … (fMEM mem chk (or_w16 (fst … (shr_w16 (fst … (shr_w16 〈psm:〈x0,x0〉〉))))
193 (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉)))
194 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
198 | false ⇒ opt_map … (fMEM mem chk addr)
199 (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk)) ]]]]]].
201 (* scrittura RS08 di un byte *)
202 ndefinition RS08_memory_filter_write ≝
203 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λval:byte8.
204 RS08_memory_filter_write_aux t s addr
206 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update t m c a val).
208 (* scrittura RS08 di un bit *)
209 ndefinition RS08_memory_filter_write_bit ≝
210 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
211 RS08_memory_filter_write_aux t s addr
212 (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
213 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update_bit t m c a sub val).
215 (* in caso di RS08 si dirotta sul filtro, altrimenti si scrive direttamente *)
216 ndefinition memory_filter_write ≝
217 λm:mcu_type.λt:memory_impl.match m
218 return λm:mcu_type.any_status m t → word16 → byte8 → option (any_status m t) with
219 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λval:byte8.
220 opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
221 (λmem.Some ? (set_mem_desc ? t s mem))
222 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λval:byte8.
223 opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
224 (λmem.Some ? (set_mem_desc ? t s mem))
225 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λval:byte8.
226 opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
227 (λmem.Some ? (set_mem_desc ? t s mem))
228 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λval:byte8.
229 RS08_memory_filter_write t s addr val
232 ndefinition memory_filter_write_bit ≝
233 λm:mcu_type.λt:memory_impl.match m
234 return λm:mcu_type.any_status m t → word16 → oct → bool → option (any_status m t) with
235 [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.λval:bool.
236 opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
237 (λmem.Some ? (set_mem_desc ? t s mem))
238 | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.λval:bool.
239 opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
240 (λmem.Some ? (set_mem_desc ? t s mem))
241 | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.λval:bool.
242 opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
243 (λmem.Some ? (set_mem_desc ? t s mem))
244 | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
245 RS08_memory_filter_write_bit t s addr sub val
249 Da utilizzarsi solo per gli aggiornamenti di PC (per il fetch),
250 NON per il caricamento degli indiretti.
251 - il caricamento degli immediati spetta al fetcher
252 (incremento progressivo di PC ciclo per ciclo, e riempimento del prefetch
253 che a questo punto DEVE poter indirizzare qualsiasi locazione puntata da PC)
254 - il caricamento degli indiretti non spetta al fetcher
256 ndefinition filtered_inc_w16 ≝
257 λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
258 get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
260 nlet rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
263 | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
266 errore1: non esiste traduzione ILL_OP
267 errore2: non e' riuscito a leggere ILL_FETCH_AD
268 altrimenti OK=info+new_pc
271 λm:mcu_type.λt:memory_impl.λs:any_status m t.
272 let pc ≝ get_pc_reg m t s in
273 let pc_next1 ≝ filtered_inc_w16 m t s pc in
274 let pc_next2 ≝ filtered_inc_w16 m t s pc_next1 in
275 match memory_filter_read m t s pc with
276 [ None ⇒ FetchERR ? ILL_FETCH_AD
277 | Some bh ⇒ match full_info_of_word16 m (Byte bh) with
278 (* non ha trovato una traduzione con 1 byte *)
279 [ None ⇒ match m with
280 (* HC05 non esistono op a 2 byte *)
281 [ HC05 ⇒ FetchERR ? ILL_OP
282 | HC08 ⇒ match eq_b8 bh 〈x9,xE〉 with
283 (* HC08 se il primo byte e' 0x9E il secondo puo' avere senso *)
284 [ true ⇒ match memory_filter_read m t s pc_next1 with
285 [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
286 [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
287 (* HC08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
288 | false ⇒ FetchERR ? ILL_OP
290 | HCS08 ⇒ match eq_b8 bh 〈x9,xE〉 with
291 (* HCS08 se il primo byte e' 0x9E il secondo puo' avere senso *)
292 [ true ⇒ match memory_filter_read m t s pc_next1 with
293 [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
294 [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
295 (* HCS08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
296 | false ⇒ FetchERR ? ILL_OP
298 (* RS08 non esistono op a 2 byte *)
299 | RS08 ⇒ FetchERR ? ILL_OP
301 (* ha trovato una traduzione con 1 byte *)
302 | Some info ⇒ FetchOK ? info pc_next1 ]].
304 (* ************************ *)
305 (* MODALITA' INDIRIZZAMENTO *)
306 (* ************************ *)
309 (* - incrementano l'indirizzo normalmente *)
310 (* - incrementano PC attraverso il filtro *)
312 (* lettura byte da addr *)
313 ndefinition loadb_from ≝
314 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
315 opt_map … (memory_filter_read m t s addr)
316 (λb.Some ? (triple … s b (filtered_plus_w16 m t s cur_pc fetched))).
318 (* lettura bit da addr *)
319 ndefinition loadbit_from ≝
320 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.
321 opt_map … (memory_filter_read_bit m t s addr sub)
322 (λb.Some ? (triple … s b (filtered_plus_w16 m t s cur_pc fetched))).
324 (* lettura word da addr *)
325 ndefinition loadw_from ≝
326 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
327 opt_map … (memory_filter_read m t s addr)
328 (λbh.opt_map … (memory_filter_read m t s (succ_w16 addr))
329 (λbl.Some ? (triple … s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc fetched)))).
331 (* scrittura byte su addr *)
332 ndefinition writeb_to ≝
333 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwriteb:byte8.
334 opt_map … (memory_filter_write m t s addr writeb)
335 (λtmps.Some ? (pair … tmps (filtered_plus_w16 m t s cur_pc fetched))).
337 (* scrittura bit su addr *)
338 ndefinition writebit_to ≝
339 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.λwriteb:bool.
340 opt_map … (memory_filter_write_bit m t s addr sub writeb)
341 (λtmps.Some ? (pair … tmps (filtered_plus_w16 m t s cur_pc fetched))).
343 (* scrittura word su addr *)
344 ndefinition writew_to ≝
345 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
346 opt_map … (memory_filter_write m t s addr (w16h writew))
347 (λtmps1.opt_map … (memory_filter_write m t tmps1 (succ_w16 addr) (w16l writew))
348 (λtmps2.Some ? (pair … tmps2 (filtered_plus_w16 m t tmps2 cur_pc fetched)))).
350 (* ausiliari per definire i tipi e la lettura/scrittura *)
352 (* ausiliaria per definire il tipo di aux_load *)
353 ndefinition aux_load_typing ≝
354 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
355 any_status m t → word16 → word16 → nat →
356 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
358 (* per non dover ramificare i vari load in byte/word *)
359 ndefinition aux_load ≝
360 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
361 [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
363 (* ausiliaria per definire il tipo di aux_write *)
364 ndefinition aux_write_typing ≝
365 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
366 any_status m t → word16 → word16 → nat →
367 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
368 option (ProdT (any_status m t) word16).
370 (* per non dover ramificare i vari load in byte/word *)
371 ndefinition aux_write ≝
372 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
373 [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
375 (* modalita' vere e proprie *)
377 (* lettura da [curpc]: IMM1 comportamento asimmetrico, quindi non si appoggia a loadb *)
378 ndefinition mode_IMM1_load ≝
379 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
380 opt_map … (memory_filter_read m t s cur_pc)
381 (λb.Some ? (triple … s b (filtered_inc_w16 m t s cur_pc))).
383 (* lettura da [curpc]: IMM1 + estensione a word *)
384 ndefinition mode_IMM1EXT_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 ? (triple … s 〈〈x0,x0〉:b〉 (filtered_inc_w16 m t s cur_pc))).
389 (* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
390 ndefinition 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 ? (triple … 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 ndefinition 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 ndefinition 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 ndefinition 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 ndefinition 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 ndefinition 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 ndefinition 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 ndefinition 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 ndefinition 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 ndefinition 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_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
464 (* lettura da X+[byte curpc] *)
465 ndefinition mode_IX1ADD_load ≝
466 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
467 opt_map … (memory_filter_read m t s cur_pc)
468 (λb.opt_map … (get_IX m t s)
469 (λaddr.Some ? (triple … s (plus_w16_d_d addr 〈〈x0,x0〉:b〉) (filtered_inc_w16 m t s cur_pc)))).
471 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
472 ndefinition mode_IX1_write ≝
473 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
474 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
475 opt_map … (get_IX m t s)
476 (λaddr.opt_map … (memory_filter_read m t s cur_pc)
477 (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
479 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
480 ndefinition mode_IX2_load ≝
481 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
482 opt_map … (get_IX m t s)
483 (λaddr.opt_map … (memory_filter_read m t s cur_pc)
484 (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
485 (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
487 (* lettura da X+[word curpc] *)
488 ndefinition mode_IX2ADD_load ≝
489 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
490 opt_map … (memory_filter_read m t s cur_pc)
491 (λbh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
492 (λbl.opt_map … (get_IX m t s)
493 (λaddr.Some ? (triple … s (plus_w16_d_d addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
495 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
496 ndefinition mode_IX2_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_IX m t s)
500 (λaddr.opt_map … (memory_filter_read m t s cur_pc)
501 (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
502 (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
504 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
505 ndefinition mode_SP1_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 (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
511 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
512 ndefinition mode_SP1_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 (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
519 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
520 ndefinition mode_SP2_load ≝
521 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
522 opt_map … (get_sp_reg m t s)
523 (λaddr.opt_map … (memory_filter_read m t s cur_pc)
524 (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
525 (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
527 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
528 ndefinition mode_SP2_write ≝
529 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
530 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
531 opt_map … (get_sp_reg m t s)
532 (λaddr.opt_map … (memory_filter_read m t s cur_pc)
533 (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
534 (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
536 (* ************************************** *)
537 (* raccordo di tutte le possibili letture *)
538 (* ************************************** *)
541 ndefinition aux_inc_indX_16 ≝
542 λm:mcu_type.λt:memory_impl.λs:any_status m t.
543 opt_map … (get_indX_16_reg m t s)
544 (λX_op.opt_map … (set_indX_16_reg m t s (succ_w16 X_op))
545 (λs_tmp.Some ? s_tmp)).
547 (* tutte le modalita' di lettura: false=loadb true=loadw *)
548 ndefinition multi_mode_load ≝
549 λbyteflag:bool.λm:mcu_type.λt:memory_impl.
551 return λbyteflag:bool.any_status m t → word16 → instr_mode →
552 option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
554 (* lettura di un byte *)
555 [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
556 (* NO: non ci sono indicazioni *)
559 | MODE_INHA ⇒ Some ? (triple … s (get_acc_8_low_reg m t s) cur_pc)
561 | MODE_INHX ⇒ opt_map … (get_indX_8_low_reg m t s)
562 (λindx.Some ? (triple … s indx cur_pc))
564 | MODE_INHH ⇒ opt_map … (get_indX_8_high_reg m t s)
565 (λindx.Some ? (triple … s indx cur_pc))
567 (* NO: solo lettura word *)
568 | MODE_INHX0ADD ⇒ None ?
569 (* NO: solo lettura word *)
570 | MODE_INHX1ADD ⇒ None ?
571 (* NO: solo lettura word *)
572 | MODE_INHX2ADD ⇒ None ?
574 (* preleva 1 byte immediato *)
575 | MODE_IMM1 ⇒ mode_IMM1_load m t s cur_pc
576 (* NO: solo lettura word *)
577 | MODE_IMM1EXT ⇒ None ?
578 (* NO: solo lettura word *)
580 (* preleva 1 byte da indirizzo diretto 1 byte *)
581 | MODE_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
582 (* preleva 1 byte da indirizzo diretto 1 word *)
583 | MODE_DIR2 ⇒ mode_DIR2_load true m t s cur_pc
584 (* preleva 1 byte da H:X *)
585 | MODE_IX0 ⇒ mode_IX0_load true m t s cur_pc
586 (* preleva 1 byte da H:X+1 byte offset *)
587 | MODE_IX1 ⇒ mode_IX1_load true m t s cur_pc
588 (* preleva 1 byte da H:X+1 word offset *)
589 | MODE_IX2 ⇒ mode_IX2_load true m t s cur_pc
590 (* preleva 1 byte da SP+1 byte offset *)
591 | MODE_SP1 ⇒ mode_SP1_load true m t s cur_pc
592 (* preleva 1 byte da SP+1 word offset *)
593 | MODE_SP2 ⇒ mode_SP2_load true m t s cur_pc
595 (* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
596 | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
597 (* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
598 | MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load m t s cur_pc
599 (* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
600 | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true m t s cur_pc
601 (* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
602 | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true m t s cur_pc
604 (* NO: solo lettura word/scrittura byte *)
605 | MODE_INHA_and_IMM1 ⇒ None ?
606 (* NO: solo lettura word/scrittura byte *)
607 | MODE_INHX_and_IMM1 ⇒ None ?
608 (* NO: solo lettura word *)
609 | MODE_IMM1_and_IMM1 ⇒ None ?
610 (* NO: solo lettura word/scrittura byte *)
611 | MODE_DIR1_and_IMM1 ⇒ None ?
612 (* NO: solo lettura word/scrittura byte *)
613 | MODE_IX0_and_IMM1 ⇒ None ?
614 (* NO: solo lettura word *)
615 | MODE_IX0p_and_IMM1 ⇒ None ?
616 (* NO: solo lettura word/scrittura byte *)
617 | MODE_IX1_and_IMM1 ⇒ None ?
618 (* NO: solo lettura word *)
619 | MODE_IX1p_and_IMM1 ⇒ None ?
620 (* NO: solo lettura word/scrittura byte *)
621 | MODE_SP1_and_IMM1 ⇒ None ?
623 (* NO: solo scrittura byte *)
624 | MODE_DIRn _ ⇒ None ?
625 (* NO: solo lettura word *)
626 | MODE_DIRn_and_IMM1 _ ⇒ None ?
627 (* preleva 1 byte da 0000 0000 0000 xxxxb *)
628 | MODE_TNY e ⇒ opt_map … (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
629 (λb.Some ? (triple … s b cur_pc))
630 (* preleva 1 byte da 0000 0000 000x xxxxb *)
631 | MODE_SRT e ⇒ opt_map … (memory_filter_read m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉)
632 (λb.Some ? (triple … s b cur_pc))
634 (* lettura di una word *)
635 | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
636 (* NO: non ci sono indicazioni *)
638 (* NO: solo lettura/scrittura byte *)
640 (* NO: solo lettura/scrittura byte *)
642 (* NO: solo lettura/scrittura byte *)
645 (* preleva 1 word immediato *)
646 | MODE_INHX0ADD ⇒ opt_map … (get_IX m t s)
647 (λw.Some ? (triple … s w cur_pc))
648 (* preleva 1 word immediato *)
649 | MODE_INHX1ADD ⇒ mode_IX1ADD_load m t s cur_pc
650 (* preleva 1 word immediato *)
651 | MODE_INHX2ADD ⇒ mode_IX2ADD_load m t s cur_pc
653 (* NO: solo lettura byte *)
655 (* preleva 1 word immediato *)
656 | MODE_IMM1EXT ⇒ mode_IMM1EXT_load m t s cur_pc
657 (* preleva 1 word immediato *)
658 | MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
659 (* preleva 1 word da indirizzo diretto 1 byte *)
660 | MODE_DIR1 ⇒ mode_DIR1_load false m t s cur_pc
661 (* preleva 1 word da indirizzo diretto 1 word *)
662 | MODE_DIR2 ⇒ mode_DIR2_load false m t s cur_pc
663 (* preleva 1 word da H:X *)
664 | MODE_IX0 ⇒ mode_IX0_load false m t s cur_pc
665 (* preleva 1 word da H:X+1 byte offset *)
666 | MODE_IX1 ⇒ mode_IX1_load false m t s cur_pc
667 (* preleva 1 word da H:X+1 word offset *)
668 | MODE_IX2 ⇒ mode_IX2_load false m t s cur_pc
669 (* preleva 1 word da SP+1 byte offset *)
670 | MODE_SP1 ⇒ mode_SP1_load false m t s cur_pc
671 (* preleva 1 word da SP+1 word offset *)
672 | MODE_SP2 ⇒ mode_SP2_load false m t s cur_pc
674 (* NO: solo lettura/scrittura byte *)
675 | MODE_DIR1_to_DIR1 ⇒ None ?
676 (* NO: solo lettura/scrittura byte *)
677 | MODE_IMM1_to_DIR1 ⇒ None ?
678 (* NO: solo lettura/scrittura byte *)
679 | MODE_IX0p_to_DIR1 ⇒ None ?
680 (* NO: solo lettura/scrittura byte *)
681 | MODE_DIR1_to_IX0p ⇒ None ?
683 (* preleva 2 byte, possibilita' modificare Io argomento *)
684 | MODE_INHA_and_IMM1 ⇒ opt_map … (mode_IMM1_load m t s cur_pc)
685 (λS_immb_and_PC.match S_immb_and_PC with
686 [ triple _ immb cur_pc' ⇒
687 Some ? (triple … s 〈(get_acc_8_low_reg m t s):immb〉 cur_pc')])
688 (* preleva 2 byte, possibilita' modificare Io argomento *)
689 | MODE_INHX_and_IMM1 ⇒ opt_map … (get_indX_8_low_reg m t s)
690 (λX_op.opt_map … (mode_IMM1_load m t s cur_pc)
691 (λS_immb_and_PC.match S_immb_and_PC with
692 [ triple _ immb cur_pc' ⇒
693 Some ? (triple … s 〈X_op:immb〉 cur_pc')]))
694 (* preleva 2 byte, NO possibilita' modificare Io argomento *)
695 | MODE_IMM1_and_IMM1 ⇒ opt_map … (mode_IMM1_load m t s cur_pc)
696 (λS_immb1_and_PC.match S_immb1_and_PC with
697 [ triple _ immb1 cur_pc' ⇒
698 opt_map … (mode_IMM1_load m t s cur_pc')
699 (λS_immb2_and_PC.match S_immb2_and_PC with
700 [ triple _ immb2 cur_pc'' ⇒
701 Some ? (triple … s 〈immb1:immb2〉 cur_pc'')])])
702 (* preleva 2 byte, possibilita' modificare Io argomento *)
703 | MODE_DIR1_and_IMM1 ⇒ opt_map … (mode_DIR1_load true m t s cur_pc)
704 (λS_dirb_and_PC.match S_dirb_and_PC with
705 [ triple _ dirb 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 [ triple _ immb cur_pc'' ⇒
709 Some ? (triple … s 〈dirb:immb〉 cur_pc'')])])
710 (* preleva 2 byte, possibilita' modificare Io argomento *)
711 | MODE_IX0_and_IMM1 ⇒ opt_map … (mode_IX0_load true m t s cur_pc)
712 (λS_ixb_and_PC.match S_ixb_and_PC with
713 [ triple _ ixb cur_pc' ⇒
714 opt_map … (mode_IMM1_load m t s cur_pc')
715 (λS_immb_and_PC.match S_immb_and_PC with
716 [ triple _ immb cur_pc'' ⇒
717 Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
718 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
719 | MODE_IX0p_and_IMM1 ⇒ opt_map … (mode_IX0_load true m t s cur_pc)
720 (λS_ixb_and_PC.match S_ixb_and_PC with
721 [ triple _ ixb cur_pc' ⇒
722 opt_map … (mode_IMM1_load m t s cur_pc')
723 (λS_immb_and_PC.match S_immb_and_PC with
724 [ triple _ immb cur_pc'' ⇒
726 opt_map … (aux_inc_indX_16 m t s)
727 (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
728 (* preleva 2 byte, possibilita' modificare Io argomento *)
729 | MODE_IX1_and_IMM1 ⇒ opt_map … (mode_IX1_load true m t s cur_pc)
730 (λS_ixb_and_PC.match S_ixb_and_PC with
731 [ triple _ ixb cur_pc' ⇒
732 opt_map … (mode_IMM1_load m t s cur_pc')
733 (λS_immb_and_PC.match S_immb_and_PC with
734 [ triple _ immb cur_pc'' ⇒
735 Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
736 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
737 | MODE_IX1p_and_IMM1 ⇒ opt_map … (mode_IX1_load true m t s cur_pc)
738 (λS_ixb_and_PC.match S_ixb_and_PC with
739 [ triple _ ixb cur_pc' ⇒
740 opt_map … (mode_IMM1_load m t s cur_pc')
741 (λS_immb_and_PC.match S_immb_and_PC with
742 [ triple _ immb cur_pc'' ⇒
744 opt_map … (aux_inc_indX_16 m t s)
745 (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
746 (* preleva 2 byte, possibilita' modificare Io argomento *)
747 | MODE_SP1_and_IMM1 ⇒ opt_map … (mode_SP1_load true m t s cur_pc)
748 (λS_spb_and_PC.match S_spb_and_PC with
749 [ triple _ spb cur_pc' ⇒
750 opt_map … (mode_IMM1_load m t s cur_pc')
751 (λS_immb_and_PC.match S_immb_and_PC with
752 [ triple _ immb cur_pc'' ⇒
753 Some ? (triple … s 〈spb:immb〉 cur_pc'')])])
755 (* NO: solo scrittura byte *)
756 | MODE_DIRn _ ⇒ None ?
757 (* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
758 | MODE_DIRn_and_IMM1 msk ⇒ opt_map … (mode_DIR1n_load m t s cur_pc msk)
759 (λS_dirbn_and_PC.match S_dirbn_and_PC with
760 [ triple _ dirbn cur_pc' ⇒
761 opt_map … (mode_IMM1_load m t s cur_pc')
762 (λS_immb_and_PC.match S_immb_and_PC with
763 [ triple _ immb cur_pc'' ⇒
764 Some ? (triple … s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
765 (* NO: solo lettura/scrittura byte *)
766 | MODE_TNY _ ⇒ None ?
767 (* NO: solo lettura/scrittura byte *)
768 | MODE_SRT _ ⇒ None ?
772 (* **************************************** *)
773 (* raccordo di tutte le possibili scritture *)
774 (* **************************************** *)
776 (* tutte le modalita' di scrittura: true=writeb, false=writew *)
777 ndefinition multi_mode_write ≝
778 λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
779 return λbyteflag:bool.any_status m t → word16 → instr_mode →
780 match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
781 option (ProdT (any_status m t) word16) with
782 (* scrittura di un byte *)
783 [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwriteb:byte8.match i with
784 (* NO: non ci sono indicazioni *)
787 | MODE_INHA ⇒ Some ? (pair … (set_acc_8_low_reg m t s writeb) cur_pc)
789 | MODE_INHX ⇒ opt_map … (set_indX_8_low_reg m t s writeb)
790 (λtmps.Some ? (pair … tmps cur_pc))
792 | MODE_INHH ⇒ opt_map … (set_indX_8_high_reg m t s writeb)
793 (λtmps.Some ? (pair … tmps cur_pc))
795 (* NO: solo lettura word *)
796 | MODE_INHX0ADD ⇒ None ?
797 (* NO: solo lettura word *)
798 | MODE_INHX1ADD ⇒ None ?
799 (* NO: solo lettura word *)
800 | MODE_INHX2ADD ⇒ None ?
802 (* NO: solo lettura byte *)
804 (* NO: solo lettura word *)
805 | MODE_IMM1EXT ⇒ None ?
806 (* NO: solo lettura word *)
808 (* scrive 1 byte su indirizzo diretto 1 byte *)
809 | MODE_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
810 (* scrive 1 byte su indirizzo diretto 1 word *)
811 | MODE_DIR2 ⇒ mode_DIR2_write true m t s cur_pc writeb
812 (* scrive 1 byte su H:X *)
813 | MODE_IX0 ⇒ mode_IX0_write true m t s cur_pc writeb
814 (* scrive 1 byte su H:X+1 byte offset *)
815 | MODE_IX1 ⇒ mode_IX1_write true m t s cur_pc writeb
816 (* scrive 1 byte su H:X+1 word offset *)
817 | MODE_IX2 ⇒ mode_IX2_write true m t s cur_pc writeb
818 (* scrive 1 byte su SP+1 byte offset *)
819 | MODE_SP1 ⇒ mode_SP1_write true m t s cur_pc writeb
820 (* scrive 1 byte su SP+1 word offset *)
821 | MODE_SP2 ⇒ mode_SP2_write true m t s cur_pc writeb
823 (* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
824 | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
825 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
826 | MODE_IMM1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
827 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
828 | MODE_IX0p_to_DIR1 ⇒ opt_map … (mode_DIR1_write true m t s cur_pc writeb)
829 (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
831 opt_map … (aux_inc_indX_16 m t S_op)
832 (λS_op'.Some ? (pair … S_op' PC_op))])
833 (* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
834 | MODE_DIR1_to_IX0p ⇒ opt_map … (mode_IX0_write true m t s cur_pc writeb)
835 (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
837 opt_map … (aux_inc_indX_16 m t S_op)
838 (λS_op'.Some ? (pair … S_op' PC_op))])
840 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
841 | MODE_INHA_and_IMM1 ⇒ Some ? (pair … (set_acc_8_low_reg m t s writeb) cur_pc)
842 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)
843 | MODE_INHX_and_IMM1 ⇒ opt_map … (set_indX_8_low_reg m t s writeb)
844 (λtmps.Some ? (pair … tmps cur_pc))
845 (* NO: solo lettura word *)
846 | MODE_IMM1_and_IMM1 ⇒ None ?
847 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
848 | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write true m t s cur_pc writeb
849 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
850 | MODE_IX0_and_IMM1 ⇒ mode_IX0_write true m t s cur_pc writeb
851 (* NO: solo lettura word *)
852 | MODE_IX0p_and_IMM1 ⇒ None ?
853 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
854 | MODE_IX1_and_IMM1 ⇒ mode_IX1_write true m t s cur_pc writeb
855 (* NO: solo lettura word *)
856 | MODE_IX1p_and_IMM1 ⇒ None ?
857 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
858 | MODE_SP1_and_IMM1 ⇒ mode_SP1_write true m t s cur_pc writeb
860 (* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
861 | MODE_DIRn msk ⇒ mode_DIR1n_write m t s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))
862 (* NO: solo lettura word *)
863 | MODE_DIRn_and_IMM1 _ ⇒ None ?
864 (* scrive 1 byte su 0000 0000 0000 xxxxb *)
865 | MODE_TNY e ⇒ opt_map … (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
866 (λtmps.Some ? (pair … tmps cur_pc))
867 (* scrive 1 byte su 0000 0000 000x xxxxb *)
868 | MODE_SRT e ⇒ opt_map … (memory_filter_write m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉 writeb)
869 (λtmps.Some ? (pair … tmps cur_pc)) ]
870 (* scrittura di una word *)
871 | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwritew:word16.match i with
872 (* NO: non ci sono indicazioni *)
874 (* NO: solo lettura/scrittura byte *)
876 (* NO: solo lettura/scrittura byte *)
878 (* NO: solo lettura/scrittura byte *)
881 (* NO: solo lettura word *)
882 | MODE_INHX0ADD ⇒ None ?
883 (* NO: solo lettura word *)
884 | MODE_INHX1ADD ⇒ None ?
885 (* NO: solo lettura word *)
886 | MODE_INHX2ADD ⇒ None ?
888 (* NO: solo lettura byte *)
890 (* NO: solo lettura word *)
891 | MODE_IMM1EXT ⇒ None ?
892 (* NO: solo lettura word *)
894 (* scrive 1 word su indirizzo diretto 1 byte *)
895 | MODE_DIR1 ⇒ mode_DIR1_write false m t s cur_pc writew
896 (* scrive 1 word su indirizzo diretto 1 word *)
897 | MODE_DIR2 ⇒ mode_DIR2_write false m t s cur_pc writew
898 (* scrive 1 word su H:X *)
899 | MODE_IX0 ⇒ mode_IX0_write false m t s cur_pc writew
900 (* scrive 1 word su H:X+1 byte offset *)
901 | MODE_IX1 ⇒ mode_IX1_write false m t s cur_pc writew
902 (* scrive 1 word su H:X+1 word offset *)
903 | MODE_IX2 ⇒ mode_IX2_write false m t s cur_pc writew
904 (* scrive 1 word su SP+1 byte offset *)
905 | MODE_SP1 ⇒ mode_SP1_write false m t s cur_pc writew
906 (* scrive 1 word su SP+1 word offset *)
907 | MODE_SP2 ⇒ mode_SP2_write false m t s cur_pc writew
909 (* NO: solo lettura/scrittura byte *)
910 | MODE_DIR1_to_DIR1 ⇒ None ?
911 (* NO: solo lettura/scrittura byte *)
912 | MODE_IMM1_to_DIR1 ⇒ None ?
913 (* NO: solo lettura/scrittura byte *)
914 | MODE_IX0p_to_DIR1 ⇒ None ?
915 (* NO: solo lettura/scrittura byte *)
916 | MODE_DIR1_to_IX0p ⇒ None ?
918 (* NO: solo lettura word/scrittura byte *)
919 | MODE_INHA_and_IMM1 ⇒ None ?
920 (* NO: solo lettura word/scrittura byte *)
921 | MODE_INHX_and_IMM1 ⇒ None ?
922 (* NO: solo lettura word *)
923 | MODE_IMM1_and_IMM1 ⇒ None ?
924 (* NO: solo lettura word/scrittura byte *)
925 | MODE_DIR1_and_IMM1 ⇒ None ?
926 (* NO: solo lettura word/scrittura byte *)
927 | MODE_IX0_and_IMM1 ⇒ None ?
928 (* NO: solo lettura word *)
929 | MODE_IX0p_and_IMM1 ⇒ None ?
930 (* NO: solo lettura word/scrittura byte *)
931 | MODE_IX1_and_IMM1 ⇒ None ?
932 (* NO: solo lettura word *)
933 | MODE_IX1p_and_IMM1 ⇒ None ?
934 (* NO: solo lettura word/scrittura byte *)
935 | MODE_SP1_and_IMM1 ⇒ None ?
937 (* NO: solo scrittura byte *)
938 | MODE_DIRn _ ⇒ None ?
939 (* NO: solo lettura word *)
940 | MODE_DIRn_and_IMM1 _ ⇒ None ?
941 (* NO: solo lettura/scrittura byte *)
942 | MODE_TNY _ ⇒ None ?
943 (* NO: solo lettura/scrittura byte *)
944 | MODE_SRT _ ⇒ None ?