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.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λ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.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λ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.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λ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) *)
- opt_map ?? (multi_mode_write m t true s_tmp1 cur_pc i R_op)
+ opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
(λS_PC.match S_PC with
[ pair s_tmp2 new_pc ⇒
(* C = carry *)
(* 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.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
(* if true, branch *)
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 *)
- opt_map ?? (multi_mode_write m t true s cur_pc i optval)
+ opt_map ?? (multi_mode_write true m t s cur_pc i optval)
(λS_PC.match S_PC with
(* newpc = nextpc *)
[ pair s_tmp1 new_pc ⇒ Some ? (pair ?? s_tmp1 new_pc) ]).
(* 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.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
(λ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.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op _ ⇒
let R_op ≝ fM M_op in
(* M = fM(M) *)
- opt_map ?? (multi_mode_write m t true s_tmp1 cur_pc i R_op)
+ opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
(λS_PC.match S_PC with
[ pair s_tmp2 new_pc ⇒
(* C = fCR (C,R) *)
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.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λ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
(* SP += extended M *)
definition execute_AIS ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
opt_map ?? (get_sp_reg m t s_tmp1)
(* H:X += extended M *)
definition execute_AIX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λ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.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒ let aux ≝
(* push (new_pc low) *)
(* if A=M, branch *)
definition execute_CBEQA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
match M_op with
(* if X=M, branch *)
definition execute_CBEQX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
match M_op with
definition execute_CLR ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* M = 0 *)
- opt_map ?? (multi_mode_write m t true s cur_pc i 〈x0,x0〉)
+ opt_map ?? (multi_mode_write true m t s cur_pc i 〈x0,x0〉)
(λS_PC.match S_PC with
[ pair s_tmp1 new_pc ⇒
(* Z = 1 *)
(* flags = H:X - M *)
definition execute_CPHX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
(λ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)
(* flags = X - M *)
definition execute_CPX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λ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)
(* if (--M)≠0, branch *)
definition execute_DBNZ ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
(λ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
- opt_map ?? (multi_mode_write m t true s_tmp1 cur_pc i MH_op')
+ opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i MH_op')
(λS_PC.match S_PC with
[ pair s_tmp2 _ ⇒
(* if (--M)≠0, branch *)
(* 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.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
(λS_M_PC.
(* newpc = M_op *)
Some ? (pair ?? (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
(* 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.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒ let aux ≝
(* push (new_pc low) *)
(* A = M *)
definition execute_LDA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
(* A = M *)
(* H:X = M *)
definition execute_LDHX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t false s cur_pc i)
+ opt_map ?? (multi_mode_load false m t s cur_pc i)
(λ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)
(* X = M *)
definition execute_LDX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λ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)
definition execute_MOV ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* R_op = M1 *)
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λS_R_PC.match S_R_PC with
[ tripleT s_tmp1 R_op tmp_pc ⇒
(* M2 = R_op *)
- opt_map ?? (multi_mode_write m t true s_tmp1 tmp_pc i R_op)
+ opt_map ?? (multi_mode_write true m t s_tmp1 tmp_pc i R_op)
(λS_PC.match S_PC with
[ pair s_tmp2 new_pc ⇒
(* Z = nR7&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 = A *)
let A_op ≝ (get_acc_8_low_reg m t s) in
- opt_map ?? (multi_mode_write m t true s cur_pc i A_op)
+ opt_map ?? (multi_mode_write true m t s cur_pc i A_op)
(λS_op_and_PC.match S_op_and_PC with
[ pair s_tmp1 new_pc ⇒
(* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
λ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)
- (λX_op.opt_map ?? (multi_mode_write m t false s cur_pc i X_op)
+ (λX_op.opt_map ?? (multi_mode_write false m t s cur_pc i X_op)
(λ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)
- (λX_op.opt_map ?? (multi_mode_write m t true s cur_pc i X_op)
+ (λX_op.opt_map ?? (multi_mode_write true m t s cur_pc i X_op)
(λS_op_and_PC.match S_op_and_PC with
[ pair s_tmp1 new_pc ⇒
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
e' immediata *)
definition execute_TST ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load m t true s cur_pc i)
+ opt_map ?? (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)