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.