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