From 826883e023c178930ca3dd69567eac23f15ef9c4 Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Tue, 2 Feb 2010 05:08:53 +0000 Subject: [PATCH] freescale porting --- .../matita/contribs/ng_assembly/depends | 5 +- .../emulator/multivm/Freescale_multivm.ma | 1231 +++++++++++++++++ .../emulator/multivm/IP2022_multivm.ma | 109 ++ .../ng_assembly/emulator/multivm/multivm.ma | 173 +++ .../emulator/multivm/multivm_base.ma | 40 + .../emulator/multivm/multivm_lemmas.ma | 57 + .../read_write/Freescale_load_write.ma | 8 +- .../emulator/read_write/IP2022_load_write.ma | 76 +- .../ng_assembly/emulator/read_write/fetch.ma | 22 +- .../emulator/read_write/load_write.ma | 10 +- .../matita/contribs/ng_assembly/num/byte8.ma | 121 +- .../contribs/ng_assembly/num/exadecim.ma | 5 + .../matita/contribs/ng_assembly/num/word16.ma | 53 + .../matita/contribs/ng_assembly/num/word24.ma | 5 + .../matita/contribs/ng_assembly/num/word32.ma | 31 + 15 files changed, 1858 insertions(+), 88 deletions(-) create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/multivm/Freescale_multivm.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/multivm/IP2022_multivm.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm_base.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm_lemmas.ma diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index ee5ea13b4..a6e34a5ba 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -23,6 +23,7 @@ num/byte8.ma common/nat.ma num/bitrigesim.ma num/comp_num.ma num/exadecim.ma emulator/model/model.ma emulator/model/HC05_model.ma emulator/model/HC08_model.ma emulator/model/HCS08_model.ma emulator/model/IP2022_model.ma emulator/model/RS08_model.ma emulator/opcodes/HC08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma +emulator/multivm/multivm.ma emulator/multivm/Freescale_multivm.ma emulator/opcodes/HC05_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma emulator/memory/memory_trees.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma @@ -31,6 +32,7 @@ num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma emulator/opcodes/RS08_table_tests.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma emulator/opcodes/Freescale_instr_mode_lemmas.ma emulator/opcodes/Freescale_instr_mode.ma num/bitrigesim_lemmas.ma num/bool_lemmas.ma num/exadecim_lemmas.ma num/oct_lemmas.ma test_errori.ma +emulator/multivm/multivm_base.ma common/theory.ma emulator/status/status_setter.ma compiler/environment.ma common/string.ma compiler/ast_type.ma common/ascii_lemmas.ma common/ascii.ma num/bool_lemmas.ma emulator/read_write/IP2022_read_write.ma emulator/read_write/read_write_base.ma emulator/status/status_setter.ma @@ -56,10 +58,10 @@ num/bool_lemmas.ma num/bool.ma emulator/model/HC08_model.ma emulator/status/status.ma emulator/memory/memory_abs.ma emulator/memory/memory_bits.ma emulator/memory/memory_func.ma emulator/memory/memory_trees.ma num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma +emulator/read_write/Freescale_load_write.ma emulator/read_write/load_write_base.ma emulator/status/status_getter.ma emulator/memory/memory_struct.ma num/byte8.ma num/oct.ma emulator/model/HC05_model.ma emulator/status/status.ma emulator/status/status_setter.ma emulator/status/status.ma -emulator/read_write/Freescale_load_write.ma emulator/read_write/load_write_base.ma emulator/status/status_getter.ma num/word32.ma num/word16.ma common/ascii.ma num/bool.ma emulator/read_write/load_write_base.ma emulator/read_write/read_write.ma @@ -78,6 +80,7 @@ emulator/status/RS08_status.ma num/word16.ma common/option_lemmas.ma common/option.ma num/bool_lemmas.ma common/option.ma num/bool.ma emulator/opcodes/pseudo_lemmas.ma emulator/opcodes/Freescale_instr_mode_lemmas.ma emulator/opcodes/Freescale_pseudo_lemmas.ma emulator/opcodes/IP2022_instr_mode_lemmas.ma emulator/opcodes/IP2022_pseudo_lemmas.ma emulator/opcodes/pseudo.ma +emulator/multivm/Freescale_multivm.ma emulator/multivm/multivm_base.ma emulator/read_write/fetch.ma emulator/read_write/load_write.ma num/byte8_lemmas.ma num/byte8.ma num/comp_num_lemmas.ma num/exadecim_lemmas.ma emulator/opcodes/RS08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma emulator/model/RS08_model.ma emulator/status/status.ma diff --git a/helm/software/matita/contribs/ng_assembly/emulator/multivm/Freescale_multivm.ma b/helm/software/matita/contribs/ng_assembly/emulator/multivm/Freescale_multivm.ma new file mode 100755 index 000000000..e9ab24946 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/multivm/Freescale_multivm.ma @@ -0,0 +1,1231 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "emulator/multivm/multivm_base.ma". +include "emulator/read_write/load_write.ma". + +(* ************************************************ *) +(* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *) +(* ************************************************ *) + +(* 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: somma con/senza carry *) +ndefinition execute_ADC_ADD_aux ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.λsetflag:bool. +λfAMC:bool → byte8 → byte8 → ProdT bool byte8. + opt_map … (multi_mode_loadb … 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 … s_tmp1 in + match fAMC (get_c_flag … s_tmp1) A_op M_op with + [ pair carry R_op ⇒ + let A7 ≝ getMSB_b8 A_op in + let M7 ≝ getMSB_b8 M_op in + let R7 ≝ getMSB_b8 R_op in + let A3 ≝ getMSB_ex (cnL ? A_op) in + let M3 ≝ getMSB_ex (cnL ? M_op) in + let R3 ≝ getMSB_ex (cnL ? R_op) in + (* A = [true] fAMC(A,M,C), [false] A *) + let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg … s_tmp1 R_op | false ⇒ s_tmp1 ] in + (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *) + let s_tmp3 ≝ set_zflb … s_tmp2 R_op in + (* C = A7&M7 | M7&nR7 | nR7&A7 *) + let s_tmp4 ≝ set_c_flag … s_tmp3 ((A7⊗M7) ⊕ (M7⊗(⊖R7)) ⊕ ((⊖R7)⊗A7)) in + (* N = R7 *) + let s_tmp5 ≝ set_nflb … s_tmp4 R_op in + (* H = A3&M3 | M3&nR3 | nR3&A3 *) + let s_tmp6 ≝ setweak_h_flag … s_tmp5 ((A3⊗M3) ⊕ (M3⊗(⊖R3)) ⊕ ((⊖R3)⊗A3)) in + (* V = A7&M7&nR7 | nA7&nM7&R7 *) + let s_tmp7 ≝ setweak_v_flag … s_tmp6 ((A7⊗M7⊗(⊖R7)) ⊕ ((⊖A7)⊗(⊖M7)⊗R7)) in + (* newpc = nextpc *) + 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 *) +(* fAM e' la logica da applicare: and/xor/or *) +ndefinition execute_AND_BIT_EOR_ORA_aux ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.λsetflag:bool. +λfAM:byte8 → byte8 → byte8. + opt_map … (multi_mode_loadb … 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 … s_tmp1) M_op in + (* A = [true] fAM(A,M), [false] A *) + let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg … s_tmp1 R_op | false ⇒ s_tmp1 ] in + (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *) + let s_tmp3 ≝ set_zflb … s_tmp2 R_op in + (* N = R7 *) + let s_tmp4 ≝ set_nflb … s_tmp3 R_op in + (* V = 0 *) + let s_tmp5 ≝ setweak_v_flag … s_tmp4 false in + (* newpc = nextpc *) + 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.λcur_pc:word16.λi:aux_im_type m. +λfMC:bool → byte8 → ProdT bool byte8. + opt_map … (multi_mode_loadb … s cur_pc i) + (λS_M_PC.match S_M_PC with + [ triple s_tmp1 M_op _ ⇒ + match fMC (get_c_flag … s_tmp1) M_op with [ pair carry R_op ⇒ + (* M = fMC(M,C) *) + opt_map … (multi_mode_writeb … s_tmp1 cur_pc auxMode_ok i R_op) + (λS_PC.match S_PC with + [ pair s_tmp2 new_pc ⇒ + (* C = carry *) + let s_tmp3 ≝ set_c_flag … s_tmp2 carry in + (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *) + let s_tmp4 ≝ set_zflb … s_tmp3 R_op in + (* N = R7 *) + let s_tmp5 ≝ set_nflb … s_tmp4 R_op in + (* V = R7 ⊙ carry *) + let s_tmp6 ≝ setweak_v_flag … s_tmp5 ((getMSB_b8 R_op) ⊙ carry) in + (* newpc = nextpc *) + Some ? (pair … s_tmp6 new_pc) ])]]). + +(* branch con byte+estensione segno *) +ndefinition branched_pc ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λb:byte8. + get_pc_reg … (set_pc_reg … s (plus_w16_d_d cur_pc (exts_w16 b))). + +(* if COND=1 branch *) +(* 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.λcur_pc:word16.λi:aux_im_type m.λfCOND:bool. + opt_map … (multi_mode_loadb … 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 … s_tmp1 new_pc M_op)) + (* newpc = nextpc *) + | 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.λcur_pc:word16.λi:aux_im_type m.λoptval:byte8. + (* Mn = filtered optval *) + opt_map … (multi_mode_writeb … s cur_pc auxMode_ok i optval) + (λS_PC.match S_PC with + (* newpc = nextpc *) + [ 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.λcur_pc:word16.λi:aux_im_type m.λfCOND:byte8 → bool. + opt_map … (multi_mode_loadw … s cur_pc i) + (λS_M_PC.match S_M_PC with + [ triple s_tmp1 M_op new_pc ⇒ match M_op with + [ mk_comp_num MH_op ML_op ⇒ + (* if COND(Mn) branch *) + match fCOND MH_op with + (* newpc = nextpc + rel *) + [ true ⇒ Some ? (pair … s_tmp1 (branched_pc … s_tmp1 new_pc ML_op)) + (* newpc = nextpc *) + | false ⇒ Some ? (pair … s_tmp1 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 *) +ndefinition execute_CMP_SBC_SUB_aux ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.λsetflag:bool. +λfAMC:bool → byte8 → byte8 → ProdT bool byte8. + opt_map … (multi_mode_loadb … 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 … s_tmp1 in + match fAMC (get_c_flag … s_tmp1) A_op M_op with + [ pair carry R_op ⇒ + let A7 ≝ getMSB_b8 A_op in + let M7 ≝ getMSB_b8 M_op in + let R7 ≝ getMSB_b8 R_op in + (* A = [true] fAMC(A,M,C), [false] A *) + let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg … s_tmp1 R_op | false ⇒ s_tmp1 ] in + (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *) + let s_tmp3 ≝ set_zflb … s_tmp2 R_op in + (* C = nA7&M7 | M7&R7 | R7&nA7 *) + let s_tmp4 ≝ set_c_flag … s_tmp3 (((⊖A7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖A7))) in + (* N = R7 *) + let s_tmp5 ≝ set_nflb … s_tmp4 R_op in + (* V = A7&nM7&nR7 | nA7&M7&R7 *) + let s_tmp6 ≝ setweak_v_flag … s_tmp5 ((A7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖A7)⊗M7⊗R7)) in + (* newpc = nextpc *) + Some ? (pair … s_tmp6 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.λcur_pc:word16.λi:aux_im_type m. +λfM:byte8 → byte8.λfV:bool → bool → bool.λfC:bool → byte8 → bool. + opt_map … (multi_mode_loadb … 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_writeb … s_tmp1 cur_pc auxMode_ok i R_op) + (λS_PC.match S_PC with + [ pair s_tmp2 new_pc ⇒ + (* C = fCR (C,R) *) + let s_tmp3 ≝ set_c_flag … s_tmp2 (fC (get_c_flag … s_tmp2) R_op) in + (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *) + let s_tmp4 ≝ set_zflb … s_tmp3 R_op in + (* N = R7 *) + let s_tmp5 ≝ set_nflb … s_tmp4 R_op in + (* V = fV (M7,R7) *) + let s_tmp6 ≝ setweak_v_flag … s_tmp5 (fV (getMSB_b8 M_op) (getMSB_b8 R_op)) in + (* newpc = nextpc *) + 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 … s) + (* [SP] = val *) + (λSP_op.opt_map … (memory_filter_write … s (extu_w32 SP_op) auxMode_ok val) + (* SP -- *) + (λs_tmp1.opt_map … (set_sp_reg … 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 … s) + (* SP ++ *) + (λSP_op.opt_map … (set_sp_reg … s (succ_w16 SP_op)) + (λs_tmp1.opt_map … (get_sp_reg … s_tmp1) + (* val = [SP] *) + (λSP_op'.opt_map … (memory_filter_read … s_tmp1 (extu_w32 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 + implementati corrispondono a 1 *) +ndefinition aux_get_CCR_aux ≝ +λopt:option bool.match opt with [ None ⇒ true | Some b ⇒ b ]. + +ndefinition aux_get_CCR ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t. + byte8_of_bits (mk_Array8T ? + (aux_get_CCR_aux (get_v_flag … s)) + true + true + (aux_get_CCR_aux (get_h_flag … s)) + (aux_get_CCR_aux (get_i_flag … s)) + (aux_get_CCR_aux (get_n_flag … s)) + (get_z_flag … s) + (get_c_flag … s)). + +(* CCR corrisponde a V11HINZC *) +(* i flag mantengono posizione costante nelle varie ALU, e se non sono + implementati si puo' usare tranquillamente setweak *) +ndefinition aux_set_CCR ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λCCR:byte8. + match bits_of_byte8 CCR with + [ mk_Array8T vf _ _ hf if nf zf cf ⇒ + setweak_v_flag … + (setweak_h_flag … + (setweak_i_flag … + (setweak_n_flag … + (set_z_flag … + (set_c_flag … s cf) zf) nf) if) hf) vf ]. + +(* **************** *) +(* LOGICA DELLA ALU *) +(* **************** *) + +(* A = A + M + C *) +ndefinition execute_ADC ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_ADC_ADD_aux … s cur_pc i true (λC_op.plus_b8_dc_dc C_op). + +(* A = A + M *) +ndefinition execute_ADD ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_ADC_ADD_aux … s cur_pc i true (λC_op.plus_b8_dc_dc false). + +(* SP += extended M *) +ndefinition execute_AIS ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadb … s cur_pc i) + (λS_M_PC.match S_M_PC with + [ triple s_tmp1 M_op new_pc ⇒ + opt_map … (get_sp_reg … s_tmp1) + (* SP += extended M *) + (λSP_op.opt_map … (set_sp_reg … s_tmp1 (plus_w16_d_d SP_op (exts_w16 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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadb … 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 … s_tmp1) + (* H:X += extended M *) + (λHX_op.opt_map … (set_indX_16_reg … s_tmp1 (plus_w16_d_d HX_op (exts_w16 M_op))) + (λs_tmp2.Some ? (pair … s_tmp2 new_pc))) ]). + +(* A = A & M *) +ndefinition execute_AND ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_AND_BIT_EOR_ORA_aux … s cur_pc i true and_b8. + +(* M = C' <- rcl M <- 0 *) +ndefinition execute_ASL ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_ASL_ASR_LSR_ROL_ROR_aux … s cur_pc i (λC_op.rcl_b8 false). + +(* M = M7 -> rcr M -> C' *) +ndefinition execute_ASR ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_ASL_ASR_LSR_ROL_ROR_aux … s cur_pc i (λC_op.λM_op.rcr_b8 (getMSB_b8 M_op) M_op). + +(* if C=0, branch *) +ndefinition execute_BCC ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_any_BRANCH … s cur_pc i (⊖(get_c_flag … s)). + +(* Mn = 0 *) +ndefinition execute_BCLRn ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_BCLRn_BSETn_aux … s cur_pc i 〈x0,x0〉. + +(* if C=1, branch *) +ndefinition execute_BCS ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_any_BRANCH … s cur_pc i (get_c_flag … s). + +(* if Z=1, branch *) +ndefinition execute_BEQ ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_any_BRANCH … s cur_pc i (get_z_flag … s). + +(* if N⊙V=0, branch *) +ndefinition execute_BGE ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_n_flag … s) + (λN_op.opt_map … (get_v_flag … s) + (λV_op.execute_any_BRANCH … s cur_pc i (⊖(N_op ⊙ V_op)))). + +(* BGND mode *) +ndefinition execute_BGND ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + 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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_n_flag … s) + (λN_op.opt_map … (get_v_flag … s) + (λV_op.execute_any_BRANCH … s cur_pc i (⊖((get_z_flag … s) ⊕ (N_op ⊙ V_op))))). + +(* if H=0, branch *) +ndefinition execute_BHCC ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_h_flag … s) + (λH_op.execute_any_BRANCH … s cur_pc i (⊖H_op)). + +(* if H=1, branch *) +ndefinition execute_BHCS ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_h_flag … s) + (λH_op.execute_any_BRANCH … s cur_pc i H_op). + +(* if C|Z=0, branch *) +ndefinition execute_BHI ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_any_BRANCH … s cur_pc i (⊖((get_c_flag … s) ⊕ (get_z_flag … s))). + +(* 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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_irq_flag … s) + (λIRQ_op.execute_any_BRANCH … s cur_pc i (⊖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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_irq_flag … s) + (λIRQ_op.execute_any_BRANCH … s cur_pc i IRQ_op). + +(* flags = A & M *) +ndefinition execute_BIT ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_AND_BIT_EOR_ORA_aux … s cur_pc i false and_b8. + +(* if Z|N⊙V=1, branch *) +ndefinition execute_BLE ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_n_flag … s) + (λN_op.opt_map … (get_v_flag … s) + (λV_op.execute_any_BRANCH … s cur_pc i ((get_z_flag … s) ⊕ (N_op ⊙ V_op)))). + +(* if C|Z=1, branch *) +ndefinition execute_BLS ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_any_BRANCH … s cur_pc i ((get_c_flag … s) ⊕ (get_z_flag … s)). + +(* if N⊙V=1, branch *) +ndefinition execute_BLT ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_n_flag … s) + (λN_op.opt_map … (get_v_flag … s) + (λV_op.execute_any_BRANCH … s cur_pc i (N_op ⊙ V_op))). + +(* if I=0, branch *) +ndefinition execute_BMC ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_i_flag … s) + (λI_op.execute_any_BRANCH … s cur_pc i (⊖I_op)). + +(* if N=1, branch *) +ndefinition execute_BMI ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_n_flag … s) + (λN_op.execute_any_BRANCH … s cur_pc i N_op). + +(* if I=1, branch *) +ndefinition execute_BMS ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_i_flag … s) + (λI_op.execute_any_BRANCH … s cur_pc i I_op). + +(* if Z=0, branch *) +ndefinition execute_BNE ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_any_BRANCH … s cur_pc i (⊖(get_z_flag … s)). + +(* if N=0, branch *) +ndefinition execute_BPL ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_n_flag … s) + (λN_op.execute_any_BRANCH … s cur_pc i (⊖N_op)). + +(* branch always *) +ndefinition execute_BRA ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_any_BRANCH … s cur_pc i true. + +(* if Mn=0 branch *) +ndefinition execute_BRCLRn ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_BRCLRn_BRSETn_aux … s cur_pc i + (λMn_op.eq_b8 Mn_op 〈x0,x0〉). + +(* branch never... come se fosse un nop da 2 byte *) +ndefinition execute_BRN ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_any_BRANCH … s cur_pc i false. + +(* if Mn=1 branch *) +ndefinition execute_BRSETn ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_BRCLRn_BRSETn_aux … s cur_pc i + (λMn_op.⊖(eq_b8 Mn_op 〈x0,x0〉)). + +(* Mn = 1 *) +ndefinition execute_BSETn ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_BCLRn_BSETn_aux … s cur_pc i 〈xF,xF〉. + +(* branch to subroutine *) +(* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *) +ndefinition execute_BSR ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t .λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadb … 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 … s_tmp1 (cnL ? new_pc)) + (* push (new_pc high) *) + (λs_tmp2.opt_map … (aux_push … s_tmp2 (cnH ? new_pc)) + (* new_pc = new_pc + rel *) + (λs_tmp3.Some ? (pair … s_tmp3 (branched_pc … 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 … s_tmp1 new_pc) + (* new_pc = new_pc + rel *) + (λs_tmp2.Some ? (pair … s_tmp2 (branched_pc … s_tmp2 new_pc M_op))) + | _ ⇒ None ? + ]]). + +(* if A=M, branch *) +ndefinition execute_CBEQA ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadw … s cur_pc i) + (λS_M_PC.match S_M_PC with + [ triple s_tmp1 M_op new_pc ⇒ + match M_op with + [ mk_comp_num MH_op ML_op ⇒ + (* if A=M, branch *) + match eq_b8 (get_acc_8_low_reg … s_tmp1) MH_op with + (* new_pc = new_pc + rel *) + [ true ⇒ Some ? (pair … s_tmp1 (branched_pc … s_tmp1 new_pc ML_op)) + (* new_pc = 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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadw … s cur_pc i) + (λS_M_PC.match S_M_PC with + [ triple s_tmp1 M_op new_pc ⇒ + match M_op with + [ mk_comp_num MH_op ML_op ⇒ + opt_map … (get_indX_8_low_reg … 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 … s_tmp1 new_pc ML_op)) + (* new_pc = 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.λcur_pc:word16.λi:aux_im_type m. + Some ? (pair … (set_c_flag … s false) cur_pc). + +(* I = 0 *) +ndefinition execute_CLI ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (set_i_flag … 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.λcur_pc:word16.λi:aux_im_type m. + (* M = 0 *) + opt_map … (multi_mode_writeb … s cur_pc auxMode_ok i 〈x0,x0〉) + (λS_PC.match S_PC with + [ pair s_tmp1 new_pc ⇒ + (* Z = 1 *) + let s_tmp2 ≝ set_z_flag … s_tmp1 true in + (* N = 0 *) + let s_tmp3 ≝ setweak_n_flag … s_tmp2 false in + (* V = 0 *) + let s_tmp4 ≝ setweak_v_flag … s_tmp3 false in + (* newpc = nextpc *) + Some ? (pair … s_tmp4 new_pc) ]). + +(* flags = A - M *) +ndefinition execute_CMP ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_CMP_SBC_SUB_aux … s cur_pc i false (λC_op.λA_op.λM_op.plus_b8_dc_dc false A_op (compl_b8 M_op)). + +(* M = not M *) +ndefinition execute_COM ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_COM_DEC_INC_NEG_aux … s cur_pc i not_b8 + (* fV = 0 *) + (λM7.λR7.false) + (* fC = 1 *) + (λC_op.λR_op.true). + +(* flags = H:X - M *) +ndefinition execute_CPHX ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadw … 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 … s_tmp1) + (λX_op. + match plus_w16_dc_dc false X_op (compl_w16 M_op) with + [ pair carry R_op ⇒ + let X15 ≝ getMSB_w16 X_op in + let M15 ≝ getMSB_w16 M_op in + let R15 ≝ getMSB_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_zflw … s_tmp1 R_op in + (* C = nX15&M15 | M15&R15 | R15&nX15 *) + let s_tmp3 ≝ set_c_flag … s_tmp2 (((⊖X15)⊗M15) ⊕ (M15⊗R15) ⊕ (R15⊗(⊖X15))) in + (* N = R15 *) + let s_tmp4 ≝ set_nflw … s_tmp3 R_op in + (* V = X15&nM15&nR15 | nX15&M15&R15 *) + let s_tmp5 ≝ setweak_v_flag … s_tmp4 ((X15⊗(⊖M15)⊗(⊖R15)) ⊕ ((⊖X15)⊗M15⊗R15)) in + (* newpc = nextpc *) + Some ? (pair … s_tmp5 new_pc) ] ) ]). + +(* flags = X - M *) +ndefinition execute_CPX ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadb … 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 … s_tmp1) + (λX_op. + match plus_b8_dc_dc false X_op (compl_b8 M_op) with + [ pair carry R_op ⇒ + let X7 ≝ getMSB_b8 X_op in + let M7 ≝ getMSB_b8 M_op in + let R7 ≝ getMSB_b8 R_op in + (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *) + let s_tmp2 ≝ set_zflb … s_tmp1 R_op in + (* C = nX7&M7 | M7&R7 | R7&nX7 *) + let s_tmp3 ≝ set_c_flag … s_tmp2 (((⊖X7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖X7))) in + (* N = R7 *) + let s_tmp4 ≝ set_nflb … s_tmp3 R_op in + (* V = X7&nM7&nR7 | nX7&M7&R7 *) + let s_tmp5 ≝ setweak_v_flag … s_tmp4 ((X7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖X7)⊗M7⊗R7)) in + (* newpc = nextpc *) + 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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_h_flag … s) + (λH. + let M_op ≝ get_acc_8_low_reg … s in + match daa_b8 H (get_c_flag … s) M_op with + [ pair carry R_op ⇒ + (* A = R *) + let s_tmp1 ≝ set_acc_8_low_reg … s R_op in + (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *) + let s_tmp2 ≝ set_zflb … s_tmp1 R_op in + (* C = carry *) + let s_tmp3 ≝ set_c_flag … s_tmp2 carry in + (* N = R7 *) + let s_tmp4 ≝ set_nflb … s_tmp3 R_op in + (* V = M7 ⊙ R7 *) + let s_tmp5 ≝ setweak_v_flag … s_tmp4 ((getMSB_b8 M_op) ⊙ (getMSB_b8 R_op)) in + (* newpc = curpc *) + Some ? (pair … s_tmp5 cur_pc) ]). + +(* if (--M)≠0, branch *) +ndefinition execute_DBNZ ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadw … s cur_pc i) + (λS_M_PC.match S_M_PC with + [ triple s_tmp1 M_op new_pc ⇒ + match M_op with + [ mk_comp_num MH_op ML_op ⇒ + (* --M *) + let MH_op' ≝ pred_b8 MH_op in + opt_map … (multi_mode_writeb … s_tmp1 cur_pc auxMode_ok 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) + (* new_pc = new_pc + rel *) + | false ⇒ Some ? (pair … s_tmp2 (branched_pc … s_tmp2 new_pc ML_op)) ]])]]). + +(* M = M - 1 *) +ndefinition execute_DEC ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_COM_DEC_INC_NEG_aux … s cur_pc i pred_b8 + (* fV = M7&nR7 *) + (λM7.λR7.M7⊗(⊖R7)) + (* fC = C *) + (λC_op.λR_op.C_op). + +(* A = H:A/X, H = H:AmodX se non c'e' overflow, altrimenti invariati *) +(* per i dettagli vedere div_b8 (modulo word16) *) +ndefinition execute_DIV ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_indX_8_high_reg … s) + (λH_op.opt_map … (get_indX_8_low_reg … s) + (λX_op.match div_b8 〈H_op:(get_acc_8_low_reg … s)〉 X_op with + [ triple quoz rest overflow ⇒ + (* C = overflow *) + let s_tmp1 ≝ set_c_flag … s overflow in + (* A = A o H:A/X *) + let s_tmp2 ≝ match overflow with + [ true ⇒ s_tmp1 + | false ⇒ set_acc_8_low_reg … s_tmp1 quoz ] in + (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *) + (* NB: che A sia cambiato o no, lo testa *) + let s_tmp3 ≝ set_zflb … s_tmp2 (get_acc_8_low_reg … s_tmp2) in + (* H = H o H:AmodX *) + opt_map … (match overflow with + [ true ⇒ Some ? s_tmp3 + | false ⇒ set_indX_8_high_reg … s_tmp3 rest]) + (λs_tmp4.Some ? (pair … s_tmp4 cur_pc)) ])). + +(* A = A ⊙ M *) +ndefinition execute_EOR ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_AND_BIT_EOR_ORA_aux … s cur_pc i true xor_b8. + +(* M = M + 1 *) +ndefinition execute_INC ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_COM_DEC_INC_NEG_aux … s cur_pc i succ_b8 + (* fV = nM7&R7 *) + (λM7.λR7.(⊖M7)⊗R7) + (* fC = C *) + (λC_op.λR_op.C_op). + +(* jmp, il nuovo indirizzo e' una WORD *) +ndefinition execute_JMP ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadw … s cur_pc i) + (λS_M_PC. + (* newpc = M_op *) + 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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadw … 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 … s_tmp1 (cnL ? new_pc)) + (* push (new_pc high) *) + (λs_tmp2.opt_map … (aux_push … s_tmp2 (cnH ? new_pc)) + (* newpc = 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 … s_tmp1 new_pc) + (* newpc = M_op *) + (λs_tmp2.Some ? (pair … s_tmp2 M_op)) + | _ ⇒ None ? + ]]). + +(* A = M *) +ndefinition execute_LDA ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadb … s cur_pc i) + (λS_M_PC.match S_M_PC with + [ triple s_tmp1 M_op new_pc ⇒ + (* A = M *) + let s_tmp2 ≝ set_acc_8_low_reg … s_tmp1 M_op in + (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *) + let s_tmp3 ≝ set_zflb … s_tmp2 M_op in + (* N = R7 *) + let s_tmp4 ≝ set_nflb … s_tmp3 M_op in + (* V = 0 *) + let s_tmp5 ≝ setweak_v_flag … s_tmp4 false in + (* newpc = nextpc *) + Some ? (pair … s_tmp5 new_pc) ]). + +(* H:X = M *) +ndefinition execute_LDHX ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadw … 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 … 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_zflw … s_tmp2 M_op in + (* N = R15 *) + let s_tmp4 ≝ set_nflw … s_tmp3 M_op in + (* V = 0 *) + let s_tmp5 ≝ setweak_v_flag … s_tmp4 false in + (* newpc = nextpc *) + Some ? (pair … s_tmp5 new_pc)) ]). + +(* X = M *) +ndefinition execute_LDX ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadb … 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 … s_tmp1 M_op) + (λs_tmp2. + (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *) + let s_tmp3 ≝ set_zflb … s_tmp2 M_op in + (* N = R7 *) + let s_tmp4 ≝ set_nflb … s_tmp3 M_op in + (* V = 0 *) + let s_tmp5 ≝ setweak_v_flag … s_tmp4 false in + (* newpc = nextpc *) + Some ? (pair … s_tmp5 new_pc)) ]). + +(* M = 0 -> rcr M -> C' *) +ndefinition execute_LSR ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_ASL_ASR_LSR_ROL_ROR_aux … s cur_pc i (λC_op.λM_op.rcr_b8 false M_op). + +(* M2 = M1 *) +ndefinition execute_MOV ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + (* R_op = M1 *) + opt_map … (multi_mode_loadb … 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_writeb … s_tmp1 tmp_pc auxMode_ok i R_op) + (λS_PC.match S_PC with + [ pair s_tmp2 new_pc ⇒ + (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *) + let s_tmp3 ≝ set_zflb … s_tmp2 R_op in + (* N = R7 *) + let s_tmp4 ≝ set_nflb … s_tmp3 R_op in + (* V = 0 *) + let s_tmp5 ≝ setweak_v_flag … s_tmp4 false in + (* newpc = nextpc *) + Some ? (pair … s_tmp5 new_pc)])]). + +(* X:A = X * A *) +ndefinition execute_MUL ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_indX_8_low_reg … s) + (λX_op.let R_op ≝ mulu_b8 X_op (get_acc_8_low_reg … s) in + opt_map … (set_indX_8_low_reg … s (cnH ? R_op)) + (λs_tmp.Some ? (pair … (set_acc_8_low_reg … s_tmp (cnL ? R_op)) cur_pc))). + +(* M = compl M *) +ndefinition execute_NEG ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_COM_DEC_INC_NEG_aux … s cur_pc i compl_b8 + (* fV = M7&R7 *) + (λM7.λR7.M7⊗R7) + (* fC = R7|R6|R5|R4|R3|R2|R1|R0 *) + (λC_op.λR_op.⊖(eq_b8 R_op 〈x0,x0〉)). + +(* nulla *) +ndefinition execute_NOP ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + Some ? (pair … s cur_pc). + +(* A = (mk_byte8 (b8l A) (b8h A)) *) +(* cioe' swap del nibble alto/nibble basso di A *) +ndefinition execute_NSA ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + match get_acc_8_low_reg … s with [ mk_comp_num ah al ⇒ + (* A = (mk_byte8 (b8l A) (b8h A)) *) + Some ? (pair … (set_acc_8_low_reg … s 〈al,ah〉) cur_pc) ]. + +(* A = A | M *) +ndefinition execute_ORA ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_AND_BIT_EOR_ORA_aux … s cur_pc i true or_b8. + +(* push A *) +ndefinition execute_PSHA ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (aux_push … s (get_acc_8_low_reg … 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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_indX_8_high_reg … s) + (λH_op.opt_map … (aux_push … 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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_indX_8_low_reg … s) + (λH_op.opt_map … (aux_push … 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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (aux_pop … s) + (λS_and_A.match S_and_A with [ pair s_tmp1 A_op ⇒ + Some ? (pair … (set_acc_8_low_reg … s_tmp1 A_op) cur_pc) ]). + +(* pop H *) +ndefinition execute_PULH ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (aux_pop … s) + (λS_and_H.match S_and_H with [ pair s_tmp1 H_op ⇒ + opt_map … (set_indX_8_high_reg … 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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (aux_pop … s) + (λS_and_X.match S_and_X with [ pair s_tmp1 X_op ⇒ + opt_map … (set_indX_8_low_reg … s_tmp1 X_op) + (λs_tmp2.Some ? (pair … s_tmp2 cur_pc))]). + +(* M = C' <- rcl M <- C *) +ndefinition execute_ROL ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_ASL_ASR_LSR_ROL_ROR_aux … s cur_pc i rcl_b8. + +(* M = C -> rcr M -> C' *) +ndefinition execute_ROR ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_ASL_ASR_LSR_ROL_ROR_aux … s cur_pc i rcr_b8. + +(* SP = 0xuuFF *) +(* lascia inalterato il byte superiore di SP *) +ndefinition execute_RSP ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_sp_reg … s) + (λSP_op.match SP_op with [ mk_comp_num sph spl ⇒ + opt_map … (set_sp_reg … 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.λcur_pc:word16.λi:aux_im_type m. + (* pop (CCR) *) + opt_map … (aux_pop … s) + (λS_and_CCR.match S_and_CCR with [ pair s_tmp1 CCR_op ⇒ + let s_tmp2 ≝ aux_set_CCR … s_tmp1 CCR_op in + (* pop (A) *) + opt_map … (aux_pop … s_tmp2) + (λS_and_A.match S_and_A with [ pair s_tmp3 A_op ⇒ + let s_tmp4 ≝ set_acc_8_low_reg … s_tmp3 A_op in + (* pop (X) *) + opt_map … (aux_pop … s_tmp4) + (λS_and_X.match S_and_X with [ pair s_tmp5 X_op ⇒ + opt_map … (set_indX_8_low_reg … s_tmp5 X_op) + (* pop (PC high) *) + (λs_tmp6.opt_map … (aux_pop … s_tmp6) + (λS_and_PCH.match S_and_PCH with [ pair s_tmp7 PCH_op ⇒ + (* pop (PC low) *) + opt_map … (aux_pop … s_tmp7) + (λ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 *) +ndefinition execute_RTS ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + let aux ≝ + (* pop (PC high) *) + opt_map … (aux_pop … s) + (λS_and_PCH.match S_and_PCH with [ pair s_tmp1 PCH_op ⇒ + (* pop (PC low) *) + opt_map … (aux_pop … s_tmp1) + (λ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 … s) + (λSPC_op.Some ? (pair … s SPC_op)) + | _ ⇒ None ? + ]. + +(* A = A - M - C *) +ndefinition execute_SBC ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_CMP_SBC_SUB_aux … s cur_pc i true + (λC_op.λA_op.λM_op.match plus_b8_dc_dc false A_op (compl_b8 M_op) with + [ pair resc resb ⇒ match C_op with + [ true ⇒ plus_b8_dc_dc false resb 〈xF,xF〉 + | false ⇒ pair … resc resb ]]). + +(* C = 1 *) +ndefinition execute_SEC ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + Some ? (pair … (set_c_flag … s true) cur_pc). + +(* I = 1 *) +ndefinition execute_SEI ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (set_i_flag … 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 + fare subroutine annidate se RA (return address) e' salvato sempre in SPC? + occore accedere a SPC e salvarne il contenuto *) +ndefinition execute_SHA ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_spc_reg … s) + (λSPC_op.opt_map … (set_spc_reg … s 〈(get_acc_8_low_reg … s):(cnL ? SPC_op)〉) + (λs_tmp1.Some ? (pair … (set_acc_8_low_reg … s_tmp1 (cnH ? SPC_op)) cur_pc))). + +(* swap SPCl,A *) +(* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono + fare subroutine annidate se RA (return address) e' salvato sempre in SPC? + occore accedere a SPC e salvarne il contenuto *) +ndefinition execute_SLA ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_spc_reg … s) + (λSPC_op.opt_map … (set_spc_reg … s 〈(cnH ? SPC_op):(get_acc_8_low_reg … s)〉) + (λs_tmp1.Some ? (pair … (set_acc_8_low_reg … s_tmp1 (cnL ? SPC_op)) cur_pc))). + +(* M = A *) +ndefinition execute_STA ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + (* M = A *) + let A_op ≝ (get_acc_8_low_reg … s) in + opt_map … (multi_mode_writeb … s cur_pc auxMode_ok 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 *) + let s_tmp2 ≝ set_zflb … s_tmp1 A_op in + (* N = A7 *) + let s_tmp3 ≝ set_nflb … s_tmp2 A_op in + (* V = 0 *) + let s_tmp4 ≝ setweak_v_flag … s_tmp3 false in + (* newpc = nextpc *) + Some ? (pair … s_tmp4 new_pc) ]). + +(* M = H:X *) +ndefinition execute_STHX ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + (* M = H:X *) + opt_map … (get_indX_16_reg … s) + (λX_op.opt_map … (multi_mode_writew … 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 *) + let s_tmp2 ≝ set_zflw … s_tmp1 X_op in + (* N = R15 *) + let s_tmp3 ≝ set_nflw … s_tmp2 X_op in + (* V = 0 *) + let s_tmp4 ≝ setweak_v_flag … s_tmp3 false in + (* newpc = nextpc *) + Some ? (pair … s_tmp4 new_pc) ])). + +(* I = 0 *) +ndefinition execute_STOP ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + Some ? (pair … (setweak_i_flag … s false) cur_pc). + +(* M = X *) +ndefinition execute_STX ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + (* M = X *) + opt_map … (get_indX_8_low_reg … s) + (λX_op.opt_map … (multi_mode_writeb … s cur_pc auxMode_ok 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 *) + let s_tmp2 ≝ set_zflb … s_tmp1 X_op in + (* N = R7 *) + let s_tmp3 ≝ set_nflb … s_tmp2 X_op in + (* V = 0 *) + let s_tmp4 ≝ setweak_v_flag … s_tmp3 false in + (* newpc = nextpc *) + Some ? (pair … s_tmp4 new_pc) ])). + +(* A = A - M *) +ndefinition execute_SUB ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + execute_CMP_SBC_SUB_aux … s cur_pc i true (λC_op.λA_op.λM_op.plus_b8_dc_dc false A_op (compl_b8 M_op)). + +(* software interrupt *) +ndefinition execute_SWI ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + (* indirizzo da cui caricare il nuovo pc *) + let vector ≝ extu_w32 (get_pc_reg … (set_pc_reg … s 〈〈xF,xF〉:〈xF,xC〉〉)) in + (* push (cur_pc low) *) + opt_map … (aux_push … s (cnL ? cur_pc)) + (* push (cur_pc high *) + (λs_tmp1.opt_map … (aux_push … s_tmp1 (cnH ? cur_pc)) + (λs_tmp2.opt_map … (get_indX_8_low_reg … s_tmp2) + (* push (X) *) + (λX_op.opt_map … (aux_push … s_tmp2 X_op) + (* push (A) *) + (λs_tmp3.opt_map … (aux_push … s_tmp3 (get_acc_8_low_reg … s_tmp3)) + (* push (CCR) *) + (λs_tmp4.opt_map … (aux_push … s_tmp4 (aux_get_CCR … s_tmp4)) + (* I = 1 *) + (λs_tmp5.opt_map … (set_i_flag … s_tmp5 true) + (* load from vector high *) + (λs_tmp6.opt_map … (memory_filter_read … s_tmp6 vector) + (* load from vector low *) + (λaddrh.opt_map … (memory_filter_read … s_tmp6 (succ_w32 vector)) + (* newpc = [vector] *) + (λaddrl.Some ? (pair … s_tmp6 〈addrh:addrl〉)))))))))). + +(* flags = A *) +ndefinition execute_TAP ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + Some ? (pair … (aux_set_CCR … s (get_acc_8_low_reg … s)) cur_pc). + +(* X = A *) +ndefinition execute_TAX ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (set_indX_8_low_reg … s (get_acc_8_low_reg … 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.λcur_pc:word16.λi:aux_im_type m. + Some ? (pair … (set_acc_8_low_reg … s (aux_get_CCR … 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.λcur_pc:word16.λi:aux_im_type m. + opt_map … (multi_mode_loadb … 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 *) + let s_tmp2 ≝ set_zflb … s_tmp1 M_op in + (* N = R7 *) + let s_tmp3 ≝ set_nflb … s_tmp2 M_op in + (* V = 0 *) + let s_tmp4 ≝ setweak_v_flag … s_tmp3 false in + (* newpc = nextpc *) + Some ? (pair … s_tmp4 new_pc) ]). + +(* H:X = SP + 1 *) +ndefinition execute_TSX ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_sp_reg … s ) + (λSP_op.opt_map … (set_indX_16_reg … s (succ_w16 SP_op)) + (* H:X = SP + 1 *) + (λs_tmp.Some ? (pair … s_tmp cur_pc))). + +(* A = X *) +ndefinition execute_TXA ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_indX_8_low_reg … s) + (λX_op.Some ? (pair … (set_acc_8_low_reg … s X_op) cur_pc)). + +(* SP = H:X - 1 *) +ndefinition execute_TXS ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + opt_map … (get_indX_16_reg … s ) + (λX_op.opt_map … (set_sp_reg … s (pred_w16 X_op)) + (* SP = H:X - 1 *) + (λs_tmp.Some ? (pair … s_tmp cur_pc))). + +(* I = 0 *) +ndefinition execute_WAIT ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + Some ? (pair … (setweak_i_flag … s false) cur_pc). + +(* raccordo *) +ndefinition Freescale_execute_any ≝ +λps:Freescale_pseudo.match ps with + [ ADC ⇒ execute_ADC (* add with carry *) + | ADD ⇒ execute_ADD (* add *) + | AIS ⇒ execute_AIS (* add immediate to SP *) + | AIX ⇒ execute_AIX (* add immediate to X *) + | AND ⇒ execute_AND (* and *) + | ASL ⇒ execute_ASL (* aritmetic shift left *) + | ASR ⇒ execute_ASR (* aritmetic shift right *) + | BCC ⇒ execute_BCC (* branch if C=0 *) + | BCLRn ⇒ execute_BCLRn (* clear bit n *) + | BCS ⇒ execute_BCS (* branch if C=1 *) + | BEQ ⇒ execute_BEQ (* branch if Z=1 *) + | BGE ⇒ execute_BGE (* branch if N⊙V=0 (great or equal) *) + | BGND ⇒ execute_BGND (* !!background mode!!*) + | BGT ⇒ execute_BGT (* branch if Z|N⊙V=0 clear (great) *) + | BHCC ⇒ execute_BHCC (* branch if H=0 *) + | BHCS ⇒ execute_BHCS (* branch if H=1 *) + | BHI ⇒ execute_BHI (* branch if C|Z=0, (higher) *) + | BIH ⇒ execute_BIH (* branch if nIRQ=1 *) + | BIL ⇒ execute_BIL (* branch if nIRQ=0 *) + | BIT ⇒ execute_BIT (* flag = and (bit test) *) + | BLE ⇒ execute_BLE (* branch if Z|N⊙V=1 (less or equal) *) + | BLS ⇒ execute_BLS (* branch if C|Z=1 (lower or same) *) + | BLT ⇒ execute_BLT (* branch if N⊙1=1 (less) *) + | BMC ⇒ execute_BMC (* branch if I=0 (interrupt mask clear) *) + | BMI ⇒ execute_BMI (* branch if N=1 (minus) *) + | BMS ⇒ execute_BMS (* branch if I=1 (interrupt mask set) *) + | BNE ⇒ execute_BNE (* branch if Z=0 *) + | BPL ⇒ execute_BPL (* branch if N=0 (plus) *) + | BRA ⇒ execute_BRA (* branch always *) + | BRCLRn ⇒ execute_BRCLRn (* branch if bit n clear *) + | BRN ⇒ execute_BRN (* branch never (nop) *) + | BRSETn ⇒ execute_BRSETn (* branch if bit n set *) + | BSETn ⇒ execute_BSETn (* set bit n *) + | BSR ⇒ execute_BSR (* branch to subroutine *) + | CBEQA ⇒ execute_CBEQA (* compare (A) and BEQ *) + | CBEQX ⇒ execute_CBEQX (* compare (X) and BEQ *) + | CLC ⇒ execute_CLC (* C=0 *) + | CLI ⇒ execute_CLI (* I=0 *) + | CLR ⇒ execute_CLR (* operand=0 *) + | CMP ⇒ execute_CMP (* flag = sub (compare A) *) + | COM ⇒ execute_COM (* not (1 complement) *) + | CPHX ⇒ execute_CPHX (* flag = sub (compare H:X) *) + | CPX ⇒ execute_CPX (* flag = sub (compare X) *) + | DAA ⇒ execute_DAA (* decimal adjust A *) + | DBNZ ⇒ execute_DBNZ (* dec and BNE *) + | DEC ⇒ execute_DEC (* operand=operand-1 (decrement) *) + | DIV ⇒ execute_DIV (* div *) + | EOR ⇒ execute_EOR (* xor *) + | INC ⇒ execute_INC (* operand=operand+1 (increment) *) + | JMP ⇒ execute_JMP (* jmp word [operand] *) + | JSR ⇒ execute_JSR (* jmp to subroutine *) + | LDA ⇒ execute_LDA (* load in A *) + | LDHX ⇒ execute_LDHX (* load in H:X *) + | LDX ⇒ execute_LDX (* load in X *) + | LSR ⇒ execute_LSR (* logical shift right *) + | MOV ⇒ execute_MOV (* move *) + | MUL ⇒ execute_MUL (* mul *) + | NEG ⇒ execute_NEG (* neg (2 complement) *) + | NOP ⇒ execute_NOP (* nop *) + | NSA ⇒ execute_NSA (* nibble swap A (al:ah <- ah:al) *) + | ORA ⇒ execute_ORA (* or *) + | PSHA ⇒ execute_PSHA (* push A *) + | PSHH ⇒ execute_PSHH (* push H *) + | PSHX ⇒ execute_PSHX (* push X *) + | PULA ⇒ execute_PULA (* pop A *) + | PULH ⇒ execute_PULH (* pop H *) + | PULX ⇒ execute_PULX (* pop X *) + | ROL ⇒ execute_ROL (* rotate left *) + | ROR ⇒ execute_ROR (* rotate right *) + | RSP ⇒ execute_RSP (* reset SP (0x00FF) *) + | RTI ⇒ execute_RTI (* return from interrupt *) + | RTS ⇒ execute_RTS (* return from subroutine *) + | SBC ⇒ execute_SBC (* sub with carry*) + | SEC ⇒ execute_SEC (* C=1 *) + | SEI ⇒ execute_SEI (* I=1 *) + | SHA ⇒ execute_SHA (* swap spc_high,A *) + | SLA ⇒ execute_SLA (* swap spc_low,A *) + | STA ⇒ execute_STA (* store from A *) + | STHX ⇒ execute_STHX (* store from H:X *) + | STOP ⇒ execute_STOP (* !!stop mode!! *) + | STX ⇒ execute_STX (* store from X *) + | SUB ⇒ execute_SUB (* sub *) + | SWI ⇒ execute_SWI (* software interrupt *) + | TAP ⇒ execute_TAP (* flag=A (transfer A to process status byte *) + | TAX ⇒ execute_TAX (* X=A (transfer A to X) *) + | TPA ⇒ execute_TPA (* A=flag (transfer process status byte to A) *) + | TST ⇒ execute_TST (* flag = sub (test) *) + | TSX ⇒ execute_TSX (* X:H=SP (transfer SP to H:X) *) + | TXA ⇒ execute_TXA (* A=X (transfer X to A) *) + | TXS ⇒ execute_TXS (* SP=X:H (transfer H:X to SP) *) + | WAIT ⇒ execute_WAIT (* !!wait mode!!*) + ]. + +(* stati speciali di esecuzione *) +ndefinition Freescale_check_susp ≝ +λps:Freescale_pseudo.match ps with + [ BGND ⇒ Some ? BGND_MODE + | STOP ⇒ Some ? STOP_MODE + | WAIT ⇒ Some ? WAIT_MODE + | _ ⇒ None ? + ]. + +(* istruzioni speciali per skip *) +ndefinition Freescale_check_skip ≝ +λps:Freescale_pseudo.false. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/multivm/IP2022_multivm.ma b/helm/software/matita/contribs/ng_assembly/emulator/multivm/IP2022_multivm.ma new file mode 100755 index 000000000..e5201540f --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/multivm/IP2022_multivm.ma @@ -0,0 +1,109 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "emulator/multivm/multivm_base.ma". +include "emulator/read_write/load_write.ma". + +(* ************************************************ *) +(* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *) +(* ************************************************ *) + +(* **************** *) +(* LOGICA DELLA ALU *) +(* **************** *) + +ndefinition execute_NO ≝ +λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m. + None (ProdT (any_status m t) word16). + +(* raccordo *) +ndefinition IP2022_execute_any ≝ +λps:IP2022_pseudo.match ps with + [ ADD ⇒ execute_NO (* add *) + | ADDC ⇒ execute_NO (* add with carry *) + | AND ⇒ execute_NO (* and *) + | BREAK ⇒ execute_NO (* enter break mode *) + | BREAKX ⇒ execute_NO (* enter break mode, after skip *) + | CALL ⇒ execute_NO (* subroutine call *) + | CLR ⇒ execute_NO (* clear *) + | CLRB ⇒ execute_NO (* clear bit *) + | CMP ⇒ execute_NO (* set flags according to sub *) + | CSE ⇒ execute_NO (* confront & skip if equal *) + | CSNE ⇒ execute_NO (* confront & skip if not equal *) + | CWDT ⇒ execute_NO (* clear watch dog -- not impl. ERR *) + | DEC ⇒ execute_NO (* decrement *) + | DECSNZ ⇒ execute_NO (* decrement & skip if not zero *) + | DECSZ ⇒ execute_NO (* decrement & skip if zero *) + | FERASE ⇒ execute_NO (* flash erase -- not impl. ERR *) + | FREAD ⇒ execute_NO (* flash read -- not impl. ERR *) + | FWRITE ⇒ execute_NO (* flash write -- not impl. ERR *) + | INC ⇒ execute_NO (* increment *) + | INCSNZ ⇒ execute_NO (* increment & skip if not zero *) + | INCSZ ⇒ execute_NO (* increment & skip if zero *) + | INT ⇒ execute_NO (* interrupt -- not impl. ERR *) + | IREAD ⇒ execute_NO (* memory read *) + | IWRITE ⇒ execute_NO (* memory write *) + | JMP ⇒ execute_NO (* jump *) + | LOADH ⇒ execute_NO (* load Data Pointer High *) + | LOADL ⇒ execute_NO (* load Data Pointer Low *) + | MOV ⇒ execute_NO (* move *) + | MULS ⇒ execute_NO (* signed mul *) + | MULU ⇒ execute_NO (* unsigned mul *) + | NOP ⇒ execute_NO (* nop *) + | NOT ⇒ execute_NO (* not *) + | OR ⇒ execute_NO (* or *) + | PAGE ⇒ execute_NO (* set Page Register *) + | POP ⇒ execute_NO (* pop *) + | PUSH ⇒ execute_NO (* push *) + | RET ⇒ execute_NO (* subroutine ret *) + | RETI ⇒ execute_NO (* interrupt ret -- not impl. ERR *) + | RETNP ⇒ execute_NO (* subroutine ret & don't restore Page Register *) + | RETW ⇒ execute_NO (* subroutine ret & load W Register *) + | RL ⇒ execute_NO (* rotate left *) + | RR ⇒ execute_NO (* rotate right *) + | SB ⇒ execute_NO (* skip if bit set *) + | SETB ⇒ execute_NO (* set bit *) + | SNB ⇒ execute_NO (* skip if bit not set *) + | SPEED ⇒ execute_NO (* set Speed Register *) + | SUB ⇒ execute_NO (* sub *) + | SUBC ⇒ execute_NO (* sub with carry *) + | SWAP ⇒ execute_NO (* swap xxxxyyyy → yyyyxxxx *) + | TEST ⇒ execute_NO (* set flags according to zero test *) + | XOR ⇒ execute_NO (* xor *) + ]. + +(* stati speciali di esecuzione *) +ndefinition IP2022_check_susp ≝ +λps:IP2022_pseudo.match ps with + [ BREAK ⇒ Some ? BGND_MODE + | BREAKX ⇒ Some ? BGND_MODE + | _ ⇒ None ? + ]. + +(* istruzioni speciali per skip *) +ndefinition IP2022_check_skip ≝ +λps:IP2022_pseudo.match ps with + [ LOADH ⇒ true + | LOADL ⇒ true + | PAGE ⇒ true + | _ ⇒ false + ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm.ma b/helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm.ma new file mode 100755 index 000000000..58b672456 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm.ma @@ -0,0 +1,173 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "emulator/multivm/Freescale_multivm.ma". +include "emulator/multivm/IP2022_multivm.ma". +include "emulator/read_write/fetch.ma". + +(* raccordo *) +ndefinition execute_any ≝ +λm.match m + return λm.aux_pseudo_type m → Πt.any_status m t → word16 → + aux_im_type m → option (ProdT (any_status m t) word16) + with + [ HC05 ⇒ λps:aux_pseudo_type ?.Freescale_execute_any ps ? + | HC08 ⇒ λps:aux_pseudo_type ?.Freescale_execute_any ps ? + | HCS08 ⇒ λps:aux_pseudo_type ?.Freescale_execute_any ps ? + | RS08 ⇒ λps:aux_pseudo_type ?.Freescale_execute_any ps ? + | IP2022 ⇒ λps:aux_pseudo_type ?.IP2022_execute_any ps ? + ]. + +(* raccordo *) +ndefinition check_susp_ps ≝ +λm.match m + return λm.aux_pseudo_type m → option susp_type + with + [ HC05 ⇒ Freescale_check_susp + | HC08 ⇒ Freescale_check_susp + | HCS08 ⇒ Freescale_check_susp + | RS08 ⇒ Freescale_check_susp + | IP2022 ⇒ IP2022_check_susp + ]. + +ndefinition check_susp_s ≝ +λm,t.λs:any_status m t. + opt_map … (get_speed_reg … s) + (λspeed.match eq_ex speed xF with + [ true ⇒ Some ? STOP_MODE + | false ⇒ None ? ]). + +ndefinition check_susp ≝ +λm,t.λs:any_status m t.λps:aux_pseudo_type m. + match check_susp_s … s with + [ None ⇒ check_susp_ps m ps + | Some susp ⇒ Some ? susp + ]. + +(* raccordo *) +ndefinition check_skip ≝ +λm.match m + return λm.aux_pseudo_type m → bool + with + [ HC05 ⇒ Freescale_check_skip + | HC08 ⇒ Freescale_check_skip + | HCS08 ⇒ Freescale_check_skip + | RS08 ⇒ Freescale_check_skip + | IP2022 ⇒ IP2022_check_skip + ]. + +(* **** *) +(* TICK *) +(* **** *) + +(* - 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 ≝ + TickERR : A → error_type → tick_result A +| TickSUSP : A → susp_type → tick_result A +| TickOK : A → tick_result A. + +(* l'esecuzione e' considerata atomica quindi nel caso di un'instruzione + da 3 cicli la successione sara' + ([fetch/decode] s,clk:None) → + ( s,clk:Some 1,pseudo,mode,3,cur_pc) → + ( s,clk:Some 2,pseudo,mode,3,cur_pc) → + ([execute] s',clk:None) *) +ndefinition tick_execute ≝ +λm,t.λs:any_status m t. +λps:aux_pseudo_type m.λi:aux_im_type m. +λcur_pc:word16. + match execute_any m ps t s cur_pc i with + (* errore! fine esecuzione *) + [ None ⇒ TickERR ? (set_clk_desc … s (None ?)) ILL_FETCH_AD + (* ok, aggiornamento centralizzato *) + | Some S_newPC ⇒ match S_newPC with + [ pair s_tmp1 new_pc ⇒ + (* clk azzerato *) + let s_tmp2 ≝ set_clk_desc … s_tmp1 (None ?) in + (* aggiornamento pc *) + let s_tmp3 ≝ match eq_w16 (get_pc_reg … s) (get_pc_reg … s_tmp1) with + (* ok, new_pc → pc *) + [ true ⇒ set_pc_reg … s_tmp2 new_pc + (* effetto collaterale modifica pc! scartare new_pc *) + | false ⇒ s_tmp2 ] in + match check_susp … s ps with + (* esecuzione continua *) + [ None ⇒ TickOK ? s_tmp3 + (* esecuzione sospesa *) + | Some susp ⇒ TickSUSP ? s_tmp3 susp + ]]]. + +(* avanza fra fetch / countdown / execute *) +ndefinition tick_skip_aux ≝ +λm,t.λs:any_status m t. + match get_skip_mode … s with + [ None ⇒ false + | Some b ⇒ b ]. + +ndefinition tick ≝ +λm,t.λs:any_status m t. + match clk_desc … s with + (* e' il momento del fetch *) + [ None ⇒ match fetch … s with + (* errore nel fetch/decode? riportato in output, nessun avanzamento *) + [ FetchERR err ⇒ TickERR ? s err + (* nessun errore nel fetch *) + | FetchOK info cur_pc ⇒ match tick_skip_aux … s with + (* skip mode! *) + [ true ⇒ TickOK ? (set_clk_desc … + (set_pc_reg … + (match check_skip m (fst4T … info) with + [ true ⇒ s | false ⇒ setweak_skip_mode … s false ]) cur_pc) (None ?)) + (* ciclo normale *) + | false ⇒ match eq_b8 〈x0,x1〉 (fth4T … info) with + (* un solo clk, execute subito *) + [ true ⇒ tick_execute … s (fst4T … info) (snd4T … info) cur_pc + (* piu' clk, execute rimandata *) + | false ⇒ TickOK ? (set_clk_desc … s + (Some ? (quintuple … 〈x0,x1〉 (fst4T … info) (snd4T … info) + (fth4T … info) cur_pc))) + ] + ] + ] + (* fetch gia' eseguito, e' il turno di execute? *) + | Some info ⇒ match eq_b8 (succ_b8 (fst5T … info)) (fth5T … info) with + (* si *) + [ true ⇒ tick_execute … s (snd5T … info) (thd5T … info) (fft5T … info) + (* no, avanzamento cur_clk *) + | false ⇒ TickOK ? (set_clk_desc … s + (Some ? (quintuple … (succ_b8 (fst5T … info)) (snd5T … info) + (thd5T … info) (fth5T … info) (fft5T … info)))) + ] + ]. + +(* ********** *) +(* ESECUZIONE *) +(* ********** *) + +nlet rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝ + match s with + [ TickERR s' error ⇒ TickERR ? s' error + | TickSUSP s' susp ⇒ TickSUSP ? s' susp + | TickOK s' ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ] + ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm_base.ma b/helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm_base.ma new file mode 100755 index 000000000..9b5f34013 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm_base.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "common/theory.ma". +include "emulator/status/status_setter.ma". + +ndefinition set_zflb ≝ +λm,t.λs:any_status m t.λb.set_z_flag … s (eq_b8 b 〈x0,x0〉). +ndefinition set_zflw ≝ +λm,t.λs:any_status m t.λw.set_z_flag … s (eq_w16 w 〈〈x0,x0〉:〈x0,x0〉〉). + +ndefinition set_nflb ≝ +λm,t.λs:any_status m t.λb.setweak_n_flag … s (getMSB_b8 b). +ndefinition set_nflw ≝ +λm,t.λs:any_status m t.λw.setweak_n_flag … s (getMSB_w16 w). + +(* enumerazione delle possibili modalita' di sospensione *) +ninductive susp_type : Type ≝ + BGND_MODE: susp_type +| STOP_MODE: susp_type +| WAIT_MODE: susp_type. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm_lemmas.ma new file mode 100755 index 000000000..4d63ea0fc --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/multivm/multivm_lemmas.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "emulator/multivm/multivm.ma". +include "common/nat_lemmas.ma". + +nlemma breakpoint_err : ∀m,t,s,err,n.execute m t (TickERR ? s err) n = TickERR ? s err. + #m; #t; #s; #err; #n; + ncases n; + ##[ ##2: #n1; ##] + nnormalize; + napply refl_eq. +nqed. + +nlemma breakpoint_susp : ∀m,t,s,susp,n.execute m t (TickSUSP ? s susp) n = TickSUSP ? s susp. + #m; #t; #s; #susp; #n; + ncases n; + ##[ ##2: #n1; ##] + nnormalize; + 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 + ##| ##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 + ##| ##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 + ##] + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma index f14b38b19..38c9053e3 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma @@ -195,7 +195,7 @@ ndefinition aux_inc_indX_16 ≝ (λs_tmp.Some ? s_tmp)). ndefinition Freescale_multi_mode_load_auxb ≝ -λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.match i with +λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with (* NO: non ci sono indicazioni *) [ MODE_INH ⇒ None ? (* restituisce A *) @@ -276,7 +276,7 @@ ndefinition Freescale_multi_mode_load_auxb ≝ ]. ndefinition Freescale_multi_mode_load_auxw ≝ -λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.match i with +λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with (* NO: non ci sono indicazioni *) [ MODE_INH ⇒ None ? (* NO: solo lettura/scrittura byte *) @@ -417,7 +417,7 @@ ndefinition Freescale_multi_mode_load_auxw ≝ (* **************************************** *) ndefinition Freescale_multi_mode_write_auxb ≝ -λm,t.λs:any_status m t.λpco,cur_pc:word16.λflag:aux_mod_type.λi:Freescale_instr_mode.λwriteb:byte8.match i with +λm,t.λs:any_status m t.λcur_pc:word16.λflag:aux_mod_type.λi:Freescale_instr_mode.λwriteb:byte8.match i with (* NO: non ci sono indicazioni *) [ MODE_INH ⇒ None ? (* scrive A *) @@ -507,7 +507,7 @@ ndefinition Freescale_multi_mode_write_auxb ≝ ]. ndefinition Freescale_multi_mode_write_auxw ≝ -λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.λwritew:word16.match i with +λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwritew:word16.match i with (* NO: non ci sono indicazioni *) [ MODE_INH ⇒ None ? (* NO: solo lettura/scrittura byte *) diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma index eccc4eefb..f7040de6d 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma @@ -25,8 +25,8 @@ include "emulator/read_write/load_write_base.ma". (* lettura da [OLD PC<<1 + 1] : argomento non caricato dal fetch word-aligned *) ndefinition mode_IMM1_load ≝ -λt:memory_impl.λs:any_status IP2022 t.λpco:word16. - mem_read_s … s (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.pco〉). +λt:memory_impl.λs:any_status IP2022 t. + mem_read_s … s (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.(get_pc_reg … s)〉). (* SCHEMA: ADDRX=0x00 [ADDRH|ADDRL] 16Kb PROGRAM RAM @@ -55,8 +55,8 @@ ndefinition mode_ADDR_write ≝ (* IMM1 > 0 : lettura/scrittura da [IMM1] *) (* else : lettura/scrittura da [IP] : IP ≥ 0x20 *) ndefinition mode_DIR1IP_aux ≝ -λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λT.λf:word32 → option T. - opt_map … (mode_IMM1_load t s pco) +λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T. + opt_map … (mode_IMM1_load t s) (λaddr.match eq_b8 addr 〈x0,x0〉 with (* xxxxxxx0 00000000 → [IP] *) [ true ⇒ opt_map … (get_ip_reg … s) @@ -71,8 +71,8 @@ ndefinition mode_DIR1IP_aux ≝ (* IMM1 < 0x80 : lettura/scrittura da [DP+IMM1] : DP+IMM1 ≥ 0x20 *) (* else : lettura/scrittura da [SP+IMM1] : SP+IMM1 ≥ 0x20 *) ndefinition mode_DPSP_aux ≝ -λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λT.λf:word32 → option T. - opt_map … (mode_IMM1_load t s pco) +λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T. + opt_map … (mode_IMM1_load t s) (λaddr.opt_map … (match getMSB_b8 addr with (* xxxxxxx1 1nnnnnnn → [SP+IMM1] *) [ true ⇒ get_sp_reg … s @@ -85,37 +85,37 @@ ndefinition mode_DPSP_aux ≝ (* FR0 *) ndefinition mode_FR0_load ≝ -λt:memory_impl.λs:any_status IP2022 t.λpco:word16. - mode_DIR1IP_aux t s pco byte8 (memory_filter_read … s). +λt:memory_impl.λs:any_status IP2022 t. + mode_DIR1IP_aux t s byte8 (memory_filter_read … s). ndefinition mode_FR0n_load ≝ -λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct. - mode_DIR1IP_aux t s pco bool (λaddr.memory_filter_read_bit … s addr sub). +λt:memory_impl.λs:any_status IP2022 t.λsub:oct. + mode_DIR1IP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub). ndefinition mode_FR0_write ≝ -λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λflag:aux_mod_type.λval:byte8. - mode_DIR1IP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val). +λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8. + mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val). ndefinition mode_FR0n_write ≝ -λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct.λval:bool. - mode_DIR1IP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val). +λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool. + mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val). (* FR1 *) ndefinition mode_FR1_load ≝ -λt:memory_impl.λs:any_status IP2022 t.λpco:word16. - mode_DPSP_aux t s pco byte8 (memory_filter_read … s). +λt:memory_impl.λs:any_status IP2022 t. + mode_DPSP_aux t s byte8 (memory_filter_read … s). ndefinition mode_FR1n_load ≝ -λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct. - mode_DPSP_aux t s pco bool (λaddr.memory_filter_read_bit … s addr sub). +λt:memory_impl.λs:any_status IP2022 t.λsub:oct. + mode_DPSP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub). ndefinition mode_FR1_write ≝ -λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λflag:aux_mod_type.λval:byte8. - mode_DPSP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val). +λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8. + mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val). ndefinition mode_FR1n_write ≝ -λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct.λval:bool. - mode_DPSP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val). +λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool. + mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val). (* ************************************** *) (* raccordo di tutte le possibili letture *) @@ -127,7 +127,7 @@ ndefinition aux_inc_addr2 ≝ set_addr_reg_sIP2022 t s (succ_w24 (succ_w24 (get_addr_reg_IP2022 (alu … s)))). ndefinition IP2022_multi_mode_load_auxb ≝ -λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λi:IP2022_instr_mode.match i with +λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with (* NO: non ci sono indicazioni *) [ MODE_INH ⇒ None ? (* NO: solo word *) @@ -138,7 +138,7 @@ ndefinition IP2022_multi_mode_load_auxb ≝ (* IMM3 *) | MODE_IMM3 o ⇒ Some ? (triple … s (extu_b8 (ex_of_oct o)) cur_pc) (* IMM8 *) - | MODE_IMM8 ⇒ opt_map … (mode_IMM1_load t s pco) + | MODE_IMM8 ⇒ opt_map … (mode_IMM1_load t s) (λb.Some ? (triple … s b cur_pc)) (* NO: solo lettura word *) | MODE_IMM13 _ ⇒ None ? @@ -153,15 +153,15 @@ ndefinition IP2022_multi_mode_load_auxb ≝ | MODE_W_and_FR1 ⇒ None ? (* [FRn] *) - | MODE_FR0n o ⇒ opt_map … (mode_FR0n_load t s pco o) + | MODE_FR0n o ⇒ opt_map … (mode_FR0n_load t s o) (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc)) (* [FRn] *) - | MODE_FR1n o ⇒ opt_map … (mode_FR1n_load t s pco o) + | MODE_FR1n o ⇒ opt_map … (mode_FR1n_load t s o) (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc)) ]. ndefinition IP2022_multi_mode_load_auxw ≝ -λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λi:IP2022_instr_mode.match i with +λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with (* NO: non ci sono indicazioni *) [ MODE_INH ⇒ None ? (* [ADDR] *) @@ -176,20 +176,20 @@ ndefinition IP2022_multi_mode_load_auxw ≝ (* NO: solo lettura byte *) | MODE_IMM8 ⇒ None ? (* IMM13 *) - | MODE_IMM13 bt ⇒ opt_map … (mode_IMM1_load t s pco) + | MODE_IMM13 bt ⇒ opt_map … (mode_IMM1_load t s) (λb.Some ? (triple … s 〈(b8_of_bit bt):b〉 cur_pc)) (* FR, W → FR *) - | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_load t s pco) + | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_load t s) (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc)) (* FR, W → FR *) - | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_load t s pco) + | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_load t s) (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc)) (* W, FR → W *) - | MODE_W_and_FR0 ⇒ opt_map … (mode_FR0_load t s pco) + | MODE_W_and_FR0 ⇒ opt_map … (mode_FR0_load t s) (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc)) (* W, FR → W *) - | MODE_W_and_FR1 ⇒ opt_map … (mode_FR1_load t s pco) + | MODE_W_and_FR1 ⇒ opt_map … (mode_FR1_load t s) (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc)) (* NO: solo byte *) @@ -203,7 +203,7 @@ ndefinition IP2022_multi_mode_load_auxw ≝ (* **************************************** *) ndefinition IP2022_multi_mode_write_auxb ≝ -λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λflag:aux_mod_type.λi:IP2022_instr_mode.λwriteb:byte8.match i with +λt.λs:any_status IP2022 t.λcur_pc:word16.λflag:aux_mod_type.λi:IP2022_instr_mode.λwriteb:byte8.match i with (* NO: non ci sono indicazioni *) [ MODE_INH ⇒ None ? (* NO: solo word *) @@ -219,10 +219,10 @@ ndefinition IP2022_multi_mode_write_auxb ≝ | MODE_IMM13 _ ⇒ None ? (* FR, W → FR *) - | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_write t s pco flag writeb) + | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_write t s flag writeb) (λs'.Some ? (pair … s' cur_pc)) (* FR, W → FR *) - | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_write t s pco flag writeb) + | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_write t s flag writeb) (λs'.Some ? (pair … s' cur_pc)) (* W, FR → W *) | MODE_W_and_FR0 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc) @@ -230,15 +230,15 @@ ndefinition IP2022_multi_mode_write_auxb ≝ | MODE_W_and_FR1 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc) (* [FRn] *) - | MODE_FR0n o ⇒ opt_map … (mode_FR0n_write t s pco o (getn_array8T o ? (bits_of_byte8 writeb))) + | MODE_FR0n o ⇒ opt_map … (mode_FR0n_write t s o (getn_array8T o ? (bits_of_byte8 writeb))) (λs'.Some ? (pair … s' cur_pc)) (* [FRn] *) - | MODE_FR1n o ⇒ opt_map … (mode_FR1n_write t s pco o (getn_array8T o ? (bits_of_byte8 writeb))) + | MODE_FR1n o ⇒ opt_map … (mode_FR1n_write t s o (getn_array8T o ? (bits_of_byte8 writeb))) (λs'.Some ? (pair … s' cur_pc)) ]. ndefinition IP2022_multi_mode_write_auxw ≝ -λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λi:IP2022_instr_mode.λwritew:word16.match i with +λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.λwritew:word16.match i with (* NO: non ci sono indicazioni *) [ MODE_INH ⇒ None ? (* [ADDR] *) diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma index 1d51f2bcf..fbdafebe0 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma @@ -31,23 +31,23 @@ ninductive error_type : Type ≝ . (* - errore: interessa solo l'errore - - ok: interessa info, vecchio pc, nuovo pc *) + - ok: interessa info, nuovo pc *) ninductive fetch_result (A:Type) : Type ≝ FetchERR : error_type → fetch_result A -| FetchOK : A → word16 → word16 → fetch_result A. +| FetchOK : A → word16 → fetch_result A. ndefinition fetch_byte_aux ≝ -λm:mcu_type.λpco,pcn:word16.λbh:byte8. +λm:mcu_type.λcur_pc:word16.λbh:byte8. match full_info_of_word16 m (Byte bh) with [ None ⇒ FetchERR ? ILL_FETCH_AD - | Some info ⇒ FetchOK ? info pco pcn + | Some info ⇒ FetchOK ? info cur_pc ]. ndefinition fetch_word_aux ≝ -λm:mcu_type.λpco,pcn:word16.λw:word16. +λm:mcu_type.λcur_pc:word16.λw:word16. match full_info_of_word16 m (Word w) with [ None ⇒ FetchERR ? ILL_FETCH_AD - | Some info ⇒ FetchOK ? info pco pcn + | Some info ⇒ FetchOK ? info cur_pc ]. (* opcode a byte : HC05 / RS08 *) @@ -55,7 +55,7 @@ ndefinition fetch_byte ≝ λm:mcu_type.λfR:word32 → option byte8.λpc:word16. match fR (extu_w32 pc) with [ None ⇒ FetchERR ? ILL_FETCH_AD - | Some bh ⇒ fetch_byte_aux m pc (succ_w16 pc) bh ]. + | Some bh ⇒ fetch_byte_aux m (succ_w16 pc) bh ]. (* opcode a byte o 0x9E + byte : HC08 / HCS08 *) ndefinition Freescale_fetch_byte_or_word ≝ @@ -65,9 +65,9 @@ ndefinition Freescale_fetch_byte_or_word ≝ | Some bh ⇒ match eq_b8 bh 〈x9,xE〉 with [ true ⇒ match fR (extu_w32 (succ_w16 pc)) with [ None ⇒ FetchERR ? ILL_FETCH_AD - | Some bl ⇒ fetch_word_aux m pc (succ_w16 (succ_w16 pc)) 〈bh:bl〉 + | Some bl ⇒ fetch_word_aux m (succ_w16 (succ_w16 pc)) 〈bh:bl〉 ] - | false ⇒ fetch_byte_aux m pc (succ_w16 pc) bh + | false ⇒ fetch_byte_aux m (succ_w16 pc) bh ] ]. @@ -81,9 +81,9 @@ ndefinition IP2022_fetch_byte_or_word ≝ | Some bh ⇒ match eq_b8 bh 〈x0,x0〉 with [ true ⇒ match fR (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.pc〉) with [ None ⇒ FetchERR ? ILL_FETCH_AD - | Some bl ⇒ fetch_word_aux m pc (succ_w16 pc) 〈bh:bl〉 + | Some bl ⇒ fetch_word_aux m (succ_w16 pc) 〈bh:bl〉 ] - | false ⇒ fetch_byte_aux m pc (succ_w16 pc) bh + | false ⇒ fetch_byte_aux m (succ_w16 pc) bh ] ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma index 73db58f81..3c24d528c 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma @@ -29,7 +29,7 @@ include "emulator/read_write/IP2022_load_write.ma". ndefinition multi_mode_loadb ≝ λm.match m - return λm.Πt.any_status m t → word16 → word16 → aux_im_type m → + return λm.Πt.any_status m t → word16 → aux_im_type m → option (Prod3T (any_status m t) byte8 word16) with [ HC05 ⇒ Freescale_multi_mode_load_auxb HC05 @@ -41,7 +41,7 @@ ndefinition multi_mode_loadb ≝ ndefinition multi_mode_loadw ≝ λm.match m - return λm.Πt.any_status m t → word16 → word16 → aux_im_type m → + return λm.Πt.any_status m t → word16 → aux_im_type m → option (Prod3T (any_status m t) word16 word16) with [ HC05 ⇒ Freescale_multi_mode_load_auxw HC05 @@ -51,15 +51,13 @@ ndefinition multi_mode_loadw ≝ | IP2022 ⇒ IP2022_multi_mode_load_auxw ]. -(* tutte le modalita' di lettura: false=loadb true=loadw *) - (* **************************************** *) (* raccordo di tutte le possibili scritture *) (* **************************************** *) ndefinition multi_mode_writeb ≝ λm.match m - return λm.Πt.any_status m t → word16 → word16 → aux_mod_type → aux_im_type m → byte8 → + return λm.Πt.any_status m t → word16 → aux_mod_type → aux_im_type m → byte8 → option (ProdT (any_status m t) word16) with [ HC05 ⇒ Freescale_multi_mode_write_auxb HC05 @@ -71,7 +69,7 @@ ndefinition multi_mode_writeb ≝ ndefinition multi_mode_writew ≝ λm.match m - return λm.Πt.any_status m t → word16 → word16 → aux_im_type m → word16 → + return λm.Πt.any_status m t → word16 → aux_im_type m → word16 → option (ProdT (any_status m t) word16) with [ HC05 ⇒ Freescale_multi_mode_write_auxw HC05 diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma index f625e71db..d3d6eddef 100755 --- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma +++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma @@ -138,6 +138,11 @@ ndefinition compl_b8 ≝ [ true ⇒ succ_b8 (not_b8 b) | false ⇒ not_b8 (pred_b8 b) ]. +(* operatore abs *) +ndefinition abs_b8 ≝ +λb:byte8.match getMSB_b8 b with + [ true ⇒ compl_b8 b | false ⇒ b ]. + (* operatore x in [inf,sup] o in sup],[inf *) ndefinition inrange_b8 ≝ λx,inf,sup:byte8. @@ -146,7 +151,7 @@ ndefinition inrange_b8 ≝ (le_b8 inf x) (le_b8 x sup). (* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *) -ndefinition mul_ex ≝ +ndefinition mulu_ex ≝ λe1,e2:exadecim.match e1 with [ x0 ⇒ match e2 with [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x0〉 | x2 ⇒ 〈x0,x0〉 | x3 ⇒ 〈x0,x0〉 @@ -230,6 +235,91 @@ ndefinition mul_ex ≝ | xC ⇒ 〈xB,x4〉 | xD ⇒ 〈xC,x3〉 | xE ⇒ 〈xD,x2〉 | xF ⇒ 〈xE,x1〉 ] ]. +(* operatore moltiplicazione con segno *) +ndefinition muls_ex ≝ +λe1,e2:exadecim.match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x0〉 | x2 ⇒ 〈x0,x0〉 | x3 ⇒ 〈x0,x0〉 + | x4 ⇒ 〈x0,x0〉 | x5 ⇒ 〈x0,x0〉 | x6 ⇒ 〈x0,x0〉 | x7 ⇒ 〈x0,x0〉 + | x8 ⇒ 〈x0,x0〉 | x9 ⇒ 〈x0,x0〉 | xA ⇒ 〈x0,x0〉 | xB ⇒ 〈x0,x0〉 + | xC ⇒ 〈x0,x0〉 | xD ⇒ 〈x0,x0〉 | xE ⇒ 〈x0,x0〉 | xF ⇒ 〈x0,x0〉 ] + | x1 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x1〉 | x2 ⇒ 〈x0,x2〉 | x3 ⇒ 〈x0,x3〉 + | x4 ⇒ 〈x0,x4〉 | x5 ⇒ 〈x0,x5〉 | x6 ⇒ 〈x0,x6〉 | x7 ⇒ 〈x0,x7〉 + | x8 ⇒ 〈xF,x8〉 | x9 ⇒ 〈xF,x9〉 | xA ⇒ 〈xF,xA〉 | xB ⇒ 〈xF,xB〉 + | xC ⇒ 〈xF,xC〉 | xD ⇒ 〈xF,xD〉 | xE ⇒ 〈xF,xE〉 | xF ⇒ 〈xF,xF〉 ] + | x2 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x2〉 | x2 ⇒ 〈x0,x4〉 | x3 ⇒ 〈x0,x6〉 + | x4 ⇒ 〈x0,x8〉 | x5 ⇒ 〈x0,xA〉 | x6 ⇒ 〈x0,xC〉 | x7 ⇒ 〈x0,xE〉 + | x8 ⇒ 〈xF,x0〉 | x9 ⇒ 〈xF,x2〉 | xA ⇒ 〈xF,x4〉 | xB ⇒ 〈xF,x6〉 + | xC ⇒ 〈xF,x8〉 | xD ⇒ 〈xF,xA〉 | xE ⇒ 〈xF,xC〉 | xF ⇒ 〈xF,xE〉 ] + | x3 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x3〉 | x2 ⇒ 〈x0,x6〉 | x3 ⇒ 〈x0,x9〉 + | x4 ⇒ 〈x0,xC〉 | x5 ⇒ 〈x0,xF〉 | x6 ⇒ 〈x1,x2〉 | x7 ⇒ 〈x1,x5〉 + | x8 ⇒ 〈xE,x8〉 | x9 ⇒ 〈xE,xB〉 | xA ⇒ 〈xE,xE〉 | xB ⇒ 〈xF,x1〉 + | xC ⇒ 〈xF,x4〉 | xD ⇒ 〈xF,x7〉 | xE ⇒ 〈xF,xA〉 | xF ⇒ 〈xF,xD〉 ] + | x4 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x4〉 | x2 ⇒ 〈x0,x8〉 | x3 ⇒ 〈x0,xC〉 + | x4 ⇒ 〈x1,x0〉 | x5 ⇒ 〈x1,x4〉 | x6 ⇒ 〈x1,x8〉 | x7 ⇒ 〈x1,xC〉 + | x8 ⇒ 〈xE,x0〉 | x9 ⇒ 〈xE,x4〉 | xA ⇒ 〈xE,x8〉 | xB ⇒ 〈xE,xC〉 + | xC ⇒ 〈xF,x0〉 | xD ⇒ 〈xF,x4〉 | xE ⇒ 〈xF,x8〉 | xF ⇒ 〈xF,xC〉 ] + | x5 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x5〉 | x2 ⇒ 〈x0,xA〉 | x3 ⇒ 〈x0,xF〉 + | x4 ⇒ 〈x1,x4〉 | x5 ⇒ 〈x1,x9〉 | x6 ⇒ 〈x1,xE〉 | x7 ⇒ 〈x2,x3〉 + | x8 ⇒ 〈xD,x8〉 | x9 ⇒ 〈xD,xD〉 | xA ⇒ 〈xE,x2〉 | xB ⇒ 〈xE,x7〉 + | xC ⇒ 〈xE,xC〉 | xD ⇒ 〈xF,x1〉 | xE ⇒ 〈xF,x6〉 | xF ⇒ 〈xF,xB〉 ] + | x6 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x6〉 | x2 ⇒ 〈x0,xC〉 | x3 ⇒ 〈x1,x2〉 + | x4 ⇒ 〈x1,x8〉 | x5 ⇒ 〈x1,xE〉 | x6 ⇒ 〈x2,x4〉 | x7 ⇒ 〈x2,xA〉 + | x8 ⇒ 〈xD,x0〉 | x9 ⇒ 〈xD,x6〉 | xA ⇒ 〈xD,xC〉 | xB ⇒ 〈xE,x2〉 + | xC ⇒ 〈xE,x8〉 | xD ⇒ 〈xE,xE〉 | xE ⇒ 〈xF,x4〉 | xF ⇒ 〈xF,xA〉 ] + | x7 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x7〉 | x2 ⇒ 〈x0,xE〉 | x3 ⇒ 〈x1,x5〉 + | x4 ⇒ 〈x1,xC〉 | x5 ⇒ 〈x2,x3〉 | x6 ⇒ 〈x2,xA〉 | x7 ⇒ 〈x3,x1〉 + | x8 ⇒ 〈xC,x8〉 | x9 ⇒ 〈xC,xF〉 | xA ⇒ 〈xD,x6〉 | xB ⇒ 〈xD,xD〉 + | xC ⇒ 〈xE,x4〉 | xD ⇒ 〈xE,xB〉 | xE ⇒ 〈xF,x2〉 | xF ⇒ 〈xF,x9〉 ] + | x8 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,x8〉 | x2 ⇒ 〈xF,x0〉 | x3 ⇒ 〈xE,x8〉 + | x4 ⇒ 〈xE,x0〉 | x5 ⇒ 〈xD,x8〉 | x6 ⇒ 〈xD,x0〉 | x7 ⇒ 〈xC,x8〉 + | x8 ⇒ 〈x4,x0〉 | x9 ⇒ 〈x3,x8〉 | xA ⇒ 〈x3,x0〉 | xB ⇒ 〈x2,x8〉 + | xC ⇒ 〈x2,x0〉 | xD ⇒ 〈x1,x8〉 | xE ⇒ 〈x1,x0〉 | xF ⇒ 〈x0,x8〉 ] + | x9 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,x9〉 | x2 ⇒ 〈xF,x2〉 | x3 ⇒ 〈xE,xB〉 + | x4 ⇒ 〈xE,x4〉 | x5 ⇒ 〈xD,xD〉 | x6 ⇒ 〈xD,x6〉 | x7 ⇒ 〈xC,xF〉 + | x8 ⇒ 〈x3,x8〉 | x9 ⇒ 〈x3,x1〉 | xA ⇒ 〈x2,xA〉 | xB ⇒ 〈x2,x3〉 + | xC ⇒ 〈x1,xC〉 | xD ⇒ 〈x1,x5〉 | xE ⇒ 〈x0,xE〉 | xF ⇒ 〈x0,x7〉 ] + | xA ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xA〉 | x2 ⇒ 〈xF,x4〉 | x3 ⇒ 〈xE,xE〉 + | x4 ⇒ 〈xE,x8〉 | x5 ⇒ 〈xE,x2〉 | x6 ⇒ 〈xD,xC〉 | x7 ⇒ 〈xD,x6〉 + | x8 ⇒ 〈x3,x0〉 | x9 ⇒ 〈x2,xA〉 | xA ⇒ 〈x2,x4〉 | xB ⇒ 〈x1,xE〉 + | xC ⇒ 〈x1,x8〉 | xD ⇒ 〈x1,x2〉 | xE ⇒ 〈x0,xC〉 | xF ⇒ 〈x0,x6〉 ] + | xB ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xB〉 | x2 ⇒ 〈xF,x6〉 | x3 ⇒ 〈xF,x1〉 + | x4 ⇒ 〈xE,xC〉 | x5 ⇒ 〈xE,x7〉 | x6 ⇒ 〈xE,x2〉 | x7 ⇒ 〈xD,xD〉 + | x8 ⇒ 〈x2,x8〉 | x9 ⇒ 〈x2,x3〉 | xA ⇒ 〈x1,xE〉 | xB ⇒ 〈x1,x9〉 + | xC ⇒ 〈x1,x4〉 | xD ⇒ 〈x0,xF〉 | xE ⇒ 〈x0,xA〉 | xF ⇒ 〈x0,x5〉 ] + | xC ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xC〉 | x2 ⇒ 〈xF,x8〉 | x3 ⇒ 〈xF,x4〉 + | x4 ⇒ 〈xF,x0〉 | x5 ⇒ 〈xE,xC〉 | x6 ⇒ 〈xE,x8〉 | x7 ⇒ 〈xE,x4〉 + | x8 ⇒ 〈x2,x0〉 | x9 ⇒ 〈x1,xC〉 | xA ⇒ 〈x1,x8〉 | xB ⇒ 〈x1,x4〉 + | xC ⇒ 〈x1,x0〉 | xD ⇒ 〈x0,xC〉 | xE ⇒ 〈x0,x8〉 | xF ⇒ 〈x0,x4〉 ] + | xD ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xD〉 | x2 ⇒ 〈xF,xA〉 | x3 ⇒ 〈xF,x7〉 + | x4 ⇒ 〈xF,x4〉 | x5 ⇒ 〈xF,x1〉 | x6 ⇒ 〈xE,xE〉 | x7 ⇒ 〈xE,xB〉 + | x8 ⇒ 〈x1,x8〉 | x9 ⇒ 〈x1,x5〉 | xA ⇒ 〈x1,x2〉 | xB ⇒ 〈x0,xF〉 + | xC ⇒ 〈x0,xC〉 | xD ⇒ 〈x0,x9〉 | xE ⇒ 〈x0,x6〉 | xF ⇒ 〈x0,x3〉 ] + | xE ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xE〉 | x2 ⇒ 〈xF,xC〉 | x3 ⇒ 〈xF,xA〉 + | x4 ⇒ 〈xF,x8〉 | x5 ⇒ 〈xF,x6〉 | x6 ⇒ 〈xF,x4〉 | x7 ⇒ 〈xF,x2〉 + | x8 ⇒ 〈x1,x0〉 | x9 ⇒ 〈x0,xE〉 | xA ⇒ 〈x0,xC〉 | xB ⇒ 〈x0,xA〉 + | xC ⇒ 〈x0,x8〉 | xD ⇒ 〈x0,x6〉 | xE ⇒ 〈x0,x4〉 | xF ⇒ 〈x0,x2〉 ] + | xF ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈xF,xF〉 | x2 ⇒ 〈xF,xE〉 | x3 ⇒ 〈xF,xD〉 + | x4 ⇒ 〈xF,xC〉 | x5 ⇒ 〈xF,xB〉 | x6 ⇒ 〈xF,xA〉 | x7 ⇒ 〈xF,x9〉 + | x8 ⇒ 〈x0,x8〉 | x9 ⇒ 〈x0,x7〉 | xA ⇒ 〈x0,x6〉 | xB ⇒ 〈x0,x5〉 + | xC ⇒ 〈x0,x4〉 | xD ⇒ 〈x0,x3〉 | xE ⇒ 〈x0,x2〉 | xF ⇒ 〈x0,x1〉 ] + ]. + (* correzione per somma su BCD *) (* input: halfcarry,carry,X(BCD+BCD) *) (* output: X',carry' *) @@ -247,7 +337,7 @@ ndefinition daa_b8 ≝ let X'' ≝ match c with [ true ⇒ plus_b8_d_d X' 〈x6,x0〉 | false ⇒ X' ] in - pair … X'' c + pair … c X'' (* [X:0x9A-0xFF] *) (* c' = 1 *) (* X' = [X:0x9A-0xFF] @@ -258,34 +348,9 @@ ndefinition daa_b8 ≝ [ true ⇒ X | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in - pair … X'' true + pair … true X'' ]. -(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *) -nlet rec div_b8_ex_aux (divd:byte8) (divs:byte8) (molt:exadecim) (q:exadecim) (n:nat) on n ≝ - let w' ≝ plus_b8_d_d divd (compl_b8 divs) in - match n with - [ O ⇒ match le_b8 divs divd with - [ true ⇒ triple … (or_ex molt q) (cnL ? w') (⊖ (eq_ex (cnH ? w') x0)) - | false ⇒ triple … q (cnL ? divd) (⊖ (eq_ex (cnH ? divd) x0)) ] - | S n' ⇒ match le_b8 divs divd with - [ true ⇒ div_b8_ex_aux w' (ror_b8 divs) (ror_ex molt) (or_ex molt q) n' - | false ⇒ div_b8_ex_aux divd (ror_b8 divs) (ror_ex molt) q n' ]]. - -ndefinition div_b8_ex ≝ -λb:byte8.λe:exadecim.match eq_ex e x0 with -(* la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato *) - [ true ⇒ triple … xF (cnL ? b) true - | false ⇒ match eq_b8 b 〈x0,x0〉 with -(* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *) - [ true ⇒ triple … x0 x0 false -(* 1) e' una divisione sensata che produrra' overflow/risultato *) -(* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *) -(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *) -(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *) -(* puo' essere sottratto al dividendo *) - | false ⇒ div_b8_ex_aux b (nat_it ? rol_b8 〈x0,e〉 nat3) x8 x0 nat3 ]]. - (* byte ricorsivi *) ninductive rec_byte8 : byte8 → Type ≝ b8_O : rec_byte8 〈x0,x0〉 diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma index 9400d9074..1951578a4 100755 --- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma @@ -1406,6 +1406,11 @@ ndefinition compl_ex ≝ | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5 | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ]. +(* operatore abs *) +ndefinition abs_ex ≝ +λe:exadecim.match getMSB_ex e with + [ true ⇒ compl_ex e | false ⇒ e ]. + (* operatore x in [inf,sup] o in sup],[inf *) ndefinition inrange_ex ≝ λx,inf,sup:exadecim. diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma index 80281eeea..f379eb1bf 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word16.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma @@ -141,6 +141,11 @@ ndefinition compl_w16 ≝ [ true ⇒ succ_w16 (not_w16 w) | false ⇒ not_w16 (pred_w16 w) ]. +(* operatore abs *) +ndefinition abs_w16 ≝ +λw:word16.match getMSB_w16 w with + [ true ⇒ compl_w16 w | false ⇒ w ]. + (* operatore x in [inf,sup] o in sup],[inf *) ndefinition inrange_w16 ≝ λx,inf,sup:word16. @@ -148,6 +153,54 @@ ndefinition inrange_w16 ≝ [ true ⇒ and_bool | false ⇒ or_bool ] (le_w16 inf x) (le_w16 x sup). +(* operatore moltiplicazione senza segno *) +(* 〈a1,a2〉 * 〈b1,b2〉 = (a1*b1) x0 x0 + x0 (a1*b2) x0 + x0 (a2*b1) x0 + x0 x0 (a2*b2) *) +ndefinition mulu_b8_aux ≝ +λw.nat_it ? rol_w16 w nat4. + +ndefinition mulu_b8 ≝ +λb1,b2:byte8. + plus_w16_d_d 〈(mulu_ex (cnH ? b1) (cnH ? b2)):〈x0,x0〉〉 + (plus_w16_d_d (mulu_b8_aux (extu_w16 (mulu_ex (cnH ? b1) (cnL ? b2)))) + (plus_w16_d_d (mulu_b8_aux (extu_w16 (mulu_ex (cnL ? b1) (cnH ? b2)))) + (extu_w16 (mulu_ex (cnL ? b1) (cnL ? b2))))). + +(* operatore moltiplicazione con segno *) +(* x * y = sgn(x) * sgn(y) * |x| * |y| *) +ndefinition muls_b8 ≝ +λb1,b2:byte8. +(* ++/-- → +, +-/-+ → - *) + match (getMSB_b8 b1) ⊙ (getMSB_b8 b2) with + (* +- -+ → - *) + [ true ⇒ compl_w16 + (* ++/-- → + *) + | false ⇒ λx.x ] (mulu_b8 (abs_b8 b1) (abs_b8 b2)). + +(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *) +nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (n:nat) on n ≝ + let w' ≝ plus_w16_d_d divd (compl_w16 divs) in + match n with + [ O ⇒ match le_w16 divs divd with + [ true ⇒ triple … (or_b8 molt q) (cnL ? w') (⊖ (eq_b8 (cnH ? w') 〈x0,x0〉)) + | false ⇒ triple … q (cnL ? divd) (⊖ (eq_b8 (cnH ? divd) 〈x0,x0〉)) ] + | S n' ⇒ match le_w16 divs divd with + [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) n' + | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q n' ]]. + +ndefinition div_b8 ≝ +λw:word16.λb:byte8.match eq_b8 b 〈x0,x0〉 with +(* la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato *) + [ true ⇒ triple … 〈xF,xF〉 (cnL ? w) true + | false ⇒ match eq_w16 w 〈〈x0,x0〉:〈x0,x0〉〉 with +(* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *) + [ true ⇒ triple … 〈x0,x0〉 〈x0,x0〉 false +(* 1) e' una divisione sensata che produrra' overflow/risultato *) +(* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *) +(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *) +(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *) +(* puo' essere sottratto al dividendo *) + | false ⇒ div_b8_aux w (nat_it ? rol_w16 (extu_w16 b) nat7) 〈x8,x0〉 〈x0,x0〉 nat7 ]]. + (* word16 ricorsive *) ninductive rec_word16 : word16 → Type ≝ w16_O : rec_word16 〈〈x0,x0〉:〈x0,x0〉〉 diff --git a/helm/software/matita/contribs/ng_assembly/num/word24.ma b/helm/software/matita/contribs/ng_assembly/num/word24.ma index c0e0d935c..4aabde771 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word24.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word24.ma @@ -192,6 +192,11 @@ ndefinition compl_w24 ≝ [ true ⇒ succ_w24 (not_w24 w) | false ⇒ not_w24 (pred_w24 w) ]. +(* operatore abs *) +ndefinition abs_w24 ≝ +λw:word24.match getMSB_w24 w with + [ true ⇒ compl_w24 w | false ⇒ w ]. + (* operatore x in [inf,sup] o in sup],[inf *) ndefinition inrange_w24 ≝ λx,inf,sup:word24. diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma index 09cd0ada2..e9b99efc3 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word32.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma @@ -144,9 +144,40 @@ ndefinition compl_w32 ≝ [ true ⇒ succ_w32 (not_w32 w) | false ⇒ not_w32 (pred_w32 w) ]. +(* operatore abs *) +ndefinition abs_w32 ≝ +λw:word32.match getMSB_w32 w with + [ true ⇒ compl_w32 w | false ⇒ w ]. + (* operatore x in [inf,sup] o in sup],[inf *) ndefinition inrange_w32 ≝ λx,inf,sup:word32. match le_w32 inf sup with [ true ⇒ and_bool | false ⇒ or_bool ] (le_w32 inf x) (le_w32 x sup). + +(* operatore moltiplicazione senza segno *) +(* 〈a1,a2〉 * 〈b1,b2〉 = (a1*b1) x0 x0 + x0 (a1*b2) x0 + x0 (a2*b1) x0 + x0 x0 (a2*b2) *) +ndefinition mulu_w16_aux ≝ +λw.nat_it ? rol_w32 w nat8. + +ndefinition mulu_w16 ≝ +λw1,w2:word16. + plus_w32_d_d 〈(mulu_b8 (cnH ? w1) (cnH ? w2)).〈〈x0,x0〉:〈x0,x0〉〉〉 + (plus_w32_d_d (mulu_w16_aux (extu_w32 (mulu_b8 (cnH ? w1) (cnL ? w2)))) + (plus_w32_d_d (mulu_w16_aux (extu_w32 (mulu_b8 (cnL ? w1) (cnH ? w2)))) + (extu_w32 (mulu_b8 (cnL ? w1) (cnL ? w2))))). + +(* operatore moltiplicazione con segno *) +(* x * y = sgn(x) * sgn(y) * |x| * |y| *) +ndefinition muls_w16 ≝ +λw1,w2:word16. +(* ++/-- → +, +-/-+ → - *) + match (getMSB_w16 w1) ⊙ (getMSB_w16 w2) with + (* +- -+ → - *) + [ true ⇒ compl_w32 + (* ++/-- → + *) + | false ⇒ λx.x ] (mulu_w16 (abs_w16 w1) (abs_w16 w2)). + +nlemma pippo : ∃b.b=(muls_w16 〈〈xC,x3〉:〈x0,x4〉〉 〈〈x7,xE〉:〈xF,x9〉〉). nnormalize; + -- 2.39.2