ndefinition 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 → ProdT byte8 bool.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
(* V = A7&M7&nR7 | nA7&nM7&R7 *)
let s_tmp7 ≝ setweak_v_flag m t s_tmp6 ((A7⊗M7⊗(⊖R7)) ⊕ ((⊖A7)⊗(⊖M7)⊗R7)) in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp7 new_pc) ]]).
+ Some ? (pair … s_tmp7 new_pc) ]]).
(* A = [true] fAM(A,M), [false] A *)
(* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
ndefinition 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 true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
let R_op ≝ fAM (get_acc_8_low_reg m t s_tmp1) M_op in
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp5 new_pc) ]).
+ Some ? (pair … s_tmp5 new_pc) ]).
(* M = fMC(M,C) *)
(* fMC e' la logica da applicare: rc_/ro_/sh_ *)
ndefinition 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 → ProdT byte8 bool.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple 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 true m t 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 *)
(* V = R7 ⊙ carry *)
let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((MSB_b8 R_op) ⊙ carry) in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp6 new_pc) ])]]).
+ Some ? (pair … s_tmp6 new_pc) ])]]).
(* estensione del segno byte → word *)
ndefinition byte_extension ≝
(* tutti i branch calcoleranno la condizione e la passeranno qui *)
ndefinition 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 true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
(* if true, branch *)
match fCOND with
(* newpc = nextpc + rel *)
- [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc M_op))
+ [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc M_op))
(* newpc = nextpc *)
- | false ⇒ Some ? (pair ?? s_tmp1 new_pc) ]]).
+ | false ⇒ Some ? (pair … s_tmp1 new_pc) ]]).
(* Mn = filtered optval *)
(* il chiamante passa 0x00 per azzerare, 0xFF per impostare il bit di M *)
ndefinition 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 true m t 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) ]).
+ [ pair s_tmp1 new_pc ⇒ Some ? (pair … s_tmp1 new_pc) ]).
(* if COND(Mn) branch *)
(* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
ndefinition 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 false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒ match M_op with
[ mk_word16 MH_op ML_op ⇒
(* if COND(Mn) branch *)
match fCOND MH_op with
(* newpc = nextpc + rel *)
- [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+ [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
(* newpc = nextpc *)
- | false ⇒ Some ? (pair ?? s_tmp1 new_pc) ]]]).
+ | false ⇒ Some ? (pair … s_tmp1 new_pc) ]]]).
(* M = fM(M) *)
(* fM e' la logica da applicare: not/neg/++/-- *)
ndefinition 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 true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op _ ⇒
let R_op ≝ fM M_op in
(* M = fM(M) *)
- opt_map ?? (multi_mode_write true m t 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) *)
(* V = fV (M7,R7) *)
let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (fV (MSB_b8 M_op) (MSB_b8 R_op)) in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp6 new_pc) ])]).
+ Some ? (pair … s_tmp6 new_pc) ])]).
(* A = [true] fAMC(A,M,C), [false] A *)
(* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
ndefinition 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 → ProdT byte8 bool.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
(* V = A7&nM7&nR7 | nA7&M7&R7 *)
let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((A7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖A7)⊗M7⊗R7)) in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp6 new_pc) ]]).
+ Some ? (pair … s_tmp6 new_pc) ]]).
(* il classico push *)
ndefinition aux_push ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
- opt_map ?? (get_sp_reg m t s)
+ opt_map … (get_sp_reg m t s)
(* [SP] = val *)
- (λSP_op.opt_map ?? (memory_filter_write m t s SP_op val)
+ (λSP_op.opt_map … (memory_filter_write m t s SP_op val)
(* SP -- *)
- (λs_tmp1.opt_map ?? (set_sp_reg m t s_tmp1 (pred_w16 SP_op))
+ (λs_tmp1.opt_map … (set_sp_reg m t s_tmp1 (pred_w16 SP_op))
(λs_tmp2.Some ? s_tmp2))).
(* il classico pop *)
(* NB: l'incremento di SP deve essere filtrato dalla ALU, quindi get(set(SP)) *)
ndefinition aux_pop ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.
- opt_map ?? (get_sp_reg m t s)
+ opt_map … (get_sp_reg m t s)
(* SP ++ *)
- (λSP_op.opt_map ?? (set_sp_reg m t s (succ_w16 SP_op))
- (λs_tmp1.opt_map ?? (get_sp_reg m t s_tmp1)
+ (λSP_op.opt_map … (set_sp_reg m t s (succ_w16 SP_op))
+ (λs_tmp1.opt_map … (get_sp_reg m t s_tmp1)
(* val = [SP] *)
- (λSP_op'.opt_map ?? (memory_filter_read m t s_tmp1 SP_op')
- (λval.Some ? (pair ?? s_tmp1 val))))).
+ (λSP_op'.opt_map … (memory_filter_read m t s_tmp1 SP_op')
+ (λval.Some ? (pair … s_tmp1 val))))).
(* CCR corrisponde a V11HINZC e cmq 1 se un flag non esiste *)
(* i flag mantengono posizione costante nelle varie ALU, e se non sono
(* SP += extended M *)
ndefinition execute_AIS ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
- opt_map ?? (get_sp_reg m t s_tmp1)
+ opt_map … (get_sp_reg m t s_tmp1)
(* SP += extended M *)
- (λSP_op.opt_map ?? (set_sp_reg m t s_tmp1 (plus_w16_d_d SP_op (byte_extension M_op)))
- (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
+ (λSP_op.opt_map … (set_sp_reg m t s_tmp1 (plus_w16_d_d SP_op (byte_extension M_op)))
+ (λs_tmp2.Some ? (pair … s_tmp2 new_pc))) ]).
(* H:X += extended M *)
ndefinition execute_AIX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
- opt_map ?? (get_indX_16_reg m t s_tmp1)
+ opt_map … (get_indX_16_reg m t s_tmp1)
(* H:X += extended M *)
- (λHX_op.opt_map ?? (set_indX_16_reg m t s_tmp1 (plus_w16_d_d HX_op (byte_extension M_op)))
- (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
+ (λHX_op.opt_map … (set_indX_16_reg m t s_tmp1 (plus_w16_d_d HX_op (byte_extension M_op)))
+ (λs_tmp2.Some ? (pair … s_tmp2 new_pc))) ]).
(* A = A & M *)
ndefinition execute_AND ≝
(* if N⊙V=0, branch *)
ndefinition execute_BGE ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
- (λN_op.opt_map ?? (get_v_flag m t s)
+ opt_map … (get_n_flag m t s)
+ (λN_op.opt_map … (get_v_flag m t s)
(λV_op.execute_any_BRANCH m t s i cur_pc (⊖(N_op ⊙ V_op)))).
(* BGND mode *)
ndefinition execute_BGND ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? s cur_pc).
+ Some ? (pair … s cur_pc).
(* if Z|N⊙V=0, branch *)
ndefinition execute_BGT ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
- (λN_op.opt_map ?? (get_v_flag m t s)
+ opt_map … (get_n_flag m t s)
+ (λN_op.opt_map … (get_v_flag m t s)
(λV_op.execute_any_BRANCH m t s i cur_pc (⊖((get_z_flag m t s) ⊕ (N_op ⊙ V_op))))).
(* if H=0, branch *)
ndefinition execute_BHCC ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_h_flag m t s)
+ opt_map … (get_h_flag m t s)
(λH_op.execute_any_BRANCH m t s i cur_pc (⊖H_op)).
(* if H=1, branch *)
ndefinition execute_BHCS ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_h_flag m t s)
+ opt_map … (get_h_flag m t s)
(λH_op.execute_any_BRANCH m t s i cur_pc H_op).
(* if C|Z=0, branch *)
(* if nIRQ=1, branch NB: irqflag e' un negato del pin *)
ndefinition execute_BIH ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_irq_flag m t s)
+ opt_map … (get_irq_flag m t s)
(λIRQ_op.execute_any_BRANCH m t s i cur_pc (⊖IRQ_op)).
(* if nIRQ=0, branch NB: irqflag e' un negato del pin *)
ndefinition execute_BIL ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_irq_flag m t s)
+ opt_map … (get_irq_flag m t s)
(λIRQ_op.execute_any_BRANCH m t s i cur_pc IRQ_op).
(* flags = A & M *)
(* if Z|N⊙V=1, branch *)
ndefinition execute_BLE ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
- (λN_op.opt_map ?? (get_v_flag m t s)
+ opt_map … (get_n_flag m t s)
+ (λN_op.opt_map … (get_v_flag m t s)
(λV_op.execute_any_BRANCH m t s i cur_pc ((get_z_flag m t s) ⊕ (N_op ⊙ V_op)))).
(* if C|Z=1, branch *)
(* if N⊙V=1, branch *)
ndefinition execute_BLT ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
- (λN_op.opt_map ?? (get_v_flag m t s)
+ opt_map … (get_n_flag m t s)
+ (λN_op.opt_map … (get_v_flag m t s)
(λV_op.execute_any_BRANCH m t s i cur_pc (N_op ⊙ V_op))).
(* if I=0, branch *)
ndefinition execute_BMC ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_i_flag m t s)
+ opt_map … (get_i_flag m t s)
(λI_op.execute_any_BRANCH m t s i cur_pc (⊖I_op)).
(* if N=1, branch *)
ndefinition execute_BMI ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
+ opt_map … (get_n_flag m t s)
(λN_op.execute_any_BRANCH m t s i cur_pc N_op).
(* if I=1, branch *)
ndefinition execute_BMS ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_i_flag m t s)
+ opt_map … (get_i_flag m t s)
(λI_op.execute_any_BRANCH m t s i cur_pc I_op).
(* if Z=0, branch *)
(* if N=0, branch *)
ndefinition execute_BPL ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_n_flag m t s)
+ opt_map … (get_n_flag m t s)
(λN_op.execute_any_BRANCH m t s i cur_pc (⊖N_op)).
(* branch always *)
(* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
ndefinition execute_BSR ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t .λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒ let aux ≝
(* push (new_pc low) *)
- opt_map ?? (aux_push m t s_tmp1 (w16l new_pc))
+ opt_map … (aux_push m t s_tmp1 (w16l new_pc))
(* push (new_pc high) *)
- (λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
+ (λs_tmp2.opt_map … (aux_push m t s_tmp2 (w16h new_pc))
(* new_pc = new_pc + rel *)
- (λs_tmp3.Some ? (pair ?? s_tmp3 (branched_pc m t s_tmp3 new_pc M_op))))
+ (λs_tmp3.Some ? (pair … s_tmp3 (branched_pc m t s_tmp3 new_pc M_op))))
in match m with
[ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
| RS08 ⇒
(* SPC = new_pc *)
- opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
+ opt_map … (set_spc_reg m t s_tmp1 new_pc)
(* new_pc = new_pc + rel *)
- (λs_tmp2.Some ? (pair ?? s_tmp2 (branched_pc m t s_tmp2 new_pc M_op)))
+ (λs_tmp2.Some ? (pair … s_tmp2 (branched_pc m t s_tmp2 new_pc M_op)))
]]).
(* if A=M, branch *)
ndefinition execute_CBEQA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
match M_op with
(* if A=M, branch *)
match eq_b8 (get_acc_8_low_reg m t s_tmp1) MH_op with
(* new_pc = new_pc + rel *)
- [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+ [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
(* new_pc = new_pc *)
- | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
+ | false ⇒ Some ? (pair … s_tmp1 new_pc)
]]]).
(* if X=M, branch *)
ndefinition execute_CBEQX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
match M_op with
[ mk_word16 MH_op ML_op ⇒
- opt_map ?? (get_indX_8_low_reg m t s_tmp1)
+ opt_map … (get_indX_8_low_reg m t s_tmp1)
(* if X=M, branch *)
(λX_op.match eq_b8 X_op MH_op with
(* new_pc = new_pc + rel *)
- [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+ [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
(* new_pc = new_pc *)
- | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
+ | false ⇒ Some ? (pair … s_tmp1 new_pc)
])]]).
(* C = 0 *)
ndefinition execute_CLC ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (set_c_flag m t s false) cur_pc).
+ Some ? (pair … (set_c_flag m t s false) cur_pc).
(* I = 0 *)
ndefinition execute_CLI ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (set_i_flag m t s false)
- (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
+ opt_map … (set_i_flag m t s false)
+ (λs_tmp.Some ? (pair … s_tmp cur_pc)).
(* M = 0 *)
ndefinition 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 true m t 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 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp4 new_pc) ]).
+ Some ? (pair … s_tmp4 new_pc) ]).
(* flags = A - M *)
ndefinition execute_CMP ≝
(* flags = H:X - M *)
ndefinition execute_CPHX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
- opt_map ?? (get_indX_16_reg m t s_tmp1)
+ opt_map … (get_indX_16_reg m t s_tmp1)
(λX_op.
match plus_w16_dc_dc X_op (compl_w16 M_op) false with
[ pair R_op carry ⇒
(* V = X15&nM15&nR15 | nX15&M15&R15 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X15⊗(⊖M15)⊗(⊖R15)) ⊕ ((⊖X15)⊗M15⊗R15)) in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
+ Some ? (pair … s_tmp5 new_pc) ] ) ]).
(* flags = X - M *)
ndefinition execute_CPX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
- opt_map ?? (get_indX_8_low_reg m t s_tmp1)
+ opt_map … (get_indX_8_low_reg m t s_tmp1)
(λX_op.
match plus_b8_dc_dc X_op (compl_b8 M_op) false with
[ pair R_op carry ⇒
(* V = X7&nM7&nR7 | nX7&M7&R7 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖X7)⊗M7⊗R7)) in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
+ Some ? (pair … s_tmp5 new_pc) ] ) ]).
(* decimal adjiust A *)
(* per i dettagli vedere daa_b8 (modulo byte8) *)
ndefinition execute_DAA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_h_flag m t s)
+ opt_map … (get_h_flag m t s)
(λH.
let M_op ≝ get_acc_8_low_reg m t s in
match daa_b8 H (get_c_flag m t s) M_op with
(* V = M7 ⊙ R7 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((MSB_b8 M_op) ⊙ (MSB_b8 R_op)) in
(* newpc = curpc *)
- Some ? (pair ?? s_tmp5 cur_pc) ]).
+ Some ? (pair … s_tmp5 cur_pc) ]).
(* if (--M)≠0, branch *)
ndefinition execute_DBNZ ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple 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 true m t 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 *)
match eq_b8 MH_op' 〈x0,x0〉 with
(* new_pc = new_pc *)
- [ true ⇒ Some ? (pair ?? s_tmp2 new_pc)
+ [ true ⇒ Some ? (pair … s_tmp2 new_pc)
(* new_pc = new_pc + rel *)
- | false ⇒ Some ? (pair ?? s_tmp2 (branched_pc m t s_tmp2 new_pc ML_op)) ]])]]).
+ | false ⇒ Some ? (pair … s_tmp2 (branched_pc m t s_tmp2 new_pc ML_op)) ]])]]).
(* M = M - 1 *)
ndefinition execute_DEC ≝
(* per i dettagli vedere div_b8 (modulo word16) *)
ndefinition execute_DIV ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_8_high_reg m t s)
- (λH_op.opt_map ?? (get_indX_8_low_reg m t s)
+ opt_map … (get_indX_8_high_reg m t s)
+ (λH_op.opt_map … (get_indX_8_low_reg m t s)
(λX_op.match div_b8 〈H_op:(get_acc_8_low_reg m t s)〉 X_op with
[ triple quoz rest overflow ⇒
(* C = overflow *)
(* NB: che A sia cambiato o no, lo testa *)
let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 (get_acc_8_low_reg m t s_tmp2) 〈x0,x0〉) in
(* H = H o H:AmodX *)
- opt_map ?? (match overflow with
+ opt_map … (match overflow with
[ true ⇒ Some ? s_tmp3
| false ⇒ set_indX_8_high_reg m t s_tmp3 rest])
- (λs_tmp4.Some ? (pair ?? s_tmp4 cur_pc)) ])).
+ (λs_tmp4.Some ? (pair … s_tmp4 cur_pc)) ])).
(* A = A ⊙ M *)
ndefinition execute_EOR ≝
(* jmp, il nuovo indirizzo e' una WORD *)
ndefinition execute_JMP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t 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))).
+ Some ? (pair … (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
(* jump to subroutine *)
(* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
ndefinition execute_JSR ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒ let aux ≝
(* push (new_pc low) *)
- opt_map ?? (aux_push m t s_tmp1 (w16l new_pc))
+ opt_map … (aux_push m t s_tmp1 (w16l new_pc))
(* push (new_pc high) *)
- (λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
+ (λs_tmp2.opt_map … (aux_push m t s_tmp2 (w16h new_pc))
(* newpc = M_op *)
- (λs_tmp3.Some ? (pair ?? s_tmp3 M_op)))
+ (λs_tmp3.Some ? (pair … s_tmp3 M_op)))
in match m with
[ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
| RS08 ⇒
(* SPC = new_pc *)
- opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
+ opt_map … (set_spc_reg m t s_tmp1 new_pc)
(* newpc = M_op *)
- (λs_tmp2.Some ? (pair ?? s_tmp2 M_op))
+ (λs_tmp2.Some ? (pair … s_tmp2 M_op))
]]).
(* A = M *)
ndefinition execute_LDA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
(* A = M *)
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp5 new_pc) ]).
+ Some ? (pair … s_tmp5 new_pc) ]).
(* H:X = M *)
ndefinition execute_LDHX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load false m t s cur_pc i)
+ opt_map … (multi_mode_load false m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
- opt_map ?? (set_indX_16_reg m t s_tmp1 M_op)
+ opt_map … (set_indX_16_reg m t s_tmp1 M_op)
(λs_tmp2.
(* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_w16 M_op 〈〈x0,x0〉:〈x0,x0〉〉) in
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp5 new_pc)) ]).
+ Some ? (pair … s_tmp5 new_pc)) ]).
(* X = M *)
ndefinition execute_LDX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
- opt_map ?? (set_indX_8_low_reg m t s_tmp1 M_op)
+ opt_map … (set_indX_8_low_reg m t s_tmp1 M_op)
(λs_tmp2.
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp5 new_pc)) ]).
+ Some ? (pair … s_tmp5 new_pc)) ]).
(* M = 0 -> rcr M -> C' *)
ndefinition execute_LSR ≝
ndefinition 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 true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_R_PC.match S_R_PC with
[ triple s_tmp1 R_op tmp_pc ⇒
(* M2 = R_op *)
- opt_map ?? (multi_mode_write true m t 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 *)
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp5 new_pc)])]).
+ Some ? (pair … s_tmp5 new_pc)])]).
(* X:A = X * A *)
ndefinition execute_MUL ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_8_low_reg m t s)
+ opt_map … (get_indX_8_low_reg m t s)
(λX_op.let R_op ≝ mul_b8 X_op (get_acc_8_low_reg m t s) in
- opt_map ?? (set_indX_8_low_reg m t s (w16h R_op))
- (λs_tmp.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
+ opt_map … (set_indX_8_low_reg m t s (w16h R_op))
+ (λs_tmp.Some ? (pair … (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
(* M = compl M *)
ndefinition execute_NEG ≝
(* nulla *)
ndefinition execute_NOP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? s cur_pc).
+ Some ? (pair … s cur_pc).
(* A = (mk_byte8 (b8l A) (b8h A)) *)
(* cioe' swap del nibble alto/nibble basso di A *)
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
match get_acc_8_low_reg m t s with [ mk_byte8 ah al ⇒
(* A = (mk_byte8 (b8l A) (b8h A)) *)
- Some ? (pair ?? (set_acc_8_low_reg m t s 〈al,ah〉) cur_pc) ].
+ Some ? (pair … (set_acc_8_low_reg m t s 〈al,ah〉) cur_pc) ].
(* A = A | M *)
ndefinition execute_ORA ≝
(* push A *)
ndefinition execute_PSHA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (aux_push m t s (get_acc_8_low_reg m t s))
- (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc)).
+ opt_map … (aux_push m t s (get_acc_8_low_reg m t s))
+ (λs_tmp1.Some ? (pair … s_tmp1 cur_pc)).
(* push H *)
ndefinition execute_PSHH ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_8_high_reg m t s)
- (λH_op.opt_map ?? (aux_push m t s H_op)
- (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
+ opt_map … (get_indX_8_high_reg m t s)
+ (λH_op.opt_map … (aux_push m t s H_op)
+ (λs_tmp1.Some ? (pair … s_tmp1 cur_pc))).
(* push X *)
ndefinition execute_PSHX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_8_low_reg m t s)
- (λH_op.opt_map ?? (aux_push m t s H_op)
- (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
+ opt_map … (get_indX_8_low_reg m t s)
+ (λH_op.opt_map … (aux_push m t s H_op)
+ (λs_tmp1.Some ? (pair … s_tmp1 cur_pc))).
(* pop A *)
ndefinition execute_PULA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (aux_pop m t s)
+ opt_map … (aux_pop m t s)
(λS_and_A.match S_and_A with [ pair s_tmp1 A_op ⇒
- Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
+ Some ? (pair … (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
(* pop H *)
ndefinition execute_PULH ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (aux_pop m t s)
+ opt_map … (aux_pop m t s)
(λS_and_H.match S_and_H with [ pair s_tmp1 H_op ⇒
- opt_map ?? (set_indX_8_high_reg m t s_tmp1 H_op)
- (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
+ opt_map … (set_indX_8_high_reg m t s_tmp1 H_op)
+ (λs_tmp2.Some ? (pair … s_tmp2 cur_pc))]).
(* pop X *)
ndefinition execute_PULX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (aux_pop m t s)
+ opt_map … (aux_pop m t s)
(λS_and_X.match S_and_X with [ pair s_tmp1 X_op ⇒
- opt_map ?? (set_indX_8_low_reg m t s_tmp1 X_op)
- (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
+ opt_map … (set_indX_8_low_reg m t s_tmp1 X_op)
+ (λs_tmp2.Some ? (pair … s_tmp2 cur_pc))]).
(* M = C' <- rcl M <- C *)
ndefinition execute_ROL ≝
(* lascia inalterato il byte superiore di SP *)
ndefinition execute_RSP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_sp_reg m t s)
+ opt_map … (get_sp_reg m t s)
(λSP_op.match SP_op with [ mk_word16 sph spl ⇒
- opt_map ?? (set_sp_reg m t s 〈sph:〈xF,xF〉〉)
- (λs_tmp.Some ? (pair ?? s_tmp cur_pc))]).
+ opt_map … (set_sp_reg m t s 〈sph:〈xF,xF〉〉)
+ (λs_tmp.Some ? (pair … s_tmp cur_pc))]).
(* return from interrupt *)
ndefinition execute_RTI ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* pop (CCR) *)
- opt_map ?? (aux_pop m t s)
+ opt_map … (aux_pop m t s)
(λS_and_CCR.match S_and_CCR with [ pair s_tmp1 CCR_op ⇒
let s_tmp2 ≝ aux_set_CCR m t s_tmp1 CCR_op in
(* pop (A) *)
- opt_map ?? (aux_pop m t s_tmp2)
+ opt_map … (aux_pop m t s_tmp2)
(λS_and_A.match S_and_A with [ pair s_tmp3 A_op ⇒
let s_tmp4 ≝ set_acc_8_low_reg m t s_tmp3 A_op in
(* pop (X) *)
- opt_map ?? (aux_pop m t s_tmp4)
+ opt_map … (aux_pop m t s_tmp4)
(λS_and_X.match S_and_X with [ pair s_tmp5 X_op ⇒
- opt_map ?? (set_indX_8_low_reg m t s_tmp5 X_op)
+ opt_map … (set_indX_8_low_reg m t s_tmp5 X_op)
(* pop (PC high) *)
- (λs_tmp6.opt_map ?? (aux_pop m t s_tmp6)
+ (λs_tmp6.opt_map … (aux_pop m t s_tmp6)
(λS_and_PCH.match S_and_PCH with [ pair s_tmp7 PCH_op ⇒
(* pop (PC low) *)
- opt_map ?? (aux_pop m t s_tmp7)
+ opt_map … (aux_pop m t s_tmp7)
(λS_and_PCL.match S_and_PCL with [ pair s_tmp8 PCL_op ⇒
- Some ? (pair ?? s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
+ Some ? (pair … s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
(* return from subroutine *)
(* HC05/HC08/HCS08 si appoggia allo stack, RS08 si appoggia a SPC *)
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
let aux ≝
(* pop (PC high) *)
- opt_map ?? (aux_pop m t s)
+ opt_map … (aux_pop m t s)
(λS_and_PCH.match S_and_PCH with [ pair s_tmp1 PCH_op ⇒
(* pop (PC low) *)
- opt_map ?? (aux_pop m t s_tmp1)
+ opt_map … (aux_pop m t s_tmp1)
(λS_and_PCL.match S_and_PCL with [ pair s_tmp2 PCL_op ⇒
- Some ? (pair ?? s_tmp2 〈PCH_op:PCL_op〉)])])
+ Some ? (pair … s_tmp2 〈PCH_op:PCL_op〉)])])
in match m with
[ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
| RS08 ⇒
(* new_pc = SPC *)
- opt_map ?? (get_spc_reg m t s)
- (λSPC_op.Some ? (pair ?? s SPC_op))
+ opt_map … (get_spc_reg m t s)
+ (λSPC_op.Some ? (pair … s SPC_op))
].
(* A = A - M - C *)
(λA_op.λM_op.λC_op.match plus_b8_dc_dc A_op (compl_b8 M_op) false with
[ pair resb resc ⇒ match C_op with
[ true ⇒ plus_b8_dc_dc resb 〈xF,xF〉 false
- | false ⇒ pair ?? resb resc ]]).
+ | false ⇒ pair … resb resc ]]).
(* C = 1 *)
ndefinition execute_SEC ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (set_c_flag m t s true) cur_pc).
+ Some ? (pair … (set_c_flag m t s true) cur_pc).
(* I = 1 *)
ndefinition execute_SEI ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (set_i_flag m t s true)
- (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
+ opt_map … (set_i_flag m t s true)
+ (λs_tmp.Some ? (pair … s_tmp cur_pc)).
(* swap SPCh,A *)
(* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
occore accedere a SPC e salvarne il contenuto *)
ndefinition execute_SHA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_spc_reg m t s)
- (λSPC_op.opt_map ?? (set_spc_reg m t s 〈(get_acc_8_low_reg m t s):(w16l SPC_op)〉)
- (λs_tmp1.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
+ opt_map … (get_spc_reg m t s)
+ (λSPC_op.opt_map … (set_spc_reg m t s 〈(get_acc_8_low_reg m t s):(w16l SPC_op)〉)
+ (λs_tmp1.Some ? (pair … (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
(* swap SPCl,A *)
(* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
occore accedere a SPC e salvarne il contenuto *)
ndefinition execute_SLA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_spc_reg m t s)
- (λSPC_op.opt_map ?? (set_spc_reg m t s 〈(w16h SPC_op):(get_acc_8_low_reg m t s)〉)
- (λs_tmp1.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
+ opt_map … (get_spc_reg m t s)
+ (λSPC_op.opt_map … (set_spc_reg m t s 〈(w16h SPC_op):(get_acc_8_low_reg m t s)〉)
+ (λs_tmp1.Some ? (pair … (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
(* M = A *)
ndefinition execute_STA ≝
λ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 true m t 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 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp4 new_pc) ]).
+ Some ? (pair … s_tmp4 new_pc) ]).
(* M = H:X *)
ndefinition execute_STHX ≝
λ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 false m t s cur_pc i X_op)
+ opt_map … (get_indX_16_reg m t s)
+ (λ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 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp4 new_pc) ])).
+ Some ? (pair … s_tmp4 new_pc) ])).
(* I = 0 *)
ndefinition execute_STOP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
+ Some ? (pair … (setweak_i_flag m t s false) cur_pc).
(* M = X *)
ndefinition execute_STX ≝
λ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 true m t s cur_pc i X_op)
+ opt_map … (get_indX_8_low_reg m t s)
+ (λ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 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp4 new_pc) ])).
+ Some ? (pair … s_tmp4 new_pc) ])).
(* A = A - M *)
ndefinition execute_SUB ≝
(* indirizzo da cui caricare il nuovo pc *)
let vector ≝ get_pc_reg m t (set_pc_reg m t s 〈〈xF,xF〉:〈xF,xC〉〉) in
(* push (cur_pc low) *)
- opt_map ?? (aux_push m t s (w16l cur_pc))
+ opt_map … (aux_push m t s (w16l cur_pc))
(* push (cur_pc high *)
- (λs_tmp1.opt_map ?? (aux_push m t s_tmp1 (w16h cur_pc))
- (λs_tmp2.opt_map ?? (get_indX_8_low_reg m t s_tmp2)
+ (λs_tmp1.opt_map … (aux_push m t s_tmp1 (w16h cur_pc))
+ (λs_tmp2.opt_map … (get_indX_8_low_reg m t s_tmp2)
(* push (X) *)
- (λX_op.opt_map ?? (aux_push m t s_tmp2 X_op)
+ (λX_op.opt_map … (aux_push m t s_tmp2 X_op)
(* push (A) *)
- (λs_tmp3.opt_map ?? (aux_push m t s_tmp3 (get_acc_8_low_reg m t s_tmp3))
+ (λs_tmp3.opt_map … (aux_push m t s_tmp3 (get_acc_8_low_reg m t s_tmp3))
(* push (CCR) *)
- (λs_tmp4.opt_map ?? (aux_push m t s_tmp4 (aux_get_CCR m t s_tmp4))
+ (λs_tmp4.opt_map … (aux_push m t s_tmp4 (aux_get_CCR m t s_tmp4))
(* I = 1 *)
- (λs_tmp5.opt_map ?? (set_i_flag m t s_tmp5 true)
+ (λs_tmp5.opt_map … (set_i_flag m t s_tmp5 true)
(* load from vector high *)
- (λs_tmp6.opt_map ?? (memory_filter_read m t s_tmp6 vector)
+ (λs_tmp6.opt_map … (memory_filter_read m t s_tmp6 vector)
(* load from vector low *)
- (λaddrh.opt_map ?? (memory_filter_read m t s_tmp6 (succ_w16 vector))
+ (λaddrh.opt_map … (memory_filter_read m t s_tmp6 (succ_w16 vector))
(* newpc = [vector] *)
- (λaddrl.Some ? (pair ?? s_tmp6 〈addrh:addrl〉)))))))))).
+ (λaddrl.Some ? (pair … s_tmp6 〈addrh:addrl〉)))))))))).
(* flags = A *)
ndefinition execute_TAP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (aux_set_CCR m t s (get_acc_8_low_reg m t s)) cur_pc).
+ Some ? (pair … (aux_set_CCR m t s (get_acc_8_low_reg m t s)) cur_pc).
(* X = A *)
ndefinition execute_TAX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (set_indX_8_low_reg m t s (get_acc_8_low_reg m t s))
- (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
+ opt_map … (set_indX_8_low_reg m t s (get_acc_8_low_reg m t s))
+ (λs_tmp.Some ? (pair … s_tmp cur_pc)).
(* A = flags *)
ndefinition execute_TPA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (set_acc_8_low_reg m t s (aux_get_CCR m t s)) cur_pc).
+ Some ? (pair … (set_acc_8_low_reg m t s (aux_get_CCR m t s)) cur_pc).
(* flags = M - 0 *)
(* implementata senza richiamare la sottrazione, la modifica dei flag
e' immediata *)
ndefinition execute_TST ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (multi_mode_load true m t s cur_pc i)
+ opt_map … (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ triple s_tmp1 M_op new_pc ⇒
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pair ?? s_tmp4 new_pc) ]).
+ Some ? (pair … s_tmp4 new_pc) ]).
(* H:X = SP + 1 *)
ndefinition execute_TSX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_sp_reg m t s )
- (λSP_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 SP_op))
+ opt_map … (get_sp_reg m t s )
+ (λSP_op.opt_map … (set_indX_16_reg m t s (succ_w16 SP_op))
(* H:X = SP + 1 *)
- (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
+ (λs_tmp.Some ? (pair … s_tmp cur_pc))).
(* A = X *)
ndefinition execute_TXA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_8_low_reg m t s)
- (λX_op.Some ? (pair ?? (set_acc_8_low_reg m t s X_op) cur_pc)).
+ opt_map … (get_indX_8_low_reg m t s)
+ (λX_op.Some ? (pair … (set_acc_8_low_reg m t s X_op) cur_pc)).
(* SP = H:X - 1 *)
ndefinition execute_TXS ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- opt_map ?? (get_indX_16_reg m t s )
- (λX_op.opt_map ?? (set_sp_reg m t s (pred_w16 X_op))
+ opt_map … (get_indX_16_reg m t s )
+ (λX_op.opt_map … (set_sp_reg m t s (pred_w16 X_op))
(* SP = H:X - 1 *)
- (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
+ (λs_tmp.Some ? (pair … s_tmp cur_pc))).
(* I = 0 *)
ndefinition execute_WAIT ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
+ Some ? (pair … (setweak_i_flag m t s false) cur_pc).
(* **** *)
(* TICK *)
| WAIT_MODE: susp_type.
(* un tipo opzione ad hoc
- - errore: errore+stato (seguira' reset o ??, cmq lo stato non va buttato)
- - sospensione: sospensione+stato (seguira' resume o ??)
+ - errore: errore+stato (seguira' reset o …, cmq lo stato non va buttato)
+ - sospensione: sospensione+stato (seguira' resume o …)
- ok: stato
*)
ninductive tick_result (A:Type) : Type ≝
(* un solo clk, execute subito *)
[ true ⇒ tick_execute m t s pseudo mode cur_pc
(* piu' clk, execute rimandata *)
- | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple ????? 〈x0,x1〉 pseudo mode tot_clk cur_pc)))
+ | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple … 〈x0,x1〉 pseudo mode tot_clk cur_pc)))
]
]
]
(* si *)
[ true ⇒ tick_execute m t s pseudo mode cur_pc
(* no, avanzamento cur_clk *)
- | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple ????? (succ_b8 cur_clk) pseudo mode tot_clk cur_pc)))
+ | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple … (succ_b8 cur_clk) pseudo mode tot_clk cur_pc)))
]
]
].
ncases n;
##[ ##2: #n1 ##]
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma breakpoint_susp : ∀m,t,s,susp,n.execute m t (TickSUSP ? s susp) n = TickSUSP ? s susp.
ncases n;
##[ ##2: #n1 ##]
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma breakpoint :
∀m,t,n1,n2,s. execute m t s (n1 + n2) = execute m t (execute m t s n1) n2.
#m; #t; #n1;
nelim n1;
- ##[ ##1: nnormalize; #n2; #s; ncases s; nnormalize; ##[ ##1,2: #x ##] #y; napply (refl_eq ??)
+ ##[ ##1: nnormalize; #n2; #s; ncases s; nnormalize; ##[ ##1,2: #x ##] #y; napply refl_eq
##| ##2: #n3; #H; #n2; #s; ncases s;
- ##[ ##1: #x; #y; nnormalize; nrewrite > (breakpoint_err m t x y n2); napply (refl_eq ??)
- ##| ##2: #x; #y; nnormalize; nrewrite > (breakpoint_susp m t x y n2); napply (refl_eq ??)
+ ##[ ##1: #x; #y; nnormalize; nrewrite > (breakpoint_err m t x y n2); napply refl_eq
+ ##| ##2: #x; #y; nnormalize; nrewrite > (breakpoint_susp m t x y n2); napply refl_eq
##| ##3: #x; nrewrite > (Sn_p_n_to_S_npn n3 n2);
nchange with ((execute m t (tick m t x) (n3+n2)) =
(execute m t (execute m t (tick m t x) n3) n2));
nrewrite > (H n2 (tick m t x));
- napply (refl_eq ??)
+ napply refl_eq
##]
##]
nqed.
projects / helm.git / blobdiff