definition execute_ADC_ADD_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
definition execute_ADC_ADD_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
definition execute_AND_BIT_EOR_ORA_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
λfAM:byte8 → byte8 → byte8.
definition execute_AND_BIT_EOR_ORA_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
λfAM:byte8 → byte8 → byte8.
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
let R_op ≝ fAM (get_acc_8_low_reg m t s_tmp1) M_op in
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
let R_op ≝ fAM (get_acc_8_low_reg m t s_tmp1) M_op in
definition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
λfMC:byte8 → bool → Prod byte8 bool.
definition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
λfMC:byte8 → bool → Prod byte8 bool.
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op _ ⇒
match fMC M_op (get_c_flag m t s_tmp1) with [ pair R_op carry ⇒
(* M = fMC(M,C) *)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op _ ⇒
match fMC M_op (get_c_flag m t s_tmp1) with [ pair R_op carry ⇒
(* M = fMC(M,C) *)
(* tutti i branch calcoleranno la condizione e la passeranno qui *)
definition execute_any_BRANCH ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:bool.
(* tutti i branch calcoleranno la condizione e la passeranno qui *)
definition execute_any_BRANCH ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:bool.
definition execute_BCLRn_BSETn_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λoptval:byte8.
(* Mn = filtered optval *)
definition execute_BCLRn_BSETn_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λoptval:byte8.
(* Mn = filtered optval *)
(* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
definition execute_BRCLRn_BRSETn_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:byte8 → bool.
(* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
definition execute_BRCLRn_BRSETn_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:byte8 → bool.
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒ match M_op with
[ mk_word16 MH_op ML_op ⇒
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒ match M_op with
[ mk_word16 MH_op ML_op ⇒
definition execute_COM_DEC_INC_NEG_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
λfM:byte8 → byte8.λfV:bool → bool → bool.λfC:bool → byte8 → bool.
definition execute_COM_DEC_INC_NEG_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
λfM:byte8 → byte8.λfV:bool → bool → bool.λfC:bool → byte8 → bool.
definition execute_SBC_SUB_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
definition execute_SBC_SUB_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (get_sp_reg m t s_tmp1)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (get_sp_reg m t s_tmp1)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (get_indX_16_reg m t s_tmp1)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (get_indX_16_reg m t s_tmp1)
(* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
definition execute_BSR ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t .λi:instr_mode.λcur_pc:word16.
(* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
definition execute_BSR ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t .λi:instr_mode.λcur_pc:word16.
(* if A=M, branch *)
definition execute_CBEQA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* if A=M, branch *)
definition execute_CBEQA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* if X=M, branch *)
definition execute_CBEQX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* if X=M, branch *)
definition execute_CBEQX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (get_indX_16_reg m t s_tmp1)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (get_indX_16_reg m t s_tmp1)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (get_indX_8_low_reg m t s_tmp1)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (get_indX_8_low_reg m t s_tmp1)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
match M_op with
[ mk_word16 MH_op ML_op ⇒
(* --M *)
let MH_op' ≝ pred_b8 MH_op in
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
match M_op with
[ mk_word16 MH_op ML_op ⇒
(* --M *)
let MH_op' ≝ pred_b8 MH_op in
(* jmp, il nuovo indirizzo e' una WORD *)
definition execute_JMP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* jmp, il nuovo indirizzo e' una WORD *)
definition execute_JMP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
definition execute_JSR ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
definition execute_JSR ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (set_indX_16_reg m t s_tmp1 M_op)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (set_indX_16_reg m t s_tmp1 M_op)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (set_indX_8_low_reg m t s_tmp1 M_op)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (set_indX_8_low_reg m t s_tmp1 M_op)
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* M = A *)
let A_op ≝ (get_acc_8_low_reg m t s) in
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* M = A *)
let A_op ≝ (get_acc_8_low_reg m t s) in
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* M = H:X *)
opt_map ?? (get_indX_16_reg m t s)
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* M = H:X *)
opt_map ?? (get_indX_16_reg m t s)
(λS_op_and_PC.match S_op_and_PC with
[ pair s_tmp1 new_pc ⇒
(* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
(λS_op_and_PC.match S_op_and_PC with
[ pair s_tmp1 new_pc ⇒
(* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* M = X *)
opt_map ?? (get_indX_8_low_reg m t s)
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* M = X *)
opt_map ?? (get_indX_8_low_reg m t s)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)