(* fAMC e' la logica da applicare: somma con/senza carry *)
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 → ProdT byte8 bool.
+λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
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
match fAMC A_op M_op (get_c_flag m t s_tmp1) with
- [ pairT R_op carry ⇒
+ [ pair R_op carry ⇒
let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
let A3 ≝ MSB_ex (b8l A_op) in let M3 ≝ MSB_ex (b8l M_op) in let R3 ≝ MSB_ex (b8l R_op) in
(* A = [true] fAMC(A,M,C), [false] A *)
(* 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 ? (pairT ?? 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 *)
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc) ]).
+ Some ? (pair ?? s_tmp5 new_pc) ]).
(* M = fMC(M,C) *)
(* fMC e' la logica da applicare: rc_/ro_/sh_ *)
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 → ProdT byte8 bool.
+λfMC:byte8 → bool → Prod byte8 bool.
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 [ pairT R_op carry ⇒
+ 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)
(λS_PC.match S_PC with
- [ pairT s_tmp2 new_pc ⇒
+ [ pair s_tmp2 new_pc ⇒
(* C = carry *)
let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
(* V = R7 ⊙ carry *)
let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((MSB_b8 R_op) ⊙ carry) in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp6 new_pc) ])]]).
+ Some ? (pair ?? s_tmp6 new_pc) ])]]).
(* estensione del segno byte → word *)
definition byte_extension ≝
(* if true, branch *)
match fCOND with
(* newpc = nextpc + rel *)
- [ true ⇒ Some ? (pairT ?? 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 ? (pairT ?? 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 *)
opt_map ?? (multi_mode_write true m t s cur_pc i optval)
(λS_PC.match S_PC with
(* newpc = nextpc *)
- [ pairT s_tmp1 new_pc ⇒ Some ? (pairT ?? 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 *)
(* if COND(Mn) branch *)
match fCOND MH_op with
(* newpc = nextpc + rel *)
- [ true ⇒ Some ? (pairT ?? 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 ? (pairT ?? s_tmp1 new_pc) ]]]).
+ | false ⇒ Some ? (pair ?? s_tmp1 new_pc) ]]]).
(* M = fM(M) *)
(* fM e' la logica da applicare: not/neg/++/-- *)
(* M = fM(M) *)
opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
(λS_PC.match S_PC with
- [ pairT s_tmp2 new_pc ⇒
+ [ pair s_tmp2 new_pc ⇒
(* C = fCR (C,R) *)
let s_tmp3 ≝ set_c_flag m t s_tmp2 (fC (get_c_flag m t s_tmp2) R_op) in
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
(* 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 ? (pairT ?? 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 *)
(* fAMC e' la logica da applicare: sottrazione con/senza carry *)
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 → ProdT byte8 bool.
+λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
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
match fAMC A_op M_op (get_c_flag m t s_tmp1) with
- [ pairT R_op carry ⇒
+ [ pair R_op carry ⇒
let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
(* A = [true] fAMC(A,M,C), [false] A *)
let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ 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 ? (pairT ?? s_tmp6 new_pc) ]]).
+ Some ? (pair ?? s_tmp6 new_pc) ]]).
(* il classico push *)
definition aux_push ≝
(λ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 ? (pairT ?? s_tmp1 val))))).
+ (λ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
opt_map ?? (get_sp_reg m t s_tmp1)
(* SP += extended M *)
(λSP_op.opt_map ?? (set_sp_reg m t s_tmp1 (plus_w16nc SP_op (byte_extension M_op)))
- (λs_tmp2.Some ? (pairT ?? s_tmp2 new_pc))) ]).
+ (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
(* H:X += extended M *)
definition execute_AIX ≝
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_w16nc HX_op (byte_extension M_op)))
- (λs_tmp2.Some ? (pairT ?? s_tmp2 new_pc))) ]).
+ (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
(* A = A & M *)
definition execute_AND ≝
(* BGND mode *)
definition execute_BGND ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? s cur_pc).
+ Some ? (pair ?? s cur_pc).
(* if Z|N⊙V=0, branch *)
definition execute_BGT ≝
(* push (new_pc high) *)
(λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
(* new_pc = new_pc + rel *)
- (λs_tmp3.Some ? (pairT ?? 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)
(* new_pc = new_pc + rel *)
- (λs_tmp2.Some ? (pairT ?? 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 *)
(* 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 ? (pairT ?? 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 ? (pairT ?? s_tmp1 new_pc)
+ | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
]]]).
(* if X=M, branch *)
(* if X=M, branch *)
(λX_op.match eq_b8 X_op MH_op with
(* new_pc = new_pc + rel *)
- [ true ⇒ Some ? (pairT ?? 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 ? (pairT ?? s_tmp1 new_pc)
+ | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
])]]).
(* C = 0 *)
definition execute_CLC ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (set_c_flag m t s false) cur_pc).
+ Some ? (pair ?? (set_c_flag m t s false) cur_pc).
(* I = 0 *)
definition 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 ? (pairT ?? s_tmp cur_pc)).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
(* M = 0 *)
definition execute_CLR ≝
(* M = 0 *)
opt_map ?? (multi_mode_write true m t s cur_pc i 〈x0,x0〉)
(λS_PC.match S_PC with
- [ pairT s_tmp1 new_pc ⇒
+ [ pair s_tmp1 new_pc ⇒
(* Z = 1 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 true in
(* N = 0 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp4 new_pc) ]).
+ Some ? (pair ?? s_tmp4 new_pc) ]).
(* flags = A - M *)
definition execute_CMP ≝
opt_map ?? (get_indX_16_reg m t s_tmp1)
(λX_op.
match plus_w16 X_op (compl_w16 M_op) false with
- [ pairT R_op carry ⇒
+ [ pair R_op carry ⇒
let X15 ≝ MSB_w16 X_op in let M15 ≝ MSB_w16 M_op in let R15 ≝ MSB_w16 R_op in
(* Z = nR15&nR14&nR13&nR12&nR11&nR10&nR9&nR8&nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 R_op 〈〈x0,x0〉:〈x0,x0〉〉) in
(* 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 ? (pairT ?? s_tmp5 new_pc) ] ) ]).
+ Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
(* flags = X - M *)
definition execute_CPX ≝
opt_map ?? (get_indX_8_low_reg m t s_tmp1)
(λX_op.
match plus_b8 X_op (compl_b8 M_op) false with
- [ pairT R_op carry ⇒
+ [ pair R_op carry ⇒
let X7 ≝ MSB_b8 X_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
(* 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 ? (pairT ?? s_tmp5 new_pc) ] ) ]).
+ Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
(* decimal adjiust A *)
(* per i dettagli vedere daa_b8 (modulo byte8) *)
(λ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
- [ pairT R_op carry ⇒
+ [ pair R_op carry ⇒
(* A = R *)
let s_tmp1 ≝ set_acc_8_low_reg m t s R_op in
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
(* 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 ? (pairT ?? s_tmp5 cur_pc) ]).
+ Some ? (pair ?? s_tmp5 cur_pc) ]).
(* if (--M)≠0, branch *)
definition execute_DBNZ ≝
let MH_op' ≝ pred_b8 MH_op in
opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i MH_op')
(λS_PC.match S_PC with
- [ pairT s_tmp2 _ ⇒
+ [ pair s_tmp2 _ ⇒
(* if (--M)≠0, branch *)
match eq_b8 MH_op' 〈x0,x0〉 with
(* new_pc = new_pc *)
- [ true ⇒ Some ? (pairT ?? s_tmp2 new_pc)
+ [ true ⇒ Some ? (pair ?? s_tmp2 new_pc)
(* new_pc = new_pc + rel *)
- | false ⇒ Some ? (pairT ?? 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 *)
definition execute_DEC ≝
opt_map ?? (match overflow with
[ true ⇒ Some ? s_tmp3
| false ⇒ set_indX_8_high_reg m t s_tmp3 rest])
- (λs_tmp4.Some ? (pairT ?? s_tmp4 cur_pc)) ])).
+ (λs_tmp4.Some ? (pair ?? s_tmp4 cur_pc)) ])).
(* A = A ⊙ M *)
definition execute_EOR ≝
opt_map ?? (multi_mode_load false m t s cur_pc i)
(λS_M_PC.
(* newpc = M_op *)
- Some ? (pairT ?? (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 *)
(* push (new_pc high) *)
(λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
(* newpc = M_op *)
- (λs_tmp3.Some ? (pairT ?? 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)
(* newpc = M_op *)
- (λs_tmp2.Some ? (pairT ?? s_tmp2 M_op))
+ (λs_tmp2.Some ? (pair ?? s_tmp2 M_op))
]]).
(* A = M *)
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc) ]).
+ Some ? (pair ?? s_tmp5 new_pc) ]).
(* H:X = M *)
definition execute_LDHX ≝
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc)) ]).
+ Some ? (pair ?? s_tmp5 new_pc)) ]).
(* X = M *)
definition execute_LDX ≝
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc)) ]).
+ Some ? (pair ?? s_tmp5 new_pc)) ]).
(* M = 0 -> rcr M -> C' *)
definition execute_LSR ≝
(* M2 = R_op *)
opt_map ?? (multi_mode_write true m t s_tmp1 tmp_pc i R_op)
(λS_PC.match S_PC with
- [ pairT s_tmp2 new_pc ⇒
+ [ pair s_tmp2 new_pc ⇒
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
(* N = R7 *)
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc)])]).
+ Some ? (pair ?? s_tmp5 new_pc)])]).
(* X:A = X * A *)
definition execute_MUL ≝
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 ? (pairT ?? (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
+ (λs_tmp.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
(* M = compl M *)
definition execute_NEG ≝
(* nulla *)
definition execute_NOP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? 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 ? (pairT ?? (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 *)
definition execute_ORA ≝
definition 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 ? (pairT ?? s_tmp1 cur_pc)).
+ (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc)).
(* push H *)
definition 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 ? (pairT ?? s_tmp1 cur_pc))).
+ (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
(* push X *)
definition 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 ? (pairT ?? s_tmp1 cur_pc))).
+ (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
(* pop A *)
definition 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)
- (λS_and_A.match S_and_A with [ pairT s_tmp1 A_op ⇒
- Some ? (pairT ?? (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
+ (λ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) ]).
(* pop H *)
definition 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)
- (λS_and_H.match S_and_H with [ pairT s_tmp1 H_op ⇒
+ (λ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 ? (pairT ?? s_tmp2 cur_pc))]).
+ (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
(* pop X *)
definition 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)
- (λS_and_X.match S_and_X with [ pairT s_tmp1 X_op ⇒
+ (λ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 ? (pairT ?? s_tmp2 cur_pc))]).
+ (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
(* M = C' <- rcl M <- C *)
definition execute_ROL ≝
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 ? (pairT ?? s_tmp cur_pc))]).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc))]).
(* return from interrupt *)
definition 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)
- (λS_and_CCR.match S_and_CCR with [ pairT s_tmp1 CCR_op ⇒
+ (λ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)
- (λS_and_A.match S_and_A with [ pairT s_tmp3 A_op ⇒
+ (λ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)
- (λS_and_X.match S_and_X with [ pairT s_tmp5 X_op ⇒
+ (λ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)
(* pop (PC high) *)
(λs_tmp6.opt_map ?? (aux_pop m t s_tmp6)
- (λS_and_PCH.match S_and_PCH with [ pairT s_tmp7 PCH_op ⇒
+ (λS_and_PCH.match S_and_PCH with [ pair s_tmp7 PCH_op ⇒
(* pop (PC low) *)
opt_map ?? (aux_pop m t s_tmp7)
- (λS_and_PCL.match S_and_PCL with [ pairT s_tmp8 PCL_op ⇒
- Some ? (pairT ?? s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
+ (λS_and_PCL.match S_and_PCL with [ pair s_tmp8 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 *)
let aux ≝
(* pop (PC high) *)
opt_map ?? (aux_pop m t s)
- (λS_and_PCH.match S_and_PCH with [ pairT s_tmp1 PCH_op ⇒
+ (λS_and_PCH.match S_and_PCH with [ pair s_tmp1 PCH_op ⇒
(* pop (PC low) *)
opt_map ?? (aux_pop m t s_tmp1)
- (λS_and_PCL.match S_and_PCL with [ pairT s_tmp2 PCL_op ⇒
- Some ? (pairT ?? s_tmp2 〈PCH_op:PCL_op〉)])])
+ (λS_and_PCL.match S_and_PCL with [ pair s_tmp2 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 ? (pairT ?? s SPC_op))
+ (λSPC_op.Some ? (pair ?? s SPC_op))
].
(* A = A - M - C *)
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
execute_SBC_SUB_aux m t s i cur_pc true
(λA_op.λM_op.λC_op.match plus_b8 A_op (compl_b8 M_op) false with
- [ pairT resb resc ⇒ match C_op with
+ [ pair resb resc ⇒ match C_op with
[ true ⇒ plus_b8 resb 〈xF,xF〉 resc
- | false ⇒ pairT ?? resb resc ]]).
+ | false ⇒ pair ?? resb resc ]]).
(* C = 1 *)
definition execute_SEC ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (set_c_flag m t s true) cur_pc).
+ Some ? (pair ?? (set_c_flag m t s true) cur_pc).
(* I = 1 *)
definition 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 ? (pairT ?? s_tmp cur_pc)).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
(* swap SPCh,A *)
(* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
λ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 ? (pairT ?? (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
+ (λ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
λ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 ? (pairT ?? (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
+ (λs_tmp1.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
(* M = A *)
definition execute_STA ≝
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)
(λS_op_and_PC.match S_op_and_PC with
- [ pairT s_tmp1 new_pc ⇒
+ [ pair s_tmp1 new_pc ⇒
(* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 A_op 〈x0,x0〉) in
(* N = A7 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp4 new_pc) ]).
+ Some ? (pair ?? s_tmp4 new_pc) ]).
(* M = H:X *)
definition execute_STHX ≝
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
- [ pairT s_tmp1 new_pc ⇒
+ [ pair s_tmp1 new_pc ⇒
(* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 X_op 〈〈x0,x0〉:〈x0,x0〉〉) in
(* N = R15 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp4 new_pc) ])).
+ Some ? (pair ?? s_tmp4 new_pc) ])).
(* I = 0 *)
definition execute_STOP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (setweak_i_flag m t s false) cur_pc).
+ Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
(* M = X *)
definition execute_STX ≝
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
- [ pairT s_tmp1 new_pc ⇒
+ [ pair s_tmp1 new_pc ⇒
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 X_op 〈x0,x0〉) in
(* N = R7 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp4 new_pc) ])).
+ Some ? (pair ?? s_tmp4 new_pc) ])).
(* A = A - M *)
definition execute_SUB ≝
(* load from vector low *)
(λaddrh.opt_map ?? (memory_filter_read m t s_tmp6 (succ_w16 vector))
(* newpc = [vector] *)
- (λaddrl.Some ? (pairT ?? s_tmp6 〈addrh:addrl〉)))))))))).
+ (λaddrl.Some ? (pair ?? s_tmp6 〈addrh:addrl〉)))))))))).
(* flags = A *)
definition execute_TAP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (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 *)
definition 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 ? (pairT ?? s_tmp cur_pc)).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
(* A = flags *)
definition execute_TPA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (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
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp4 new_pc) ]).
+ Some ? (pair ?? s_tmp4 new_pc) ]).
(* H:X = SP + 1 *)
definition execute_TSX ≝
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 ? (pairT ?? s_tmp cur_pc))).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
(* A = X *)
definition 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 ? (pairT ?? (set_acc_8_low_reg m t s X_op) cur_pc)).
+ (λX_op.Some ? (pair ?? (set_acc_8_low_reg m t s X_op) cur_pc)).
(* SP = H:X - 1 *)
definition execute_TXS ≝
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 ? (pairT ?? s_tmp cur_pc))).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
(* I = 0 *)
definition execute_WAIT ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (setweak_i_flag m t s false) cur_pc).
+ Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
(* **** *)
(* TICK *)
| Some status_and_newpc ⇒
(* aggiornamento centralizzato di pc e clk *)
match status_and_newpc with
- [ pairT s_tmp1 new_pc ⇒
+ [ pair s_tmp1 new_pc ⇒
let s_tmp2 ≝ set_pc_reg m t s_tmp1 new_pc in
let s_tmp3 ≝ set_clk_desc m t s_tmp2 (None ?) in
let abs_magic ≝ magic_of_opcode abs_pseudo in
projects / helm.git / blobdiff