helm/software/matita/contribs/ng_assembly/freescale/multivm.ma

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