]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly2/emulator/multivm/Freescale_multivm.ma
wip ....
[helm.git] / helm / software / matita / contribs / ng_assembly2 / emulator / multivm / Freescale_multivm.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/multivm/multivm_base.ma".
24 include "emulator/read_write/load_write.ma".
25
26 (* ************************************************ *)
27 (* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
28 (* ************************************************ *)
29
30 (* A = [true] fAMC(A,M,C), [false] A *)
31 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
32 (* fAMC e' la logica da applicare: somma con/senza carry *)
33 ndefinition execute_ADC_ADD_aux ≝
34 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.λsetflag:bool.
35 λfAMC:bool → byte8 → byte8 → ProdT bool byte8.
36  opt_map … (multi_mode_loadb … s cur_pc i)
37   (λS_M_PC.match S_M_PC with
38    [ triple s_tmp1 M_op new_pc ⇒
39     let A_op ≝ get_acc_8_low_reg … s_tmp1 in
40     match fAMC (get_c_flag … s_tmp1) A_op M_op with
41      [ pair carry R_op ⇒
42       let A7 ≝ getMSBc ? A_op in
43       let M7 ≝ getMSBc ? M_op in
44       let R7 ≝ getMSBc ? R_op in
45       let A3 ≝ getMSBc ? (cnL ? A_op) in
46       let M3 ≝ getMSBc ? (cnL ? M_op) in
47       let R3 ≝ getMSBc ? (cnL ? R_op) in
48       (* A = [true] fAMC(A,M,C), [false] A *)
49       let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg … s_tmp1 R_op | false ⇒ s_tmp1 ] in
50       (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
51       let s_tmp3 ≝ set_zflb … s_tmp2 R_op in
52       (* C = A7&M7 | M7&nR7 | nR7&A7 *)
53       let s_tmp4 ≝ set_c_flag … s_tmp3 ((A7⊗M7) ⊕ (M7⊗(⊖R7)) ⊕ ((⊖R7)⊗A7)) in
54       (* N = R7 *)
55       let s_tmp5 ≝ set_nflb … s_tmp4 R_op in
56       (* H = A3&M3 | M3&nR3 | nR3&A3 *)
57       let s_tmp6 ≝ setweak_h_flag … s_tmp5 ((A3⊗M3) ⊕ (M3⊗(⊖R3)) ⊕ ((⊖R3)⊗A3)) in
58       (* V = A7&M7&nR7 | nA7&nM7&R7 *)
59       let s_tmp7 ≝ setweak_v_flag … s_tmp6 ((A7⊗M7⊗(⊖R7)) ⊕ ((⊖A7)⊗(⊖M7)⊗R7)) in
60       (* newpc = nextpc *)
61       Some ? (pair … s_tmp7 new_pc) ]]).
62
63 (* A = [true] fAM(A,M), [false] A *)
64 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
65 (* fAM e' la logica da applicare: and/xor/or *)
66 ndefinition execute_AND_BIT_EOR_ORA_aux ≝
67 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.λsetflag:bool.
68 λfAM:byte8 → byte8 → byte8.
69  opt_map … (multi_mode_loadb … s cur_pc i)
70   (λS_M_PC.match S_M_PC with
71    [ triple s_tmp1 M_op new_pc ⇒
72     let R_op ≝ fAM (get_acc_8_low_reg … s_tmp1) M_op in
73     (* A = [true] fAM(A,M), [false] A *) 
74     let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg … s_tmp1 R_op | false ⇒ s_tmp1 ] in
75     (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
76     let s_tmp3 ≝ set_zflb … s_tmp2 R_op in
77     (* N = R7 *) 
78     let s_tmp4 ≝ set_nflb … s_tmp3 R_op in
79     (* V = 0 *) 
80     let s_tmp5 ≝ setweak_v_flag … s_tmp4 false in
81     (* newpc = nextpc *)
82     Some ? (pair … s_tmp5 new_pc) ]).
83
84 (* M = fMC(M,C) *)
85 (* fMC e' la logica da applicare: rc_/ro_/sh_ *)
86 ndefinition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
87 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
88 λfMC:bool → byte8 → ProdT bool byte8.
89  opt_map … (multi_mode_loadb … s cur_pc i)
90   (λS_M_PC.match S_M_PC with
91    [ triple s_tmp1 M_op _ ⇒
92     match fMC (get_c_flag … s_tmp1) M_op with [ pair carry R_op ⇒
93     (* M = fMC(M,C) *)
94     opt_map … (multi_mode_writeb … s_tmp1 cur_pc auxMode_ok i R_op)
95      (λS_PC.match S_PC with
96       [ pair s_tmp2 new_pc ⇒
97       (* C = carry *)
98       let s_tmp3 ≝ set_c_flag … s_tmp2 carry in
99       (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
100       let s_tmp4 ≝ set_zflb … s_tmp3 R_op in
101       (* N = R7 *)
102       let s_tmp5 ≝ set_nflb … s_tmp4 R_op in
103       (* V = R7 ⊙ carry *)
104       let s_tmp6 ≝ setweak_v_flag … s_tmp5 ((getMSBc ? R_op) ⊙ carry) in
105       (* newpc = nextpc *)
106       Some ? (pair … s_tmp6 new_pc) ])]]).
107
108 (* branch con byte+estensione segno *)
109 ndefinition branched_pc ≝
110 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λb:byte8.
111  get_pc_reg … (set_pc_reg … s (plusc_d_d ? cur_pc (exts_w16  b))).
112
113 (* if COND=1 branch *)
114 (* tutti i branch calcoleranno la condizione e la passeranno qui *)
115 ndefinition execute_any_BRANCH ≝
116 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.λfCOND:bool.
117  opt_map … (multi_mode_loadb … s cur_pc i)
118   (λS_M_PC.match S_M_PC with
119    [ triple s_tmp1 M_op new_pc ⇒
120     (* if true, branch *) 
121     match fCOND with
122      (* newpc = nextpc + rel *)
123      [ true ⇒ Some ? (pair … s_tmp1 (branched_pc … s_tmp1 new_pc M_op))
124      (* newpc = nextpc *)
125      | false ⇒ Some ? (pair … s_tmp1 new_pc) ]]).
126
127 (* Mn = filtered optval *) 
128 (* il chiamante passa 0x00 per azzerare, 0xFF per impostare il bit di M *)
129 ndefinition execute_BCLRn_BSETn_aux ≝
130 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.λoptval:byte8.
131  (* Mn = filtered optval *)
132  opt_map … (multi_mode_writeb … s cur_pc auxMode_ok i optval)
133   (λS_PC.match S_PC with
134    (* newpc = nextpc *)
135    [ pair s_tmp1 new_pc ⇒ Some ? (pair … s_tmp1 new_pc) ]).
136
137 (* if COND(Mn) branch *)
138 (* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
139 ndefinition execute_BRCLRn_BRSETn_aux ≝
140 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.λfCOND:byte8 → bool.
141  opt_map … (multi_mode_loadw … s cur_pc i)
142   (λS_M_PC.match S_M_PC with
143    [ triple s_tmp1 M_op new_pc ⇒ match M_op with
144     [ mk_comp_num MH_op ML_op ⇒
145      (* if COND(Mn) branch *)
146      match fCOND MH_op with
147       (* newpc = nextpc + rel *)
148       [ true ⇒ Some ? (pair … s_tmp1 (branched_pc … s_tmp1 new_pc ML_op))
149       (* newpc = nextpc *)
150       | false ⇒ Some ? (pair … s_tmp1 new_pc) ]]]).
151
152 (* A = [true] fAMC(A,M,C), [false] A *)
153 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
154 (* fAMC e' la logica da applicare: sottrazione con/senza carry *)
155 ndefinition execute_CMP_SBC_SUB_aux ≝
156 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.λsetflag:bool.
157 λfAMC:bool → byte8 → byte8 → ProdT bool byte8.
158  opt_map … (multi_mode_loadb … s cur_pc i)
159   (λS_M_PC.match S_M_PC with
160    [ triple s_tmp1 M_op new_pc ⇒
161     let A_op ≝ get_acc_8_low_reg … s_tmp1 in
162     match fAMC (get_c_flag … s_tmp1) A_op M_op with
163      [ pair carry R_op ⇒
164       let A7 ≝ getMSBc ? A_op in
165       let M7 ≝ getMSBc ? M_op in
166       let R7 ≝ getMSBc ? R_op in
167       (* A = [true] fAMC(A,M,C), [false] A *)
168       let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg … s_tmp1 R_op | false ⇒ s_tmp1 ] in
169       (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
170       let s_tmp3 ≝ set_zflb … s_tmp2 R_op in
171       (* C = nA7&M7 | M7&R7 | R7&nA7 *)
172       let s_tmp4 ≝ set_c_flag … s_tmp3 (((⊖A7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖A7))) in
173       (* N = R7 *) 
174       let s_tmp5 ≝ set_nflb … s_tmp4 R_op in
175       (* V = A7&nM7&nR7 | nA7&M7&R7 *)
176       let s_tmp6 ≝ setweak_v_flag … s_tmp5 ((A7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖A7)⊗M7⊗R7)) in
177       (* newpc = nextpc *)
178       Some ? (pair … s_tmp6 new_pc) ]]).
179
180 (* M = fM(M) *)
181 (* fM e' la logica da applicare: not/neg/++/-- *)
182 ndefinition execute_COM_DEC_INC_NEG_aux ≝
183 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
184 λfM:byte8 → byte8.λfV:bool → bool → bool.λfC:bool → byte8 → bool.
185  opt_map … (multi_mode_loadb … s cur_pc i)
186   (λS_M_PC.match S_M_PC with
187    [ triple s_tmp1 M_op _ ⇒
188     let R_op ≝ fM M_op in
189     (* M = fM(M) *)
190     opt_map … (multi_mode_writeb … s_tmp1 cur_pc auxMode_ok i R_op)
191      (λS_PC.match S_PC with
192       [ pair s_tmp2 new_pc ⇒
193       (* C = fCR (C,R) *)
194       let s_tmp3 ≝ set_c_flag … s_tmp2 (fC (get_c_flag … s_tmp2) R_op) in
195       (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
196       let s_tmp4 ≝ set_zflb … s_tmp3 R_op in
197       (* N = R7 *)
198       let s_tmp5 ≝ set_nflb … s_tmp4 R_op in
199       (* V = fV (M7,R7) *)
200       let s_tmp6 ≝ setweak_v_flag … s_tmp5 (fV (getMSBc ? M_op) (getMSBc ? R_op)) in
201       (* newpc = nextpc *)
202       Some ? (pair … s_tmp6 new_pc) ])]).
203
204 (* il classico push *)
205 ndefinition aux_push ≝
206 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
207  opt_map … (get_sp_reg … s)
208   (* [SP] = val *)
209   (λSP_op.opt_map … (memory_filter_write … s SP_op auxMode_ok val)
210    (* SP -- *)
211    (λs_tmp1.opt_map … (set_sp_reg … s_tmp1 (predc ? SP_op))
212     (λs_tmp2.Some ? s_tmp2))).
213
214 (* il classico pop *)
215 (* NB: l'incremento di SP deve essere filtrato dalla ALU, quindi get(set(SP)) *)
216 ndefinition aux_pop ≝
217 λm:mcu_type.λt:memory_impl.λs:any_status m t.
218  opt_map … (get_sp_reg … s)
219   (* SP ++ *)
220   (λSP_op.opt_map … (set_sp_reg … s (succc ? SP_op))
221    (λs_tmp1.opt_map … (get_sp_reg … s_tmp1)
222     (* val = [SP] *)
223     (λSP_op'.opt_map … (memory_filter_read … s_tmp1 SP_op')
224      (λval.Some ? (pair … s_tmp1 val))))).
225
226 (* CCR corrisponde a V11HINZC e cmq 1 se un flag non esiste *)
227 (* i flag mantengono posizione costante nelle varie ALU, e se non sono
228    implementati corrispondono a 1 *)
229 ndefinition aux_get_CCR_aux ≝
230 λopt:option bool.match opt with [ None ⇒ true | Some b ⇒ b ].
231
232 ndefinition aux_get_CCR ≝
233 λm:mcu_type.λt:memory_impl.λs:any_status m t.
234  byte8_of_bits (mk_Array8T ?
235   (aux_get_CCR_aux (get_v_flag … s))
236   true
237   true
238   (aux_get_CCR_aux (get_h_flag … s))
239   (aux_get_CCR_aux (get_i_flag … s))
240   (aux_get_CCR_aux (get_n_flag … s))
241   (get_z_flag … s)
242   (get_c_flag … s)).
243
244 (* CCR corrisponde a V11HINZC *)
245 (* i flag mantengono posizione costante nelle varie ALU, e se non sono
246    implementati si puo' usare tranquillamente setweak *)
247 ndefinition aux_set_CCR ≝
248 λm:mcu_type.λt:memory_impl.λs:any_status m t.λCCR:byte8.
249  match bits_of_byte8 CCR with
250   [ mk_Array8T vf _ _ hf if nf zf cf ⇒
251    setweak_v_flag …
252     (setweak_h_flag …
253      (setweak_i_flag …
254       (setweak_n_flag …
255        (set_z_flag …
256         (set_c_flag … s cf) zf) nf) if) hf) vf ].
257
258 (* **************** *)
259 (* LOGICA DELLA ALU *)
260 (* **************** *)
261
262 (* A = A + M + C *)
263 ndefinition execute_ADC ≝
264 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
265  execute_ADC_ADD_aux … s cur_pc i true (λC_op.plusc_dc_dc ? C_op).
266
267 (* A = A + M *)
268 ndefinition execute_ADD ≝
269 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
270  execute_ADC_ADD_aux … s cur_pc i true (λC_op.plusc_dc_dc ? false).
271
272 (* SP += extended M *)
273 ndefinition execute_AIS ≝
274 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
275  opt_map … (multi_mode_loadb … s cur_pc i)
276   (λS_M_PC.match S_M_PC with
277    [ triple s_tmp1 M_op new_pc ⇒
278    opt_map … (get_sp_reg … s_tmp1)
279     (* SP += extended M *)
280     (λSP_op.opt_map … (set_sp_reg … s_tmp1 (plusc_d_d ? SP_op (exts_w16 M_op)))
281      (λs_tmp2.Some ? (pair … s_tmp2 new_pc))) ]).
282
283 (* H:X += extended M *)
284 ndefinition execute_AIX ≝
285 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
286  opt_map … (multi_mode_loadb … s cur_pc i)
287   (λS_M_PC.match S_M_PC with
288    [ triple s_tmp1 M_op new_pc ⇒
289    opt_map … (get_indX_16_reg … s_tmp1)
290     (* H:X += extended M *)
291     (λHX_op.opt_map … (set_indX_16_reg … s_tmp1 (plusc_d_d ? HX_op (exts_w16 M_op)))
292      (λs_tmp2.Some ? (pair … s_tmp2 new_pc))) ]).
293
294 (* A = A & M *)
295 ndefinition execute_AND ≝
296 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
297  execute_AND_BIT_EOR_ORA_aux … s cur_pc i true (andc ?).
298
299 (* M = C' <- rcl M <- 0 *)
300 ndefinition execute_ASL ≝
301 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
302  execute_ASL_ASR_LSR_ROL_ROR_aux … s cur_pc i (λC_op.rclc ? false).
303
304 (* M = M7 -> rcr M -> C' *)
305 ndefinition execute_ASR ≝
306 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
307  execute_ASL_ASR_LSR_ROL_ROR_aux … s cur_pc i (λC_op.λM_op.rcrc ? (getMSBc ? M_op) M_op).
308
309 (* if C=0, branch *) 
310 ndefinition execute_BCC ≝
311 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
312  execute_any_BRANCH … s cur_pc i (⊖(get_c_flag … s)).
313
314 (* Mn = 0 *)
315 ndefinition execute_BCLRn ≝
316 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
317  execute_BCLRn_BSETn_aux … s cur_pc i 〈x0,x0〉.
318
319 (* if C=1, branch *) 
320 ndefinition execute_BCS ≝
321 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
322  execute_any_BRANCH … s cur_pc i (get_c_flag … s).
323
324 (* if Z=1, branch *)
325 ndefinition execute_BEQ ≝
326 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
327  execute_any_BRANCH … s cur_pc i (get_z_flag … s).
328
329 (* if N⊙V=0, branch *)
330 ndefinition execute_BGE ≝
331 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
332  opt_map … (get_n_flag … s)
333   (λN_op.opt_map … (get_v_flag … s)
334    (λV_op.execute_any_BRANCH … s cur_pc i (⊖(N_op ⊙ V_op)))).
335
336 (* BGND mode *)
337 ndefinition execute_BGND ≝
338 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
339  Some ? (pair … s cur_pc).
340
341 (* if Z|N⊙V=0, branch *)
342 ndefinition execute_BGT ≝
343 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
344  opt_map … (get_n_flag … s)
345   (λN_op.opt_map … (get_v_flag … s)
346    (λV_op.execute_any_BRANCH … s cur_pc i (⊖((get_z_flag … s) ⊕ (N_op ⊙ V_op))))).
347
348 (* if H=0, branch *)
349 ndefinition execute_BHCC ≝
350 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
351  opt_map … (get_h_flag … s)
352   (λH_op.execute_any_BRANCH … s cur_pc i (⊖H_op)).
353
354 (* if H=1, branch *)
355 ndefinition execute_BHCS ≝
356 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
357  opt_map … (get_h_flag … s)
358   (λH_op.execute_any_BRANCH … s cur_pc i H_op).
359
360 (* if C|Z=0, branch *)
361 ndefinition execute_BHI ≝
362 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
363  execute_any_BRANCH … s cur_pc i (⊖((get_c_flag … s) ⊕ (get_z_flag … s))).
364
365 (* if nIRQ=1, branch NB: irqflag e' un negato del pin *)
366 ndefinition execute_BIH ≝
367 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
368  opt_map … (get_irq_flag … s)
369   (λIRQ_op.execute_any_BRANCH … s cur_pc i (⊖IRQ_op)).
370
371 (* if nIRQ=0, branch NB: irqflag e' un negato del pin *)
372 ndefinition execute_BIL ≝
373 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
374  opt_map … (get_irq_flag … s)
375   (λIRQ_op.execute_any_BRANCH … s cur_pc i IRQ_op).
376
377 (* flags = A & M *)
378 ndefinition execute_BIT ≝
379 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
380  execute_AND_BIT_EOR_ORA_aux … s cur_pc i false (andc ?).
381
382 (* if Z|N⊙V=1, branch *)
383 ndefinition execute_BLE ≝
384 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
385  opt_map … (get_n_flag … s)
386   (λN_op.opt_map … (get_v_flag … s)
387    (λV_op.execute_any_BRANCH … s cur_pc i ((get_z_flag … s) ⊕ (N_op ⊙ V_op)))).
388
389 (* if C|Z=1, branch *)
390 ndefinition execute_BLS ≝
391 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
392  execute_any_BRANCH … s cur_pc i ((get_c_flag … s) ⊕ (get_z_flag … s)).
393
394 (* if N⊙V=1, branch *)
395 ndefinition execute_BLT ≝
396 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
397  opt_map … (get_n_flag … s)
398   (λN_op.opt_map … (get_v_flag … s)
399    (λV_op.execute_any_BRANCH … s cur_pc i (N_op ⊙ V_op))).
400
401 (* if I=0, branch *)
402 ndefinition execute_BMC ≝
403 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
404  opt_map … (get_i_flag … s)
405   (λI_op.execute_any_BRANCH … s cur_pc i (⊖I_op)).
406
407 (* if N=1, branch *)
408 ndefinition execute_BMI ≝
409 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
410  opt_map … (get_n_flag … s)
411   (λN_op.execute_any_BRANCH … s cur_pc i N_op).
412
413 (* if I=1, branch *)
414 ndefinition execute_BMS ≝
415 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
416  opt_map … (get_i_flag … s)
417   (λI_op.execute_any_BRANCH … s cur_pc i I_op).
418
419 (* if Z=0, branch *)
420 ndefinition execute_BNE ≝
421 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
422  execute_any_BRANCH … s cur_pc i (⊖(get_z_flag … s)).
423
424 (* if N=0, branch *)
425 ndefinition execute_BPL ≝
426 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
427  opt_map … (get_n_flag … s)
428   (λN_op.execute_any_BRANCH … s cur_pc i (⊖N_op)).
429
430 (* branch always *)
431 ndefinition execute_BRA ≝
432 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
433  execute_any_BRANCH … s cur_pc i true.
434
435 (* if Mn=0 branch *)
436 ndefinition execute_BRCLRn ≝
437 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
438  execute_BRCLRn_BRSETn_aux … s cur_pc i
439   (λMn_op.eqc ? Mn_op (zeroc ?)).
440
441 (* branch never... come se fosse un nop da 2 byte *)
442 ndefinition execute_BRN ≝
443 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
444  execute_any_BRANCH … s cur_pc i false.
445
446 (* if Mn=1 branch *)
447 ndefinition execute_BRSETn ≝
448 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
449  execute_BRCLRn_BRSETn_aux … s cur_pc i
450   (λMn_op.⊖(eqc ? Mn_op (zeroc ?))).
451
452 (* Mn = 1 *)
453 ndefinition execute_BSETn ≝
454 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
455  execute_BCLRn_BSETn_aux … s cur_pc i 〈xF,xF〉.
456
457 (* branch to subroutine *)
458 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
459 ndefinition execute_BSR ≝
460 λm:mcu_type.λt:memory_impl.λs:any_status m t .λcur_pc:word16.λi:aux_im_type m.
461  opt_map … (multi_mode_loadb … s cur_pc i)
462   (λS_M_PC.match S_M_PC with
463    [ triple s_tmp1 M_op new_pc ⇒ let aux ≝
464     (* push (new_pc low) *)
465     opt_map … (aux_push … s_tmp1 (cnL ? new_pc))
466      (* push (new_pc high) *)
467      (λs_tmp2.opt_map … (aux_push … s_tmp2 (cnH ? new_pc))
468       (* new_pc = new_pc + rel *)
469       (λs_tmp3.Some ? (pair … s_tmp3 (branched_pc … s_tmp3 new_pc M_op))))
470      in match m with
471     [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
472     | RS08 ⇒
473      (* SPC = new_pc *) 
474      opt_map … (set_spc_reg … s_tmp1 new_pc)
475       (* new_pc = new_pc + rel *)
476       (λs_tmp2.Some ? (pair … s_tmp2 (branched_pc … s_tmp2 new_pc M_op)))
477     | _ ⇒ None ?
478     ]]).
479
480 (* if A=M, branch *)
481 ndefinition execute_CBEQA ≝
482 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
483  opt_map … (multi_mode_loadw … s cur_pc i)
484   (λS_M_PC.match S_M_PC with
485    [ triple s_tmp1 M_op new_pc ⇒
486     match M_op with
487      [ mk_comp_num MH_op ML_op ⇒
488       (* if A=M, branch *)
489       match eqc ? (get_acc_8_low_reg … s_tmp1) MH_op with
490        (* new_pc = new_pc + rel *)
491        [ true ⇒ Some ? (pair … s_tmp1 (branched_pc … s_tmp1 new_pc ML_op))
492        (* new_pc = new_pc *)
493        | false ⇒ Some ? (pair … s_tmp1 new_pc)
494        ]]]).
495
496 (* if X=M, branch *)
497 ndefinition execute_CBEQX ≝
498 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
499  opt_map … (multi_mode_loadw … s cur_pc i)
500   (λS_M_PC.match S_M_PC with
501    [ triple s_tmp1 M_op new_pc ⇒
502     match M_op with
503      [ mk_comp_num MH_op ML_op ⇒
504       opt_map … (get_indX_8_low_reg … s_tmp1)
505        (* if X=M, branch *)
506        (λX_op.match eqc ? X_op MH_op with
507         (* new_pc = new_pc + rel *)
508         [ true ⇒ Some ? (pair … s_tmp1 (branched_pc … s_tmp1 new_pc ML_op))
509         (* new_pc = new_pc *)
510         | false ⇒ Some ? (pair … s_tmp1 new_pc)
511         ])]]).
512
513 (* C = 0 *)
514 ndefinition execute_CLC ≝
515 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
516  Some ? (pair … (set_c_flag … s false) cur_pc).
517
518 (* I = 0 *)
519 ndefinition execute_CLI ≝
520 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
521  opt_map … (set_i_flag … s false)
522   (λs_tmp.Some ? (pair … s_tmp cur_pc)).
523
524 (* M = 0 *)
525 ndefinition execute_CLR ≝
526 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
527  (* M = 0 *)
528  opt_map … (multi_mode_writeb … s cur_pc auxMode_ok i 〈x0,x0〉)
529   (λS_PC.match S_PC with
530    [ pair s_tmp1 new_pc ⇒
531    (* Z = 1 *)
532    let s_tmp2 ≝ set_z_flag … s_tmp1 true in
533    (* N = 0 *)
534    let s_tmp3 ≝ setweak_n_flag … s_tmp2 false in
535    (* V = 0 *)
536    let s_tmp4 ≝ setweak_v_flag … s_tmp3 false in
537    (* newpc = nextpc *)
538    Some ? (pair … s_tmp4 new_pc) ]).
539
540 (* flags = A - M *)
541 ndefinition execute_CMP ≝
542 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
543  execute_CMP_SBC_SUB_aux … s cur_pc i false (λC_op.λA_op.λM_op.plusc_dc_dc ? false A_op (complc ? M_op)). 
544
545 (* M = not M *)
546 ndefinition execute_COM ≝
547 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
548  execute_COM_DEC_INC_NEG_aux … s cur_pc i (notc ?)
549  (* fV = 0 *)
550  (λM7.λR7.false)
551  (* fC = 1 *)
552  (λC_op.λR_op.true).
553
554 (* flags = H:X - M *)
555 ndefinition execute_CPHX ≝
556 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
557  opt_map … (multi_mode_loadw … s cur_pc i)
558   (λS_M_PC.match S_M_PC with
559    [ triple s_tmp1 M_op new_pc ⇒
560     opt_map … (get_indX_16_reg … s_tmp1)
561      (λX_op. 
562       match plusc_dc_dc ? false X_op (complc ? M_op) with
563        [ pair carry R_op ⇒
564         let X15 ≝ getMSBc ? X_op in
565         let M15 ≝ getMSBc ? M_op in
566         let R15 ≝ getMSBc ? R_op in
567         (* Z = nR15&nR14&nR13&nR12&nR11&nR10&nR9&nR8&nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
568         let s_tmp2 ≝ set_zflw … s_tmp1 R_op in
569         (* C = nX15&M15 | M15&R15 | R15&nX15 *)
570         let s_tmp3 ≝ set_c_flag … s_tmp2 (((⊖X15)⊗M15) ⊕ (M15⊗R15) ⊕ (R15⊗(⊖X15))) in
571         (* N = R15 *) 
572         let s_tmp4 ≝ set_nflw … s_tmp3 R_op in
573         (* V = X15&nM15&nR15 | nX15&M15&R15 *)
574         let s_tmp5 ≝ setweak_v_flag … s_tmp4 ((X15⊗(⊖M15)⊗(⊖R15)) ⊕ ((⊖X15)⊗M15⊗R15)) in
575         (* newpc = nextpc *)
576         Some ? (pair … s_tmp5 new_pc) ] ) ]).
577
578 (* flags = X - M *)
579 ndefinition execute_CPX ≝
580 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
581  opt_map … (multi_mode_loadb … s cur_pc i)
582   (λS_M_PC.match S_M_PC with
583    [ triple s_tmp1 M_op new_pc ⇒
584     opt_map … (get_indX_8_low_reg … s_tmp1)
585      (λX_op. 
586       match plusc_dc_dc ? false X_op (complc ? M_op) with
587        [ pair carry R_op ⇒
588         let X7 ≝ getMSBc ? X_op in
589         let M7 ≝ getMSBc ? M_op in
590         let R7 ≝ getMSBc ? R_op in
591         (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
592         let s_tmp2 ≝ set_zflb … s_tmp1 R_op in
593         (* C = nX7&M7 | M7&R7 | R7&nX7 *)
594         let s_tmp3 ≝ set_c_flag … s_tmp2 (((⊖X7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖X7))) in
595         (* N = R7 *) 
596         let s_tmp4 ≝ set_nflb … s_tmp3 R_op in
597         (* V = X7&nM7&nR7 | nX7&M7&R7 *)
598         let s_tmp5 ≝ setweak_v_flag … s_tmp4 ((X7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖X7)⊗M7⊗R7)) in
599         (* newpc = nextpc *)
600         Some ? (pair … s_tmp5 new_pc) ] ) ]).
601
602 (* decimal adjiust A *)
603 (* per i dettagli vedere daa_b8 (modulo byte8) *)
604 ndefinition execute_DAA ≝
605 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
606  opt_map … (get_h_flag … s)
607   (λH.
608    let M_op ≝ get_acc_8_low_reg … s in
609    match daa_b8 H (get_c_flag … s) M_op with
610     [ pair carry R_op ⇒
611      (* A = R *)
612      let s_tmp1 ≝ set_acc_8_low_reg … s R_op in
613      (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
614      let s_tmp2 ≝ set_zflb … s_tmp1 R_op in
615      (* C = carry *)
616      let s_tmp3 ≝ set_c_flag … s_tmp2 carry in
617      (* N = R7 *) 
618      let s_tmp4 ≝ set_nflb … s_tmp3 R_op in
619      (* V = M7 ⊙ R7 *)
620      let s_tmp5 ≝ setweak_v_flag … s_tmp4 ((getMSBc ? M_op) ⊙ (getMSBc ? R_op)) in
621      (* newpc = curpc *)
622      Some ? (pair … s_tmp5 cur_pc) ]).
623
624 (* if (--M)≠0, branch *)
625 ndefinition execute_DBNZ ≝
626 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
627  opt_map … (multi_mode_loadw … s cur_pc i)
628   (λS_M_PC.match S_M_PC with
629    [ triple s_tmp1 M_op new_pc ⇒
630     match M_op with
631      [ mk_comp_num MH_op ML_op ⇒
632      (* --M *)
633      let MH_op' ≝ predc ? MH_op in
634      opt_map … (multi_mode_writeb … s_tmp1 cur_pc auxMode_ok i MH_op')
635       (λS_PC.match S_PC with
636        [ pair s_tmp2 _ ⇒
637         (* if (--M)≠0, branch *)
638         match eqc ? MH_op' (zeroc ?) with
639          (* new_pc = new_pc *)
640          [ true ⇒ Some ? (pair … s_tmp2 new_pc)
641          (* new_pc = new_pc + rel *)
642          | false ⇒ Some ? (pair … s_tmp2 (branched_pc … s_tmp2 new_pc ML_op)) ]])]]).
643
644 (* M = M - 1 *)
645 ndefinition execute_DEC ≝
646 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
647  execute_COM_DEC_INC_NEG_aux … s cur_pc i (predc ?)
648  (* fV = M7&nR7 *)
649  (λM7.λR7.M7⊗(⊖R7))
650  (* fC = C *)
651  (λC_op.λR_op.C_op).
652
653 (* A = H:A/X, H = H:AmodX se non c'e' overflow, altrimenti invariati *)
654 (* per i dettagli vedere div_b8 (modulo word16) *)
655 ndefinition execute_DIV ≝
656 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
657  opt_map … (get_indX_8_high_reg … s)
658   (λH_op.opt_map … (get_indX_8_low_reg … s)
659    (λX_op.match div_b8 〈H_op:(get_acc_8_low_reg … s)〉 X_op with
660     [ triple quoz rest overflow ⇒
661      (* C = overflow *)
662      let s_tmp1 ≝ set_c_flag … s overflow in
663      (* A = A o H:A/X *)
664      let s_tmp2 ≝ match overflow with
665       [ true ⇒ s_tmp1
666       | false ⇒ set_acc_8_low_reg … s_tmp1 quoz ] in
667      (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
668      (* NB: che A sia cambiato o no, lo testa *)
669      let s_tmp3 ≝ set_zflb … s_tmp2 (get_acc_8_low_reg … s_tmp2) in
670      (* H = H o H:AmodX *)
671      opt_map … (match overflow with
672                  [ true ⇒ Some ? s_tmp3
673                  | false ⇒ set_indX_8_high_reg … s_tmp3 rest])
674       (λs_tmp4.Some ? (pair … s_tmp4 cur_pc)) ])).
675
676 (* A = A ⊙ M *)
677 ndefinition execute_EOR ≝
678 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
679  execute_AND_BIT_EOR_ORA_aux … s cur_pc i true (xorc ?).
680
681 (* M = M + 1 *)
682 ndefinition execute_INC ≝
683 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
684  execute_COM_DEC_INC_NEG_aux … s cur_pc i (succc ?)
685  (* fV = nM7&R7 *)
686  (λM7.λR7.(⊖M7)⊗R7)
687  (* fC = C *)
688  (λC_op.λR_op.C_op).
689
690 (* jmp, il nuovo indirizzo e' una WORD *)
691 ndefinition execute_JMP ≝
692 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
693  opt_map … (multi_mode_loadw … s cur_pc i)
694   (λS_M_PC.
695    (* newpc = M_op *)
696    Some ? (pair … (fst3T … S_M_PC) (snd3T … S_M_PC))).
697
698 (* jump to subroutine *)
699 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
700 ndefinition execute_JSR ≝
701 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
702  opt_map … (multi_mode_loadw … s cur_pc i)
703   (λS_M_PC.match S_M_PC with
704    [ triple s_tmp1 M_op new_pc ⇒ let aux ≝
705     (* push (new_pc low) *)
706     opt_map … (aux_push … s_tmp1 (cnL ? new_pc))
707      (* push (new_pc high) *)
708      (λs_tmp2.opt_map … (aux_push … s_tmp2 (cnH ? new_pc))
709       (* newpc = M_op *)
710       (λs_tmp3.Some ? (pair … s_tmp3 M_op)))
711      in match m with
712     [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
713     | RS08 ⇒
714      (* SPC = new_pc *) 
715      opt_map … (set_spc_reg … s_tmp1 new_pc)
716       (* newpc = M_op *)
717       (λs_tmp2.Some ? (pair … s_tmp2 M_op))
718     | _ ⇒ None ?
719     ]]).
720
721 (* A = M *)
722 ndefinition execute_LDA ≝
723 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
724  opt_map … (multi_mode_loadb … s cur_pc i)
725   (λS_M_PC.match S_M_PC with
726    [ triple s_tmp1 M_op new_pc ⇒
727     (* A = M *) 
728     let s_tmp2 ≝ set_acc_8_low_reg … s_tmp1 M_op in
729     (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
730     let s_tmp3 ≝ set_zflb … s_tmp2 M_op in
731     (* N = R7 *) 
732     let s_tmp4 ≝ set_nflb … s_tmp3 M_op in
733     (* V = 0 *) 
734     let s_tmp5 ≝ setweak_v_flag … s_tmp4 false in
735     (* newpc = nextpc *)
736     Some ? (pair … s_tmp5 new_pc) ]).
737
738 (* H:X = M *)
739 ndefinition execute_LDHX ≝
740 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
741  opt_map … (multi_mode_loadw … s cur_pc i)
742   (λS_M_PC.match S_M_PC with
743    [ triple s_tmp1 M_op new_pc ⇒
744     opt_map … (set_indX_16_reg … s_tmp1 M_op)
745      (λs_tmp2.
746       (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
747       let s_tmp3 ≝ set_zflw … s_tmp2 M_op in
748       (* N = R15 *)
749       let s_tmp4 ≝ set_nflw … s_tmp3 M_op in
750       (* V = 0 *) 
751       let s_tmp5 ≝ setweak_v_flag … s_tmp4 false in
752       (* newpc = nextpc *)
753       Some ? (pair … s_tmp5 new_pc)) ]).
754
755 (* X = M *)
756 ndefinition execute_LDX ≝
757 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
758  opt_map … (multi_mode_loadb … s cur_pc i)
759   (λS_M_PC.match S_M_PC with
760    [ triple s_tmp1 M_op new_pc ⇒
761     opt_map … (set_indX_8_low_reg … s_tmp1 M_op)
762      (λs_tmp2.
763       (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
764       let s_tmp3 ≝ set_zflb … s_tmp2 M_op in
765       (* N = R7 *)
766       let s_tmp4 ≝ set_nflb … s_tmp3 M_op in
767       (* V = 0 *) 
768       let s_tmp5 ≝ setweak_v_flag … s_tmp4 false in
769       (* newpc = nextpc *)
770       Some ? (pair … s_tmp5 new_pc)) ]).
771
772 (* M = 0 -> rcr M -> C' *)
773 ndefinition execute_LSR ≝
774 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
775  execute_ASL_ASR_LSR_ROL_ROR_aux … s cur_pc i (λC_op.λM_op.rcrc ? false M_op).
776
777 (* M2 = M1 *)
778 ndefinition execute_MOV ≝
779 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
780  (* R_op = M1 *)
781  opt_map … (multi_mode_loadb … s cur_pc i)
782   (λS_R_PC.match S_R_PC with
783    [ triple s_tmp1 R_op tmp_pc ⇒
784     (* M2 = R_op *)
785     opt_map … (multi_mode_writeb … s_tmp1 tmp_pc auxMode_ok i R_op)
786      (λS_PC.match S_PC with
787       [ pair s_tmp2 new_pc ⇒
788        (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
789        let s_tmp3 ≝ set_zflb … s_tmp2 R_op in
790        (* N = R7 *)
791        let s_tmp4 ≝ set_nflb … s_tmp3 R_op in
792        (* V = 0 *) 
793        let s_tmp5 ≝ setweak_v_flag … s_tmp4 false in
794        (* newpc = nextpc *)
795        Some ? (pair … s_tmp5 new_pc)])]).
796
797 (* X:A = X * A *)
798 ndefinition execute_MUL ≝
799 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
800  opt_map … (get_indX_8_low_reg … s)
801   (λX_op.let R_op ≝ mulu_b8 X_op (get_acc_8_low_reg … s) in
802    opt_map … (set_indX_8_low_reg … s (cnH ? R_op))
803     (λs_tmp.Some ? (pair … (set_acc_8_low_reg … s_tmp (cnL ? R_op)) cur_pc))).
804
805 (* M = compl M *)
806 ndefinition execute_NEG ≝
807 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
808  execute_COM_DEC_INC_NEG_aux … s cur_pc i (complc ?)
809  (* fV = M7&R7 *)
810  (λM7.λR7.M7⊗R7)
811  (* fC = R7|R6|R5|R4|R3|R2|R1|R0 *)
812  (λC_op.λR_op.⊖(eqc ? R_op (zeroc ?))).
813
814 (* nulla *)
815 ndefinition execute_NOP ≝
816 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
817  Some ? (pair … s cur_pc).
818
819 (* A = (mk_byte8 (b8l A) (b8h A)) *)
820 (* cioe' swap del nibble alto/nibble basso di A *)
821 ndefinition execute_NSA ≝
822 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
823  match get_acc_8_low_reg … s with [ mk_comp_num ah al ⇒
824   (* A = (mk_byte8 (b8l A) (b8h A)) *)
825   Some ? (pair … (set_acc_8_low_reg … s 〈al,ah〉) cur_pc) ].
826
827 (* A = A | M *)
828 ndefinition execute_ORA ≝
829 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
830  execute_AND_BIT_EOR_ORA_aux … s cur_pc i true (orc ?).
831
832 (* push A *)
833 ndefinition execute_PSHA ≝
834 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
835  opt_map … (aux_push … s (get_acc_8_low_reg … s))
836   (λs_tmp1.Some ? (pair … s_tmp1 cur_pc)).
837
838 (* push H *)
839 ndefinition execute_PSHH ≝
840 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
841  opt_map … (get_indX_8_high_reg … s)
842   (λH_op.opt_map … (aux_push … s H_op)
843    (λs_tmp1.Some ? (pair … s_tmp1 cur_pc))).
844
845 (* push X *)
846 ndefinition execute_PSHX ≝
847 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
848  opt_map … (get_indX_8_low_reg … s)
849   (λH_op.opt_map … (aux_push … s H_op)
850    (λs_tmp1.Some ? (pair … s_tmp1 cur_pc))).
851
852 (* pop A *)
853 ndefinition execute_PULA ≝
854 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
855  opt_map … (aux_pop … s)
856   (λS_and_A.match S_and_A with [ pair s_tmp1 A_op ⇒
857    Some ? (pair … (set_acc_8_low_reg … s_tmp1 A_op) cur_pc) ]).
858
859 (* pop H *)
860 ndefinition execute_PULH ≝
861 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
862  opt_map … (aux_pop … s)
863   (λS_and_H.match S_and_H with [ pair s_tmp1 H_op ⇒
864    opt_map … (set_indX_8_high_reg … s_tmp1 H_op)
865     (λs_tmp2.Some ? (pair … s_tmp2 cur_pc))]).
866
867 (* pop X *)
868 ndefinition execute_PULX ≝
869 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
870  opt_map … (aux_pop … s)
871   (λS_and_X.match S_and_X with [ pair s_tmp1 X_op ⇒
872    opt_map … (set_indX_8_low_reg … s_tmp1 X_op)
873     (λs_tmp2.Some ? (pair … s_tmp2 cur_pc))]).
874
875 (* M = C' <- rcl M <- C *)
876 ndefinition execute_ROL ≝
877 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
878  execute_ASL_ASR_LSR_ROL_ROR_aux … s cur_pc i (rclc ?).
879
880 (* M = C -> rcr M -> C' *)
881 ndefinition execute_ROR ≝
882 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
883  execute_ASL_ASR_LSR_ROL_ROR_aux … s cur_pc i (rcrc ?).
884
885 (* SP = 0xuuFF *)
886 (* lascia inalterato il byte superiore di SP *)
887 ndefinition execute_RSP ≝
888 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
889  opt_map … (get_sp_reg … s)
890   (λSP_op.match SP_op with [ mk_comp_num sph spl ⇒
891    opt_map … (set_sp_reg … s 〈sph:〈xF,xF〉〉)
892     (λs_tmp.Some ? (pair … s_tmp cur_pc))]).
893
894 (* return from interrupt *)
895 ndefinition execute_RTI ≝
896 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
897  (* pop (CCR) *)
898  opt_map … (aux_pop … s)
899   (λS_and_CCR.match S_and_CCR with [ pair s_tmp1 CCR_op ⇒
900    let s_tmp2 ≝ aux_set_CCR … s_tmp1 CCR_op in
901    (* pop (A) *)
902    opt_map … (aux_pop … s_tmp2)
903     (λS_and_A.match S_and_A with [ pair s_tmp3 A_op ⇒
904      let s_tmp4 ≝ set_acc_8_low_reg … s_tmp3 A_op in
905      (* pop (X) *)
906      opt_map … (aux_pop … s_tmp4)
907       (λS_and_X.match S_and_X with [ pair s_tmp5 X_op ⇒
908        opt_map … (set_indX_8_low_reg … s_tmp5 X_op)
909         (* pop (PC high) *)
910         (λs_tmp6.opt_map … (aux_pop … s_tmp6)
911          (λS_and_PCH.match S_and_PCH with [ pair s_tmp7 PCH_op ⇒
912           (* pop (PC low) *)
913           opt_map … (aux_pop … s_tmp7)
914            (λS_and_PCL.match S_and_PCL with [ pair s_tmp8 PCL_op ⇒
915             Some ? (pair … s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
916
917 (* return from subroutine *)
918 (* HC05/HC08/HCS08 si appoggia allo stack, RS08 si appoggia a SPC *)
919 ndefinition execute_RTS ≝
920 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
921  let aux ≝
922   (* pop (PC high) *)
923   opt_map … (aux_pop … s)
924    (λS_and_PCH.match S_and_PCH with [ pair s_tmp1 PCH_op ⇒
925     (* pop (PC low) *)
926     opt_map … (aux_pop … s_tmp1)
927      (λS_and_PCL.match S_and_PCL with [ pair s_tmp2 PCL_op ⇒
928       Some ? (pair … s_tmp2 〈PCH_op:PCL_op〉)])])
929  in match m with
930   [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
931   | RS08 ⇒
932    (* new_pc = SPC *)
933    opt_map … (get_spc_reg … s)
934     (λSPC_op.Some ? (pair … s SPC_op))
935   | _ ⇒ None ?
936   ].
937
938 (* A = A - M - C *)
939 ndefinition execute_SBC ≝
940 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
941  execute_CMP_SBC_SUB_aux … s cur_pc i true
942  (λC_op.λA_op.λM_op.match plusc_dc_dc ? false A_op (complc ? M_op) with
943   [ pair resc resb ⇒ match C_op with
944    [ true ⇒ plusc_dc_dc ? false resb 〈xF,xF〉
945    | false ⇒ pair … resc resb ]]).
946
947 (* C = 1 *)
948 ndefinition execute_SEC ≝
949 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
950  Some ? (pair … (set_c_flag … s true) cur_pc).
951
952 (* I = 1 *)
953 ndefinition execute_SEI ≝
954 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
955  opt_map … (set_i_flag … s true)
956   (λs_tmp.Some ? (pair … s_tmp cur_pc)).
957
958 (* swap SPCh,A *)
959 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
960           fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
961           occore accedere a SPC e salvarne il contenuto *)
962 ndefinition execute_SHA ≝
963 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
964  opt_map … (get_spc_reg … s)
965   (λSPC_op.opt_map … (set_spc_reg … s 〈(get_acc_8_low_reg … s):(cnL ? SPC_op)〉)
966    (λs_tmp1.Some ? (pair … (set_acc_8_low_reg … s_tmp1 (cnH ? SPC_op)) cur_pc))).
967
968 (* swap SPCl,A *)
969 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
970           fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
971           occore accedere a SPC e salvarne il contenuto *)
972 ndefinition execute_SLA ≝
973 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
974  opt_map … (get_spc_reg … s)
975   (λSPC_op.opt_map … (set_spc_reg … s 〈(cnH ? SPC_op):(get_acc_8_low_reg … s)〉)
976    (λs_tmp1.Some ? (pair … (set_acc_8_low_reg … s_tmp1 (cnL ? SPC_op)) cur_pc))).
977
978 (* M = A *)
979 ndefinition execute_STA ≝
980 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
981  (* M = A *)
982  let A_op ≝ (get_acc_8_low_reg … s) in
983  opt_map … (multi_mode_writeb … s cur_pc auxMode_ok i A_op)
984   (λS_op_and_PC.match S_op_and_PC with
985    [ pair s_tmp1 new_pc ⇒
986    (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
987    let s_tmp2 ≝ set_zflb … s_tmp1 A_op in
988    (* N = A7 *)
989    let s_tmp3 ≝ set_nflb … s_tmp2 A_op in
990    (* V = 0 *)
991    let s_tmp4 ≝ setweak_v_flag … s_tmp3 false in
992    (* newpc = nextpc *)
993    Some ? (pair … s_tmp4 new_pc) ]).
994
995 (* M = H:X *)
996 ndefinition execute_STHX ≝
997 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
998  (* M = H:X *)
999  opt_map … (get_indX_16_reg … s)
1000   (λX_op.opt_map … (multi_mode_writew … s cur_pc i X_op)
1001    (λS_op_and_PC.match S_op_and_PC with
1002     [ pair s_tmp1 new_pc ⇒
1003      (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1004      let s_tmp2 ≝ set_zflw … s_tmp1 X_op in
1005      (* N = R15 *)
1006      let s_tmp3 ≝ set_nflw … s_tmp2 X_op in
1007      (* V = 0 *)
1008      let s_tmp4 ≝ setweak_v_flag … s_tmp3 false in
1009      (* newpc = nextpc *)
1010       Some ? (pair … s_tmp4 new_pc) ])).
1011
1012 (* I = 0 *)
1013 ndefinition execute_STOP ≝
1014 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1015  Some ? (pair … (setweak_i_flag … s false) cur_pc).
1016
1017 (* M = X *)
1018 ndefinition execute_STX ≝
1019 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1020  (* M = X *)
1021  opt_map … (get_indX_8_low_reg … s)
1022   (λX_op.opt_map … (multi_mode_writeb … s cur_pc auxMode_ok i X_op)
1023    (λS_op_and_PC.match S_op_and_PC with
1024     [ pair s_tmp1 new_pc ⇒
1025      (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1026      let s_tmp2 ≝ set_zflb … s_tmp1 X_op in
1027      (* N = R7 *)
1028      let s_tmp3 ≝ set_nflb … s_tmp2 X_op in
1029      (* V = 0 *)
1030      let s_tmp4 ≝ setweak_v_flag … s_tmp3 false in
1031      (* newpc = nextpc *)
1032      Some ? (pair … s_tmp4 new_pc) ])).
1033
1034 (* A = A - M *)
1035 ndefinition execute_SUB ≝
1036 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1037  execute_CMP_SBC_SUB_aux … s cur_pc i true (λC_op.λA_op.λM_op.plusc_dc_dc ? false A_op (complc ? M_op)).
1038
1039 (* software interrupt *)
1040 ndefinition execute_SWI ≝
1041 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1042  (* indirizzo da cui caricare il nuovo pc *)
1043  let vector ≝ get_pc_reg … (set_pc_reg … s 〈〈xF,xF〉:〈xF,xC〉〉) in
1044  (* push (cur_pc low) *)
1045  opt_map … (aux_push … s (cnL ? cur_pc))
1046   (* push (cur_pc high *)
1047   (λs_tmp1.opt_map … (aux_push … s_tmp1 (cnH ? cur_pc))
1048    (λs_tmp2.opt_map … (get_indX_8_low_reg … s_tmp2)
1049     (* push (X) *)
1050     (λX_op.opt_map … (aux_push … s_tmp2 X_op)
1051      (* push (A) *)
1052      (λs_tmp3.opt_map … (aux_push … s_tmp3 (get_acc_8_low_reg … s_tmp3))
1053       (* push (CCR) *)
1054       (λs_tmp4.opt_map … (aux_push … s_tmp4 (aux_get_CCR … s_tmp4))
1055        (* I = 1 *)
1056        (λs_tmp5.opt_map … (set_i_flag … s_tmp5 true)
1057         (* load from vector high *)
1058         (λs_tmp6.opt_map … (memory_filter_read … s_tmp6 vector)
1059          (* load from vector low *)
1060          (λaddrh.opt_map … (memory_filter_read … s_tmp6 (succc ? vector))
1061           (* newpc = [vector] *)
1062           (λaddrl.Some ? (pair … s_tmp6 〈addrh:addrl〉)))))))))).
1063
1064 (* flags = A *)
1065 ndefinition execute_TAP ≝
1066 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1067  Some ? (pair … (aux_set_CCR … s (get_acc_8_low_reg … s)) cur_pc). 
1068
1069 (* X = A *)
1070 ndefinition execute_TAX ≝
1071 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1072  opt_map … (set_indX_8_low_reg … s (get_acc_8_low_reg … s))
1073   (λs_tmp.Some ? (pair … s_tmp cur_pc)).
1074
1075 (* A = flags *)
1076 ndefinition execute_TPA ≝
1077 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1078  Some ? (pair … (set_acc_8_low_reg … s (aux_get_CCR … s)) cur_pc).
1079
1080 (* flags = M - 0 *)
1081 (* implementata senza richiamare la sottrazione, la modifica dei flag
1082    e' immediata *)
1083 ndefinition execute_TST ≝
1084 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1085  opt_map … (multi_mode_loadb … s cur_pc i)
1086   (λS_M_PC.match S_M_PC with
1087    [ triple s_tmp1 M_op new_pc ⇒
1088     (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1089     let s_tmp2 ≝ set_zflb … s_tmp1 M_op in
1090     (* N = R7 *) 
1091     let s_tmp3 ≝ set_nflb … s_tmp2 M_op in
1092     (* V = 0 *) 
1093     let s_tmp4 ≝ setweak_v_flag … s_tmp3 false in
1094     (* newpc = nextpc *)
1095     Some ? (pair … s_tmp4 new_pc) ]).
1096
1097 (* H:X = SP + 1 *)
1098 ndefinition execute_TSX ≝
1099 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1100  opt_map … (get_sp_reg … s )
1101   (λSP_op.opt_map … (set_indX_16_reg … s (succc ? SP_op))
1102    (* H:X = SP + 1 *)
1103    (λs_tmp.Some ? (pair … s_tmp cur_pc))).
1104
1105 (* A = X *)
1106 ndefinition execute_TXA ≝
1107 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1108  opt_map … (get_indX_8_low_reg … s)
1109   (λX_op.Some ? (pair … (set_acc_8_low_reg … s X_op) cur_pc)).
1110
1111 (* SP = H:X - 1 *)
1112 ndefinition execute_TXS ≝
1113 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1114  opt_map … (get_indX_16_reg … s )
1115   (λX_op.opt_map … (set_sp_reg … s (predc ? X_op))
1116    (* SP = H:X - 1 *)
1117    (λs_tmp.Some ? (pair … s_tmp cur_pc))).
1118
1119 (* I = 0 *)
1120 ndefinition execute_WAIT ≝
1121 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
1122  Some ? (pair … (setweak_i_flag … s false) cur_pc).
1123
1124 (* raccordo *)
1125 ndefinition Freescale_execute_any ≝
1126 λps:Freescale_pseudo.match ps with
1127   [ ADC    ⇒ execute_ADC    (* add with carry *)
1128   | ADD    ⇒ execute_ADD    (* add *)
1129   | AIS    ⇒ execute_AIS    (* add immediate to SP *)
1130   | AIX    ⇒ execute_AIX    (* add immediate to X *)
1131   | AND    ⇒ execute_AND    (* and *)
1132   | ASL    ⇒ execute_ASL    (* aritmetic shift left *)
1133   | ASR    ⇒ execute_ASR    (* aritmetic shift right *)
1134   | BCC    ⇒ execute_BCC    (* branch if C=0 *)
1135   | BCLRn  ⇒ execute_BCLRn  (* clear bit n *)
1136   | BCS    ⇒ execute_BCS    (* branch if C=1 *)
1137   | BEQ    ⇒ execute_BEQ    (* branch if Z=1 *)
1138   | BGE    ⇒ execute_BGE    (* branch if N⊙V=0 (great or equal) *)
1139   | BGND   ⇒ execute_BGND   (* !!background mode!!*)
1140   | BGT    ⇒ execute_BGT    (* branch if Z|N⊙V=0 clear (great) *)
1141   | BHCC   ⇒ execute_BHCC   (* branch if H=0 *)
1142   | BHCS   ⇒ execute_BHCS   (* branch if H=1 *)
1143   | BHI    ⇒ execute_BHI    (* branch if C|Z=0, (higher) *)
1144   | BIH    ⇒ execute_BIH    (* branch if nIRQ=1 *)
1145   | BIL    ⇒ execute_BIL    (* branch if nIRQ=0 *)
1146   | BIT    ⇒ execute_BIT    (* flag = and (bit test) *)
1147   | BLE    ⇒ execute_BLE    (* branch if Z|N⊙V=1 (less or equal) *)
1148   | BLS    ⇒ execute_BLS    (* branch if C|Z=1 (lower or same) *)
1149   | BLT    ⇒ execute_BLT    (* branch if N⊙1=1 (less) *)
1150   | BMC    ⇒ execute_BMC    (* branch if I=0 (interrupt mask clear) *)
1151   | BMI    ⇒ execute_BMI    (* branch if N=1 (minus) *)
1152   | BMS    ⇒ execute_BMS    (* branch if I=1 (interrupt mask set) *)
1153   | BNE    ⇒ execute_BNE    (* branch if Z=0 *)
1154   | BPL    ⇒ execute_BPL    (* branch if N=0 (plus) *)
1155   | BRA    ⇒ execute_BRA    (* branch always *)
1156   | BRCLRn ⇒ execute_BRCLRn (* branch if bit n clear *)
1157   | BRN    ⇒ execute_BRN    (* branch never (nop) *)
1158   | BRSETn ⇒ execute_BRSETn (* branch if bit n set *)
1159   | BSETn  ⇒ execute_BSETn  (* set bit n *)
1160   | BSR    ⇒ execute_BSR    (* branch to subroutine *)
1161   | CBEQA  ⇒ execute_CBEQA  (* compare (A) and BEQ *)
1162   | CBEQX  ⇒ execute_CBEQX  (* compare (X) and BEQ *)
1163   | CLC    ⇒ execute_CLC    (* C=0 *)
1164   | CLI    ⇒ execute_CLI    (* I=0 *)
1165   | CLR    ⇒ execute_CLR    (* operand=0 *)
1166   | CMP    ⇒ execute_CMP    (* flag = sub (compare A) *)
1167   | COM    ⇒ execute_COM    (* not (1 complement) *)
1168   | CPHX   ⇒ execute_CPHX   (* flag = sub (compare H:X) *)
1169   | CPX    ⇒ execute_CPX    (* flag = sub (compare X) *)
1170   | DAA    ⇒ execute_DAA    (* decimal adjust A *)
1171   | DBNZ   ⇒ execute_DBNZ   (* dec and BNE *)
1172   | DEC    ⇒ execute_DEC    (* operand=operand-1 (decrement) *)
1173   | DIV    ⇒ execute_DIV    (* div *)
1174   | EOR    ⇒ execute_EOR    (* xor *)
1175   | INC    ⇒ execute_INC    (* operand=operand+1 (increment) *)
1176   | JMP    ⇒ execute_JMP    (* jmp word [operand] *)
1177   | JSR    ⇒ execute_JSR    (* jmp to subroutine *)
1178   | LDA    ⇒ execute_LDA    (* load in A *)
1179   | LDHX   ⇒ execute_LDHX   (* load in H:X *)
1180   | LDX    ⇒ execute_LDX    (* load in X *)
1181   | LSR    ⇒ execute_LSR    (* logical shift right *)
1182   | MOV    ⇒ execute_MOV    (* move *)
1183   | MUL    ⇒ execute_MUL    (* mul *)
1184   | NEG    ⇒ execute_NEG    (* neg (2 complement) *)
1185   | NOP    ⇒ execute_NOP    (* nop *)
1186   | NSA    ⇒ execute_NSA    (* nibble swap A (al:ah <- ah:al) *)
1187   | ORA    ⇒ execute_ORA    (* or *)
1188   | PSHA   ⇒ execute_PSHA   (* push A *)
1189   | PSHH   ⇒ execute_PSHH   (* push H *)
1190   | PSHX   ⇒ execute_PSHX   (* push X *)
1191   | PULA   ⇒ execute_PULA   (* pop A *)
1192   | PULH   ⇒ execute_PULH   (* pop H *)
1193   | PULX   ⇒ execute_PULX   (* pop X *)
1194   | ROL    ⇒ execute_ROL    (* rotate left *)
1195   | ROR    ⇒ execute_ROR    (* rotate right *)
1196   | RSP    ⇒ execute_RSP    (* reset SP (0x00FF) *)
1197   | RTI    ⇒ execute_RTI    (* return from interrupt *)
1198   | RTS    ⇒ execute_RTS    (* return from subroutine *)
1199   | SBC    ⇒ execute_SBC    (* sub with carry*)
1200   | SEC    ⇒ execute_SEC    (* C=1 *)
1201   | SEI    ⇒ execute_SEI    (* I=1 *)
1202   | SHA    ⇒ execute_SHA    (* swap spc_high,A *)
1203   | SLA    ⇒ execute_SLA    (* swap spc_low,A *)
1204   | STA    ⇒ execute_STA    (* store from A *)
1205   | STHX   ⇒ execute_STHX   (* store from H:X *)
1206   | STOP   ⇒ execute_STOP   (* !!stop mode!! *)
1207   | STX    ⇒ execute_STX    (* store from X *)
1208   | SUB    ⇒ execute_SUB    (* sub *)
1209   | SWI    ⇒ execute_SWI    (* software interrupt *)
1210   | TAP    ⇒ execute_TAP    (* flag=A (transfer A to process status byte *)
1211   | TAX    ⇒ execute_TAX    (* X=A (transfer A to X) *)
1212   | TPA    ⇒ execute_TPA    (* A=flag (transfer process status byte to A) *)
1213   | TST    ⇒ execute_TST    (* flag = sub (test) *)
1214   | TSX    ⇒ execute_TSX    (* X:H=SP (transfer SP to H:X) *)
1215   | TXA    ⇒ execute_TXA    (* A=X (transfer X to A) *)
1216   | TXS    ⇒ execute_TXS    (* SP=X:H (transfer H:X to SP) *)
1217   | WAIT   ⇒ execute_WAIT   (* !!wait mode!!*)
1218   ].
1219
1220 (* stati speciali di esecuzione *)
1221 ndefinition Freescale_check_susp ≝
1222 λps:Freescale_pseudo.match ps with
1223  [ BGND ⇒ Some ? BGND_MODE
1224  | STOP ⇒ Some ? STOP_MODE
1225  | WAIT ⇒ Some ? WAIT_MODE
1226  | _ ⇒ None ?
1227  ].
1228
1229 (* istruzioni speciali per skip *)
1230 ndefinition Freescale_check_skip ≝
1231 λps:Freescale_pseudo.false.
1232
1233 (* motiplicatore del ciclo di durata *)
1234 ndefinition Freescale_clk_mult ≝
1235 λm,t.λs:any_status m t.nat1.