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