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