From 34cdd4af2d7bdac3bab74a54123fbfcb02fa0403 Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Sun, 24 Jan 2010 05:44:00 +0000 Subject: [PATCH] freescale porting --- .../matita/contribs/ng_assembly/depends | 96 ++-- .../emulator/opcodes/HC05_table.ma | 4 +- .../emulator/opcodes/HC08_table.ma | 4 +- .../emulator/opcodes/HC08_table_tests.ma | 4 +- .../emulator/opcodes/HCS08_table.ma | 4 +- .../emulator/opcodes/HCS08_table_tests.ma | 4 +- .../emulator/opcodes/IP2022_instr_mode.ma | 82 ++++ .../emulator/opcodes/IP2022_opcode.ma | 126 +++++ .../emulator/opcodes/IP2022_table.ma | 457 ++++++++++++++++++ .../emulator/opcodes/IP2022_table_tests.ma | 105 ++++ .../emulator/opcodes/RS08_table.ma | 4 +- .../ng_assembly/emulator/opcodes/opcode.ma | 50 +- .../translation/IP2022_translation.ma | 58 +++ .../emulator/translation/translation.ma | 36 +- .../emulator/translation/translation_base.ma | 2 + 15 files changed, 904 insertions(+), 132 deletions(-) create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_opcode.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table_tests.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/translation/IP2022_translation.ma diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index 760ac25aa..4de80ff8f 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -1,94 +1,78 @@ -freescale/multivm_lemmas.ma common/nat_lemmas.ma freescale/multivm.ma -freescale/status.ma freescale/opcode_base.ma memory/memory_abs.ma common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma -opcodes/RS08_table.ma common/list.ma opcodes/RS08_opcode_base.ma opcodes/byte_or_word.ma +emulator/opcodes/HC05_table_tests.ma emulator/opcodes/HC05_table.ma emulator/opcodes/opcode.ma num/bool.ma common/theory.ma -freescale_tests/micro_tests10.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma -freescale/table_HCS08_tests.ma freescale/opcode.ma freescale/table_HCS08.ma compiler/preast_tree.ma common/string.ma compiler/ast_type.ma num/word32.ma -opcodes/HCS08_opcode_base.ma num/word16.ma -freescale/multivm.ma freescale/load_write.ma -freescale_tests/medium_tests_tools.ma freescale/multivm.ma -freescale/opcode_base_lemmas.ma freescale/opcode_base.ma num/bool_lemmas.ma +emulator/status/HC08_status.ma num/word16.ma +common/nat.ma num/bool.ma common/nat_to_num.ma common/nat.ma num/word32.ma common/string_lemmas.ma common/ascii_lemmas.ma common/list_utility_lemmas.ma common/string.ma -common/nat.ma num/bool.ma compiler/ast_type_lemmas.ma common/list_utility_lemmas.ma compiler/ast_type.ma -freescale_tests/micro_tests3.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma -memory/memory_bits.ma memory/memory_trees.ma num/quatern.ma num/bool.ma num/exadecim.ma common/nat.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma -freescale/table_HC05_tests.ma freescale/opcode.ma freescale/table_HC05.ma -opcodes/opcode.ma common/list.ma opcodes/HC05_opcode_base.ma opcodes/HC08_opcode_base.ma opcodes/HCS08_opcode_base.ma opcodes/RS08_opcode_base.ma opcodes/byte_or_word.ma num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.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/RS08_status.ma num/byte8.ma num/bitrigesim.ma num/exadecim.ma -opcodes/HC08_opcode_base.ma num/word16.ma -freescale_tests/micro_tests4bis.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma -freescale/load_write.ma freescale/model.ma freescale/translation.ma -freescale/table_RS08.ma common/list.ma freescale/opcode_base.ma +emulator/opcodes/HC08_table.ma common/list.ma emulator/opcodes/HC08_instr_mode.ma emulator/opcodes/HC08_opcode.ma emulator/opcodes/byte_or_word.ma common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma -freescale_tests/micro_tests6.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma +emulator/opcodes/HC05_table.ma common/list.ma emulator/opcodes/HC05_instr_mode.ma emulator/opcodes/HC05_opcode.ma emulator/opcodes/byte_or_word.ma common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma -opcodes/RS08_opcode_base.ma num/word16.ma -opcodes/HC05_opcode_base.ma num/word16.ma -freescale/table_RS08_tests.ma freescale/opcode.ma freescale/table_RS08.ma -freescale/translation.ma common/option.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma -freescale/translation_lemmas.ma freescale/translation.ma num/byte8_lemmas.ma -memory/memory_func.ma common/list.ma common/option.ma memory/memory_struct.ma num/word32.ma +emulator/translation/HCS08_translation.ma emulator/translation/translation_base.ma +emulator/memory/memory_trees.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma +emulator/opcodes/IP2022_opcode.ma num/bool.ma num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma -freescale_tests/micro_tests9.ma common/nat_to_num.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma -opcodes/HCS08_table_tests.ma freescale/opcode.ma +emulator/opcodes/RS08_table_tests.ma emulator/opcodes/RS08_table.ma emulator/opcodes/opcode.ma test_errori.ma -freescale_tests/micro_tests2.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma compiler/environment.ma common/string.ma compiler/ast_type.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 common/ascii_lemmas.ma common/ascii.ma num/bool_lemmas.ma -freescale/model.ma freescale/status.ma -freescale/table_HC05.ma common/list.ma freescale/opcode_base.ma -opcodes/HC08_table.ma common/list.ma opcodes/HC08_opcode_base.ma opcodes/byte_or_word.ma -opcodes/HC08_table_tests.ma 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/string.ma common/ascii.ma common/list_utility.ma common/theory.ma +emulator/opcodes/byte_or_word.ma num/word16.ma compiler/ast_type.ma common/list_utility.ma num/word16.ma num/byte8.ma -freescale_tests/micro_tests5.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma +emulator/opcodes/IP2022_instr_mode.ma num/word16.ma +emulator/translation/HC08_translation.ma emulator/translation/translation_base.ma common/prod.ma num/bool.ma +emulator/opcodes/HCS08_opcode.ma num/bool.ma +emulator/opcodes/HC08_opcode.ma num/bool.ma num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma -freescale_tests/medium_tests.ma common/list_utility.ma common/nat_to_num.ma freescale_tests/medium_tests_tools.ma -memory/memory_trees.ma common/list.ma common/option.ma memory/memory_struct.ma num/word32.ma +emulator/status/status_getter.ma emulator/status/status.ma num/bool_lemmas.ma num/bool.ma -freescale/opcode_base_lemmas1.ma freescale/opcode_base_lemmas_instrmode.ma freescale/opcode_base_lemmas_opcode.ma num/word16_lemmas.ma -freescale/table_HC08.ma common/list.ma freescale/opcode_base.ma -opcodes/HC05_table_tests.ma opcodes/opcode.ma -memory/memory_struct.ma num/byte8.ma num/oct.ma +emulator/memory/memory_abs.ma emulator/memory/memory_bits.ma emulator/memory/memory_func.ma emulator/memory/memory_trees.ma +emulator/opcodes/RS08_opcode.ma num/bool.ma num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma -freescale/table_HCS08.ma common/list.ma freescale/opcode_base.ma -memory/memory_abs.ma memory/memory_bits.ma memory/memory_func.ma memory/memory_trees.ma +emulator/memory/memory_struct.ma num/byte8.ma num/oct.ma +emulator/translation/RS08_translation.ma emulator/translation/translation_base.ma +emulator/status/status_setter.ma emulator/status/status.ma +emulator/translation/HC05_translation.ma emulator/translation/translation_base.ma num/word32.ma num/word16.ma common/ascii.ma num/bool.ma -freescale_tests/micro_tests8.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma -freescale/opcode_base.ma num/word16.ma -freescale/status_lemmas.ma common/option_lemmas.ma common/prod_lemmas.ma freescale/opcode_base_lemmas1.ma freescale/status.ma num/word16_lemmas.ma -freescale_tests/micro_tests_tools.ma common/list.ma num/word16.ma +emulator/opcodes/HCS08_table_tests.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/opcode.ma +emulator/opcodes/HC05_instr_mode.ma num/word16.ma +emulator/opcodes/IP2022_table_tests.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/opcode.ma num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma -freescale_tests/micro_tests1.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma -opcodes/HCS08_table.ma common/list.ma opcodes/HCS08_opcode_base.ma opcodes/byte_or_word.ma -freescale/table_HC08_tests.ma freescale/opcode.ma freescale/table_HC08.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 +emulator/status/RS08_status.ma num/word16.ma +emulator/opcodes/HC08_instr_mode.ma num/word16.ma +emulator/opcodes/opcode.ma common/list.ma emulator/opcodes/HC05_instr_mode.ma emulator/opcodes/HC05_opcode.ma emulator/opcodes/HC08_instr_mode.ma emulator/opcodes/HC08_opcode.ma emulator/opcodes/HCS08_opcode.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_opcode.ma emulator/opcodes/RS08_instr_mode.ma emulator/opcodes/RS08_opcode.ma emulator/opcodes/byte_or_word.ma common/option.ma num/bool.ma common/option_lemmas.ma common/option.ma num/bool_lemmas.ma num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma -freescale/opcode_base_lemmas_opcode.ma freescale/opcode_base.ma num/bool_lemmas.ma -freescale_tests/micro_tests4.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma +emulator/opcodes/RS08_table.ma common/list.ma emulator/opcodes/RS08_instr_mode.ma emulator/opcodes/RS08_opcode.ma emulator/opcodes/byte_or_word.ma common/sigma.ma common/theory.ma common/list_lemmas.ma common/list.ma +emulator/opcodes/HCS08_table.ma common/list.ma emulator/opcodes/HC08_instr_mode.ma emulator/opcodes/HCS08_opcode.ma emulator/opcodes/byte_or_word.ma +emulator/translation/IP2022_translation.ma emulator/translation/translation_base.ma universe/universe.ma common/list.ma common/nat_lemmas.ma common/prod.ma num/bitrigesim.ma num/bool.ma -opcodes/byte_or_word.ma num/word16.ma -opcodes/HC05_table.ma common/list.ma opcodes/HC05_opcode_base.ma opcodes/byte_or_word.ma -freescale/opcode_base_lemmas_instrmode.ma freescale/opcode_base.ma num/bitrigesim_lemmas.ma num/exadecim_lemmas.ma num/oct_lemmas.ma common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma +emulator/translation/translation.ma emulator/translation/HC05_translation.ma emulator/translation/HC08_translation.ma emulator/translation/HCS08_translation.ma emulator/translation/IP2022_translation.ma emulator/translation/RS08_translation.ma num/oct.ma num/bool.ma common/list.ma common/theory.ma -freescale/opcode.ma common/list.ma freescale/opcode_base.ma -freescale_tests/micro_tests7.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma -opcodes/RS08_table_tests.ma freescale/opcode.ma +emulator/opcodes/HC08_table_tests.ma emulator/opcodes/HC08_table.ma emulator/opcodes/opcode.ma +emulator/opcodes/HC05_opcode.ma num/bool.ma diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_table.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_table.ma index 4217195ff..0f2822bf7 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_table.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_table.ma @@ -30,9 +30,7 @@ include "common/list.ma". (* ***************** *) (* definizione come concatenazione finale di liste per velocizzare il parsing *) -(* ogni riga e' (any_opcode m) (instr_mode) (opcode esadecimale) (#cicli esecuzione) *) -(* NB: l'uso di any_opcode m + concatenazione finale tutte liste - impedisce di introdurre opcode disomogenei (per mcu) *) +(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *) ndefinition opcode_table_HC05_1 ≝ [ diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table.ma index 65e3c1e53..9a0ec7478 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table.ma @@ -30,9 +30,7 @@ include "common/list.ma". (* ***************** *) (* definizione come concatenazione finale di liste per velocizzare il parsing *) -(* ogni riga e' (any_opcode m) (instr_mode) (opcode esadecimale) (#cicli esecuzione) *) -(* NB: l'uso di any_opcode m + concatenazione finale tutte liste - impedisce di introdurre opcode disomogenei (per mcu) *) +(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *) ndefinition opcode_table_HC08_1 ≝ [ diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table_tests.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table_tests.ma index aa792b55e..06b4d2657 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table_tests.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_table_tests.ma @@ -78,8 +78,8 @@ ndefinition HC08_not_impl_word ≝ (* test bytecode non implementati *) nlemma ok_word_table_HC08 : forall_b8 (λb. - (test_not_impl_byte b HC08_not_impl_word ⊙ eq_w16 (get_word_count HC08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗ - (⊖ (test_not_impl_byte b HC08_not_impl_word) ⊙ eq_w16 (get_word_count HC08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x0〉〉)) + (test_not_impl_byte b HC08_not_impl_word ⊙ eq_w16 (get_word_count HC08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗ + (⊖ (test_not_impl_byte b HC08_not_impl_word) ⊙ eq_w16 (get_word_count HC08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x0〉〉)) = true. napply refl_eq. nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table.ma index 2982dbb57..742e8b8ee 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table.ma @@ -30,9 +30,7 @@ include "common/list.ma". (* ****************** *) (* definizione come concatenazione finale di liste per velocizzare il parsing *) -(* ogni riga e' (any_opcode m) (instr_mode) (opcode esadecimale) (#cicli esecuzione) *) -(* NB: l'uso di any_opcode m + concatenazione finale tutte liste - impedisce di introdurre opcode disomogenei (per mcu) *) +(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *) ndefinition opcode_table_HCS08_1 ≝ [ diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table_tests.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table_tests.ma index 60a40cb73..c7b9c1549 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table_tests.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_table_tests.ma @@ -73,8 +73,8 @@ ndefinition HCS08_not_impl_word ≝ (* test bytecode non implementati *) nlemma ok_word_table_HCS08 : forall_b8 (λb. - (test_not_impl_byte b HCS08_not_impl_word ⊙ eq_w16 (get_word_count HCS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗ - (⊖ (test_not_impl_byte b HCS08_not_impl_word) ⊙ eq_w16 (get_word_count HCS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉)) + (test_not_impl_byte b HCS08_not_impl_word ⊙ eq_w16 (get_word_count HCS08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗ + (⊖ (test_not_impl_byte b HCS08_not_impl_word) ⊙ eq_w16 (get_word_count HCS08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉)) = true. napply refl_eq. nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma new file mode 100755 index 000000000..45548e7b1 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma @@ -0,0 +1,82 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "num/word16.ma". + +(* ********************************************** *) +(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *) +(* ********************************************** *) + +(* enumerazione delle modalita' di indirizzamento = caricamento degli operandi *) +ninductive IP2022_instr_mode: Type ≝ + (* nessun operando : formato xxxxxxxx xxxxxxxx *) + MODE_INH : IP2022_instr_mode + + (* #lit3 → / : formato xxxxxxxx xxxxxkkk *) +| MODE_IMM3 : oct → IP2022_instr_mode + (* W, #lit8 → W : formato xxxxxxxx kkkkkkkk [load 1 byte arg] *) +| MODE_IMM8 : IP2022_instr_mode + (* #lit13 → / : formato xxxkkkkk kkkkkkkk [load 1 byte arg] *) +| MODE_IMM13 : bitrigesim → IP2022_instr_mode + + (* FR, W → FR : formato xxxxxxx0 ffffffff [load 1 byte arg] *) +| MODE_FR0_and_W : IP2022_instr_mode + (* FR, W → FR : formato xxxxxxx1 ffffffff [load 1 byte arg] *) +| MODE_FR1_and_W : IP2022_instr_mode + (* W, FR → W : formato xxxxxxx0 ffffffff [load 1 byte arg] *) +| MODE_W_and_FR0 : IP2022_instr_mode + (* W, FR → W : formato xxxxxxx1 ffffffff [load 1 byte arg] *) +| MODE_W_and_FR1 : IP2022_instr_mode + + (* FR(bitN) → FR(bitN) : formato xxxxbbb0 ffffffff [load 1 byte arg] *) +| MODE_FR0n : oct → IP2022_instr_mode + (* FR(bitN) → FR(bitN) : formato xxxxbbb1 ffffffff [load 1 byte arg] *) +| MODE_FR1n : oct → IP2022_instr_mode +. + +ndefinition eq_IP2022_im ≝ +λi1,i2:IP2022_instr_mode. + match i1 with + [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ] + | MODE_IMM3 o1 ⇒ match i2 with [ MODE_IMM3 o2 ⇒ eq_oct o1 o2 | _ ⇒ false ] + | MODE_IMM8 ⇒ match i2 with [ MODE_IMM8 ⇒ true | _ ⇒ false ] + | MODE_IMM13 t1 ⇒ match i2 with [ MODE_IMM13 t2 ⇒ eq_bit t1 t2 | _ ⇒ false ] + | MODE_FR0_and_W ⇒ match i2 with [ MODE_FR0_and_W ⇒ true | _ ⇒ false ] + | MODE_FR1_and_W ⇒ match i2 with [ MODE_FR1_and_W ⇒ true | _ ⇒ false ] + | MODE_W_and_FR0 ⇒ match i2 with [ MODE_W_and_FR0 ⇒ true | _ ⇒ false ] + | MODE_W_and_FR1 ⇒ match i2 with [ MODE_W_and_FR1 ⇒ true | _ ⇒ false ] + | MODE_FR0n o1 ⇒ match i2 with [ MODE_FR0n o2 ⇒ eq_oct o1 o2 | _ ⇒ false ] + | MODE_FR1n o1 ⇒ match i2 with [ MODE_FR1n o2 ⇒ eq_oct o1 o2 | _ ⇒ false ] + ]. + +(* iteratore sulle modalita' *) +ndefinition forall_IP2022_im ≝ λP:IP2022_instr_mode → bool. + P MODE_INH +⊗ forall_oct (λo.P (MODE_IMM3 o)) +⊗ P MODE_IMM8 +⊗ forall_bit (λt.P (MODE_IMM13 t)) +⊗ P MODE_FR0_and_W +⊗ P MODE_FR1_and_W +⊗ P MODE_W_and_FR0 +⊗ P MODE_W_and_FR1 +⊗ forall_oct (λo.P (MODE_FR0n o)) +⊗ forall_oct (λo.P (MODE_FR1n o)). diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_opcode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_opcode.ma new file mode 100755 index 000000000..315862e7d --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_opcode.ma @@ -0,0 +1,126 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "num/bool.ma". + +(* ********************************************** *) +(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *) +(* ********************************************** *) + +(* enumerazione delle istruzioni *) +ninductive IP2022_opcode: Type ≝ + ADD : IP2022_opcode (* add *) +| ADDC : IP2022_opcode (* add with carry *) +| AND : IP2022_opcode (* and *) +| BREAK : IP2022_opcode (* enter break mode *) +| BREAKX : IP2022_opcode (* enter break mode, after skip *) +| CALL : IP2022_opcode (* subroutine call *) +| CLR : IP2022_opcode (* clear *) +| CLRB : IP2022_opcode (* clear bit *) +| CMP : IP2022_opcode (* set flags according to sub *) +| CSE : IP2022_opcode (* confront & skip if equal *) +| CSNE : IP2022_opcode (* confront & skip if not equal *) +| CWDT : IP2022_opcode (* clear watch dog -- not impl. ERR *) +| DEC : IP2022_opcode (* decrement *) +| DECSNZ : IP2022_opcode (* decrement & skip if not zero *) +| DECSZ : IP2022_opcode (* decrement & skip if zero *) +| FERASE : IP2022_opcode (* flash erase -- not impl. ERR *) +| FREAD : IP2022_opcode (* flash read -- not impl. ERR *) +| FWRITE : IP2022_opcode (* flash write -- not impl. ERR *) +| INC : IP2022_opcode (* increment *) +| INCSNZ : IP2022_opcode (* increment & skip if not zero *) +| INCSZ : IP2022_opcode (* increment & skip if zero *) +| INT : IP2022_opcode (* interrupt -- not impl. ERR *) +| IREAD : IP2022_opcode (* memory read *) +| IREADI : IP2022_opcode (* memory read & inc *) +| IWRITE : IP2022_opcode (* memory write *) +| IWRITEI : IP2022_opcode (* memory write & inc *) +| JMP : IP2022_opcode (* jump *) +| LOADH : IP2022_opcode (* load Data Pointer High *) +| LOADL : IP2022_opcode (* load Data Pointer Low *) +| MOV : IP2022_opcode (* move *) +| MULS : IP2022_opcode (* signed mul *) +| MULU : IP2022_opcode (* unsigned mul *) +| NOP : IP2022_opcode (* nop *) +| NOT : IP2022_opcode (* not *) +| OR : IP2022_opcode (* or *) +| PAGE : IP2022_opcode (* set Page Register *) +| POP : IP2022_opcode (* pop *) +| PUSH : IP2022_opcode (* push *) +| RET : IP2022_opcode (* subroutine ret *) +| RETI : IP2022_opcode (* interrupt ret -- not impl. ERR *) +| RETNP : IP2022_opcode (* subroutine ret & don't restore Page Register *) +| RETW : IP2022_opcode (* subroutine ret & load W Register *) +| RL : IP2022_opcode (* rotate left *) +| RR : IP2022_opcode (* rotate right *) +| SB : IP2022_opcode (* skip if bit set *) +| SETB : IP2022_opcode (* set bit *) +| SNB : IP2022_opcode (* skip if bit not set *) +| SPEED : IP2022_opcode (* set Speed Register *) +| SUB : IP2022_opcode (* sub *) +| SUBC : IP2022_opcode (* sub with carry *) +| SWAP : IP2022_opcode (* swap xxxxyyyy → yyyyxxxx *) +| TEST : IP2022_opcode (* set flags according to zero test *) +| XOR : IP2022_opcode (* xor *) +. + +ndefinition eq_IP2022_op ≝ +λop1,op2:IP2022_opcode. + match op1 with + [ ADD ⇒ match op2 with [ ADD ⇒ true | _ ⇒ false ] | ADDC ⇒ match op2 with [ ADDC ⇒ true | _ ⇒ false ] + | AND ⇒ match op2 with [ AND ⇒ true | _ ⇒ false ] | BREAK ⇒ match op2 with [ BREAK ⇒ true | _ ⇒ false ] + | BREAKX ⇒ match op2 with [ BREAKX ⇒ true | _ ⇒ false ] | CALL ⇒ match op2 with [ CALL ⇒ true | _ ⇒ false ] + | CLR ⇒ match op2 with [ CLR ⇒ true | _ ⇒ false ] | CLRB ⇒ match op2 with [ CLRB ⇒ true | _ ⇒ false ] + | CMP ⇒ match op2 with [ CMP ⇒ true | _ ⇒ false ] | CSE ⇒ match op2 with [ CSE ⇒ true | _ ⇒ false ] + | CSNE ⇒ match op2 with [ CSNE ⇒ true | _ ⇒ false ] | CWDT ⇒ match op2 with [ CWDT ⇒ true | _ ⇒ false ] + | DEC ⇒ match op2 with [ DEC ⇒ true | _ ⇒ false ] | DECSNZ ⇒ match op2 with [ DECSNZ ⇒ true | _ ⇒ false ] + | DECSZ ⇒ match op2 with [ DECSZ ⇒ true | _ ⇒ false ] | FERASE ⇒ match op2 with [ FERASE ⇒ true | _ ⇒ false ] + | FREAD ⇒ match op2 with [ FREAD ⇒ true | _ ⇒ false ] | FWRITE ⇒ match op2 with [ FWRITE ⇒ true | _ ⇒ false ] + | INC ⇒ match op2 with [ INC ⇒ true | _ ⇒ false ] | INCSNZ ⇒ match op2 with [ INCSNZ ⇒ true | _ ⇒ false ] + | INCSZ ⇒ match op2 with [ INCSZ ⇒ true | _ ⇒ false ] | INT ⇒ match op2 with [ INT ⇒ true | _ ⇒ false ] + | IREAD ⇒ match op2 with [ IREAD ⇒ true | _ ⇒ false ] | IREADI ⇒ match op2 with [ IREADI ⇒ true | _ ⇒ false ] + | IWRITE ⇒ match op2 with [ IWRITE ⇒ true | _ ⇒ false ] | IWRITEI ⇒ match op2 with [ IWRITEI ⇒ true | _ ⇒ false ] + | JMP ⇒ match op2 with [ JMP ⇒ true | _ ⇒ false ] | LOADH ⇒ match op2 with [ LOADH ⇒ true | _ ⇒ false ] + | LOADL ⇒ match op2 with [ LOADL ⇒ true | _ ⇒ false ] | MOV ⇒ match op2 with [ MOV ⇒ true | _ ⇒ false ] + | MULS ⇒ match op2 with [ MULS ⇒ true | _ ⇒ false ] | MULU ⇒ match op2 with [ MULU ⇒ true | _ ⇒ false ] + | NOP ⇒ match op2 with [ NOP ⇒ true | _ ⇒ false ] | NOT ⇒ match op2 with [ NOT ⇒ true | _ ⇒ false ] + | OR ⇒ match op2 with [ OR ⇒ true | _ ⇒ false ] | PAGE ⇒ match op2 with [ PAGE ⇒ true | _ ⇒ false ] + | POP ⇒ match op2 with [ POP ⇒ true | _ ⇒ false ] | PUSH ⇒ match op2 with [ PUSH ⇒ true | _ ⇒ false ] + | RET ⇒ match op2 with [ RET ⇒ true | _ ⇒ false ] | RETI ⇒ match op2 with [ RETI ⇒ true | _ ⇒ false ] + | RETNP ⇒ match op2 with [ RETNP ⇒ true | _ ⇒ false ] | RETW ⇒ match op2 with [ RETW ⇒ true | _ ⇒ false ] + | RL ⇒ match op2 with [ RL ⇒ true | _ ⇒ false ] | RR ⇒ match op2 with [ RR ⇒ true | _ ⇒ false ] + | SB ⇒ match op2 with [ SB ⇒ true | _ ⇒ false ] | SETB ⇒ match op2 with [ SETB ⇒ true | _ ⇒ false ] + | SNB ⇒ match op2 with [ SNB ⇒ true | _ ⇒ false ] | SPEED ⇒ match op2 with [ SPEED ⇒ true | _ ⇒ false ] + | SUB ⇒ match op2 with [ SUB ⇒ true | _ ⇒ false ] | SUBC ⇒ match op2 with [ SUBC ⇒ true | _ ⇒ false ] + | SWAP ⇒ match op2 with [ SWAP ⇒ true | _ ⇒ false ] | TEST ⇒ match op2 with [ TEST ⇒ true | _ ⇒ false ] + | XOR ⇒ match op2 with [ XOR ⇒ true | _ ⇒ false ] + ]. + +(* iteratore sugli opcode *) +ndefinition forall_IP2022_op ≝ λP:IP2022_opcode → bool. + P ADD ⊗ P ADDC ⊗ P AND ⊗ P BREAK ⊗ P BREAKX ⊗ P CALL ⊗ P CLR ⊗ P CLRB ⊗ + P CMP ⊗ P CSE ⊗ P CSNE ⊗ P CWDT ⊗ P DEC ⊗ P DECSNZ ⊗ P DECSZ ⊗ P FERASE ⊗ + P FREAD ⊗ P FWRITE ⊗ P INC ⊗ P INCSNZ ⊗ P INCSZ ⊗ P INT ⊗ P IREAD ⊗ P IREADI ⊗ + P IWRITE ⊗ P IWRITEI ⊗ P JMP ⊗ P LOADH ⊗ P LOADL ⊗ P MOV ⊗ P MULS ⊗ P MULU ⊗ + P NOP ⊗ P NOT ⊗ P OR ⊗ P PAGE ⊗ P POP ⊗ P PUSH ⊗ P RET ⊗ P RETI ⊗ + P RETNP ⊗ P RETW ⊗ P RL ⊗ P RR ⊗ P SB ⊗ P SETB ⊗ P SNB ⊗ P SPEED ⊗ + P SUB ⊗ P SUBC ⊗ P SWAP ⊗ P TEST ⊗ P XOR. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table.ma new file mode 100755 index 000000000..0cddf72bc --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table.ma @@ -0,0 +1,457 @@ +(**************************************************************************) +(* ___ *) +(* ||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/opcodes/IP2022_opcode.ma". +include "emulator/opcodes/IP2022_instr_mode.ma". +include "emulator/opcodes/byte_or_word.ma". +include "common/list.ma". + +(* ******************* *) +(* TABELLA DELL'IP2022 *) +(* ******************* *) + +(* definizione come concatenazione finale di liste per velocizzare il parsing *) +(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *) + +ndefinition opcode_table_IP2022_1 ≝ +[ + quadruple … ADD MODE_FR0_and_W (Byte 〈x1,xE〉) 〈x0,x1〉 +; quadruple … ADD MODE_FR1_and_W (Byte 〈x1,xF〉) 〈x0,x1〉 +; quadruple … ADD MODE_W_and_FR0 (Byte 〈x1,xC〉) 〈x0,x1〉 +; quadruple … ADD MODE_W_and_FR1 (Byte 〈x1,xD〉) 〈x0,x1〉 +; quadruple … ADD MODE_IMM8 (Byte 〈x7,xB〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_2 ≝ +[ + quadruple … ADDC MODE_FR0_and_W (Byte 〈x5,xE〉) 〈x0,x1〉 +; quadruple … ADDC MODE_FR1_and_W (Byte 〈x5,xF〉) 〈x0,x1〉 +; quadruple … ADDC MODE_W_and_FR0 (Byte 〈x5,xC〉) 〈x0,x1〉 +; quadruple … ADDC MODE_W_and_FR1 (Byte 〈x5,xD〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_3 ≝ +[ + quadruple … AND MODE_FR0_and_W (Byte 〈x1,x6〉) 〈x0,x1〉 +; quadruple … AND MODE_FR1_and_W (Byte 〈x1,x7〉) 〈x0,x1〉 +; quadruple … AND MODE_W_and_FR0 (Byte 〈x1,x4〉) 〈x0,x1〉 +; quadruple … AND MODE_W_and_FR1 (Byte 〈x1,x5〉) 〈x0,x1〉 +; quadruple … AND MODE_IMM8 (Byte 〈x7,xE〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_4 ≝ +[ + quadruple … BREAK MODE_INH (Word 〈〈x0,x0〉:〈x0,x1〉〉) 〈x0,x1〉 +; quadruple … BREAKX MODE_INH (Word 〈〈x0,x0〉:〈x0,x5〉〉) 〈x0,x1〉 +; quadruple … CWDT MODE_INH (Word 〈〈x0,x0〉:〈x0,x4〉〉) 〈x0,x1〉 +; quadruple … FERASE MODE_INH (Word 〈〈x0,x0〉:〈x0,x3〉〉) 〈x0,x1〉 +; quadruple … FREAD MODE_INH (Word 〈〈x0,x0〉:〈x1,xB〉〉) 〈x0,x1〉 +; quadruple … FWRITE MODE_INH (Word 〈〈x0,x0〉:〈x1,xA〉〉) 〈x0,x1〉 +; quadruple … INT MODE_INH (Word 〈〈x0,x0〉:〈x0,x6〉〉) 〈x0,x3〉 +; quadruple … IREAD MODE_INH (Word 〈〈x0,x0〉:〈x1,x9〉〉) 〈x0,x4〉 (* blocking *) +; quadruple … IREADI MODE_INH (Word 〈〈x0,x0〉:〈x1,xD〉〉) 〈x0,x4〉 (* blocking *) +; quadruple … IWRITE MODE_INH (Word 〈〈x0,x0〉:〈x1,x8〉〉) 〈x0,x4〉 (* blocking *) +; quadruple … IWRITEI MODE_INH (Word 〈〈x0,x0〉:〈x1,xC〉〉) 〈x0,x4〉 (* blocking *) +; quadruple … NOP MODE_INH (Word 〈〈x0,x0〉:〈x0,x0〉〉) 〈x0,x1〉 +; quadruple … RET MODE_INH (Word 〈〈x0,x0〉:〈x0,x7〉〉) 〈x0,x3〉 +; quadruple … RETNP MODE_INH (Word 〈〈x0,x0〉:〈x0,x2〉〉) 〈x0,x3〉 +]. + +ndefinition opcode_table_IP2022_5 ≝ +[ + quadruple … CALL (MODE_IMM13 t00) (Byte 〈xC,x0〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t01) (Byte 〈xC,x1〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t02) (Byte 〈xC,x2〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t03) (Byte 〈xC,x3〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t04) (Byte 〈xC,x4〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t05) (Byte 〈xC,x5〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t06) (Byte 〈xC,x6〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t07) (Byte 〈xC,x7〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t08) (Byte 〈xC,x8〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t09) (Byte 〈xC,x9〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t0A) (Byte 〈xC,xA〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t0B) (Byte 〈xC,xB〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t0C) (Byte 〈xC,xC〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t0D) (Byte 〈xC,xD〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t0E) (Byte 〈xC,xE〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t0F) (Byte 〈xC,xF〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t10) (Byte 〈xD,x0〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t11) (Byte 〈xD,x1〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t12) (Byte 〈xD,x2〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t13) (Byte 〈xD,x3〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t14) (Byte 〈xD,x4〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t15) (Byte 〈xD,x5〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t16) (Byte 〈xD,x6〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t17) (Byte 〈xD,x7〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t18) (Byte 〈xD,x8〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t19) (Byte 〈xD,x9〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t1A) (Byte 〈xD,xA〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t1B) (Byte 〈xD,xB〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t1C) (Byte 〈xD,xC〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t1D) (Byte 〈xD,xD〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t1E) (Byte 〈xD,xE〉) 〈x0,x3〉 +; quadruple … CALL (MODE_IMM13 t1F) (Byte 〈xD,xF〉) 〈x0,x3〉 +]. + +ndefinition opcode_table_IP2022_6 ≝ +[ + quadruple … CLR MODE_FR0_and_W (Byte 〈x0,x6〉) 〈x0,x1〉 +; quadruple … CLR MODE_FR1_and_W (Byte 〈x0,x7〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_7 ≝ +[ + quadruple … CLRB (MODE_FR0n o0) (Byte 〈x8,x0〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR1n o0) (Byte 〈x8,x1〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR0n o1) (Byte 〈x8,x2〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR1n o1) (Byte 〈x8,x3〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR0n o2) (Byte 〈x8,x4〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR1n o2) (Byte 〈x8,x5〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR0n o3) (Byte 〈x8,x6〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR1n o3) (Byte 〈x8,x7〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR0n o4) (Byte 〈x8,x8〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR1n o4) (Byte 〈x8,x9〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR0n o5) (Byte 〈x8,xA〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR1n o5) (Byte 〈x8,xB〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR0n o6) (Byte 〈x8,xC〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR1n o6) (Byte 〈x8,xD〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR0n o7) (Byte 〈x8,xE〉) 〈x0,x1〉 +; quadruple … CLRB (MODE_FR1n o7) (Byte 〈x8,xF〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_8 ≝ +[ + quadruple … CMP MODE_W_and_FR0 (Byte 〈x0,x4〉) 〈x0,x1〉 +; quadruple … CMP MODE_W_and_FR1 (Byte 〈x0,x5〉) 〈x0,x1〉 +; quadruple … CMP MODE_IMM8 (Byte 〈x7,x9〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_9 ≝ +[ + quadruple … CSE MODE_W_and_FR0 (Byte 〈x4,x2〉) 〈x0,x1〉 +; quadruple … CSE MODE_W_and_FR1 (Byte 〈x4,x3〉) 〈x0,x1〉 +; quadruple … CSE MODE_IMM8 (Byte 〈x7,x7〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_10 ≝ +[ + quadruple … CSNE MODE_W_and_FR0 (Byte 〈x4,x0〉) 〈x0,x1〉 +; quadruple … CSNE MODE_W_and_FR1 (Byte 〈x4,x1〉) 〈x0,x1〉 +; quadruple … CSNE MODE_IMM8 (Byte 〈x7,x6〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_11 ≝ +[ + quadruple … DEC MODE_FR0_and_W (Byte 〈x0,xE〉) 〈x0,x1〉 +; quadruple … DEC MODE_FR1_and_W (Byte 〈x0,xF〉) 〈x0,x1〉 +; quadruple … DEC MODE_W_and_FR0 (Byte 〈x0,xC〉) 〈x0,x1〉 +; quadruple … DEC MODE_W_and_FR1 (Byte 〈x0,xD〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_12 ≝ +[ + quadruple … DECSNZ MODE_FR0_and_W (Byte 〈x4,xE〉) 〈x0,x1〉 +; quadruple … DECSNZ MODE_FR1_and_W (Byte 〈x4,xF〉) 〈x0,x1〉 +; quadruple … DECSNZ MODE_W_and_FR0 (Byte 〈x4,xC〉) 〈x0,x1〉 +; quadruple … DECSNZ MODE_W_and_FR1 (Byte 〈x4,xD〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_13 ≝ +[ + quadruple … DECSZ MODE_FR0_and_W (Byte 〈x2,xE〉) 〈x0,x1〉 +; quadruple … DECSZ MODE_FR1_and_W (Byte 〈x2,xF〉) 〈x0,x1〉 +; quadruple … DECSZ MODE_W_and_FR0 (Byte 〈x2,xC〉) 〈x0,x1〉 +; quadruple … DECSZ MODE_W_and_FR1 (Byte 〈x2,xD〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_14 ≝ +[ + quadruple … INC MODE_FR0_and_W (Byte 〈x2,xA〉) 〈x0,x1〉 +; quadruple … INC MODE_FR1_and_W (Byte 〈x2,xB〉) 〈x0,x1〉 +; quadruple … INC MODE_W_and_FR0 (Byte 〈x2,x8〉) 〈x0,x1〉 +; quadruple … INC MODE_W_and_FR1 (Byte 〈x2,x9〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_15 ≝ +[ + quadruple … INCSNZ MODE_FR0_and_W (Byte 〈x5,xA〉) 〈x0,x1〉 +; quadruple … INCSNZ MODE_FR1_and_W (Byte 〈x5,xB〉) 〈x0,x1〉 +; quadruple … INCSNZ MODE_W_and_FR0 (Byte 〈x5,x8〉) 〈x0,x1〉 +; quadruple … INCSNZ MODE_W_and_FR1 (Byte 〈x5,x9〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_16 ≝ +[ + quadruple … INCSZ MODE_FR0_and_W (Byte 〈x3,xE〉) 〈x0,x1〉 +; quadruple … INCSZ MODE_FR1_and_W (Byte 〈x3,xF〉) 〈x0,x1〉 +; quadruple … INCSZ MODE_W_and_FR0 (Byte 〈x3,xC〉) 〈x0,x1〉 +; quadruple … INCSZ MODE_W_and_FR1 (Byte 〈x3,xD〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_17 ≝ +[ + quadruple … JMP (MODE_IMM13 t00) (Byte 〈xE,x0〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t01) (Byte 〈xE,x1〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t02) (Byte 〈xE,x2〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t03) (Byte 〈xE,x3〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t04) (Byte 〈xE,x4〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t05) (Byte 〈xE,x5〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t06) (Byte 〈xE,x6〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t07) (Byte 〈xE,x7〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t08) (Byte 〈xE,x8〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t09) (Byte 〈xE,x9〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t0A) (Byte 〈xE,xA〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t0B) (Byte 〈xE,xB〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t0C) (Byte 〈xE,xC〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t0D) (Byte 〈xE,xD〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t0E) (Byte 〈xE,xE〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t0F) (Byte 〈xE,xF〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t10) (Byte 〈xF,x0〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t11) (Byte 〈xF,x1〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t12) (Byte 〈xF,x2〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t13) (Byte 〈xF,x3〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t14) (Byte 〈xF,x4〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t15) (Byte 〈xF,x5〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t16) (Byte 〈xF,x6〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t17) (Byte 〈xF,x7〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t18) (Byte 〈xF,x8〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t19) (Byte 〈xF,x9〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t1A) (Byte 〈xF,xA〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t1B) (Byte 〈xF,xB〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t1C) (Byte 〈xF,xC〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t1D) (Byte 〈xF,xD〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t1E) (Byte 〈xF,xE〉) 〈x0,x3〉 +; quadruple … JMP (MODE_IMM13 t1F) (Byte 〈xF,xF〉) 〈x0,x3〉 +]. + +ndefinition opcode_table_IP2022_18 ≝ +[ + quadruple … LOADH MODE_IMM8 (Byte 〈x7,x0〉) 〈x0,x1〉 +; quadruple … LOADL MODE_IMM8 (Byte 〈x7,x1〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_19 ≝ +[ + quadruple … MOV MODE_FR0_and_W (Byte 〈x0,x2〉) 〈x0,x1〉 +; quadruple … MOV MODE_FR1_and_W (Byte 〈x0,x3〉) 〈x0,x1〉 +; quadruple … MOV MODE_W_and_FR0 (Byte 〈x2,x0〉) 〈x0,x1〉 +; quadruple … MOV MODE_W_and_FR1 (Byte 〈x2,x1〉) 〈x0,x1〉 +; quadruple … MOV MODE_IMM8 (Byte 〈x7,xC〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_20 ≝ +[ + quadruple … MULS MODE_W_and_FR0 (Byte 〈x5,x4〉) 〈x0,x1〉 +; quadruple … MULS MODE_W_and_FR1 (Byte 〈x5,x5〉) 〈x0,x1〉 +; quadruple … MULS MODE_IMM8 (Byte 〈x7,x3〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_21 ≝ +[ + quadruple … MULU MODE_W_and_FR0 (Byte 〈x5,x0〉) 〈x0,x1〉 +; quadruple … MULU MODE_W_and_FR1 (Byte 〈x5,x1〉) 〈x0,x1〉 +; quadruple … MULU MODE_IMM8 (Byte 〈x7,x2〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_22 ≝ +[ + quadruple … NOT MODE_FR0_and_W (Byte 〈x2,x6〉) 〈x0,x1〉 +; quadruple … NOT MODE_FR1_and_W (Byte 〈x2,x7〉) 〈x0,x1〉 +; quadruple … NOT MODE_W_and_FR0 (Byte 〈x2,x4〉) 〈x0,x1〉 +; quadruple … NOT MODE_W_and_FR1 (Byte 〈x2,x5〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_23 ≝ +[ + quadruple … OR MODE_FR0_and_W (Byte 〈x1,x2〉) 〈x0,x1〉 +; quadruple … OR MODE_FR1_and_W (Byte 〈x1,x3〉) 〈x0,x1〉 +; quadruple … OR MODE_W_and_FR0 (Byte 〈x1,x0〉) 〈x0,x1〉 +; quadruple … OR MODE_W_and_FR1 (Byte 〈x1,x1〉) 〈x0,x1〉 +; quadruple … OR MODE_IMM8 (Byte 〈x7,xD〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_24 ≝ +[ + quadruple … PAGE (MODE_IMM3 o0) (Word 〈〈x0,x0〉:〈x1,x0〉〉) 〈x0,x1〉 +; quadruple … PAGE (MODE_IMM3 o1) (Word 〈〈x0,x0〉:〈x1,x1〉〉) 〈x0,x1〉 +; quadruple … PAGE (MODE_IMM3 o2) (Word 〈〈x0,x0〉:〈x1,x2〉〉) 〈x0,x1〉 +; quadruple … PAGE (MODE_IMM3 o3) (Word 〈〈x0,x0〉:〈x1,x3〉〉) 〈x0,x1〉 +; quadruple … PAGE (MODE_IMM3 o4) (Word 〈〈x0,x0〉:〈x1,x4〉〉) 〈x0,x1〉 +; quadruple … PAGE (MODE_IMM3 o5) (Word 〈〈x0,x0〉:〈x1,x5〉〉) 〈x0,x1〉 +; quadruple … PAGE (MODE_IMM3 o6) (Word 〈〈x0,x0〉:〈x1,x6〉〉) 〈x0,x1〉 +; quadruple … PAGE (MODE_IMM3 o7) (Word 〈〈x0,x0〉:〈x1,x7〉〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_25 ≝ +[ + quadruple … POP MODE_FR0_and_W (Byte 〈x4,x6〉) 〈x0,x1〉 +; quadruple … POP MODE_FR1_and_W (Byte 〈x4,x7〉) 〈x0,x1〉 +; quadruple … PUSH MODE_W_and_FR0 (Byte 〈x4,x4〉) 〈x0,x1〉 +; quadruple … PUSH MODE_W_and_FR1 (Byte 〈x4,x5〉) 〈x0,x1〉 +; quadruple … PUSH MODE_IMM8 (Byte 〈x7,x4〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_26 ≝ +[ + quadruple … RETI (MODE_IMM3 o0) (Word 〈〈x0,x0〉:〈x0,x8〉〉) 〈x0,x3〉 +; quadruple … RETI (MODE_IMM3 o1) (Word 〈〈x0,x0〉:〈x0,x9〉〉) 〈x0,x3〉 +; quadruple … RETI (MODE_IMM3 o2) (Word 〈〈x0,x0〉:〈x0,xA〉〉) 〈x0,x3〉 +; quadruple … RETI (MODE_IMM3 o3) (Word 〈〈x0,x0〉:〈x0,xB〉〉) 〈x0,x3〉 +; quadruple … RETI (MODE_IMM3 o4) (Word 〈〈x0,x0〉:〈x0,xC〉〉) 〈x0,x3〉 +; quadruple … RETI (MODE_IMM3 o5) (Word 〈〈x0,x0〉:〈x0,xD〉〉) 〈x0,x3〉 +; quadruple … RETI (MODE_IMM3 o6) (Word 〈〈x0,x0〉:〈x0,xE〉〉) 〈x0,x3〉 +; quadruple … RETI (MODE_IMM3 o7) (Word 〈〈x0,x0〉:〈x0,xF〉〉) 〈x0,x3〉 +]. + +ndefinition opcode_table_IP2022_27 ≝ +[ quadruple … RETW MODE_IMM8 (Byte 〈x7,x8〉) 〈x0,x3〉 ]. + +ndefinition opcode_table_IP2022_28 ≝ +[ + quadruple … RL MODE_FR0_and_W (Byte 〈x3,x6〉) 〈x0,x1〉 +; quadruple … RL MODE_FR1_and_W (Byte 〈x3,x7〉) 〈x0,x1〉 +; quadruple … RL MODE_W_and_FR0 (Byte 〈x3,x4〉) 〈x0,x1〉 +; quadruple … RL MODE_W_and_FR1 (Byte 〈x3,x5〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_29 ≝ +[ + quadruple … RR MODE_FR0_and_W (Byte 〈x3,x2〉) 〈x0,x1〉 +; quadruple … RR MODE_FR1_and_W (Byte 〈x3,x3〉) 〈x0,x1〉 +; quadruple … RR MODE_W_and_FR0 (Byte 〈x3,x0〉) 〈x0,x1〉 +; quadruple … RR MODE_W_and_FR1 (Byte 〈x3,x1〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_30 ≝ +[ + quadruple … SB (MODE_FR0n o0) (Byte 〈xB,x0〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR1n o0) (Byte 〈xB,x1〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR0n o1) (Byte 〈xB,x2〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR1n o1) (Byte 〈xB,x3〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR0n o2) (Byte 〈xB,x4〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR1n o2) (Byte 〈xB,x5〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR0n o3) (Byte 〈xB,x6〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR1n o3) (Byte 〈xB,x7〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR0n o4) (Byte 〈xB,x8〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR1n o4) (Byte 〈xB,x9〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR0n o5) (Byte 〈xB,xA〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR1n o5) (Byte 〈xB,xB〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR0n o6) (Byte 〈xB,xC〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR1n o6) (Byte 〈xB,xD〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR0n o7) (Byte 〈xB,xE〉) 〈x0,x1〉 +; quadruple … SB (MODE_FR1n o7) (Byte 〈xB,xF〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_31 ≝ +[ + quadruple … SETB (MODE_FR0n o0) (Byte 〈x9,x0〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR1n o0) (Byte 〈x9,x1〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR0n o1) (Byte 〈x9,x2〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR1n o1) (Byte 〈x9,x3〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR0n o2) (Byte 〈x9,x4〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR1n o2) (Byte 〈x9,x5〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR0n o3) (Byte 〈x9,x6〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR1n o3) (Byte 〈x9,x7〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR0n o4) (Byte 〈x9,x8〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR1n o4) (Byte 〈x9,x9〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR0n o5) (Byte 〈x9,xA〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR1n o5) (Byte 〈x9,xB〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR0n o6) (Byte 〈x9,xC〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR1n o6) (Byte 〈x9,xD〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR0n o7) (Byte 〈x9,xE〉) 〈x0,x1〉 +; quadruple … SETB (MODE_FR1n o7) (Byte 〈x9,xF〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_32 ≝ +[ + quadruple … SNB (MODE_FR0n o0) (Byte 〈xA,x0〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR1n o0) (Byte 〈xA,x1〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR0n o1) (Byte 〈xA,x2〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR1n o1) (Byte 〈xA,x3〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR0n o2) (Byte 〈xA,x4〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR1n o2) (Byte 〈xA,x5〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR0n o3) (Byte 〈xA,x6〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR1n o3) (Byte 〈xA,x7〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR0n o4) (Byte 〈xA,x8〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR1n o4) (Byte 〈xA,x9〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR0n o5) (Byte 〈xA,xA〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR1n o5) (Byte 〈xA,xB〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR0n o6) (Byte 〈xA,xC〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR1n o6) (Byte 〈xA,xD〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR0n o7) (Byte 〈xA,xE〉) 〈x0,x1〉 +; quadruple … SNB (MODE_FR1n o7) (Byte 〈xA,xF〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_33 ≝ +[ quadruple … SPEED MODE_IMM8 (Byte 〈x0,x1〉) 〈x0,x1〉 ]. + +ndefinition opcode_table_IP2022_34 ≝ +[ + quadruple … SUB MODE_FR0_and_W (Byte 〈x0,xA〉) 〈x0,x1〉 +; quadruple … SUB MODE_FR1_and_W (Byte 〈x0,xB〉) 〈x0,x1〉 +; quadruple … SUB MODE_W_and_FR0 (Byte 〈x0,x8〉) 〈x0,x1〉 +; quadruple … SUB MODE_W_and_FR1 (Byte 〈x0,x9〉) 〈x0,x1〉 +; quadruple … SUB MODE_IMM8 (Byte 〈x7,xA〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_35 ≝ +[ + quadruple … SUBC MODE_FR0_and_W (Byte 〈x4,xA〉) 〈x0,x1〉 +; quadruple … SUBC MODE_FR1_and_W (Byte 〈x4,xB〉) 〈x0,x1〉 +; quadruple … SUBC MODE_W_and_FR0 (Byte 〈x4,x8〉) 〈x0,x1〉 +; quadruple … SUBC MODE_W_and_FR1 (Byte 〈x4,x9〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_36 ≝ +[ + quadruple … SWAP MODE_FR0_and_W (Byte 〈x3,xA〉) 〈x0,x1〉 +; quadruple … SWAP MODE_FR1_and_W (Byte 〈x3,xB〉) 〈x0,x1〉 +; quadruple … SWAP MODE_W_and_FR0 (Byte 〈x3,x8〉) 〈x0,x1〉 +; quadruple … SWAP MODE_W_and_FR1 (Byte 〈x3,x9〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_37 ≝ +[ + quadruple … TEST MODE_FR0_and_W (Byte 〈x2,x2〉) 〈x0,x1〉 +; quadruple … TEST MODE_FR1_and_W (Byte 〈x2,x3〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022_38 ≝ +[ + quadruple … XOR MODE_FR0_and_W (Byte 〈x1,xA〉) 〈x0,x1〉 +; quadruple … XOR MODE_FR1_and_W (Byte 〈x1,xB〉) 〈x0,x1〉 +; quadruple … XOR MODE_W_and_FR0 (Byte 〈x1,x8〉) 〈x0,x1〉 +; quadruple … XOR MODE_W_and_FR1 (Byte 〈x1,x9〉) 〈x0,x1〉 +; quadruple … XOR MODE_IMM8 (Byte 〈x7,xF〉) 〈x0,x1〉 +]. + +ndefinition opcode_table_IP2022 ≝ + opcode_table_IP2022_1 @ opcode_table_IP2022_2 @ opcode_table_IP2022_3 @ opcode_table_IP2022_4 @ + opcode_table_IP2022_5 @ opcode_table_IP2022_6 @ opcode_table_IP2022_7 @ opcode_table_IP2022_8 @ + opcode_table_IP2022_9 @ opcode_table_IP2022_10 @ opcode_table_IP2022_11 @ opcode_table_IP2022_12 @ + opcode_table_IP2022_13 @ opcode_table_IP2022_14 @ opcode_table_IP2022_15 @ opcode_table_IP2022_16 @ + opcode_table_IP2022_17 @ opcode_table_IP2022_18 @ opcode_table_IP2022_19 @ opcode_table_IP2022_20 @ + opcode_table_IP2022_21 @ opcode_table_IP2022_22 @ opcode_table_IP2022_23 @ opcode_table_IP2022_24 @ + opcode_table_IP2022_25 @ opcode_table_IP2022_26 @ opcode_table_IP2022_27 @ opcode_table_IP2022_28 @ + opcode_table_IP2022_29 @ opcode_table_IP2022_30 @ opcode_table_IP2022_31 @ opcode_table_IP2022_32 @ + opcode_table_IP2022_33 @ opcode_table_IP2022_34 @ opcode_table_IP2022_35 @ opcode_table_IP2022_36 @ + opcode_table_IP2022_37 @ opcode_table_IP2022_38. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table_tests.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table_tests.ma new file mode 100755 index 000000000..c753b181b --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table_tests.ma @@ -0,0 +1,105 @@ +(**************************************************************************) +(* ___ *) +(* ||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/opcodes/opcode.ma". +include "emulator/opcodes/IP2022_table.ma". + +(* ******************* *) +(* TABELLA DELL'IP2022 *) +(* ******************* *) + +(* IP2022: opcode non implementati come da manuale (byte) *) +ndefinition IP2022_not_impl_byte ≝ + [〈x0,x0〉;〈x5,x2〉;〈x5,x3〉;〈x5,x6〉;〈x5,x7〉;〈x6,x0〉;〈x6,x1〉;〈x6,x2〉 + ;〈x6,x3〉;〈x6,x4〉;〈x6,x5〉;〈x6,x6〉;〈x6,x7〉;〈x6,x8〉;〈x6,x9〉;〈x6,xA〉 + ;〈x6,xB〉;〈x6,xC〉;〈x6,xD〉;〈x6,xE〉;〈x6,xF〉;〈x7,x5〉 ]. + +(* test bytecode non implementati *) +nlemma ok_byte_table_IP2022 : forall_b8 (λb. + (test_not_impl_byte b IP2022_not_impl_byte ⊙ eq_w16 (get_byte_count IP2022 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗ + (⊖ (test_not_impl_byte b IP2022_not_impl_byte) ⊙ eq_w16 (get_byte_count IP2022 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022) 〈〈x0,x0〉:〈x0,x0〉〉)) + = true. + napply refl_eq. +nqed. + +(* IP2022: opcode non implementati come da manuale (0x00+byte) *) +ndefinition IP2022_not_impl_word ≝ + [〈x1,xE〉;〈x1,xF〉 + ;〈x2,x0〉;〈x2,x1〉;〈x2,x2〉;〈x2,x3〉;〈x2,x4〉;〈x2,x5〉;〈x2,x6〉;〈x2,x7〉 + ;〈x2,x8〉;〈x2,x9〉;〈x2,xA〉;〈x2,xB〉;〈x2,xC〉;〈x2,xD〉;〈x2,xE〉;〈x2,xF〉 + ;〈x3,x0〉;〈x3,x1〉;〈x3,x2〉;〈x3,x3〉;〈x3,x4〉;〈x3,x5〉;〈x3,x6〉;〈x3,x7〉 + ;〈x3,x8〉;〈x3,x9〉;〈x3,xA〉;〈x3,xB〉;〈x3,xC〉;〈x3,xD〉;〈x3,xE〉;〈x3,xF〉 + ;〈x4,x0〉;〈x4,x1〉;〈x4,x2〉;〈x4,x3〉;〈x4,x4〉;〈x4,x5〉;〈x4,x6〉;〈x4,x7〉 + ;〈x4,x8〉;〈x4,x9〉;〈x4,xA〉;〈x4,xB〉;〈x4,xC〉;〈x4,xD〉;〈x4,xE〉;〈x4,xF〉 + ;〈x5,x0〉;〈x5,x1〉;〈x5,x2〉;〈x5,x3〉;〈x5,x4〉;〈x5,x5〉;〈x5,x6〉;〈x5,x7〉 + ;〈x5,x8〉;〈x5,x9〉;〈x5,xA〉;〈x5,xB〉;〈x5,xC〉;〈x5,xD〉;〈x5,xE〉;〈x5,xF〉 + ;〈x6,x0〉;〈x6,x1〉;〈x6,x2〉;〈x6,x3〉;〈x6,x4〉;〈x6,x5〉;〈x6,x6〉;〈x6,x7〉 + ;〈x6,x8〉;〈x6,x9〉;〈x6,xA〉;〈x6,xB〉;〈x6,xC〉;〈x6,xD〉;〈x6,xE〉;〈x6,xF〉 + ;〈x7,x0〉;〈x7,x1〉;〈x7,x2〉;〈x7,x3〉;〈x7,x4〉;〈x7,x5〉;〈x7,x6〉;〈x7,x7〉 + ;〈x7,x8〉;〈x7,x9〉;〈x7,xA〉;〈x7,xB〉;〈x7,xC〉;〈x7,xD〉;〈x7,xE〉;〈x7,xF〉 + ;〈x8,x0〉;〈x8,x1〉;〈x8,x2〉;〈x8,x3〉;〈x8,x4〉;〈x8,x5〉;〈x8,x6〉;〈x8,x7〉 + ;〈x8,x8〉;〈x8,x9〉;〈x8,xA〉;〈x8,xB〉;〈x8,xC〉;〈x8,xD〉;〈x8,xE〉;〈x8,xF〉 + ;〈x9,x0〉;〈x9,x1〉;〈x9,x2〉;〈x9,x3〉;〈x9,x4〉;〈x9,x5〉;〈x9,x6〉;〈x9,x7〉 + ;〈x9,x8〉;〈x9,x9〉;〈x9,xA〉;〈x9,xB〉;〈x9,xC〉;〈x9,xD〉;〈x9,xE〉;〈x9,xF〉 + ;〈xA,x0〉;〈xA,x1〉;〈xA,x2〉;〈xA,x3〉;〈xA,x4〉;〈xA,x5〉;〈xA,x6〉;〈xA,x7〉 + ;〈xA,x8〉;〈xA,x9〉;〈xA,xA〉;〈xA,xB〉;〈xA,xC〉;〈xA,xD〉;〈xA,xE〉;〈xA,xF〉 + ;〈xB,x0〉;〈xB,x1〉;〈xB,x2〉;〈xB,x3〉;〈xB,x4〉;〈xB,x5〉;〈xB,x6〉;〈xB,x7〉 + ;〈xB,x8〉;〈xB,x9〉;〈xB,xA〉;〈xB,xB〉;〈xB,xC〉;〈xB,xD〉;〈xB,xE〉;〈xB,xF〉 + ;〈xC,x0〉;〈xC,x1〉;〈xC,x2〉;〈xC,x3〉;〈xC,x4〉;〈xC,x5〉;〈xC,x6〉;〈xC,x7〉 + ;〈xC,x8〉;〈xC,x9〉;〈xC,xA〉;〈xC,xB〉;〈xC,xC〉;〈xC,xD〉;〈xC,xE〉;〈xC,xF〉 + ;〈xD,x0〉;〈xD,x1〉;〈xD,x2〉;〈xD,x3〉;〈xD,x4〉;〈xD,x5〉;〈xD,x6〉;〈xD,x7〉 + ;〈xD,x8〉;〈xD,x9〉;〈xD,xA〉;〈xD,xB〉;〈xD,xC〉;〈xD,xD〉;〈xD,xE〉;〈xD,xF〉 + ;〈xE,x0〉;〈xE,x1〉;〈xE,x2〉;〈xE,x3〉;〈xE,x4〉;〈xE,x5〉;〈xE,x6〉;〈xE,x7〉 + ;〈xE,x8〉;〈xE,x9〉;〈xE,xA〉;〈xE,xB〉;〈xE,xC〉;〈xE,xD〉;〈xE,xE〉;〈xE,xF〉 + ;〈xF,x0〉;〈xF,x1〉;〈xF,x2〉;〈xF,x3〉;〈xF,x4〉;〈xF,x5〉;〈xF,x6〉;〈xF,x7〉 + ;〈xF,x8〉;〈xF,x9〉;〈xF,xA〉;〈xF,xB〉;〈xF,xC〉;〈xF,xD〉;〈xF,xE〉;〈xF,xF〉 + ]. + +(* test bytecode non implementati *) +nlemma ok_word_table_IP2022 : forall_b8 (λb. + (test_not_impl_byte b IP2022_not_impl_word ⊙ eq_w16 (get_word_count IP2022 〈〈x0,x0〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗ + (⊖ (test_not_impl_byte b IP2022_not_impl_word) ⊙ eq_w16 (get_word_count IP2022 〈〈x0,x0〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022) 〈〈x0,x0〉:〈x0,x0〉〉)) + = true. + napply refl_eq. +nqed. + +(* tutti op implementati *) +nlemma ok_pseudo_table_IP2022 : + forall_op IP2022 (λo. + le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count IP2022 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022)) = true. + napply refl_eq. +nqed. + +(* tutte im implementate *) +nlemma ok_mode_table_IP2022 : + forall_im IP2022 (λi. + le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count IP2022 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022)) = true. + napply refl_eq. +nqed. + +(* nessuna ripetizione di combinazione op + imm *) +nlemma ok_OpIm_table_IP2022 : + forall_im IP2022 (λi. + forall_op IP2022 (λo. + le_w16 (get_OpIm_count IP2022 o i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022) 〈〈x0,x0〉:〈x0,x1〉〉)) = true. + napply refl_eq. +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_table.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_table.ma index da3194b0c..56fa8b5fa 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_table.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_table.ma @@ -30,9 +30,7 @@ include "common/list.ma". (* ***************** *) (* definizione come concatenazione finale di liste per velocizzare il parsing *) -(* ogni riga e' (any_opcode m) (instr_mode) (opcode esadecimale) (#cicli esecuzione) *) -(* NB: l'uso di any_opcode m + concatenazione finale tutte liste - impedisce di introdurre opcode disomogenei (per mcu) *) +(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *) ndefinition opcode_table_RS08_1 ≝ [ diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode.ma index a1b696d83..4c3f8c849 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode.ma @@ -27,6 +27,8 @@ include "emulator/opcodes/HC08_instr_mode.ma". include "emulator/opcodes/HCS08_opcode.ma". include "emulator/opcodes/RS08_opcode.ma". include "emulator/opcodes/RS08_instr_mode.ma". +include "emulator/opcodes/IP2022_opcode.ma". +include "emulator/opcodes/IP2022_instr_mode.ma". include "emulator/opcodes/byte_or_word.ma". include "common/list.ma". @@ -36,10 +38,11 @@ include "common/list.ma". (* enumerazione delle ALU *) ninductive mcu_type: Type ≝ - HC05 : mcu_type -| HC08 : mcu_type -| HCS08 : mcu_type -| RS08 : mcu_type. + HC05 : mcu_type +| HC08 : mcu_type +| HCS08 : mcu_type +| RS08 : mcu_type +| IP2022 : mcu_type. ndefinition eq_mcutype ≝ λm1,m2:mcu_type. @@ -48,6 +51,7 @@ ndefinition eq_mcutype ≝ | HC08 ⇒ match m2 with [ HC08 ⇒ true | _ ⇒ false ] | HCS08 ⇒ match m2 with [ HCS08 ⇒ true | _ ⇒ false ] | RS08 ⇒ match m2 with [ RS08 ⇒ true | _ ⇒ false ] + | IP2022 ⇒ match m2 with [ IP2022 ⇒ true | _ ⇒ false ] ]. ndefinition aux_op_type ≝ @@ -56,6 +60,7 @@ ndefinition aux_op_type ≝ | HC08 ⇒ HC08_opcode | HCS08 ⇒ HCS08_opcode | RS08 ⇒ RS08_opcode + | IP2022 ⇒ IP2022_opcode ]. ndefinition aux_im_type ≝ @@ -64,6 +69,7 @@ ndefinition aux_im_type ≝ | HC08 ⇒ HC08_instr_mode | HCS08 ⇒ HC08_instr_mode | RS08 ⇒ RS08_instr_mode + | IP2022 ⇒ IP2022_instr_mode ]. ndefinition eq_op ≝ @@ -75,6 +81,7 @@ ndefinition eq_op ≝ | HC08 ⇒ eq_HC08_op | HCS08 ⇒ eq_HCS08_op | RS08 ⇒ eq_RS08_op + | IP2022 ⇒ eq_IP2022_op ]. ndefinition eq_im ≝ @@ -86,6 +93,7 @@ ndefinition eq_im ≝ | HC08 ⇒ eq_HC08_im | HCS08 ⇒ eq_HC08_im | RS08 ⇒ eq_RS08_im + | IP2022 ⇒ eq_IP2022_im ]. ndefinition forall_op ≝ @@ -97,6 +105,7 @@ ndefinition forall_op ≝ | HC08 ⇒ forall_HC08_op | HCS08 ⇒ forall_HCS08_op | RS08 ⇒ forall_RS08_op + | IP2022 ⇒ forall_IP2022_op ]. ndefinition forall_im ≝ @@ -108,6 +117,7 @@ ndefinition forall_im ≝ | HC08 ⇒ forall_HC08_im | HCS08 ⇒ forall_HC08_im | RS08 ⇒ forall_RS08_im + | IP2022 ⇒ forall_IP2022_im ]. (* ********************************************* *) @@ -129,15 +139,15 @@ nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_typ ] ]. -(* su tutta la lista quante volte compare la word (0x9E+byte) *) -nlet rec get_word_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝ +(* su tutta la lista quante volte compare la word *) +nlet rec get_word_count (m:mcu_type) (w:word16) (c:word16) (l:list (aux_table_type m)) on l ≝ match l with [ nil ⇒ c | cons hd tl ⇒ match thd4T … hd with - [ Byte _ ⇒ get_word_count m b c tl - | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with - [ true ⇒ get_word_count m b (succ_w16 c) tl - | false ⇒ get_word_count m b c tl + [ Byte _ ⇒ get_word_count m w c tl + | Word w' ⇒ match eq_w16 w w' with + [ true ⇒ get_word_count m w (succ_w16 c) tl + | false ⇒ get_word_count m w c tl ] ] ]. @@ -172,26 +182,6 @@ nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝ ] ]. -(* o e' non implementato? *) -nlet rec test_not_impl_pseudo (m:mcu_type) (o:aux_op_type m) (l:list (aux_op_type m)) on l ≝ - match l with - [ nil ⇒ false - | cons hd tl ⇒ match eq_op m o hd with - [ true ⇒ true - | false ⇒ test_not_impl_pseudo m o tl - ] - ]. - -(* i e' non implementato? *) -nlet rec test_not_impl_mode (m:mcu_type) (i:aux_im_type m) (l:list (aux_im_type m)) on l ≝ - match l with - [ nil ⇒ false - | cons hd tl ⇒ match eq_im m i hd with - [ true ⇒ true - | false ⇒ test_not_impl_mode m i tl - ] - ]. - (* su tutta la lista quante volte compare la coppia opcode,instr_mode *) nlet rec get_OpIm_count (m:mcu_type) (o:aux_op_type m) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝ match l with diff --git a/helm/software/matita/contribs/ng_assembly/emulator/translation/IP2022_translation.ma b/helm/software/matita/contribs/ng_assembly/emulator/translation/IP2022_translation.ma new file mode 100755 index 000000000..c3d8efcc6 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/translation/IP2022_translation.ma @@ -0,0 +1,58 @@ +(**************************************************************************) +(* ___ *) +(* ||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/translation/translation_base.ma". + +(* ******************************************************* *) +(* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *) +(* ******************************************************* *) + +(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *) +ninductive IP2022_MA_check : IP2022_instr_mode → Type ≝ + maINH : IP2022_MA_check MODE_INH +| maIMM3 : ∀n.IP2022_MA_check (MODE_IMM3 n) +| maIMM8 : byte8 → IP2022_MA_check MODE_IMM8 +| maIMM13 : ∀t.byte8 → IP2022_MA_check (MODE_IMM13 t) +| maFR0_and_W : byte8 → IP2022_MA_check MODE_FR0_and_W +| maFR1_and_W : byte8 → IP2022_MA_check MODE_FR1_and_W +| maW_and_FR0 : byte8 → IP2022_MA_check MODE_W_and_FR0 +| maW_and_FR1 : byte8 → IP2022_MA_check MODE_W_and_FR1 +| maFR0n : ∀n.byte8 → IP2022_MA_check (MODE_FR0n n) +| maFR1n : ∀n.byte8 → IP2022_MA_check (MODE_FR1n n) +. + +(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param: + MA_check i → list (t_byte8 m) *) +ndefinition IP2022_args_picker ≝ +λi:aux_im_type IP2022.λargs:IP2022_MA_check i. + match args with + [ maINH ⇒ nil ? + | maIMM3 _ ⇒ nil ? + | maIMM8 b ⇒ [ TByte IP2022 b ] + | maIMM13 _ b ⇒ [ TByte IP2022 b ] + | maFR0_and_W b ⇒ [ TByte IP2022 b ] + | maFR1_and_W b ⇒ [ TByte IP2022 b ] + | maW_and_FR0 b ⇒ [ TByte IP2022 b ] + | maW_and_FR1 b ⇒ [ TByte IP2022 b ] + | maFR0n _ b ⇒ [ TByte IP2022 b ] + | maFR1n _ b ⇒ [ TByte IP2022 b ] + ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma b/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma index 64bda08ec..4cd470862 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma @@ -24,6 +24,7 @@ include "emulator/translation/HC05_translation.ma". include "emulator/translation/HC08_translation.ma". include "emulator/translation/HCS08_translation.ma". include "emulator/translation/RS08_translation.ma". +include "emulator/translation/IP2022_translation.ma". (* ******************************************************* *) (* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *) @@ -39,6 +40,7 @@ ndefinition MA_check ≝ | HC08 ⇒ HC08_MA_check | HCS08 ⇒ HCS08_MA_check | RS08 ⇒ RS08_MA_check + | IP2022 ⇒ IP2022_MA_check ]. (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param: @@ -52,6 +54,7 @@ ndefinition args_picker ≝ | HC08 ⇒ HC08_args_picker | HCS08 ⇒ HCS08_args_picker | RS08 ⇒ RS08_args_picker + | IP2022 ⇒ IP2022_args_picker ]. (* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *) @@ -95,37 +98,10 @@ ndefinition compile ≝ ]. (* detipatore del compilato: (t_byte8 m) → byte8 *) -nlet rec source_to_byte8_HC05_aux (p1:list (t_byte8 HC05)) (p2:list byte8) ≝ +nlet rec source_to_byte8_aux (m:mcu_type) (p2:list byte8) (p1:list (t_byte8 m)) on p1 ≝ match p1 with [ nil ⇒ p2 - | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC05_aux tl (p2@[b]) ] + | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_aux m (p2@[b]) tl ] ]. -nlet rec source_to_byte8_HC08_aux (p1:list (t_byte8 HC08)) (p2:list byte8) ≝ - match p1 with - [ nil ⇒ p2 - | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC08_aux tl (p2@[b]) ] - ]. - -nlet rec source_to_byte8_HCS08_aux (p1:list (t_byte8 HCS08)) (p2:list byte8) ≝ - match p1 with - [ nil ⇒ p2 - | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HCS08_aux tl (p2@[b]) ] - ]. - -nlet rec source_to_byte8_RS08_aux (p1:list (t_byte8 RS08)) (p2:list byte8) ≝ - match p1 with - [ nil ⇒ p2 - | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_RS08_aux tl (p2@[b]) ] - ]. - -ndefinition source_to_byte8 ≝ -λm:mcu_type. - match m - return λm:mcu_type.list (t_byte8 m) → list byte8 - with - [ HC05 ⇒ λl:list (t_byte8 HC05).source_to_byte8_HC05_aux l [] - | HC08 ⇒ λl:list (t_byte8 HC08).source_to_byte8_HC08_aux l [] - | HCS08 ⇒ λl:list (t_byte8 HCS08).source_to_byte8_HCS08_aux l [] - | RS08 ⇒ λl:list (t_byte8 RS08).source_to_byte8_RS08_aux l [] - ]. +ndefinition source_to_byte8 ≝ λm:mcu_type.source_to_byte8_aux m []. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/translation/translation_base.ma b/helm/software/matita/contribs/ng_assembly/emulator/translation/translation_base.ma index 2df75d816..8548eb583 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/translation/translation_base.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/translation/translation_base.ma @@ -26,6 +26,7 @@ include "emulator/opcodes/HC05_table.ma". include "emulator/opcodes/HC08_table.ma". include "emulator/opcodes/HCS08_table.ma". include "emulator/opcodes/RS08_table.ma". +include "emulator/opcodes/IP2022_table.ma". (* ***************************** *) (* TRADUZIONE ESADECIMALE → INFO *) @@ -41,6 +42,7 @@ ndefinition opcode_table ≝ | HC08 ⇒ opcode_table_HC08 | HCS08 ⇒ opcode_table_HCS08 | RS08 ⇒ opcode_table_RS08 + | IP2022 ⇒ opcode_table_IP2022 ]. (* traduzione mcu+esadecimale → info *) -- 2.39.2