]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/ng_assembly2/emulator/read_write/Freescale_load_write.ma
mod change (-x)
[helm.git] / matitaB / matita / contribs / ng_assembly2 / emulator / read_write / Freescale_load_write.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "emulator/read_write/load_write_base.ma".
24 include "emulator/status/status_getter.ma".
25
26 (* accesso argomenti immediati solo da segmento 0 [mem_read_s … o0] *)
27 (* accesso indiretto solo da segmento 0 filtrato [aux_load] *)
28
29 ndefinition code_seg ≝ o0.
30
31 (* lettura da [curpc]: IMM1 *)
32 ndefinition mode_IMM1_load ≝
33 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
34  opt_map … (mem_read_s … s code_seg cur_pc)
35   (λb.Some ? (triple … s b (succc ? cur_pc))).
36
37 (* lettura da [curpc]: IMM1 + estensione a word *)
38 ndefinition mode_IMM1EXT_load ≝
39 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
40  opt_map … (mem_read_s …  s code_seg cur_pc)
41   (λb.Some ? (triple … s (extu_w16 b) (succc ? cur_pc))).
42
43 (* lettura da [curpc]: IMM2 *)
44 ndefinition mode_IMM2_load ≝
45 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
46  opt_map … (mem_read_s …  s code_seg cur_pc)
47   (λbh.opt_map … (mem_read_s …  s code_seg (succc ? cur_pc))
48    (λbl.Some ? (triple … s 〈bh:bl〉 (succc ? (succc ? cur_pc))))).
49
50 (* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
51 ndefinition mode_DIR1_load ≝
52 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
53  opt_map … (mem_read_s …  s code_seg cur_pc)
54   (λaddr.(aux_load … byteflag) s (extu_w16 addr) cur_pc x1).
55
56 (* lettura da [byte [curpc]]: loadbit *)
57 ndefinition mode_DIR1n_load ≝
58 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
59  opt_map … (mem_read_s …  s  code_seg cur_pc)
60   (λaddr.loadbit_from … s (extu_w16 addr) sub cur_pc x1).
61
62 (* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
63 ndefinition mode_DIR1_write ≝
64 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
65 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
66  opt_map … (mem_read_s …  s code_seg cur_pc)
67   (λaddr.(aux_write … byteflag) s (extu_w16 addr) auxMode_ok cur_pc x1 writebw).
68
69 (* scrittura su [byte [curpc]]: writebit *)
70 ndefinition mode_DIR1n_write ≝
71 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
72  opt_map … (mem_read_s …  s code_seg cur_pc)
73   (λaddr.writebit_to … s (extu_w16 addr) sub cur_pc x1 writeb).
74
75 (* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
76 ndefinition mode_DIR2_load ≝
77 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
78  opt_map … (mem_read_s …  s code_seg cur_pc)
79   (λaddrh.opt_map … (mem_read_s …  s code_seg (succc ? cur_pc))
80    (λaddrl.(aux_load … byteflag) s 〈addrh:addrl〉 cur_pc x2)).
81
82 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
83 ndefinition mode_DIR2_write ≝
84 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
85 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
86  opt_map … (mem_read_s …  s code_seg cur_pc)
87   (λaddrh.opt_map … (mem_read_s …  s code_seg (succc ? cur_pc))
88    (λaddrl.(aux_write … byteflag) s 〈addrh:addrl〉 auxMode_ok cur_pc x2 writebw)).
89
90 ndefinition get_IX ≝
91 λm:mcu_type.λt:memory_impl.λs:any_status m t.
92  match m with
93   [ HC05 ⇒ opt_map … (get_indX_8_low_reg … s) (λindx.Some ? (extu_w16 indx)) 
94   | HC08 ⇒ opt_map … (get_indX_16_reg … s) (λindx.Some ? indx) 
95   | HCS08 ⇒ opt_map … (get_indX_16_reg … s) (λindx.Some ? indx) 
96   | RS08 ⇒ None ?
97   | IP2022 ⇒ None ? ].
98
99 (* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
100 ndefinition mode_IX0_load ≝
101 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
102  opt_map … (get_IX … s)
103   (λaddr.(aux_load … byteflag) s addr cur_pc x0).
104
105 (* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
106 ndefinition mode_IX0_write ≝
107 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
108 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
109  opt_map … (get_IX … s)
110   (λaddr.(aux_write … byteflag) s addr auxMode_ok cur_pc x0 writebw).
111
112 (* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
113 ndefinition mode_IX1_load ≝
114 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
115  opt_map … (get_IX … s)
116   (λaddr.opt_map … (mem_read_s …  s code_seg cur_pc)
117    (λoffs.(aux_load … byteflag) s (plusc_d_d ? addr (extu_w16 offs)) cur_pc x1)).
118
119 (* lettura da X+[byte curpc] *)
120 ndefinition mode_IX1ADD_load ≝
121 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
122  opt_map … (get_IX … s)
123   (λaddr.opt_map … (mem_read_s …  s code_seg cur_pc)
124    (λb.Some ? (triple … s (plusc_d_d ? addr (extu_w16 b)) (succc ? cur_pc)))).
125
126 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
127 ndefinition mode_IX1_write ≝
128 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
129 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
130  opt_map … (get_IX … s)
131   (λaddr.opt_map … (mem_read_s …  s code_seg cur_pc)
132    (λoffs.(aux_write … byteflag) s (plusc_d_d ? addr (extu_w16 offs)) auxMode_ok cur_pc x1 writebw)).
133
134 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
135 ndefinition mode_IX2_load ≝
136 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
137  opt_map … (get_IX … s)
138   (λaddr.opt_map … (mem_read_s …  s code_seg cur_pc)
139    (λoffsh.opt_map … (mem_read_s …  s code_seg (succc ? cur_pc))
140     (λoffsl.(aux_load … byteflag) s (plusc_d_d ? addr 〈offsh:offsl〉) cur_pc x2))).
141
142 (* lettura da X+[word curpc] *)
143 ndefinition mode_IX2ADD_load ≝
144 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
145  opt_map … (get_IX … s)
146   (λaddr.opt_map … (mem_read_s …  s code_seg cur_pc)
147    (λbh.opt_map … (mem_read_s …  s code_seg (succc ? cur_pc))
148     (λbl.Some ? (triple … s (plusc_d_d ? addr 〈bh:bl〉) (succc ? (succc ? cur_pc)))))).
149
150 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
151 ndefinition mode_IX2_write ≝
152 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
153 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
154  opt_map … (get_IX … s)
155   (λaddr.opt_map … (mem_read_s …  s code_seg cur_pc)
156    (λoffsh.opt_map … (mem_read_s …  s code_seg (succc ? cur_pc))
157     (λoffsl.(aux_write … byteflag) s (plusc_d_d ? addr 〈offsh:offsl〉) auxMode_ok cur_pc x2 writebw))).
158
159 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
160 ndefinition mode_SP1_load ≝
161 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
162  opt_map … (get_sp_reg … s)
163   (λaddr.opt_map … (mem_read_s …  s code_seg cur_pc)
164    (λoffs.(aux_load … byteflag) s (plusc_d_d ? addr (extu_w16 offs)) cur_pc x1)).
165
166 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
167 ndefinition mode_SP1_write ≝
168 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
169 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
170  opt_map … (get_sp_reg … s)
171   (λaddr.opt_map … (mem_read_s …  s code_seg cur_pc)
172    (λoffs.(aux_write … byteflag) s (plusc_d_d ? addr (extu_w16 offs)) auxMode_ok cur_pc x1 writebw)).
173
174 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
175 ndefinition mode_SP2_load ≝
176 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
177  opt_map … (get_sp_reg … s)
178   (λaddr.opt_map … (mem_read_s …  s code_seg cur_pc)
179    (λoffsh.opt_map … (mem_read_s …  s code_seg (succc ? cur_pc))
180     (λoffsl.(aux_load … byteflag) s (plusc_d_d ? addr 〈offsh:offsl〉) cur_pc x2))).
181
182 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
183 ndefinition mode_SP2_write ≝
184 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
185 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
186  opt_map … (get_sp_reg … s)
187   (λaddr.opt_map … (mem_read_s …  s code_seg cur_pc)
188    (λoffsh.opt_map … (mem_read_s …  s code_seg (succc ? cur_pc))
189     (λoffsl.(aux_write … byteflag) s (plusc_d_d ? addr 〈offsh:offsl〉) auxMode_ok cur_pc x2 writebw))).
190
191 (* ************************************** *)
192 (* raccordo di tutte le possibili letture *)
193 (* ************************************** *)
194
195 (* H:X++ *)
196 ndefinition aux_inc_indX_16 ≝
197 λm:mcu_type.λt:memory_impl.λs:any_status m t.
198  opt_map … (get_indX_16_reg … s)
199   (λX_op.opt_map … (set_indX_16_reg … s (succc ? X_op))
200    (λs_tmp.Some ? s_tmp)).
201
202 ndefinition Freescale_multi_mode_load_auxb ≝
203 λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
204 (* NO: non ci sono indicazioni *)
205    [ MODE_INH  ⇒ None ?
206 (* restituisce A *)
207    | MODE_INHA ⇒ Some ? (triple … s (get_acc_8_low_reg … s) cur_pc)
208 (* restituisce X *)
209    | MODE_INHX ⇒ opt_map … (get_indX_8_low_reg … s)
210                   (λindx.Some ? (triple … s indx cur_pc))
211 (* restituisce H *)
212    | MODE_INHH ⇒ opt_map … (get_indX_8_high_reg … s)
213                   (λindx.Some ? (triple … s indx cur_pc))
214
215 (* NO: solo lettura word *)
216   | MODE_INHX0ADD ⇒ None ?
217 (* NO: solo lettura word *)
218   | MODE_INHX1ADD ⇒ None ?
219 (* NO: solo lettura word *)
220   | MODE_INHX2ADD ⇒ None ?
221
222 (* preleva 1 byte immediato *) 
223    | MODE_IMM1 ⇒ mode_IMM1_load … s cur_pc
224 (* NO: solo lettura word *)
225    | MODE_IMM1EXT ⇒ None ?
226 (* NO: solo lettura word *)
227    | MODE_IMM2 ⇒ None ?
228 (* preleva 1 byte da indirizzo diretto 1 byte *) 
229    | MODE_DIR1 ⇒ mode_DIR1_load true … s cur_pc
230 (* preleva 1 byte da indirizzo diretto 1 word *)
231    | MODE_DIR2 ⇒ mode_DIR2_load true … s cur_pc
232 (* preleva 1 byte da H:X *)
233    | MODE_IX0  ⇒ mode_IX0_load true … s cur_pc
234 (* preleva 1 byte da H:X+1 byte offset *)
235    | MODE_IX1  ⇒ mode_IX1_load true … s cur_pc
236 (* preleva 1 byte da H:X+1 word offset *)
237    | MODE_IX2  ⇒ mode_IX2_load true … s cur_pc
238 (* preleva 1 byte da SP+1 byte offset *)
239    | MODE_SP1  ⇒ mode_SP1_load true … s cur_pc
240 (* preleva 1 byte da SP+1 word offset *)
241    | MODE_SP2  ⇒ mode_SP2_load true … s cur_pc
242
243 (* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
244    | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true … s cur_pc
245 (* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
246    | MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load … s cur_pc
247 (* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
248    | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true … s cur_pc
249 (* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
250    | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true … s cur_pc
251
252 (* NO: solo lettura word/scrittura byte *)
253    | MODE_INHA_and_IMM1 ⇒ None ?
254 (* NO: solo lettura word/scrittura byte *)     
255    | MODE_INHX_and_IMM1 ⇒ None ?
256 (* NO: solo lettura word *) 
257    | MODE_IMM1_and_IMM1 ⇒ None ?
258 (* NO: solo lettura word/scrittura byte *) 
259    | MODE_DIR1_and_IMM1 ⇒ None ?
260 (* NO: solo lettura word/scrittura byte *) 
261    | MODE_IX0_and_IMM1  ⇒ None ?
262 (* NO: solo lettura word *) 
263    | MODE_IX0p_and_IMM1 ⇒ None ?
264 (* NO: solo lettura word/scrittura byte *) 
265    | MODE_IX1_and_IMM1  ⇒ None ?
266 (* NO: solo lettura word *) 
267    | MODE_IX1p_and_IMM1 ⇒ None ?
268 (* NO: solo lettura word/scrittura byte *) 
269    | MODE_SP1_and_IMM1  ⇒ None ?
270
271 (* NO: solo scrittura byte *)
272    | MODE_DIRn _          ⇒ None ?
273 (* NO: solo lettura word *)
274    | MODE_DIRn_and_IMM1 _ ⇒ None ?
275 (* preleva 1 byte da 0000 0000 0000 xxxxb *)
276    | MODE_TNY e           ⇒ opt_map … (memory_filter_read … s (extu2_w16 e))
277                              (λb.Some ? (triple … s b cur_pc))
278 (* preleva 1 byte da 0000 0000 000x xxxxb *)
279    | MODE_SRT t           ⇒ opt_map … (memory_filter_read … s (extu_w16 (b8_of_bit t)))
280                              (λb.Some ? (triple … s b cur_pc))
281    ].
282
283 ndefinition Freescale_multi_mode_load_auxw ≝
284 λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
285 (* NO: non ci sono indicazioni *)
286    [ MODE_INH  ⇒ None ?
287 (* NO: solo lettura/scrittura byte *)
288    | MODE_INHA ⇒ None ?
289 (* NO: solo lettura/scrittura byte *)
290    | MODE_INHX ⇒ None ?
291 (* NO: solo lettura/scrittura byte *)
292    | MODE_INHH ⇒ None ?
293
294 (* preleva 1 word immediato *) 
295   | MODE_INHX0ADD ⇒ opt_map … (get_IX … s)
296                      (λw.Some ? (triple … s w cur_pc))
297 (* preleva 1 word immediato *) 
298   | MODE_INHX1ADD ⇒ mode_IX1ADD_load … s cur_pc
299 (* preleva 1 word immediato *) 
300   | MODE_INHX2ADD ⇒ mode_IX2ADD_load … s cur_pc
301
302 (* NO: solo lettura byte *)
303    | MODE_IMM1 ⇒ None ?
304 (* preleva 1 word immediato *) 
305    | MODE_IMM1EXT ⇒ mode_IMM1EXT_load … s cur_pc
306 (* preleva 1 word immediato *) 
307    | MODE_IMM2 ⇒ mode_IMM2_load … s cur_pc
308 (* preleva 1 word da indirizzo diretto 1 byte *) 
309    | MODE_DIR1 ⇒ mode_DIR1_load false … s cur_pc
310 (* preleva 1 word da indirizzo diretto 1 word *) 
311    | MODE_DIR2 ⇒ mode_DIR2_load false … s cur_pc
312 (* preleva 1 word da H:X *)
313    | MODE_IX0  ⇒ mode_IX0_load false … s cur_pc
314 (* preleva 1 word da H:X+1 byte offset *)
315    | MODE_IX1  ⇒ mode_IX1_load false … s cur_pc
316 (* preleva 1 word da H:X+1 word offset *)
317    | MODE_IX2  ⇒ mode_IX2_load false … s cur_pc
318 (* preleva 1 word da SP+1 byte offset *)
319    | MODE_SP1  ⇒ mode_SP1_load false … s cur_pc
320 (* preleva 1 word da SP+1 word offset *)
321    | MODE_SP2  ⇒ mode_SP2_load false … s cur_pc
322
323 (* NO: solo lettura/scrittura byte *)
324    | MODE_DIR1_to_DIR1 ⇒ None ?
325 (* NO: solo lettura/scrittura byte *)
326    | MODE_IMM1_to_DIR1 ⇒ None ?
327 (* NO: solo lettura/scrittura byte *)
328    | MODE_IX0p_to_DIR1 ⇒ None ?
329 (* NO: solo lettura/scrittura byte *)
330    | MODE_DIR1_to_IX0p ⇒ None ?
331
332 (* preleva 2 byte, possibilita' modificare Io argomento *)
333    | MODE_INHA_and_IMM1 ⇒ opt_map … (mode_IMM1_load … s cur_pc)
334                            (λS_immb_and_PC.match S_immb_and_PC with
335                             [ triple _ immb cur_pc' ⇒
336                              Some ? (triple … s 〈(get_acc_8_low_reg … s):immb〉 cur_pc')])
337 (* preleva 2 byte, possibilita' modificare Io argomento *)
338    | MODE_INHX_and_IMM1 ⇒ opt_map … (get_indX_8_low_reg … s)
339                            (λX_op.opt_map … (mode_IMM1_load … s cur_pc)
340                             (λS_immb_and_PC.match S_immb_and_PC with
341                              [ triple _ immb cur_pc' ⇒
342                               Some ? (triple … s 〈X_op:immb〉 cur_pc')]))
343 (* preleva 2 byte, NO possibilita' modificare Io argomento *)               
344    | MODE_IMM1_and_IMM1 ⇒ opt_map … (mode_IMM1_load … s cur_pc)
345                            (λS_immb1_and_PC.match S_immb1_and_PC with
346                             [ triple _ immb1 cur_pc' ⇒
347                              opt_map … (mode_IMM1_load … s cur_pc')
348                               (λS_immb2_and_PC.match S_immb2_and_PC with
349                                [ triple _ immb2 cur_pc'' ⇒
350                                 Some ? (triple … s 〈immb1:immb2〉 cur_pc'')])])
351 (* preleva 2 byte, possibilita' modificare Io argomento *)
352    | MODE_DIR1_and_IMM1 ⇒ opt_map … (mode_DIR1_load true … s cur_pc)
353                            (λS_dirb_and_PC.match S_dirb_and_PC with
354                             [ triple _ dirb cur_pc' ⇒
355                              opt_map … (mode_IMM1_load … s cur_pc')
356                               (λS_immb_and_PC.match S_immb_and_PC with
357                                [ triple _ immb cur_pc'' ⇒
358                                 Some ? (triple … s 〈dirb:immb〉 cur_pc'')])])
359 (* preleva 2 byte, possibilita' modificare Io argomento *)
360    | MODE_IX0_and_IMM1  ⇒ opt_map … (mode_IX0_load true … s cur_pc)
361                            (λS_ixb_and_PC.match S_ixb_and_PC with
362                             [ triple _ ixb cur_pc' ⇒
363                              opt_map … (mode_IMM1_load … s cur_pc')
364                               (λS_immb_and_PC.match S_immb_and_PC with
365                                [ triple _ immb cur_pc'' ⇒
366                                 Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
367 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
368    | MODE_IX0p_and_IMM1 ⇒ opt_map … (mode_IX0_load true … s cur_pc)
369                            (λS_ixb_and_PC.match S_ixb_and_PC with
370                             [ triple _ ixb cur_pc' ⇒
371                              opt_map … (mode_IMM1_load … s cur_pc')
372                               (λS_immb_and_PC.match S_immb_and_PC with
373                                [ triple _ immb cur_pc'' ⇒
374                                 (* H:X++ *)
375                                 opt_map … (aux_inc_indX_16 … s)
376                                  (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
377 (* preleva 2 byte, possibilita' modificare Io argomento *)
378    | MODE_IX1_and_IMM1  ⇒ opt_map … (mode_IX1_load true … s cur_pc)
379                            (λS_ixb_and_PC.match S_ixb_and_PC with
380                             [ triple _ ixb cur_pc' ⇒
381                              opt_map … (mode_IMM1_load … s cur_pc')
382                               (λS_immb_and_PC.match S_immb_and_PC with
383                                [ triple _ immb cur_pc'' ⇒
384                                 Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
385 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
386    | MODE_IX1p_and_IMM1 ⇒ opt_map … (mode_IX1_load true … s cur_pc)
387                            (λS_ixb_and_PC.match S_ixb_and_PC with
388                             [ triple _ ixb cur_pc' ⇒
389                              opt_map … (mode_IMM1_load … s cur_pc')
390                               (λS_immb_and_PC.match S_immb_and_PC with
391                                [ triple _ immb cur_pc'' ⇒
392                                 (* H:X++ *)
393                                 opt_map … (aux_inc_indX_16 … s)
394                                  (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
395 (* preleva 2 byte, possibilita' modificare Io argomento *)
396    | MODE_SP1_and_IMM1  ⇒ opt_map … (mode_SP1_load true … s cur_pc)
397                            (λS_spb_and_PC.match S_spb_and_PC with
398                             [ triple _ spb cur_pc' ⇒
399                              opt_map … (mode_IMM1_load … s cur_pc')
400                               (λS_immb_and_PC.match S_immb_and_PC with
401                                [ triple _ immb cur_pc'' ⇒
402                                 Some ? (triple … s 〈spb:immb〉 cur_pc'')])])
403
404 (* NO: solo scrittura byte *)
405    | MODE_DIRn _            ⇒ None ?
406 (* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
407    | MODE_DIRn_and_IMM1 msk ⇒ opt_map … (mode_DIR1n_load … s cur_pc msk)
408                                (λS_dirbn_and_PC.match S_dirbn_and_PC with
409                                 [ triple _ dirbn cur_pc'   ⇒
410                                  opt_map … (mode_IMM1_load … s cur_pc')
411                                   (λS_immb_and_PC.match S_immb_and_PC with
412                                    [ triple _ immb cur_pc'' ⇒
413                                      Some ? (triple … s 〈(extu_b8 match dirbn with [ true ⇒ x1 | false ⇒ x0 ]):immb〉 cur_pc'') ])])
414 (* NO: solo lettura/scrittura byte *)
415    | MODE_TNY _             ⇒ None ?
416 (* NO: solo lettura/scrittura byte *)
417    | MODE_SRT _             ⇒ None ?
418    ].
419
420 (* **************************************** *)
421 (* raccordo di tutte le possibili scritture *)
422 (* **************************************** *)
423
424 ndefinition Freescale_multi_mode_write_auxb ≝
425 λm,t.λs:any_status m t.λcur_pc:word16.λflag:aux_mod_type.λi:Freescale_instr_mode.λwriteb:byte8.match i with
426 (* NO: non ci sono indicazioni *)
427   [ MODE_INH        ⇒ None ?
428 (* scrive A *)
429   | MODE_INHA       ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
430 (* scrive X *)
431   | MODE_INHX       ⇒ opt_map … (set_indX_8_low_reg … s writeb)
432                       (λtmps.Some ? (pair … tmps cur_pc)) 
433 (* scrive H *)
434   | MODE_INHH       ⇒ opt_map … (set_indX_8_high_reg … s writeb)
435                        (λtmps.Some ? (pair … tmps cur_pc)) 
436
437 (* NO: solo lettura word *)
438   | MODE_INHX0ADD ⇒ None ?
439 (* NO: solo lettura word *)
440   | MODE_INHX1ADD ⇒ None ?
441 (* NO: solo lettura word *)
442   | MODE_INHX2ADD ⇒ None ?
443
444 (* NO: solo lettura byte *)
445   | MODE_IMM1       ⇒ None ?
446 (* NO: solo lettura word *)
447   | MODE_IMM1EXT    ⇒ None ?
448 (* NO: solo lettura word *)
449   | MODE_IMM2       ⇒ None ?
450 (* scrive 1 byte su indirizzo diretto 1 byte *)
451   | MODE_DIR1       ⇒ mode_DIR1_write true … s cur_pc writeb
452 (* scrive 1 byte su indirizzo diretto 1 word *)
453   | MODE_DIR2       ⇒ mode_DIR2_write true … s cur_pc writeb
454 (* scrive 1 byte su H:X *)
455   | MODE_IX0        ⇒ mode_IX0_write true … s cur_pc writeb
456 (* scrive 1 byte su H:X+1 byte offset *)
457   | MODE_IX1        ⇒ mode_IX1_write true … s cur_pc writeb
458 (* scrive 1 byte su H:X+1 word offset *)
459   | MODE_IX2        ⇒ mode_IX2_write true … s cur_pc writeb
460 (* scrive 1 byte su SP+1 byte offset *)
461   | MODE_SP1        ⇒ mode_SP1_write true … s cur_pc writeb
462 (* scrive 1 byte su SP+1 word offset *)
463   | MODE_SP2        ⇒ mode_SP2_write true … s cur_pc writeb
464
465 (* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
466   | MODE_DIR1_to_DIR1   ⇒ mode_DIR1_write true … s cur_pc writeb
467 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
468   | MODE_IMM1_to_DIR1   ⇒ mode_DIR1_write true … s cur_pc writeb
469 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
470   | MODE_IX0p_to_DIR1   ⇒ opt_map … (mode_DIR1_write true … s cur_pc writeb)
471                            (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
472                             (* H:X++ *)
473                             opt_map … (aux_inc_indX_16 … S_op)
474                              (λS_op'.Some ? (pair … S_op' PC_op))])
475 (* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
476   | MODE_DIR1_to_IX0p   ⇒ opt_map … (mode_IX0_write true … s cur_pc writeb)
477                            (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
478                             (* H:X++ *)
479                             opt_map … (aux_inc_indX_16 … S_op)
480                              (λS_op'.Some ? (pair … S_op' PC_op))])
481
482 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
483   | MODE_INHA_and_IMM1 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
484 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)  
485   | MODE_INHX_and_IMM1 ⇒ opt_map … (set_indX_8_low_reg … s writeb)
486                            (λtmps.Some ? (pair … tmps cur_pc)) 
487 (* NO: solo lettura word *) 
488   | MODE_IMM1_and_IMM1 ⇒ None ?
489 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *) 
490   | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write true … s cur_pc writeb
491 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
492   | MODE_IX0_and_IMM1  ⇒ mode_IX0_write true … s cur_pc writeb
493 (* NO: solo lettura word *) 
494   | MODE_IX0p_and_IMM1 ⇒ None ?
495 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
496   | MODE_IX1_and_IMM1  ⇒ mode_IX1_write true … s cur_pc writeb
497 (* NO: solo lettura word *) 
498   | MODE_IX1p_and_IMM1 ⇒ None ?
499 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
500   | MODE_SP1_and_IMM1  ⇒ mode_SP1_write true … s cur_pc writeb
501
502 (* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
503   | MODE_DIRn msk ⇒ mode_DIR1n_write … s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))   
504 (* NO: solo lettura word *)
505   | MODE_DIRn_and_IMM1 _ ⇒ None ?
506 (* scrive 1 byte su 0000 0000 0000 xxxxb *)
507   | MODE_TNY e ⇒ opt_map … (memory_filter_write … s (extu2_w16 e) auxMode_ok writeb)
508                    (λtmps.Some ? (pair … tmps cur_pc))
509 (* scrive 1 byte su 0000 0000 000x xxxxb *)
510   | MODE_SRT e ⇒ opt_map … (memory_filter_write … s (extu_w16 (b8_of_bit e)) auxMode_ok writeb)
511                       (λtmps.Some ? (pair … tmps cur_pc))
512   ].
513
514 ndefinition Freescale_multi_mode_write_auxw ≝
515 λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwritew:word16.match i with
516 (* NO: non ci sono indicazioni *)
517   [ MODE_INH        ⇒ None ?
518 (* NO: solo lettura/scrittura byte *)
519   | MODE_INHA       ⇒ None ?
520 (* NO: solo lettura/scrittura byte *)
521   | MODE_INHX       ⇒ None ?
522 (* NO: solo lettura/scrittura byte *)
523   | MODE_INHH       ⇒ None ?
524
525 (* NO: solo lettura word *)
526   | MODE_INHX0ADD ⇒ None ?
527 (* NO: solo lettura word *)
528   | MODE_INHX1ADD ⇒ None ?
529 (* NO: solo lettura word *)
530   | MODE_INHX2ADD ⇒ None ?
531
532 (* NO: solo lettura byte *)
533   | MODE_IMM1       ⇒ None ?
534 (* NO: solo lettura word *)
535   | MODE_IMM1EXT    ⇒ None ?
536 (* NO: solo lettura word *)
537   | MODE_IMM2       ⇒ None ?
538 (* scrive 1 word su indirizzo diretto 1 byte *) 
539   | MODE_DIR1       ⇒ mode_DIR1_write false … s cur_pc writew
540 (* scrive 1 word su indirizzo diretto 1 word *)
541   | MODE_DIR2       ⇒ mode_DIR2_write false … s cur_pc writew
542 (* scrive 1 word su H:X *)
543   | MODE_IX0        ⇒ mode_IX0_write false … s cur_pc writew
544 (* scrive 1 word su H:X+1 byte offset *)
545   | MODE_IX1        ⇒ mode_IX1_write false … s cur_pc writew
546 (* scrive 1 word su H:X+1 word offset *)
547   | MODE_IX2        ⇒ mode_IX2_write false … s cur_pc writew
548 (* scrive 1 word su SP+1 byte offset *)
549   | MODE_SP1        ⇒ mode_SP1_write false … s cur_pc writew
550 (* scrive 1 word su SP+1 word offset *)
551   | MODE_SP2        ⇒ mode_SP2_write false … s cur_pc writew
552
553 (* NO: solo lettura/scrittura byte *)
554   | MODE_DIR1_to_DIR1 ⇒ None ?
555 (* NO: solo lettura/scrittura byte *)
556   | MODE_IMM1_to_DIR1 ⇒ None ?
557 (* NO: solo lettura/scrittura byte *)
558   | MODE_IX0p_to_DIR1 ⇒ None ?
559 (* NO: solo lettura/scrittura byte *)
560   | MODE_DIR1_to_IX0p ⇒ None ?
561
562 (* NO: solo lettura word/scrittura byte *)
563   | MODE_INHA_and_IMM1 ⇒ None ?
564 (* NO: solo lettura word/scrittura byte *)     
565   | MODE_INHX_and_IMM1 ⇒ None ?
566 (* NO: solo lettura word *) 
567   | MODE_IMM1_and_IMM1 ⇒ None ?
568 (* NO: solo lettura word/scrittura byte *) 
569   | MODE_DIR1_and_IMM1 ⇒ None ?
570 (* NO: solo lettura word/scrittura byte *) 
571   | MODE_IX0_and_IMM1  ⇒ None ?
572 (* NO: solo lettura word *) 
573   | MODE_IX0p_and_IMM1 ⇒ None ?
574 (* NO: solo lettura word/scrittura byte *)
575   | MODE_IX1_and_IMM1  ⇒ None ?
576 (* NO: solo lettura word *) 
577   | MODE_IX1p_and_IMM1 ⇒ None ?
578 (* NO: solo lettura word/scrittura byte *) 
579   | MODE_SP1_and_IMM1  ⇒ None ?
580
581 (* NO: solo scrittura byte *)
582   | MODE_DIRn _          ⇒ None ?
583 (* NO: solo lettura word *)
584   | MODE_DIRn_and_IMM1 _ ⇒ None ?
585 (* NO: solo lettura/scrittura byte *)
586   | MODE_TNY _           ⇒ None ?
587 (* NO: solo lettura/scrittura byte *)
588   | MODE_SRT _           ⇒ None ?
589   ].