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