From b082cb1e1fc9dbd471d16d2eb231e883e96e588f Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Fri, 29 Jan 2010 07:48:08 +0000 Subject: [PATCH] freescale porting --- .../matita/contribs/ng_assembly/depends | 6 +- .../ng_assembly/emulator/model/HC05_model.ma | 12 +- .../ng_assembly/emulator/model/HC08_model.ma | 12 +- .../ng_assembly/emulator/model/HCS08_model.ma | 12 +- .../emulator/model/IP2022_model.ma | 16 +- .../ng_assembly/emulator/model/RS08_model.ma | 12 +- .../emulator/read_write/IP2022_read_write.ma | 280 ++++++++++++++++++ .../emulator/read_write/RS08_read_write.ma | 149 ++++++++++ .../emulator/read_write/read_write.ma | 89 ++++++ .../emulator/read_write/read_write_base.ma | 32 ++ .../emulator/status/IP2022_status.ma | 43 ++- .../emulator/status/RS08_status.ma | 4 - .../emulator/status/status_setter.ma | 19 +- .../contribs/ng_assembly/num/exadecim.ma | 12 + .../matita/contribs/ng_assembly/num/oct.ma | 93 +++++- 15 files changed, 724 insertions(+), 67 deletions(-) create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/read_write/RS08_read_write.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write_base.ma diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index 32007179e..96a1dd500 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -15,7 +15,7 @@ num/quatern.ma num/bool.ma num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma emulator/status/IP2022_status_lemmas.ma emulator/memory/memory_struct_lemmas.ma emulator/status/IP2022_status.ma num/oct_lemmas.ma num/word16_lemmas.ma num/word24_lemmas.ma num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma -emulator/status/status_lemmas.ma emulator/status/HC05_status_lemmas.ma emulator/status/HC08_status_lemmas.ma emulator/status/IP2022_status_lemmas.ma emulator/status/RS08_status_lemmas.ma +emulator/status/status_lemmas.ma common/option_lemmas.ma common/prod_lemmas.ma emulator/opcodes/opcode_lemmas.ma emulator/status/HC05_status_lemmas.ma emulator/status/HC08_status_lemmas.ma emulator/status/IP2022_status_lemmas.ma emulator/status/RS08_status_lemmas.ma emulator/status/status.ma emulator/status/status.ma emulator/memory/memory_abs.ma emulator/opcodes/opcode.ma emulator/status/HC05_status.ma emulator/status/HC08_status.ma emulator/status/IP2022_status.ma emulator/status/RS08_status.ma 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 @@ -34,12 +34,14 @@ emulator/opcodes/RS08_table_tests.ma emulator/opcodes/RS08_table.ma emulator/opc test_errori.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 emulator/translation/translation_base.ma common/option.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/opcode.ma emulator/opcodes/IP2022_table.ma common/list.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_opcode.ma emulator/opcodes/byte_or_word.ma emulator/status/HC05_status.ma num/word16.ma emulator/memory/memory_bits.ma emulator/memory/memory_trees.ma common/theory.ma common/string.ma common/ascii.ma common/list_utility.ma +emulator/read_write/RS08_read_write.ma emulator/status/status_setter.ma emulator/opcodes/byte_or_word.ma num/word16.ma compiler/ast_type.ma common/list_utility.ma num/word16.ma num/byte8.ma @@ -74,9 +76,11 @@ emulator/opcodes/HC05_instr_mode.ma num/word16.ma emulator/opcodes/IP2022_table_tests.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/opcode.ma emulator/status/IP2022_status.ma emulator/memory/memory_struct.ma num/word16.ma num/word24.ma num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma +emulator/read_write/read_write.ma emulator/read_write/IP2022_read_write.ma emulator/read_write/RS08_read_write.ma emulator/memory/memory_func.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma emulator/opcodes/RS08_instr_mode.ma num/word16.ma num/comp_num_lemmas.ma num/bool_lemmas.ma num/comp_num.ma +emulator/read_write/read_write_base.ma common/theory.ma emulator/status/RS08_status.ma num/word16.ma emulator/opcodes/HC05_opcode_lemmas.ma emulator/opcodes/HC05_opcode.ma num/bool_lemmas.ma emulator/opcodes/HC08_instr_mode.ma num/word16.ma diff --git a/helm/software/matita/contribs/ng_assembly/emulator/model/HC05_model.ma b/helm/software/matita/contribs/ng_assembly/emulator/model/HC05_model.ma index 8fbd3da12..33a24f46b 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/model/HC05_model.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/model/HC05_model.ma @@ -43,12 +43,10 @@ ndefinition memory_type_of_FamilyHC05 ≝ (* etc.. *) ]. -(* - parametrizzati i non deterministici rispetto a tutti i valori casuali +(* parametrizzati i non deterministici rispetto a tutti i valori casuali che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5). l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione - (reset V-low), la memoria ed il check possono essere passati -*) + (reset V-low), la memoria ed il check possono essere passati *) ndefinition start_of_model_HC05 ≝ λmcu:HC05_model.λt:memory_impl. λmem:aux_mem_type t.λchk:aux_chk_type t. @@ -78,11 +76,9 @@ ndefinition start_of_model_HC05 ≝ (*..*) ]. -(* - cio' che non viene resettato mantiene il valore precedente: nella documentazione +(* cio' che non viene resettato mantiene il valore precedente: nella documentazione viene riportato come "unaffected"/"indeterminate"/"unpredictable" - il soft RESET e' diverso da un calo di tensione e la ram non variera' -*) + il soft RESET e' diverso da un calo di tensione e la ram non variera' *) ndefinition reset_of_model_HC05 ≝ λt:memory_impl.λs:any_status HC05 t. (mk_any_status HC05 t diff --git a/helm/software/matita/contribs/ng_assembly/emulator/model/HC08_model.ma b/helm/software/matita/contribs/ng_assembly/emulator/model/HC08_model.ma index 0400439ae..066dcb74a 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/model/HC08_model.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/model/HC08_model.ma @@ -48,12 +48,10 @@ ndefinition memory_type_of_FamilyHC08 ≝ (* etc... *) ]. -(* - parametrizzati i non deterministici rispetto a tutti i valori casuali +(* parametrizzati i non deterministici rispetto a tutti i valori casuali che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5). l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione - (reset V-low), la memoria ed il check possono essere passati -*) + (reset V-low), la memoria ed il check possono essere passati *) ndefinition start_of_model_HC08 ≝ λmcu:HC08_model.λt:memory_impl. λmem:aux_mem_type t.λchk:aux_chk_type t. @@ -77,11 +75,9 @@ ndefinition start_of_model_HC08 ≝ (* chk *) chk (* clk: reset *) (None ?). -(* - cio' che non viene resettato mantiene il valore precedente: nella documentazione +(* cio' che non viene resettato mantiene il valore precedente: nella documentazione viene riportato come "unaffected"/"indeterminate"/"unpredictable" - il soft RESET e' diverso da un calo di tensione e la ram non variera' -*) + il soft RESET e' diverso da un calo di tensione e la ram non variera' *) ndefinition reset_of_model_HC08 ≝ λt:memory_impl.λs:any_status HC08 t. (mk_any_status HC08 t diff --git a/helm/software/matita/contribs/ng_assembly/emulator/model/HCS08_model.ma b/helm/software/matita/contribs/ng_assembly/emulator/model/HCS08_model.ma index 71acc536a..40f928dd4 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/model/HCS08_model.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/model/HCS08_model.ma @@ -50,12 +50,10 @@ ndefinition memory_type_of_FamilyHCS08 ≝ (* etc... *) ]. -(* - parametrizzati i non deterministici rispetto a tutti i valori casuali +(* parametrizzati i non deterministici rispetto a tutti i valori casuali che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5). l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione - (reset V-low), la memoria ed il check possono essere passati -*) + (reset V-low), la memoria ed il check possono essere passati *) ndefinition start_of_model_HCS08 ≝ λmcu:HCS08_model.λt:memory_impl. λmem:aux_mem_type t.λchk:aux_chk_type t. @@ -79,11 +77,9 @@ ndefinition start_of_model_HCS08 ≝ (* chk *) chk (* clk: reset *) (None ?). -(* - cio' che non viene resettato mantiene il valore precedente: nella documentazione +(* cio' che non viene resettato mantiene il valore precedente: nella documentazione viene riportato come "unaffected"/"indeterminate"/"unpredictable" - il soft RESET e' diverso da un calo di tensione e la ram non variera' -*) + il soft RESET e' diverso da un calo di tensione e la ram non variera' *) ndefinition reset_of_model_HCS08 ≝ λt:memory_impl.λs:any_status HCS08 t. (mk_any_status HCS08 t diff --git a/helm/software/matita/contribs/ng_assembly/emulator/model/IP2022_model.ma b/helm/software/matita/contribs/ng_assembly/emulator/model/IP2022_model.ma index 30e8f1f03..03b3745b9 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/model/IP2022_model.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/model/IP2022_model.ma @@ -35,7 +35,9 @@ ndefinition memory_type_of_FamilyIP2022 ≝ λm:IP2022_model.match m with [ IP2K ⇒ [ -(* 0x00000080-0x00000FFF *) triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x8,x0〉〉〉 〈〈x0,xF〉:〈x8,x0〉〉 MEM_READ_WRITE (* 3968 GPR+RAM+STACK *) +(* 0x00000008-0x00000008 *) triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x8〉〉〉 〈〈x0,x0〉:〈x0,x1〉〉 MEM_READ_ONLY (* PCH read only memory reg *) +(* 0x0000000E-0x0000000E *) ; triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xE〉〉〉 〈〈x0,x0〉:〈x0,x1〉〉 MEM_READ_ONLY (* PCH read only memory reg *) +(* 0x00000080-0x00000FFF *) ; triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x8,x0〉〉〉 〈〈x0,xF〉:〈x8,x0〉〉 MEM_READ_WRITE (* 3968 GPR+RAM+STACK *) (* 0x02000000-0x02003FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_WRITE (* 16384B PROGRAM RAM *) (* 0x02010000-0x02013FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x1〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *) (* 0x02014000-0x02017FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x1〉〉.〈〈x4,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *) @@ -49,12 +51,10 @@ ndefinition IP2022_gpr_base ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉: (* punto di riferimento per accessi ($PC) ($ADDR) *) ndefinition IP2022_ram_base ≝ 〈〈〈x0,x2〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉. -(* - parametrizzati i non deterministici rispetto a tutti i valori casuali +(* parametrizzati i non deterministici rispetto a tutti i valori casuali che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5). l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione - (reset V-low), la memoria ed il check possono essere passati -*) + (reset V-low), la memoria ed il check possono essere passati *) ndefinition start_of_model_IP2022 ≝ λmcu:IP2022_model.λt:memory_impl. λmem:aux_mem_type t.λchk:aux_chk_type t. @@ -81,11 +81,9 @@ ndefinition start_of_model_IP2022 ≝ (* chk *) chk (* clk: reset *) (None ?)). -(* - cio' che non viene resettato mantiene il valore precedente: nella documentazione +(* cio' che non viene resettato mantiene il valore precedente: nella documentazione viene riportato come "unaffected"/"indeterminate"/"unpredictable" - il soft RESET e' diverso da un calo di tensione e la ram non variera' -*) + il soft RESET e' diverso da un calo di tensione e la ram non variera' *) ndefinition reset_of_model_IP2022 ≝ λt:memory_impl.λs:any_status IP2022 t. (mk_any_status IP2022 t diff --git a/helm/software/matita/contribs/ng_assembly/emulator/model/RS08_model.ma b/helm/software/matita/contribs/ng_assembly/emulator/model/RS08_model.ma index da72476ef..618b2ace0 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/model/RS08_model.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/model/RS08_model.ma @@ -52,12 +52,10 @@ ndefinition memory_type_of_FamilyRS08 ≝ (* 0x3800-0x3FFF *) ; triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x3,x8〉:〈x0,x0〉〉〉 〈〈x0,x8〉:〈x0,x0〉〉 MEM_READ_ONLY (* 2048B FLASH *) ] ]. -(* - parametrizzati i non deterministici rispetto a tutti i valori casuali +(* parametrizzati i non deterministici rispetto a tutti i valori casuali che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5). l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione - (reset V-low), la memoria ed il check possono essere passati -*) + (reset V-low), la memoria ed il check possono essere passati *) ndefinition start_of_model_RS08 ≝ λmcu:RS08_model.λt:memory_impl. λmem:aux_mem_type t.λchk:aux_chk_type t. @@ -76,11 +74,9 @@ ndefinition start_of_model_RS08 ≝ (* chk *) chk (* clk: reset *) (None ?)). -(* - cio' che non viene resettato mantiene il valore precedente: nella documentazione +(* cio' che non viene resettato mantiene il valore precedente: nella documentazione viene riportato come "unaffected"/"indeterminate"/"unpredictable" - il soft RESET e' diverso da un calo di tensione e la ram non variera' -*) + il soft RESET e' diverso da un calo di tensione e la ram non variera' *) ndefinition reset_of_model_RS08 ≝ λt:memory_impl.λs:any_status RS08 t. (mk_any_status RS08 t diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma new file mode 100755 index 000000000..3cb7b1f51 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma @@ -0,0 +1,280 @@ +(**************************************************************************) +(* ___ *) +(* ||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/status/status_setter.ma". +include "emulator/read_write/read_write_base.ma". + +ndefinition IP2022_ADDRSEL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x2〉〉〉. +ndefinition IP2022_ADDRX_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x3〉〉〉. +ndefinition IP2022_IPH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x4〉〉〉. +ndefinition IP2022_IPL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x5〉〉〉. +ndefinition IP2022_SPH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x6〉〉〉. +ndefinition IP2022_SPL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x7〉〉〉. +ndefinition IP2022_PCH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x8〉〉〉. +ndefinition IP2022_PCL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x9〉〉〉. +ndefinition IP2022_W_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xA〉〉〉. +ndefinition IP2022_STATUS_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xB〉〉〉. +ndefinition IP2022_DPH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xC〉〉〉. +ndefinition IP2022_DPL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xD〉〉〉. +ndefinition IP2022_SPEED_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xE〉〉〉. +ndefinition IP2022_MULH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xF〉〉〉. +ndefinition IP2022_ADDRH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x0〉〉〉. +ndefinition IP2022_ADDRL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x1〉〉〉. +ndefinition IP2022_DATAH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x2〉〉〉. +ndefinition IP2022_DATAL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x3〉〉〉. +ndefinition IP2022_CALLH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x4〉〉〉. +ndefinition IP2022_CALLL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x5〉〉〉. + +(* **** *) +(* READ *) +(* **** *) + +(* NB: non ci sono strane indirezioni, + solo registri memory mapped da intercettare *) +ndefinition IP2022_memory_filter_read_aux ≝ +λt:memory_impl.λs:any_status IP2022 t.λaddr:word32. +λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option T. +(* intercettare le locazioni memory mapped *) + match eq_w32 addr IP2022_ADDRSEL_loc with + [ true ⇒ fREG (addrsel_reg_IP2022 (alu … s)) + | false ⇒ + match eq_w32 addr IP2022_ADDRX_loc with + [ true ⇒ fREG (w24x (get_addrarray (addrsel_reg_IP2022 (alu … s)) + (addr_array_IP2022 (alu … s)))) + | false ⇒ + match eq_w32 addr IP2022_IPH_loc with + [ true ⇒ fREG (cnH ? (ip_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_IPL_loc with + [ true ⇒ fREG (cnL ? (ip_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_SPH_loc with + [ true ⇒ fREG (cnH ? (sp_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_SPL_loc with + [ true ⇒ fREG (cnL ? (sp_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_PCH_loc with + [ true ⇒ fREG (cnH ? (pc_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_PCL_loc with + [ true ⇒ fREG (cnL ? (pc_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_W_loc with + [ true ⇒ fREG (acc_low_reg_IP2022 (alu … s)) + | false ⇒ + (* PAGE[7:5] Z[2] H[1] C [0] *) + match eq_w32 addr IP2022_STATUS_loc with + [ true ⇒ fREG 〈(rol_ex (ex_of_oct (page_reg_IP2022 (alu … s)))), + (or_ex (or_ex (match z_flag_IP2022 (alu … s) with + [ true ⇒ x4 | false ⇒ x0 ]) + (match h_flag_IP2022 (alu … s) with + [ true ⇒ x2 | false ⇒ x0 ])) + (match c_flag_IP2022 (alu … s) with + [ true ⇒ x1 | false ⇒ x0 ]))〉 + | false ⇒ + match eq_w32 addr IP2022_DPH_loc with + [ true ⇒ fREG (cnH ? (dp_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_DPL_loc with + [ true ⇒ fREG (cnL ? (dp_reg_IP2022 (alu … s))) + | false ⇒ + (* SPEED[3:0] *) + match eq_w32 addr IP2022_SPEED_loc with + [ true ⇒ fREG 〈x0,(speed_reg_IP2022 (alu … s))〉 + | false ⇒ + match eq_w32 addr IP2022_MULH_loc with + [ true ⇒ fREG (mulh_reg_IP2022 (alu … s)) + | false ⇒ + match eq_w32 addr IP2022_ADDRH_loc with + [ true ⇒ fREG (w24h (get_addrarray (addrsel_reg_IP2022 (alu … s)) + (addr_array_IP2022 (alu … s)))) + | false ⇒ + match eq_w32 addr IP2022_ADDRL_loc with + [ true ⇒ fREG (w24l (get_addrarray (addrsel_reg_IP2022 (alu … s)) + (addr_array_IP2022 (alu … s)))) + | false ⇒ + match eq_w32 addr IP2022_DATAH_loc with + [ true ⇒ fREG (cnH ? (data_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_DATAL_loc with + [ true ⇒ fREG (cnL ? (data_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_CALLH_loc with + [ true ⇒ fREG (cnH ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s)))) + | false ⇒ + match eq_w32 addr IP2022_CALLL_loc with + [ true ⇒ fREG (cnL ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s)))) +(* accesso normale *) + | false ⇒ fMEM (mem_desc … s) (chk_desc … s) addr + ]]]]]]]]]]]]]]]]]]]]. + +(* lettura IP2022 di un byte *) +ndefinition IP2022_memory_filter_read ≝ +λt:memory_impl.λs:any_status IP2022 t.λaddr:word32. + IP2022_memory_filter_read_aux t s addr byte8 + (λb.Some byte8 b) + (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read t m c a). + +(* lettura IP2022 di un bit *) +ndefinition IP2022_memory_filter_read_bit ≝ +λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.λsub:oct. + IP2022_memory_filter_read_aux t s addr bool + (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b))) + (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read_bit t m c a sub). + +(* ***** *) +(* WRITE *) +(* ***** *) + +ndefinition high_write_aux_w16 ≝ +λf:byte8 → byte8.λw:word16.〈(f (cnH ? w)):(cnL ? w)〉. + +ndefinition low_write_aux_w16 ≝ +λf:byte8 → byte8.λw:word16.λflag:aux_mod_type. + 〈((match flag with + [ auxMode_ok ⇒ λx.x + | auxMode_inc ⇒ succ_b8 + | auxMode_dec ⇒ pred_b8 ]) (cnH ? w)): + (f (cnL ? w))〉. + +ndefinition ext_write_aux_w24 ≝ +λf:byte8 → byte8.λw:word24.〈(f (w24x w));(w24h w);(w24l w)〉. + +ndefinition high_write_aux_w24 ≝ +λf:byte8 → byte8.λw:word24.〈(w24x w);(f (w24h w));(w24l w)〉. + +ndefinition low_write_aux_w24 ≝ +λf:byte8 → byte8.λw:word24.λflag:aux_mod_type. + match (match flag with + [ auxMode_ok ⇒ λx.x + | auxMode_inc ⇒ succ_w16 + | auxMode_dec ⇒ pred_w16 ]) 〈(w24x w):(w24h w)〉 with + [ mk_comp_num wx' wh' ⇒ 〈wx';wh';(w24l w)〉 ]. + +(* flag di carry: riportare il carry al byte logicamente superiore *) +ndefinition IP2022_memory_filter_write_aux ≝ +λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type. +λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option (aux_mem_type t). +(* intercettare le locazioni memory mapped *) + match eq_w32 addr IP2022_ADDRSEL_loc with + [ true ⇒ set_addrsel_reg … s (fREG (addrsel_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_ADDRX_loc with + [ true ⇒ set_addr_reg … s (ext_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s)) + (addr_array_IP2022 (alu … s)))) + | false ⇒ + match eq_w32 addr IP2022_IPH_loc with + [ true ⇒ set_ip_reg … s (high_write_aux_w16 fREG (ip_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_IPL_loc with + [ true ⇒ set_ip_reg … s (low_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)) flag) + | false ⇒ + match eq_w32 addr IP2022_SPH_loc with + [ true ⇒ set_sp_reg … s (high_write_aux_w16 fREG (sp_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_SPL_loc with + [ true ⇒ set_sp_reg … s (low_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)) flag) + | false ⇒ + match eq_w32 addr IP2022_PCL_loc with + [ true ⇒ Some ? (set_pc_reg … s (low_write_aux_w16 fREG (pc_reg_IP2022 (alu … s)) flag)) + | false ⇒ + match eq_w32 addr IP2022_W_loc with + [ true ⇒ Some ? (set_acc_8_low_reg … s (fREG (acc_low_reg_IP2022 (alu … s)))) + | false ⇒ + match eq_w32 addr IP2022_DPH_loc with + [ true ⇒ set_dp_reg … s (high_write_aux_w16 fREG (dp_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_DPL_loc with + [ true ⇒ set_dp_reg … s (low_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)) flag) + | false ⇒ + match eq_w32 addr IP2022_MULH_loc with + [ true ⇒ set_mulh_reg … s (fREG (mulh_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_ADDRH_loc with + [ true ⇒ set_addr_reg … s (high_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s)) + (addr_array_IP2022 (alu … s)))) + | false ⇒ + match eq_w32 addr IP2022_ADDRL_loc with + [ true ⇒ set_addr_reg … s (low_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s)) + (addr_array_IP2022 (alu … s))) flag) + | false ⇒ + match eq_w32 addr IP2022_DATAH_loc with + [ true ⇒ set_data_reg … s (high_write_aux_w16 fREG (data_reg_IP2022 (alu … s))) + | false ⇒ + match eq_w32 addr IP2022_DATAL_loc with + [ true ⇒ set_data_reg … s (low_write_aux_w16 fREG (data_reg_IP2022 (alu … s)) flag) + | false ⇒ + match eq_w32 addr IP2022_CALLH_loc with + [ true ⇒ set_call_reg … s (high_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s)))) + | false ⇒ + match eq_w32 addr IP2022_CALLL_loc with + [ true ⇒ set_call_reg … s (low_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))) flag) +(* accesso normale *) + | false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr) + (λmem'.Some ? (set_mem_desc … s mem')) ]]]]]]]]]]]]]]]]]. + +(* scrittura IP2022 di un byte *) +ndefinition IP2022_memory_filter_write ≝ +λt:memory_impl.λs:any_status IP2022 t. +λaddr:word32.λflag:aux_mod_type.λval:byte8. + (* PAGE[7:5] Z[2] H[1] C [0] *) + match eq_w32 addr IP2022_STATUS_loc with + [ true ⇒ Some ? (set_alu … s + (set_page_reg_IP2022 + (set_z_flag_IP2022 + (set_h_flag_IP2022 + (set_c_flag_IP2022 (alu … s) + (getn_array8T o7 ? (bits_of_byte8 val))) + (getn_array8T o6 ? (bits_of_byte8 val))) + (getn_array8T o5 ? (bits_of_byte8 val))) + (oct_of_exH (cnH ? val)))) + (* accesso a registro_non_spezzato/normale *) + | false ⇒ IP2022_memory_filter_write_aux t s addr flag + (λb.val) + (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update t m c a val) ]. + +(* scrittura IP2022 di un bit *) +ndefinition IP2022_memory_filter_write_bit ≝ +λt:memory_impl.λs:any_status IP2022 t. +λaddr:word32.λsub:oct.λval:bool. + (* PAGE[7:5] Z[2] H[1] C [0] *) + match eq_w32 addr IP2022_STATUS_loc with + [ true ⇒ Some ? (set_alu … s + (match sub with + [ o0 ⇒ set_page_reg_IP2022 (alu … s) + ((match val with [ true ⇒ or_oct o4 | false ⇒ and_oct o3 ]) + (page_reg_IP2022 (alu … s))) + | o1 ⇒ set_page_reg_IP2022 (alu … s) + ((match val with [ true ⇒ or_oct o2 | false ⇒ and_oct o5 ]) + (page_reg_IP2022 (alu … s))) + | o2 ⇒ set_page_reg_IP2022 (alu … s) + ((match val with [ true ⇒ or_oct o1 | false ⇒ and_oct o6 ]) + (page_reg_IP2022 (alu … s))) + | o5 ⇒ set_z_flag_IP2022 (alu … s) val + | o6 ⇒ set_h_flag_IP2022 (alu … s) val + | o7 ⇒ set_c_flag_IP2022 (alu … s) val + | _ ⇒ alu … s ])) + (* accesso a registro_non_spezzato/normale *) + | false ⇒ IP2022_memory_filter_write_aux t s addr auxMode_ok + (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val)) + (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update_bit t m c a sub val) ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/RS08_read_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/RS08_read_write.ma new file mode 100755 index 000000000..bec7454a4 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/RS08_read_write.ma @@ -0,0 +1,149 @@ +(**************************************************************************) +(* ___ *) +(* ||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/status/status_setter.ma". + +(* **** *) +(* READ *) +(* **** *) + +(* NB: fare molta attenzione alle note sulle combinazioni possibili perche' + il comportamento della memoria nell'RS08 e' strano e ci sono + precise condizioni che impediscono una semantica circolare dell'accesso + (divergenza=assenza di definizione) *) +ndefinition RS08_memory_filter_read_aux ≝ +λt:memory_impl.λs:any_status RS08 t.λaddr:word32. +λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option T. +(* solo indirizzi nei 64Kb *) + match gt_w16 (cnH ? addr) 〈〈x0,x0〉:〈x0,x0〉〉 with + [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) addr + | false ⇒ +(* possibili accessi al registro X + 1) addr=000F: diretto + 2) addr=000E (X =0F): indiretto + 3) addr=00CF (PS=00): paging + [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo: + non si possono combinare due effetti contemporaneamente! + per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni *) + match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xF〉〉 ⊕ + (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x0,xF〉) ⊕ + (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with + [ true ⇒ fREG (x_map_RS08 (alu … s)) + | false ⇒ +(* possibili accessi al registro PS + 1) addr=001F: diretto + 2) addr=000E (X =1F): indiretto + 3) addr=00DF (PS=00): paging *) + match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x1,xF〉〉 ⊕ + (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x1,xF〉) ⊕ + (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with + [ true ⇒ fREG (ps_map_RS08 (alu … s)) + | false ⇒ +(* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging + altrimenti sarebbero 2 indirezioni *) + match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 with + [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:(x_map_RS08 (alu … s))〉〉 + | false ⇒ +(* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *) + match inrange_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with + [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) + (〈〈〈x0,x0〉:〈x0,x0〉〉.(or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉)) + (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉))〉) +(* accesso normale *) + | false ⇒ fMEM (mem_desc … s) (chk_desc … s) addr ]]]]]. + +(* lettura RS08 di un byte *) +ndefinition RS08_memory_filter_read ≝ +λt:memory_impl.λs:any_status RS08 t.λaddr:word32. + RS08_memory_filter_read_aux t s addr byte8 + (λb.Some byte8 b) + (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read t m c a). + +(* lettura RS08 di un bit *) +ndefinition RS08_memory_filter_read_bit ≝ +λt:memory_impl.λs:any_status RS08 t.λaddr:word32.λsub:oct. + RS08_memory_filter_read_aux t s addr bool + (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b))) + (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read_bit t m c a sub). + +(* ***** *) +(* WRITE *) +(* ***** *) + +ndefinition RS08_memory_filter_write_aux ≝ +λt:memory_impl.λs:any_status RS08 t.λaddr:word32. +λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option (aux_mem_type t). +(* solo indirizzi nei 64Kb *) + match gt_w16 (cnH ? addr) 〈〈x0,x0〉:〈x0,x0〉〉 with + [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr) + (λmem'.Some ? (set_mem_desc … s mem')) + | false ⇒ +(* possibili accessi al registro X + 1) addr=000F: diretto + 2) addr=000E (X =0F): indiretto + 3) addr=00CF (PS=00): paging + [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo: + non si possono combinare due effetti contemporaneamente! + per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni *) + match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xF〉〉 ⊕ + (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x0,xF〉) ⊕ + (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with + [ true ⇒ set_x_map … s (fREG (x_map_RS08 (alu … s))) + | false ⇒ +(* possibili accessi al registro PS + 1) addr=001F: diretto + 2) addr=000E (X =1F): indiretto + 3) addr=00DF (PS=00): paging *) + match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x1,xF〉〉 ⊕ + (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x1,xF〉) ⊕ + (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with + [ true ⇒ set_ps_map … s (fREG (x_map_RS08 (alu … s))) + | false ⇒ +(* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging + altrimenti sarebbero 2 indirezioni *) + match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 with + [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:(x_map_RS08 (alu … s))〉〉) + (λmem'.Some ? (set_mem_desc … s mem')) + | false ⇒ +(* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *) + match inrange_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with + [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) + (〈〈〈x0,x0〉:〈x0,x0〉〉.(or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉)) + (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉))〉)) + (λmem'.Some ? (set_mem_desc … s mem')) +(* accesso normale *) + | false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr) + (λmem'.Some ? (set_mem_desc … s mem')) ]]]]]. + +(* scrittura RS08 di un byte *) +ndefinition RS08_memory_filter_write ≝ +λt:memory_impl.λs:any_status RS08 t.λaddr:word32.λval:byte8. + RS08_memory_filter_write_aux t s addr + (λb.val) + (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update t m c a val). + +(* scrittura RS08 di un bit *) +ndefinition RS08_memory_filter_write_bit ≝ +λt:memory_impl.λs:any_status RS08 t.λaddr:word32.λsub:oct.λval:bool. + RS08_memory_filter_write_aux t s addr + (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val)) + (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update_bit t m c a sub val). diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma new file mode 100755 index 000000000..56c26a943 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma @@ -0,0 +1,89 @@ +(**************************************************************************) +(* ___ *) +(* ||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/read_write/RS08_read_write.ma". +include "emulator/read_write/IP2022_read_write.ma". + +(* in caso di RS08/IP2022 si dirotta sul filtro, altrimenti si legge direttamente *) +ndefinition memory_filter_read ≝ +λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word32 → option byte8 with + [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32. + mem_read t (mem_desc ? t s) (chk_desc ? t s) addr + | HC08 ⇒ λs:any_status HC08 t.λaddr:word32. + mem_read t (mem_desc ? t s) (chk_desc ? t s) addr + | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32. + mem_read t (mem_desc ? t s) (chk_desc ? t s) addr + | RS08 ⇒ λs:any_status RS08 t.λaddr:word32. + RS08_memory_filter_read t s addr + | IP2022 ⇒ λs:any_status IP2022 t.λaddr:word32. + IP2022_memory_filter_read t s addr + ]. + +ndefinition memory_filter_read_bit ≝ +λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word32 → oct → option bool with + [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λsub:oct. + mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub + | HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λsub:oct. + mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub + | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λsub:oct. + mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub + | RS08 ⇒ λs:any_status RS08 t.λaddr:word32.λsub:oct. + RS08_memory_filter_read_bit t s addr sub + | IP2022 ⇒ λs:any_status IP2022 t.λaddr:word32.λsub:oct. + IP2022_memory_filter_read_bit t s addr sub + ]. + +ndefinition memory_filter_write ≝ +λm:mcu_type.λt:memory_impl.match m + return λm:mcu_type.any_status m t → word32 → aux_mod_type → byte8 → option (any_status m t) with + [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λflag:aux_mod_type.λval:byte8. + opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val) + (λmem.Some ? (set_mem_desc ? t s mem)) + | HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8. + opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val) + (λmem.Some ? (set_mem_desc ? t s mem)) + | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8. + opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val) + (λmem.Some ? (set_mem_desc ? t s mem)) + | RS08 ⇒ λs:any_status RS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8. + RS08_memory_filter_write t s addr val + | IP2022 ⇒ λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type.λval:byte8. + IP2022_memory_filter_write t s addr flag val + ]. + +ndefinition memory_filter_write_bit ≝ +λm:mcu_type.λt:memory_impl.match m + return λm:mcu_type.any_status m t → word32 → oct → bool → option (any_status m t) with + [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λsub:oct.λval:bool. + opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val) + (λmem.Some ? (set_mem_desc ? t s mem)) + | HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λsub:oct.λval:bool. + opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val) + (λmem.Some ? (set_mem_desc ? t s mem)) + | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λsub:oct.λval:bool. + opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val) + (λmem.Some ? (set_mem_desc ? t s mem)) + | RS08 ⇒ λs:any_status RS08 t.λaddr:word32.λsub:oct.λval:bool. + RS08_memory_filter_write_bit t s addr sub val + | IP2022 ⇒ λs:any_status IP2022 t.λaddr:word32.λsub:oct.λval:bool. + IP2022_memory_filter_write_bit t s addr sub val + ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write_base.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write_base.ma new file mode 100755 index 000000000..a6a55a996 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write_base.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +(* flag ausiliario per la scrittura + normale / con riporto(+) / con riporto(-) *) +ninductive aux_mod_type : Type ≝ + auxMode_ok : aux_mod_type +| auxMode_inc : aux_mod_type +| auxMode_dec : aux_mod_type +. + diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma index ad920e71f..875ee2477 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma @@ -42,11 +42,11 @@ ndefinition new_callstack ≝ ndefinition pop_callstack ≝ λcs:aux_callstack_type. - pair ?? (a16_1 ? cs) - (mk_Array16T ? (a16_2 ? cs) (a16_3 ? cs) (a16_4 ? cs) (a16_5 ? cs) - (a16_6 ? cs) (a16_7 ? cs) (a16_8 ? cs) (a16_9 ? cs) - (a16_10 ? cs) (a16_11 ? cs) (a16_12 ? cs) (a16_13 ? cs) - (a16_14 ? cs) (a16_15 ? cs) (a16_16 ? cs) 〈〈xF,xF〉:〈xF,xF〉〉). + pair … (a16_1 ? cs) + (mk_Array16T ? (a16_2 ? cs) (a16_3 ? cs) (a16_4 ? cs) (a16_5 ? cs) + (a16_6 ? cs) (a16_7 ? cs) (a16_8 ? cs) (a16_9 ? cs) + (a16_10 ? cs) (a16_11 ? cs) (a16_12 ? cs) (a16_13 ? cs) + (a16_14 ? cs) (a16_15 ? cs) (a16_16 ? cs) 〈〈xF,xF〉:〈xF,xF〉〉). ndefinition push_callstack ≝ λcs:aux_callstack_type.λtop. @@ -66,19 +66,13 @@ ndefinition new_addrarray ≝ (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉). -ndefinition get_low3bits ≝ -λaddrsel:byte8. - match cnL ? addrsel with - [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7 - | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ]. - ndefinition get_addrarray ≝ λaddrsel:byte8.λaa:aux_addrarray_type. - getn_array8T (get_low3bits addrsel) ? aa. + getn_array8T (oct_of_exL (cnL ? addrsel)) ? aa. ndefinition set_addrarray ≝ λaddrsel:byte8.λaa:aux_addrarray_type.λv. - setn_array8T (get_low3bits addrsel) ? aa v. + setn_array8T (oct_of_exL (cnL ? addrsel)) ? aa v. (* *********************************** *) (* STATUS INTERNO DEL PROCESSORE (ALU) *) @@ -262,6 +256,29 @@ ndefinition push_call_reg_IP2022 ≝ (c_flag_IP2022 alu) (skip_mode_IP2022 alu). +ndefinition pop_call_reg_IP2022 ≝ +λalu. + match pop_callstack (call_stack_IP2022 alu) with + [ pair val call' ⇒ + pair … val + (mk_alu_IP2022 + (acc_low_reg_IP2022 alu) + (mulh_reg_IP2022 alu) + (addrsel_reg_IP2022 alu) + (addr_array_IP2022 alu) + call' + (ip_reg_IP2022 alu) + (dp_reg_IP2022 alu) + (data_reg_IP2022 alu) + (sp_reg_IP2022 alu) + (pc_reg_IP2022 alu) + (speed_reg_IP2022 alu) + (page_reg_IP2022 alu) + (h_flag_IP2022 alu) + (z_flag_IP2022 alu) + (c_flag_IP2022 alu) + (skip_mode_IP2022 alu)) ]. + (* setter specifico IP2022 di IP *) ndefinition set_ip_reg_IP2022 ≝ λalu.λip':word16. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma index 2b84717f8..e446b292f 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma @@ -44,16 +44,12 @@ nrecord alu_RS08: Type ≝ (* X: registro indice parte bassa *) (* NB: in realta' e' mappato in memoria e non risiede nella ALU *) (* la lettura/scrittura avviene tramite la locazione [0x000F] *) - (* la funzione memory_filter_read/write si occupera' di intercettare *) - (* e deviare sul registro le letture/scritture (modulo load_write) *) x_map_RS08 : byte8; (* PS: registro selezione di pagina *) (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *) (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *) (* NB: in realta' e' mappato in memoria e non risiede nella ALU *) (* la lettura/scrittura avviene tramite la locazione [0x001F] *) - (* la funzione memory_filter_read/write si occupera' di intercettare *) - (* e deviare sul registro le letture/scritture (modulo load_write) *) ps_map_RS08 : byte8; (* Z: flag zero *) diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma index 3f1a62839..e28410878 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma @@ -275,11 +275,20 @@ ndefinition push_call_reg ≝ | IP2022 ⇒ Some ? push_call_reg_IP2022 ]) (λf.Some ? (set_alu m t s (f (alu m t s) call'))). -(* push debole di CALL *) -ndefinition pushweak_call_reg ≝ -λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16. - match push_call_reg m t s call' with - [ None ⇒ s | Some s' ⇒ s' ]. +(* pop forte di CALL *) +ndefinition pop_call_reg ≝ +λm:mcu_type. + match m + return λm.Πt.any_status m t → option (ProdT word16 (any_status m t)) + with + [ HC05 ⇒ λt:memory_impl.λs:any_status HC05 t.None ? + | HC08 ⇒ λt:memory_impl.λs:any_status HC08 t.None ? + | HCS08 ⇒ λt:memory_impl.λs:any_status HCS08 t.None ? + | RS08 ⇒ λt:memory_impl.λs:any_status RS08 t.None ? + | IP2022 ⇒ λt:memory_impl.λs:any_status IP2022 t. + match pop_call_reg_IP2022 (alu … s) with + [ pair val alu' ⇒ Some ? (pair … val (set_alu … s alu')) ] + ]. (* REGISTRO IP *) diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma index 6face1d21..07c19464a 100755 --- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma @@ -1434,3 +1434,15 @@ ndefinition ex_of_qu ≝ ndefinition ex_of_oct ≝ λn.match n with [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ]. + +(* esadecimali xNNNN → ottali *) +ndefinition oct_of_exL ≝ +λn.match n with + [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7 + | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ]. + +(* esadecimali NNNNx → ottali *) +ndefinition oct_of_exH ≝ +λn.match n with + [ x0 ⇒ o0 | x1 ⇒ o0 | x2 ⇒ o1 | x3 ⇒ o1 | x4 ⇒ o2 | x5 ⇒ o2 | x6 ⇒ o3 | x7 ⇒ o3 + | x8 ⇒ o4 | x9 ⇒ o4 | xA ⇒ o5 | xB ⇒ o5 | xC ⇒ o6 | xD ⇒ o6 | xE ⇒ o7 | xF ⇒ o7 ]. diff --git a/helm/software/matita/contribs/ng_assembly/num/oct.ma b/helm/software/matita/contribs/ng_assembly/num/oct.ma index fbdbacd5d..d6bfa21e7 100755 --- a/helm/software/matita/contribs/ng_assembly/num/oct.ma +++ b/helm/software/matita/contribs/ng_assembly/num/oct.ma @@ -36,6 +36,10 @@ ninductive oct : Type ≝ | o6: oct | o7: oct. +(* iteratore sugli ottali *) +ndefinition forall_oct ≝ λP. + P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7. + (* operatore = *) ndefinition eq_oct ≝ λn1,n2:oct. @@ -50,9 +54,92 @@ ndefinition eq_oct ≝ | o7 ⇒ match n2 with [ o7 ⇒ true | _ ⇒ false ] ]. -(* iteratore sugli ottali *) -ndefinition forall_oct ≝ λP. - P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7. +(* operatore and *) +ndefinition and_oct ≝ +λe1,e2:oct.match e1 with + [ o0 ⇒ match e2 with + [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0 + | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o0 | o7 ⇒ o0 ] + | o1 ⇒ match e2 with + [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1 + | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o0 | o7 ⇒ o1 ] + | o2 ⇒ match e2 with + [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2 + | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o2 | o7 ⇒ o2 ] + | o3 ⇒ match e2 with + [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 + | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ] + | o4 ⇒ match e2 with + [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0 + | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o4 | o7 ⇒ o4 ] + | o5 ⇒ match e2 with + [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1 + | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o4 | o7 ⇒ o5 ] + | o6 ⇒ match e2 with + [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2 + | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o6 | o7 ⇒ o6 ] + | o7 ⇒ match e2 with + [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 + | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ] + ]. + +(* operatore or *) +ndefinition or_oct ≝ +λe1,e2:oct.match e1 with + [ o0 ⇒ match e2 with + [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 + | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ] + | o1 ⇒ match e2 with + [ o0 ⇒ o1 | o1 ⇒ o1 | o2 ⇒ o3 | o3 ⇒ o3 + | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ] + | o2 ⇒ match e2 with + [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o2 | o3 ⇒ o3 + | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ] + | o3 ⇒ match e2 with + [ o0 ⇒ o3 | o1 ⇒ o3 | o2 ⇒ o3 | o3 ⇒ o3 + | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ] + | o4 ⇒ match e2 with + [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7 + | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ] + | o5 ⇒ match e2 with + [ o0 ⇒ o5 | o1 ⇒ o5 | o2 ⇒ o7 | o3 ⇒ o7 + | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ] + | o6 ⇒ match e2 with + [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o6 | o3 ⇒ o7 + | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ] + | o7 ⇒ match e2 with + [ o0 ⇒ o7 | o1 ⇒ o7 | o2 ⇒ o7 | o3 ⇒ o7 + | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ] + ]. + +(* operatore xor *) +ndefinition xor_oct ≝ +λe1,e2:oct.match e1 with + [ o0 ⇒ match e2 with + [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 + | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ] + | o1 ⇒ match e2 with + [ o0 ⇒ o1 | o1 ⇒ o0 | o2 ⇒ o3 | o3 ⇒ o2 + | o4 ⇒ o5 | o5 ⇒ o4 | o6 ⇒ o7 | o7 ⇒ o6 ] + | o2 ⇒ match e2 with + [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o0 | o3 ⇒ o1 + | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o4 | o7 ⇒ o5 ] + | o3 ⇒ match e2 with + [ o0 ⇒ o3 | o1 ⇒ o2 | o2 ⇒ o1 | o3 ⇒ o0 + | o4 ⇒ o7 | o5 ⇒ o6 | o6 ⇒ o5 | o7 ⇒ o4 ] + | o4 ⇒ match e2 with + [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7 + | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ] + | o5 ⇒ match e2 with + [ o0 ⇒ o5 | o1 ⇒ o4 | o2 ⇒ o7 | o3 ⇒ o6 + | o4 ⇒ o1 | o5 ⇒ o0 | o6 ⇒ o3 | o7 ⇒ o2 ] + | o6 ⇒ match e2 with + [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o4 | o3 ⇒ o5 + | o4 ⇒ o2 | o5 ⇒ o3 | o6 ⇒ o0 | o7 ⇒ o1 ] + | o7 ⇒ match e2 with + [ o0 ⇒ o7 | o1 ⇒ o6 | o2 ⇒ o5 | o3 ⇒ o4 + | o4 ⇒ o3 | o5 ⇒ o2 | o6 ⇒ o1 | o7 ⇒ o0 ] + ]. (* operatore successore *) ndefinition succ_oct ≝ -- 2.39.2