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