From: Cosimo Oliboni Date: Sat, 30 Jan 2010 08:49:34 +0000 (+0000) Subject: freescale porting X-Git-Tag: make_still_working~3084 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eb4144a401147a44a9620169eb6dafeb8f5a2c17;p=helm.git freescale porting --- diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index 96a1dd500..ef408e293 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -1,7 +1,8 @@ num/word24_lemmas.ma num/byte8_lemmas.ma num/word24.ma +emulator/read_write/FREESCALE_load_write_base.ma emulator/read_write/load_write_base.ma emulator/status/status_getter.ma emulator/model/HCS08_model.ma emulator/status/status.ma common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma -emulator/opcodes/HC05_table_tests.ma emulator/opcodes/HC05_table.ma emulator/opcodes/opcode.ma +emulator/opcodes/HC05_table_tests.ma emulator/opcodes/HC05_table.ma emulator/opcodes/pseudo.ma num/bool.ma common/theory.ma compiler/preast_tree.ma common/string.ma compiler/ast_type.ma num/word32.ma emulator/status/RS08_status_lemmas.ma emulator/status/RS08_status.ma num/word16_lemmas.ma @@ -9,35 +10,37 @@ 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 +emulator/opcodes/IP2022_pseudo.ma num/bool.ma compiler/ast_type_lemmas.ma common/list_utility_lemmas.ma compiler/ast_type.ma emulator/memory/memory_struct_lemmas.ma emulator/memory/memory_struct.ma num/bool_lemmas.ma 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 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 +emulator/status/status_lemmas.ma common/option_lemmas.ma common/prod_lemmas.ma emulator/opcodes/pseudo_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/pseudo.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 -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 +emulator/opcodes/HC08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma -emulator/opcodes/RS08_opcode_lemmas.ma emulator/opcodes/RS08_opcode.ma num/bool_lemmas.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 +emulator/opcodes/HC05_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma emulator/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 -emulator/opcodes/HCS08_opcode_lemmas.ma emulator/opcodes/HCS08_opcode.ma num/bool_lemmas.ma +emulator/read_write/RS08_load_write.ma emulator/read_write/FREESCALE_load_write_base.ma +emulator/opcodes/Freescale_pseudo.ma num/bool.ma +emulator/read_write/HC08_load_write.ma emulator/read_write/FREESCALE_load_write_base.ma num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma -emulator/opcodes/HC08_opcode_lemmas.ma emulator/opcodes/HC08_opcode.ma num/bool_lemmas.ma -emulator/opcodes/RS08_table_tests.ma emulator/opcodes/RS08_table.ma emulator/opcodes/opcode.ma +emulator/opcodes/RS08_table_tests.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma +emulator/opcodes/Freescale_instr_mode_lemmas.ma emulator/opcodes/Freescale_instr_mode.ma num/bool_lemmas.ma num/oct_lemmas.ma 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/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/pseudo.ma +emulator/opcodes/IP2022_table.ma common/list.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.ma emulator/status/HC05_status.ma num/word16.ma +emulator/opcodes/Freescale_pseudo_lemmas.ma emulator/opcodes/Freescale_pseudo.ma num/bool_lemmas.ma emulator/memory/memory_bits.ma emulator/memory/memory_trees.ma common/theory.ma common/string.ma common/ascii.ma common/list_utility.ma @@ -46,64 +49,57 @@ emulator/opcodes/byte_or_word.ma num/word16.ma compiler/ast_type.ma common/list_utility.ma num/word16.ma num/byte8.ma common/prod.ma num/bool.ma -emulator/translation/HC08_translation.ma emulator/translation/translation_base.ma emulator/opcodes/IP2022_instr_mode.ma num/word16.ma -emulator/opcodes/HCS08_opcode.ma num/bool.ma -emulator/opcodes/HC08_opcode.ma num/bool.ma +emulator/translation/HC08_translation.ma emulator/translation/translation_base.ma num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma emulator/status/HC05_status_lemmas.ma emulator/status/HC05_status.ma num/word16_lemmas.ma emulator/status/status_getter.ma emulator/status/status_setter.ma -emulator/opcodes/opcode_lemmas.ma emulator/opcodes/HC05_instr_mode_lemmas.ma emulator/opcodes/HC05_opcode_lemmas.ma emulator/opcodes/HC08_instr_mode_lemmas.ma emulator/opcodes/HC08_opcode_lemmas.ma emulator/opcodes/HCS08_opcode_lemmas.ma emulator/opcodes/IP2022_instr_mode_lemmas.ma emulator/opcodes/IP2022_opcode_lemmas.ma emulator/opcodes/RS08_instr_mode_lemmas.ma emulator/opcodes/RS08_opcode_lemmas.ma emulator/opcodes/opcode.ma num/word24.ma num/byte8.ma num/bool_lemmas.ma num/bool.ma -emulator/opcodes/HC08_instr_mode_lemmas.ma emulator/opcodes/HC08_instr_mode.ma num/bool_lemmas.ma num/oct_lemmas.ma emulator/model/HC08_model.ma emulator/status/status.ma emulator/memory/memory_abs.ma emulator/memory/memory_bits.ma emulator/memory/memory_func.ma emulator/memory/memory_trees.ma -emulator/opcodes/RS08_opcode.ma num/bool.ma num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma -emulator/translation/RS08_translation.ma emulator/translation/translation_base.ma emulator/memory/memory_struct.ma num/byte8.ma num/oct.ma -emulator/opcodes/HC05_instr_mode_lemmas.ma emulator/opcodes/HC05_instr_mode.ma num/bool_lemmas.ma num/oct_lemmas.ma +emulator/translation/RS08_translation.ma emulator/translation/translation_base.ma emulator/model/HC05_model.ma emulator/status/status.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 +emulator/read_write/load_write_base.ma emulator/read_write/read_write.ma emulator/model/IP2022_model.ma emulator/status/status.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 +emulator/opcodes/HCS08_table_tests.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/pseudo.ma +emulator/opcodes/IP2022_table_tests.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/pseudo.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 +emulator/read_write/read_write.ma emulator/read_write/IP2022_read_write.ma emulator/read_write/RS08_read_write.ma +emulator/opcodes/Freescale_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 -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_lemmas.ma common/option.ma num/bool_lemmas.ma common/option.ma num/bool.ma +emulator/opcodes/pseudo_lemmas.ma emulator/opcodes/Freescale_instr_mode_lemmas.ma emulator/opcodes/Freescale_pseudo_lemmas.ma emulator/opcodes/IP2022_instr_mode_lemmas.ma emulator/opcodes/IP2022_pseudo_lemmas.ma emulator/opcodes/pseudo.ma num/byte8_lemmas.ma num/byte8.ma num/comp_num_lemmas.ma num/exadecim_lemmas.ma +emulator/opcodes/RS08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma emulator/model/RS08_model.ma emulator/status/status.ma -emulator/opcodes/IP2022_opcode_lemmas.ma emulator/opcodes/IP2022_opcode.ma num/bool_lemmas.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 num/comp_num.ma num/exadecim.ma common/sigma.ma common/theory.ma common/list_lemmas.ma common/list.ma emulator/status/HC08_status_lemmas.ma emulator/status/HC08_status.ma num/word16_lemmas.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/opcodes/HCS08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.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 +emulator/read_write/HC05_load_write.ma emulator/read_write/FREESCALE_load_write_base.ma +emulator/opcodes/pseudo.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.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 +emulator/read_write/fetch.ma emulator/status/status_getter.ma emulator/translation/translation_base.ma emulator/opcodes/IP2022_instr_mode_lemmas.ma emulator/opcodes/IP2022_instr_mode.ma num/bitrigesim_lemmas.ma num/bool_lemmas.ma num/oct_lemmas.ma num/oct.ma num/bool.ma common/list.ma common/theory.ma -emulator/opcodes/RS08_instr_mode_lemmas.ma emulator/opcodes/RS08_instr_mode.ma num/bitrigesim_lemmas.ma num/bool_lemmas.ma num/exadecim_lemmas.ma num/oct_lemmas.ma -emulator/opcodes/HC08_table_tests.ma emulator/opcodes/HC08_table.ma emulator/opcodes/opcode.ma -emulator/opcodes/HC05_opcode.ma num/bool.ma +emulator/opcodes/HC08_table_tests.ma emulator/opcodes/HC08_table.ma emulator/opcodes/pseudo.ma +emulator/opcodes/IP2022_pseudo_lemmas.ma emulator/opcodes/IP2022_pseudo.ma num/bool_lemmas.ma diff --git a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_func.ma b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_func.ma index 9f75b5497..d823d2e8d 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_func.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_func.ma @@ -32,7 +32,7 @@ include "common/list.ma". (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *) ndefinition mf_check_update_ranged ≝ λf:word32 → memory_type.λaddr:word32.λrange:word16.λv. - λx.match inrange_w32 x addr (plus_w32_d_d addr 〈〈〈x0,x0〉:〈x0,x0〉〉.range〉) with + λx.match inrange_w32 x addr (plus_w32_d_d addr (ext_word32 range)) with [ true ⇒ v | false ⇒ f x ]. @@ -74,6 +74,6 @@ nlet rec mf_load_from_source_at (old_mem:word32 → byte8) (src:list byte8) (add (* la locazione corrisponde al punto corrente di source *) [ true ⇒ hd (* la locazione e' piu' avanti? ricorsione *) - | false ⇒ (mf_load_from_source_at old_mem tl (plus_w32_d_d addr 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x1〉〉〉)) x + | false ⇒ (mf_load_from_source_at old_mem tl (succ_w32 addr)) x ] ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_instr_mode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_instr_mode.ma new file mode 100755 index 000000000..9c0513ded --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_instr_mode.ma @@ -0,0 +1,187 @@ +(**************************************************************************) +(* ___ *) +(* ||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 Freescale_instr_mode: Type ≝ + (* INHERENT = nessun operando *) + MODE_INH : Freescale_instr_mode + (* INHERENT = nessun operando (A implicito) *) +| MODE_INHA : Freescale_instr_mode + (* INHERENT = nessun operando (X implicito) *) +| MODE_INHX : Freescale_instr_mode + (* INHERENT = nessun operando (H implicito) *) +| MODE_INHH : Freescale_instr_mode + + (* INHERENT_ADDRESS = nessun operando (HX implicito) *) +| MODE_INHX0ADD : Freescale_instr_mode + (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *) +| MODE_INHX1ADD : Freescale_instr_mode + (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *) +| MODE_INHX2ADD : Freescale_instr_mode + + (* IMMEDIATE = operando valore immediato byte = 0xbb *) +| MODE_IMM1 : Freescale_instr_mode + (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *) +| MODE_IMM1EXT : Freescale_instr_mode + (* IMMEDIATE = operando valore immediato word = 0xwwww *) +| MODE_IMM2 : Freescale_instr_mode + (* DIRECT = operando offset byte = [0x00bb] *) +| MODE_DIR1 : Freescale_instr_mode + (* DIRECT = operando offset word = [0xwwww] *) +| MODE_DIR2 : Freescale_instr_mode + (* INDEXED = nessun operando (implicito [X] *) +| MODE_IX0 : Freescale_instr_mode + (* INDEXED = operando offset relativo byte = [X+0x00bb] *) +| MODE_IX1 : Freescale_instr_mode + (* INDEXED = operando offset relativo word = [X+0xwwww] *) +| MODE_IX2 : Freescale_instr_mode + (* INDEXED = operando offset relativo byte = [SP+0x00bb] *) +| MODE_SP1 : Freescale_instr_mode + (* INDEXED = operando offset relativo word = [SP+0xwwww] *) +| MODE_SP2 : Freescale_instr_mode + + (* DIRECT → DIRECT = carica da diretto/scrive su diretto *) +| MODE_DIR1_to_DIR1 : Freescale_instr_mode + (* IMMEDIATE → DIRECT = carica da immediato/scrive su diretto *) +| MODE_IMM1_to_DIR1 : Freescale_instr_mode + (* INDEXED++ → DIRECT = carica da [X]/scrive su diretto/H:X++ *) +| MODE_IX0p_to_DIR1 : Freescale_instr_mode + (* DIRECT → INDEXED++ = carica da diretto/scrive su [X]/H:X++ *) +| MODE_DIR1_to_IX0p : Freescale_instr_mode + + (* INHERENT(A) + IMMEDIATE *) +| MODE_INHA_and_IMM1 : Freescale_instr_mode + (* INHERENT(X) + IMMEDIATE *) +| MODE_INHX_and_IMM1 : Freescale_instr_mode + (* IMMEDIATE + IMMEDIATE *) +| MODE_IMM1_and_IMM1 : Freescale_instr_mode + (* DIRECT + IMMEDIATE *) +| MODE_DIR1_and_IMM1 : Freescale_instr_mode + (* INDEXED + IMMEDIATE *) +| MODE_IX0_and_IMM1 : Freescale_instr_mode + (* INDEXED++ + IMMEDIATE *) +| MODE_IX0p_and_IMM1 : Freescale_instr_mode + (* INDEXED + IMMEDIATE *) +| MODE_IX1_and_IMM1 : Freescale_instr_mode + (* INDEXED++ + IMMEDIATE *) +| MODE_IX1p_and_IMM1 : Freescale_instr_mode + (* INDEXED + IMMEDIATE *) +| MODE_SP1_and_IMM1 : Freescale_instr_mode + + (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *) + (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *) +| MODE_DIRn : oct → Freescale_instr_mode + (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *) + (* + operando valore immediato byte *) + (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *) +| MODE_DIRn_and_IMM1 : oct → Freescale_instr_mode + (* TINY = nessun operando (diretto implicito 4bit = [0x00000000:0000iiii]) *) +| MODE_TNY : exadecim → Freescale_instr_mode + (* SHORT = nessun operando (diretto implicito 5bit = [0x00000000:000iiiii]) *) +| MODE_SRT : bitrigesim → Freescale_instr_mode +. + +ndefinition eq_Freescale_im ≝ +λi1,i2:Freescale_instr_mode. + match i1 with + [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ] + | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ] + | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ true | _ ⇒ false ] + | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ true | _ ⇒ false ] + | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ true | _ ⇒ false ] + | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ true | _ ⇒ false ] + | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ true | _ ⇒ false ] + | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ] + | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ true | _ ⇒ false ] + | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ] + | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ] + | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ true | _ ⇒ false ] + | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ true | _ ⇒ false ] + | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ true | _ ⇒ false ] + | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ true | _ ⇒ false ] + | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ true | _ ⇒ false ] + | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ true | _ ⇒ false ] + | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ true | _ ⇒ false ] + | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ true | _ ⇒ false ] + | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ true | _ ⇒ false ] + | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ true | _ ⇒ false ] + | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ true | _ ⇒ false ] + | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ true | _ ⇒ false ] + | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ true | _ ⇒ false ] + | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ true | _ ⇒ false ] + | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ true | _ ⇒ false ] + | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ true | _ ⇒ false ] + | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ true | _ ⇒ false ] + | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ true | _ ⇒ false ] + | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ true | _ ⇒ false ] + | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ] + | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eq_oct n1 n2 | _ ⇒ false ] + | MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eq_ex e1 e2 | _ ⇒ false ] + | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bit t1 t2 | _ ⇒ false ] + ]. + +ndefinition forall_Freescale_im ≝ λP:Freescale_instr_mode → bool. + P MODE_INH +⊗ P MODE_INHA +⊗ P MODE_INHX +⊗ P MODE_INHH + +⊗ P MODE_INHX0ADD +⊗ P MODE_INHX1ADD +⊗ P MODE_INHX2ADD + +⊗ P MODE_IMM1 +⊗ P MODE_IMM1EXT +⊗ P MODE_IMM2 +⊗ P MODE_DIR1 +⊗ P MODE_DIR2 +⊗ P MODE_IX0 +⊗ P MODE_IX1 +⊗ P MODE_IX2 +⊗ P MODE_SP1 +⊗ P MODE_SP2 + +⊗ P MODE_DIR1_to_DIR1 +⊗ P MODE_IMM1_to_DIR1 +⊗ P MODE_IX0p_to_DIR1 +⊗ P MODE_DIR1_to_IX0p + +⊗ P MODE_INHA_and_IMM1 +⊗ P MODE_INHX_and_IMM1 +⊗ P MODE_IMM1_and_IMM1 +⊗ P MODE_DIR1_and_IMM1 +⊗ P MODE_IX0_and_IMM1 +⊗ P MODE_IX0p_and_IMM1 +⊗ P MODE_IX1_and_IMM1 +⊗ P MODE_IX1p_and_IMM1 +⊗ P MODE_SP1_and_IMM1 + +⊗ forall_oct (λo. P (MODE_DIRn o)) +⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o)) +⊗ forall_ex (λe. P (MODE_TNY e)) +⊗ forall_bit (λt. P (MODE_SRT t)). diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_instr_mode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_instr_mode_lemmas.ma new file mode 100755 index 000000000..4e41de678 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_instr_mode_lemmas.ma @@ -0,0 +1,73 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lemmas.ma". +include "emulator/opcodes/Freescale_instr_mode.ma". +include "num/oct_lemmas.ma". +include "num/bitrigesim_lemmas.ma". +include "num/exadecim_lemmas.ma". + +nlemma eq_to_eqFreescaleim : ∀n1,n2.n1 = n2 → eq_Freescale_im n1 n2 = true. + #n1; #n2; #H; + nrewrite > H; + nelim n2; + ##[ ##31,32: #o; nrewrite > (eq_to_eqoct … (refl_eq …)) + ##| ##33: #e; nrewrite > (eq_to_eqex … (refl_eq …)) + ##| ##34: #t; nrewrite > (eq_to_eqbit … (refl_eq …)) ##] + napply refl_eq. +nqed. + +nlemma neqFreescaleim_to_neq : ∀n1,n2.eq_Freescale_im n1 n2 = false → n1 ≠ n2. + #n1; #n2; #H; + napply (not_to_not (n1 = n2) (eq_Freescale_im n1 n2 = true) …); + ##[ ##1: napply (eq_to_eqFreescaleim n1 n2) + ##| ##2: napply (eqfalse_to_neqtrue … H) + ##] +nqed. + +(* !!! per brevita... *) +naxiom eqFreescaleim_to_eq : ∀c1,c2.eq_Freescale_im c1 c2 = true → c1 = c2. + +nlemma neq_to_neqFreescaleim : ∀n1,n2.n1 ≠ n2 → eq_Freescale_im n1 n2 = false. + #n1; #n2; #H; + napply (neqtrue_to_eqfalse (eq_Freescale_im n1 n2)); + napply (not_to_not (eq_Freescale_im n1 n2 = true) (n1 = n2) ? H); + napply (eqFreescaleim_to_eq n1 n2). +nqed. + +nlemma decidable_Freescaleim : ∀x,y:Freescale_instr_mode.decidable (x = y). + #x; #y; nnormalize; + napply (or2_elim (eq_Freescale_im x y = true) (eq_Freescale_im x y = false) ? (decidable_bexpr ?)); + ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqFreescaleim_to_eq … H)) + ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqFreescaleim_to_neq … H)) + ##] +nqed. + +nlemma symmetric_eqFreescaleim : symmetricT Freescale_instr_mode bool eq_Freescale_im. + #n1; #n2; + napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_Freescaleim n1 n2)); + ##[ ##1: #H; nrewrite > H; napply refl_eq + ##| ##2: #H; nrewrite > (neq_to_neqFreescaleim n1 n2 H); + napply (symmetric_eq ? (eq_Freescale_im n2 n1) false); + napply (neq_to_neqFreescaleim n2 n1 (symmetric_neq ? n1 n2 H)) + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_pseudo.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_pseudo.ma new file mode 100755 index 000000000..85a129cee --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_pseudo.ma @@ -0,0 +1,187 @@ +(**************************************************************************) +(* ___ *) +(* ||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 Freescale_pseudo: Type ≝ + ADC : Freescale_pseudo (* add with carry *) +| ADD : Freescale_pseudo (* add *) +| AIS : Freescale_pseudo (* add immediate to SP *) +| AIX : Freescale_pseudo (* add immediate to X *) +| AND : Freescale_pseudo (* and *) +| ASL : Freescale_pseudo (* aritmetic shift left *) +| ASR : Freescale_pseudo (* aritmetic shift right *) +| BCC : Freescale_pseudo (* branch if C=0 *) +| BCLRn : Freescale_pseudo (* clear bit n *) +| BCS : Freescale_pseudo (* branch if C=1 *) +| BEQ : Freescale_pseudo (* branch if Z=1 *) +| BGE : Freescale_pseudo (* branch if N⊙V=0 (great or equal) *) +| BGND : Freescale_pseudo (* !!background mode!! *) +| BGT : Freescale_pseudo (* branch if Z|N⊙V=0 clear (great) *) +| BHCC : Freescale_pseudo (* branch if H=0 *) +| BHCS : Freescale_pseudo (* branch if H=1 *) +| BHI : Freescale_pseudo (* branch if C|Z=0, (higher) *) +| BIH : Freescale_pseudo (* branch if nIRQ=1 *) +| BIL : Freescale_pseudo (* branch if nIRQ=0 *) +| BIT : Freescale_pseudo (* flag = and (bit test) *) +| BLE : Freescale_pseudo (* branch if Z|N⊙V=1 (less or equal) *) +| BLS : Freescale_pseudo (* branch if C|Z=1 (lower or same) *) +| BLT : Freescale_pseudo (* branch if N⊙1=1 (less) *) +| BMC : Freescale_pseudo (* branch if I=0 (interrupt mask clear) *) +| BMI : Freescale_pseudo (* branch if N=1 (minus) *) +| BMS : Freescale_pseudo (* branch if I=1 (interrupt mask set) *) +| BNE : Freescale_pseudo (* branch if Z=0 *) +| BPL : Freescale_pseudo (* branch if N=0 (plus) *) +| BRA : Freescale_pseudo (* branch always *) +| BRCLRn : Freescale_pseudo (* branch if bit n clear *) +| BRN : Freescale_pseudo (* branch never (nop) *) +| BRSETn : Freescale_pseudo (* branch if bit n set *) +| BSETn : Freescale_pseudo (* set bit n *) +| BSR : Freescale_pseudo (* branch to subroutine *) +| CBEQA : Freescale_pseudo (* compare (A) and BEQ *) +| CBEQX : Freescale_pseudo (* compare (X) and BEQ *) +| CLC : Freescale_pseudo (* C=0 *) +| CLI : Freescale_pseudo (* I=0 *) +| CLR : Freescale_pseudo (* operand=0 *) +| CMP : Freescale_pseudo (* flag = sub (compare A) *) +| COM : Freescale_pseudo (* not (1 complement) *) +| CPHX : Freescale_pseudo (* flag = sub (compare H:X) *) +| CPX : Freescale_pseudo (* flag = sub (compare X) *) +| DAA : Freescale_pseudo (* decimal adjust A *) +| DBNZ : Freescale_pseudo (* dec and BNE *) +| DEC : Freescale_pseudo (* operand=operand-1 (decrement) *) +| DIV : Freescale_pseudo (* div *) +| EOR : Freescale_pseudo (* xor *) +| INC : Freescale_pseudo (* operand=operand+1 (increment) *) +| JMP : Freescale_pseudo (* jmp word [operand] *) +| JSR : Freescale_pseudo (* jmp to subroutine *) +| LDA : Freescale_pseudo (* load in A *) +| LDHX : Freescale_pseudo (* load in H:X *) +| LDX : Freescale_pseudo (* load in X *) +| LSR : Freescale_pseudo (* logical shift right *) +| MOV : Freescale_pseudo (* move *) +| MUL : Freescale_pseudo (* mul *) +| NEG : Freescale_pseudo (* neg (2 complement) *) +| NOP : Freescale_pseudo (* nop *) +| NSA : Freescale_pseudo (* nibble swap A (al:ah <- ah:al) *) +| ORA : Freescale_pseudo (* or *) +| PSHA : Freescale_pseudo (* push A *) +| PSHH : Freescale_pseudo (* push H *) +| PSHX : Freescale_pseudo (* push X *) +| PULA : Freescale_pseudo (* pop A *) +| PULH : Freescale_pseudo (* pop H *) +| PULX : Freescale_pseudo (* pop X *) +| ROL : Freescale_pseudo (* rotate left *) +| ROR : Freescale_pseudo (* rotate right *) +| RSP : Freescale_pseudo (* reset SP (0x00FF) *) +| RTI : Freescale_pseudo (* return from interrupt *) +| RTS : Freescale_pseudo (* return from subroutine *) +| SBC : Freescale_pseudo (* sub with carry*) +| SEC : Freescale_pseudo (* C=1 *) +| SEI : Freescale_pseudo (* I=1 *) +| SHA : Freescale_pseudo (* swap spc_high,A *) +| SLA : Freescale_pseudo (* swap spc_low,A *) +| STA : Freescale_pseudo (* store from A *) +| STHX : Freescale_pseudo (* store from H:X *) +| STOP : Freescale_pseudo (* !!stop mode!! *) +| STX : Freescale_pseudo (* store from X *) +| SUB : Freescale_pseudo (* sub *) +| SWI : Freescale_pseudo (* software interrupt *) +| TAP : Freescale_pseudo (* flag=A (transfer A to process status byte *) +| TAX : Freescale_pseudo (* X=A (transfer A to X) *) +| TPA : Freescale_pseudo (* A=flag (transfer process status byte to A) *) +| TST : Freescale_pseudo (* flag = sub (test) *) +| TSX : Freescale_pseudo (* X:H=SP (transfer SP to H:X) *) +| TXA : Freescale_pseudo (* A=X (transfer X to A) *) +| TXS : Freescale_pseudo (* SP=X:H (transfer H:X to SP) *) +| WAIT : Freescale_pseudo (* !!wait mode!! *) +. + +ndefinition eq_Freescale_pseudo ≝ +λps1,ps2:Freescale_pseudo. + match ps1 with + [ ADC ⇒ match ps2 with [ ADC ⇒ true | _ ⇒ false ] | ADD ⇒ match ps2 with [ ADD ⇒ true | _ ⇒ false ] + | AIS ⇒ match ps2 with [ AIS ⇒ true | _ ⇒ false ] | AIX ⇒ match ps2 with [ AIX ⇒ true | _ ⇒ false ] + | AND ⇒ match ps2 with [ AND ⇒ true | _ ⇒ false ] | ASL ⇒ match ps2 with [ ASL ⇒ true | _ ⇒ false ] + | ASR ⇒ match ps2 with [ ASR ⇒ true | _ ⇒ false ] | BCC ⇒ match ps2 with [ BCC ⇒ true | _ ⇒ false ] + | BCLRn ⇒ match ps2 with [ BCLRn ⇒ true | _ ⇒ false ] | BCS ⇒ match ps2 with [ BCS ⇒ true | _ ⇒ false ] + | BEQ ⇒ match ps2 with [ BEQ ⇒ true | _ ⇒ false ] | BGE ⇒ match ps2 with [ BGE ⇒ true | _ ⇒ false ] + | BGND ⇒ match ps2 with [ BGND ⇒ true | _ ⇒ false ] | BGT ⇒ match ps2 with [ BGT ⇒ true | _ ⇒ false ] + | BHCC ⇒ match ps2 with [ BHCC ⇒ true | _ ⇒ false ] | BHCS ⇒ match ps2 with [ BHCS ⇒ true | _ ⇒ false ] + | BHI ⇒ match ps2 with [ BHI ⇒ true | _ ⇒ false ] | BIH ⇒ match ps2 with [ BIH ⇒ true | _ ⇒ false ] + | BIL ⇒ match ps2 with [ BIL ⇒ true | _ ⇒ false ] | BIT ⇒ match ps2 with [ BIT ⇒ true | _ ⇒ false ] + | BLE ⇒ match ps2 with [ BLE ⇒ true | _ ⇒ false ] | BLS ⇒ match ps2 with [ BLS ⇒ true | _ ⇒ false ] + | BLT ⇒ match ps2 with [ BLT ⇒ true | _ ⇒ false ] | BMC ⇒ match ps2 with [ BMC ⇒ true | _ ⇒ false ] + | BMI ⇒ match ps2 with [ BMI ⇒ true | _ ⇒ false ] | BMS ⇒ match ps2 with [ BMS ⇒ true | _ ⇒ false ] + | BNE ⇒ match ps2 with [ BNE ⇒ true | _ ⇒ false ] | BPL ⇒ match ps2 with [ BPL ⇒ true | _ ⇒ false ] + | BRA ⇒ match ps2 with [ BRA ⇒ true | _ ⇒ false ] | BRCLRn ⇒ match ps2 with [ BRCLRn ⇒ true | _ ⇒ false ] + | BRN ⇒ match ps2 with [ BRN ⇒ true | _ ⇒ false ] | BRSETn ⇒ match ps2 with [ BRSETn ⇒ true | _ ⇒ false ] + | BSETn ⇒ match ps2 with [ BSETn ⇒ true | _ ⇒ false ] | BSR ⇒ match ps2 with [ BSR ⇒ true | _ ⇒ false ] + | CBEQA ⇒ match ps2 with [ CBEQA ⇒ true | _ ⇒ false ] | CBEQX ⇒ match ps2 with [ CBEQX ⇒ true | _ ⇒ false ] + | CLC ⇒ match ps2 with [ CLC ⇒ true | _ ⇒ false ] | CLI ⇒ match ps2 with [ CLI ⇒ true | _ ⇒ false ] + | CLR ⇒ match ps2 with [ CLR ⇒ true | _ ⇒ false ] | CMP ⇒ match ps2 with [ CMP ⇒ true | _ ⇒ false ] + | COM ⇒ match ps2 with [ COM ⇒ true | _ ⇒ false ] | CPHX ⇒ match ps2 with [ CPHX ⇒ true | _ ⇒ false ] + | CPX ⇒ match ps2 with [ CPX ⇒ true | _ ⇒ false ] | DAA ⇒ match ps2 with [ DAA ⇒ true | _ ⇒ false ] + | DBNZ ⇒ match ps2 with [ DBNZ ⇒ true | _ ⇒ false ] | DEC ⇒ match ps2 with [ DEC ⇒ true | _ ⇒ false ] + | DIV ⇒ match ps2 with [ DIV ⇒ true | _ ⇒ false ] | EOR ⇒ match ps2 with [ EOR ⇒ true | _ ⇒ false ] + | INC ⇒ match ps2 with [ INC ⇒ true | _ ⇒ false ] | JMP ⇒ match ps2 with [ JMP ⇒ true | _ ⇒ false ] + | JSR ⇒ match ps2 with [ JSR ⇒ true | _ ⇒ false ] | LDA ⇒ match ps2 with [ LDA ⇒ true | _ ⇒ false ] + | LDHX ⇒ match ps2 with [ LDHX ⇒ true | _ ⇒ false ] | LDX ⇒ match ps2 with [ LDX ⇒ true | _ ⇒ false ] + | LSR ⇒ match ps2 with [ LSR ⇒ true | _ ⇒ false ] | MOV ⇒ match ps2 with [ MOV ⇒ true | _ ⇒ false ] + | MUL ⇒ match ps2 with [ MUL ⇒ true | _ ⇒ false ] | NEG ⇒ match ps2 with [ NEG ⇒ true | _ ⇒ false ] + | NOP ⇒ match ps2 with [ NOP ⇒ true | _ ⇒ false ] | NSA ⇒ match ps2 with [ NSA ⇒ true | _ ⇒ false ] + | ORA ⇒ match ps2 with [ ORA ⇒ true | _ ⇒ false ] | PSHA ⇒ match ps2 with [ PSHA ⇒ true | _ ⇒ false ] + | PSHH ⇒ match ps2 with [ PSHH ⇒ true | _ ⇒ false ] | PSHX ⇒ match ps2 with [ PSHX ⇒ true | _ ⇒ false ] + | PULA ⇒ match ps2 with [ PULA ⇒ true | _ ⇒ false ] | PULH ⇒ match ps2 with [ PULH ⇒ true | _ ⇒ false ] + | PULX ⇒ match ps2 with [ PULX ⇒ true | _ ⇒ false ] | ROL ⇒ match ps2 with [ ROL ⇒ true | _ ⇒ false ] + | ROR ⇒ match ps2 with [ ROR ⇒ true | _ ⇒ false ] | RSP ⇒ match ps2 with [ RSP ⇒ true | _ ⇒ false ] + | RTI ⇒ match ps2 with [ RTI ⇒ true | _ ⇒ false ] | RTS ⇒ match ps2 with [ RTS ⇒ true | _ ⇒ false ] + | SBC ⇒ match ps2 with [ SBC ⇒ true | _ ⇒ false ] | SEC ⇒ match ps2 with [ SEC ⇒ true | _ ⇒ false ] + | SEI ⇒ match ps2 with [ SEI ⇒ true | _ ⇒ false ] | SHA ⇒ match ps2 with [ SHA ⇒ true | _ ⇒ false ] + | SLA ⇒ match ps2 with [ SLA ⇒ true | _ ⇒ false ] | STA ⇒ match ps2 with [ STA ⇒ true | _ ⇒ false ] + | STHX ⇒ match ps2 with [ STHX ⇒ true | _ ⇒ false ] | STOP ⇒ match ps2 with [ STOP ⇒ true | _ ⇒ false ] + | STX ⇒ match ps2 with [ STX ⇒ true | _ ⇒ false ] | SUB ⇒ match ps2 with [ SUB ⇒ true | _ ⇒ false ] + | SWI ⇒ match ps2 with [ SWI ⇒ true | _ ⇒ false ] | TAP ⇒ match ps2 with [ TAP ⇒ true | _ ⇒ false ] + | TAX ⇒ match ps2 with [ TAX ⇒ true | _ ⇒ false ] | TPA ⇒ match ps2 with [ TPA ⇒ true | _ ⇒ false ] + | TST ⇒ match ps2 with [ TST ⇒ true | _ ⇒ false ] | TSX ⇒ match ps2 with [ TSX ⇒ true | _ ⇒ false ] + | TXA ⇒ match ps2 with [ TXA ⇒ true | _ ⇒ false ] | TXS ⇒ match ps2 with [ TXS ⇒ true | _ ⇒ false ] + | WAIT ⇒ match ps2 with [ WAIT ⇒ true | _ ⇒ false ] + ]. + +ndefinition forall_Freescale_pseudo ≝ λP:Freescale_pseudo → bool. + P ADC ⊗ P ADD ⊗ P AIS ⊗ P AIX ⊗ P AND ⊗ P ASL ⊗ P ASR ⊗ P BCC ⊗ + P BCLRn ⊗ P BCS ⊗ P BEQ ⊗ P BGE ⊗ P BGND ⊗ P BGT ⊗ P BHCC ⊗ P BHCS ⊗ + P BHI ⊗ P BIH ⊗ P BIL ⊗ P BIT ⊗ P BLE ⊗ P BLS ⊗ P BLT ⊗ P BMC ⊗ + P BMI ⊗ P BMS ⊗ P BNE ⊗ P BPL ⊗ P BRA ⊗ P BRCLRn ⊗ P BRN ⊗ P BRSETn ⊗ + P BSETn ⊗ P BSR ⊗ P CBEQA ⊗ P CBEQX ⊗ P CLC ⊗ P CLI ⊗ P CLR ⊗ P CMP ⊗ + P COM ⊗ P CPHX ⊗ P CPX ⊗ P DAA ⊗ P DBNZ ⊗ P DEC ⊗ P DIV ⊗ P EOR ⊗ + P INC ⊗ P JMP ⊗ P JSR ⊗ P LDA ⊗ P LDHX ⊗ P LDX ⊗ P LSR ⊗ P MOV ⊗ + P MUL ⊗ P NEG ⊗ P NOP ⊗ P NSA ⊗ P ORA ⊗ P PSHA ⊗ P PSHH ⊗ P PSHX ⊗ + P PULA ⊗ P PULH ⊗ P PULX ⊗ P ROL ⊗ P ROR ⊗ P RSP ⊗ P RTI ⊗ P RTS ⊗ + P SBC ⊗ P SEC ⊗ P SEI ⊗ P SHA ⊗ P SLA ⊗ P STA ⊗ P STHX ⊗ P STOP ⊗ + P STX ⊗ P SUB ⊗ P SWI ⊗ P TAP ⊗ P TAX ⊗ P TPA ⊗ P TST ⊗ P TSX ⊗ + P TXA ⊗ P TXS ⊗ P WAIT. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_pseudo_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_pseudo_lemmas.ma new file mode 100755 index 000000000..05b04b741 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/Freescale_pseudo_lemmas.ma @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lemmas.ma". +include "emulator/opcodes/Freescale_pseudo.ma". + +nlemma eq_to_eqFreescalepseudo : ∀n1,n2.n1 = n2 → eq_Freescale_pseudo n1 n2 = true. + #n1; #n2; #H; + nrewrite > H; + nelim n2; + nnormalize; + napply refl_eq. +nqed. + +nlemma neqFreescalepseudo_to_neq : ∀n1,n2.eq_Freescale_pseudo n1 n2 = false → n1 ≠ n2. + #n1; #n2; #H; + napply (not_to_not (n1 = n2) (eq_Freescale_pseudo n1 n2 = true) …); + ##[ ##1: napply (eq_to_eqFreescalepseudo n1 n2) + ##| ##2: napply (eqfalse_to_neqtrue … H) + ##] +nqed. + +(* !!! per brevita... *) +naxiom eqFreescalepseudo_to_eq : ∀c1,c2.eq_Freescale_pseudo c1 c2 = true → c1 = c2. + +nlemma neq_to_neqFreescalepseudo : ∀n1,n2.n1 ≠ n2 → eq_Freescale_pseudo n1 n2 = false. + #n1; #n2; #H; + napply (neqtrue_to_eqfalse (eq_Freescale_pseudo n1 n2)); + napply (not_to_not (eq_Freescale_pseudo n1 n2 = true) (n1 = n2) ? H); + napply (eqFreescalepseudo_to_eq n1 n2). +nqed. + +nlemma decidable_Freescalepseudo : ∀x,y:Freescale_pseudo.decidable (x = y). + #x; #y; nnormalize; + napply (or2_elim (eq_Freescale_pseudo x y = true) (eq_Freescale_pseudo x y = false) ? (decidable_bexpr ?)); + ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqFreescalepseudo_to_eq … H)) + ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqFreescalepseudo_to_neq … H)) + ##] +nqed. + +nlemma symmetric_eqFreescalepseudo : symmetricT Freescale_pseudo bool eq_Freescale_pseudo. + #n1; #n2; + napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_Freescalepseudo n1 n2)); + ##[ ##1: #H; nrewrite > H; napply refl_eq + ##| ##2: #H; nrewrite > (neq_to_neqFreescalepseudo n1 n2 H); + napply (symmetric_eq ? (eq_Freescale_pseudo n2 n1) false); + napply (neq_to_neqFreescalepseudo n2 n1 (symmetric_neq ? n1 n2 H)) + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_instr_mode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_instr_mode.ma deleted file mode 100755 index 161aa920d..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_instr_mode.ma +++ /dev/null @@ -1,109 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 HC05_instr_mode: Type ≝ - (* INHERENT = nessun operando *) - MODE_INH : HC05_instr_mode - (* INHERENT = nessun operando (A implicito) *) -| MODE_INHA : HC05_instr_mode - (* INHERENT = nessun operando (X implicito) *) -| MODE_INHX : HC05_instr_mode - - (* INHERENT_ADDRESS = nessun operando (HX implicito) *) -| MODE_INHX0ADD : HC05_instr_mode - (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *) -| MODE_INHX1ADD : HC05_instr_mode - (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *) -| MODE_INHX2ADD : HC05_instr_mode - - (* IMMEDIATE = operando valore immediato byte = 0xbb *) -| MODE_IMM1 : HC05_instr_mode - (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *) -| MODE_IMM1EXT : HC05_instr_mode - (* IMMEDIATE = operando valore immediato word = 0xwwww *) -| MODE_IMM2 : HC05_instr_mode - (* DIRECT = operando offset byte = [0x00bb] *) -| MODE_DIR1 : HC05_instr_mode - (* DIRECT = operando offset word = [0xwwww] *) -| MODE_DIR2 : HC05_instr_mode - (* INDEXED = nessun operando (implicito [X] *) -| MODE_IX0 : HC05_instr_mode - (* INDEXED = operando offset relativo byte = [X+0x00bb] *) -| MODE_IX1 : HC05_instr_mode - (* INDEXED = operando offset relativo word = [X+0xwwww] *) -| MODE_IX2 : HC05_instr_mode - - (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *) - (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *) -| MODE_DIRn : oct → HC05_instr_mode - (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *) - (* + operando valore immediato byte *) - (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *) -| MODE_DIRn_and_IMM1 : oct → HC05_instr_mode -. - -ndefinition eq_HC05_im ≝ -λi1,i2:HC05_instr_mode. - match i1 with - [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ] - | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ] - | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ true | _ ⇒ false ] - | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ true | _ ⇒ false ] - | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ true | _ ⇒ false ] - | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ true | _ ⇒ false ] - | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ] - | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ true | _ ⇒ false ] - | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ] - | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ] - | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ true | _ ⇒ false ] - | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ true | _ ⇒ false ] - | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ true | _ ⇒ false ] - | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ true | _ ⇒ false ] - | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ] - | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eq_oct n1 n2 | _ ⇒ false ] - ]. - -(* iteratore sulle modalita' *) -ndefinition forall_HC05_im ≝ λP:HC05_instr_mode → bool. - P MODE_INH -⊗ P MODE_INHA -⊗ P MODE_INHX -⊗ P MODE_INHX0ADD -⊗ P MODE_INHX1ADD -⊗ P MODE_INHX2ADD -⊗ P MODE_IMM1 -⊗ P MODE_IMM1EXT -⊗ P MODE_IMM2 -⊗ P MODE_DIR1 -⊗ P MODE_DIR2 -⊗ P MODE_IX0 -⊗ P MODE_IX1 -⊗ P MODE_IX2 -⊗ forall_oct (λo. P (MODE_DIRn o)) -⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o)). diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_instr_mode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_instr_mode_lemmas.ma deleted file mode 100755 index 87f22cbe0..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_instr_mode_lemmas.ma +++ /dev/null @@ -1,69 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_lemmas.ma". -include "emulator/opcodes/HC05_instr_mode.ma". -include "num/oct_lemmas.ma". - -nlemma eq_to_eqHC05im : ∀n1,n2.n1 = n2 → eq_HC05_im n1 n2 = true. - #n1; #n2; #H; - nrewrite > H; - nelim n2; - ##[ ##15,16: #o; nrewrite > (eq_to_eqoct … (refl_eq …)) ##] - napply refl_eq. -nqed. - -nlemma neqHC05im_to_neq : ∀n1,n2.eq_HC05_im n1 n2 = false → n1 ≠ n2. - #n1; #n2; #H; - napply (not_to_not (n1 = n2) (eq_HC05_im n1 n2 = true) …); - ##[ ##1: napply (eq_to_eqHC05im n1 n2) - ##| ##2: napply (eqfalse_to_neqtrue … H) - ##] -nqed. - -(* !!! per brevita... *) -naxiom eqHC05im_to_eq : ∀c1,c2.eq_HC05_im c1 c2 = true → c1 = c2. - -nlemma neq_to_neqHC05im : ∀n1,n2.n1 ≠ n2 → eq_HC05_im n1 n2 = false. - #n1; #n2; #H; - napply (neqtrue_to_eqfalse (eq_HC05_im n1 n2)); - napply (not_to_not (eq_HC05_im n1 n2 = true) (n1 = n2) ? H); - napply (eqHC05im_to_eq n1 n2). -nqed. - -nlemma decidable_HC05im : ∀x,y:HC05_instr_mode.decidable (x = y). - #x; #y; nnormalize; - napply (or2_elim (eq_HC05_im x y = true) (eq_HC05_im x y = false) ? (decidable_bexpr ?)); - ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqHC05im_to_eq … H)) - ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqHC05im_to_neq … H)) - ##] -nqed. - -nlemma symmetric_eqHC05im : symmetricT HC05_instr_mode bool eq_HC05_im. - #n1; #n2; - napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_HC05im n1 n2)); - ##[ ##1: #H; nrewrite > H; napply refl_eq - ##| ##2: #H; nrewrite > (neq_to_neqHC05im n1 n2 H); - napply (symmetric_eq ? (eq_HC05_im n2 n1) false); - napply (neq_to_neqHC05im n2 n1 (symmetric_neq ? n1 n2 H)) - ##] -nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_opcode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_opcode.ma deleted file mode 100755 index 3062ea3f4..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_opcode.ma +++ /dev/null @@ -1,140 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 HC05_opcode: Type ≝ - ADC : HC05_opcode (* add with carry *) -| ADD : HC05_opcode (* add *) -| AND : HC05_opcode (* and *) -| ASL : HC05_opcode (* aritmetic shift left *) -| ASR : HC05_opcode (* aritmetic shift right *) -| BCC : HC05_opcode (* branch if C=0 *) -| BCLRn : HC05_opcode (* clear bit n *) -| BCS : HC05_opcode (* branch if C=1 *) -| BEQ : HC05_opcode (* branch if Z=1 *) -| BHCC : HC05_opcode (* branch if H=0 *) -| BHCS : HC05_opcode (* branch if H=1 *) -| BHI : HC05_opcode (* branch if C|Z=0, (higher) *) -| BIH : HC05_opcode (* branch if nIRQ=1 *) -| BIL : HC05_opcode (* branch if nIRQ=0 *) -| BIT : HC05_opcode (* flag = and (bit test) *) -| BLS : HC05_opcode (* branch if C|Z=1 (lower or same) *) -| BMC : HC05_opcode (* branch if I=0 (interrupt mask clear) *) -| BMI : HC05_opcode (* branch if N=1 (minus) *) -| BMS : HC05_opcode (* branch if I=1 (interrupt mask set) *) -| BNE : HC05_opcode (* branch if Z=0 *) -| BPL : HC05_opcode (* branch if N=0 (plus) *) -| BRA : HC05_opcode (* branch always *) -| BRCLRn : HC05_opcode (* branch if bit n clear *) -| BRN : HC05_opcode (* branch never (nop) *) -| BRSETn : HC05_opcode (* branch if bit n set *) -| BSETn : HC05_opcode (* set bit n *) -| BSR : HC05_opcode (* branch to subroutine *) -| CLC : HC05_opcode (* C=0 *) -| CLI : HC05_opcode (* I=0 *) -| CLR : HC05_opcode (* operand=0 *) -| CMP : HC05_opcode (* flag = sub (compare A) *) -| COM : HC05_opcode (* not (1 complement) *) -| CPX : HC05_opcode (* flag = sub (compare X) *) -| DEC : HC05_opcode (* operand=operand-1 (decrement) *) -| EOR : HC05_opcode (* xor *) -| INC : HC05_opcode (* operand=operand+1 (increment) *) -| JMP : HC05_opcode (* jmp word [operand] *) -| JSR : HC05_opcode (* jmp to subroutine *) -| LDA : HC05_opcode (* load in A *) -| LDX : HC05_opcode (* load in X *) -| LSR : HC05_opcode (* logical shift right *) -| MUL : HC05_opcode (* mul *) -| NEG : HC05_opcode (* neg (2 complement) *) -| NOP : HC05_opcode (* nop *) -| ORA : HC05_opcode (* or *) -| ROL : HC05_opcode (* rotate left *) -| ROR : HC05_opcode (* rotate right *) -| RSP : HC05_opcode (* reset SP (0x00FF) *) -| RTI : HC05_opcode (* return from interrupt *) -| RTS : HC05_opcode (* return from subroutine *) -| SBC : HC05_opcode (* sub with carry*) -| SEC : HC05_opcode (* C=1 *) -| SEI : HC05_opcode (* I=1 *) -| STA : HC05_opcode (* store from A *) -| STOP : HC05_opcode (* !!stop mode!! *) -| STX : HC05_opcode (* store from X *) -| SUB : HC05_opcode (* sub *) -| SWI : HC05_opcode (* software interrupt *) -| TAX : HC05_opcode (* X=A (transfer A to X) *) -| TST : HC05_opcode (* flag = sub (test) *) -| TXA : HC05_opcode (* A=X (transfer X to A) *) -| WAIT : HC05_opcode (* !!wait mode!! *) -. - -ndefinition eq_HC05_op ≝ -λop1,op2:HC05_opcode. - match op1 with - [ ADC ⇒ match op2 with [ ADC ⇒ true | _ ⇒ false ] | ADD ⇒ match op2 with [ ADD ⇒ true | _ ⇒ false ] - | AND ⇒ match op2 with [ AND ⇒ true | _ ⇒ false ] | ASL ⇒ match op2 with [ ASL ⇒ true | _ ⇒ false ] - | ASR ⇒ match op2 with [ ASR ⇒ true | _ ⇒ false ] | BCC ⇒ match op2 with [ BCC ⇒ true | _ ⇒ false ] - | BCLRn ⇒ match op2 with [ BCLRn ⇒ true | _ ⇒ false ] | BCS ⇒ match op2 with [ BCS ⇒ true | _ ⇒ false ] - | BEQ ⇒ match op2 with [ BEQ ⇒ true | _ ⇒ false ] | BHCC ⇒ match op2 with [ BHCC ⇒ true | _ ⇒ false ] - | BHCS ⇒ match op2 with [ BHCS ⇒ true | _ ⇒ false ] | BHI ⇒ match op2 with [ BHI ⇒ true | _ ⇒ false ] - | BIH ⇒ match op2 with [ BIH ⇒ true | _ ⇒ false ] | BIL ⇒ match op2 with [ BIL ⇒ true | _ ⇒ false ] - | BIT ⇒ match op2 with [ BIT ⇒ true | _ ⇒ false ] | BLS ⇒ match op2 with [ BLS ⇒ true | _ ⇒ false ] - | BMC ⇒ match op2 with [ BMC ⇒ true | _ ⇒ false ] | BMI ⇒ match op2 with [ BMI ⇒ true | _ ⇒ false ] - | BMS ⇒ match op2 with [ BMS ⇒ true | _ ⇒ false ] | BNE ⇒ match op2 with [ BNE ⇒ true | _ ⇒ false ] - | BPL ⇒ match op2 with [ BPL ⇒ true | _ ⇒ false ] | BRA ⇒ match op2 with [ BRA ⇒ true | _ ⇒ false ] - | BRCLRn ⇒ match op2 with [ BRCLRn ⇒ true | _ ⇒ false ] | BRN ⇒ match op2 with [ BRN ⇒ true | _ ⇒ false ] - | BRSETn ⇒ match op2 with [ BRSETn ⇒ true | _ ⇒ false ] | BSETn ⇒ match op2 with [ BSETn ⇒ true | _ ⇒ false ] - | BSR ⇒ match op2 with [ BSR ⇒ true | _ ⇒ false ] | CLC ⇒ match op2 with [ CLC ⇒ true | _ ⇒ false ] - | CLI ⇒ match op2 with [ CLI ⇒ true | _ ⇒ false ] | CLR ⇒ match op2 with [ CLR ⇒ true | _ ⇒ false ] - | CMP ⇒ match op2 with [ CMP ⇒ true | _ ⇒ false ] | COM ⇒ match op2 with [ COM ⇒ true | _ ⇒ false ] - | CPX ⇒ match op2 with [ CPX ⇒ true | _ ⇒ false ] | DEC ⇒ match op2 with [ DEC ⇒ true | _ ⇒ false ] - | EOR ⇒ match op2 with [ EOR ⇒ true | _ ⇒ false ] | INC ⇒ match op2 with [ INC ⇒ true | _ ⇒ false ] - | JMP ⇒ match op2 with [ JMP ⇒ true | _ ⇒ false ] | JSR ⇒ match op2 with [ JSR ⇒ true | _ ⇒ false ] - | LDA ⇒ match op2 with [ LDA ⇒ true | _ ⇒ false ] | LDX ⇒ match op2 with [ LDX ⇒ true | _ ⇒ false ] - | LSR ⇒ match op2 with [ LSR ⇒ true | _ ⇒ false ] | MUL ⇒ match op2 with [ MUL ⇒ true | _ ⇒ false ] - | NEG ⇒ match op2 with [ NEG ⇒ true | _ ⇒ false ] | NOP ⇒ match op2 with [ NOP ⇒ true | _ ⇒ false ] - | ORA ⇒ match op2 with [ ORA ⇒ true | _ ⇒ false ] | ROL ⇒ match op2 with [ ROL ⇒ true | _ ⇒ false ] - | ROR ⇒ match op2 with [ ROR ⇒ true | _ ⇒ false ] | RSP ⇒ match op2 with [ RSP ⇒ true | _ ⇒ false ] - | RTI ⇒ match op2 with [ RTI ⇒ true | _ ⇒ false ] | RTS ⇒ match op2 with [ RTS ⇒ true | _ ⇒ false ] - | SBC ⇒ match op2 with [ SBC ⇒ true | _ ⇒ false ] | SEC ⇒ match op2 with [ SEC ⇒ true | _ ⇒ false ] - | SEI ⇒ match op2 with [ SEI ⇒ true | _ ⇒ false ] | STA ⇒ match op2 with [ STA ⇒ true | _ ⇒ false ] - | STOP ⇒ match op2 with [ STOP ⇒ true | _ ⇒ false ] | STX ⇒ match op2 with [ STX ⇒ true | _ ⇒ false ] - | SUB ⇒ match op2 with [ SUB ⇒ true | _ ⇒ false ] | SWI ⇒ match op2 with [ SWI ⇒ true | _ ⇒ false ] - | TAX ⇒ match op2 with [ TAX ⇒ true | _ ⇒ false ] | TST ⇒ match op2 with [ TST ⇒ true | _ ⇒ false ] - | TXA ⇒ match op2 with [ TXA ⇒ true | _ ⇒ false ] | WAIT ⇒ match op2 with [ WAIT ⇒ true | _ ⇒ false ] - ]. - -(* iteratore sugli opcode *) -ndefinition forall_HC05_op ≝ λP:HC05_opcode → bool. - P ADC ⊗ P ADD ⊗ P AND ⊗ P ASL ⊗ P ASR ⊗ P BCC ⊗ P BCLRn ⊗ P BCS ⊗ - P BEQ ⊗ P BHCC ⊗ P BHCS ⊗ P BHI ⊗ P BIH ⊗ P BIL ⊗ P BIT ⊗ P BLS ⊗ - P BMC ⊗ P BMI ⊗ P BMS ⊗ P BNE ⊗ P BPL ⊗ P BRA ⊗ P BRCLRn ⊗ P BRN ⊗ - P BRSETn ⊗ P BSETn ⊗ P BSR ⊗ P CLC ⊗ P CLI ⊗ P CLR ⊗ P CMP ⊗ P COM ⊗ - P CPX ⊗ P DEC ⊗ P EOR ⊗ P INC ⊗ P JMP ⊗ P JSR ⊗ P LDA ⊗ P LDX ⊗ - P LSR ⊗ P MUL ⊗ P NEG ⊗ P NOP ⊗ P ORA ⊗ P ROL ⊗ P ROR ⊗ P RSP ⊗ - P RTI ⊗ P RTS ⊗ P SBC ⊗ P SEC ⊗ P SEI ⊗ P STA ⊗ P STOP ⊗ P STX ⊗ - P SUB ⊗ P SWI ⊗ P TAX ⊗ P TST ⊗ P TXA ⊗ P WAIT. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_opcode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_opcode_lemmas.ma deleted file mode 100755 index 041c5548b..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_opcode_lemmas.ma +++ /dev/null @@ -1,68 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_lemmas.ma". -include "emulator/opcodes/HC05_opcode.ma". - -nlemma eq_to_eqHC05op : ∀n1,n2.n1 = n2 → eq_HC05_op n1 n2 = true. - #n1; #n2; #H; - nrewrite > H; - nelim n2; - nnormalize; - napply refl_eq. -nqed. - -nlemma neqHC05op_to_neq : ∀n1,n2.eq_HC05_op n1 n2 = false → n1 ≠ n2. - #n1; #n2; #H; - napply (not_to_not (n1 = n2) (eq_HC05_op n1 n2 = true) …); - ##[ ##1: napply (eq_to_eqHC05op n1 n2) - ##| ##2: napply (eqfalse_to_neqtrue … H) - ##] -nqed. - -(* !!! per brevita... *) -naxiom eqHC05op_to_eq : ∀c1,c2.eq_HC05_op c1 c2 = true → c1 = c2. - -nlemma neq_to_neqHC05op : ∀n1,n2.n1 ≠ n2 → eq_HC05_op n1 n2 = false. - #n1; #n2; #H; - napply (neqtrue_to_eqfalse (eq_HC05_op n1 n2)); - napply (not_to_not (eq_HC05_op n1 n2 = true) (n1 = n2) ? H); - napply (eqHC05op_to_eq n1 n2). -nqed. - -nlemma decidable_HC05op : ∀x,y:HC05_opcode.decidable (x = y). - #x; #y; nnormalize; - napply (or2_elim (eq_HC05_op x y = true) (eq_HC05_op x y = false) ? (decidable_bexpr ?)); - ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqHC05op_to_eq … H)) - ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqHC05op_to_neq … H)) - ##] -nqed. - -nlemma symmetric_eqHC05op : symmetricT HC05_opcode bool eq_HC05_op. - #n1; #n2; - napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_HC05op n1 n2)); - ##[ ##1: #H; nrewrite > H; napply refl_eq - ##| ##2: #H; nrewrite > (neq_to_neqHC05op n1 n2 H); - napply (symmetric_eq ? (eq_HC05_op n2 n1) false); - napply (neq_to_neqHC05op n2 n1 (symmetric_neq ? n1 n2 H)) - ##] -nqed. 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 0f2822bf7..20b16ec86 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 @@ -20,8 +20,8 @@ (* *) (* ********************************************************************** *) -include "emulator/opcodes/HC05_opcode.ma". -include "emulator/opcodes/HC05_instr_mode.ma". +include "emulator/opcodes/Freescale_pseudo.ma". +include "emulator/opcodes/Freescale_instr_mode.ma". include "emulator/opcodes/byte_or_word.ma". include "common/list.ma". diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_table_tests.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_table_tests.ma index debb76922..917a66665 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_table_tests.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_table_tests.ma @@ -20,7 +20,7 @@ (* *) (* ********************************************************************** *) -include "emulator/opcodes/opcode.ma". +include "emulator/opcodes/pseudo.ma". include "emulator/opcodes/HC05_table.ma". (* ***************** *) @@ -39,36 +39,56 @@ ndefinition HC05_not_impl_byte ≝ ;〈xA,x7〉;〈xA,xC〉;〈xA,xF〉 ]. -(* test bytecode non implementati *) -(* !!! per brevita... *) -(*nlemma ok_byte_table_HC05 : forall_b8 (λb. +nlemma ok_byte_table_HC05 : forall_b8 (λb. (test_not_impl_byte b HC05_not_impl_byte ⊙ eq_w16 (get_byte_count HC05 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC05) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗ (⊖ (test_not_impl_byte b HC05_not_impl_byte) ⊙ eq_w16 (get_byte_count HC05 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC05) 〈〈x0,x0〉:〈x0,x0〉〉)) = true. napply refl_eq. -nqed.*) +nqed. -(* tutti op implementati *) -(* !!! per brevita... *) -(*nlemma ok_pseudo_table_HC05 : - forall_op HC05 (λo. - le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count HC05 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC05)) = true. +(* HC05: pseudocodici non implementati come da manuale *) +ndefinition HC05_not_impl_pseudo ≝ + [ AIS ; AIX ; BGE ; BGND ; BGT ; BLE ; BLT ; CBEQA ; CBEQX ; CPHX ; DAA + ; DBNZ ; DIV ; LDHX ; MOV ; NSA ; PSHA ; PSHH ; PSHX ; PULA ; PULH ; PULX + ; SHA ; SLA ; STHX ; TAP ; TPA ; TSX ; TXS ]. + +nlemma ok_pseudo_table_HC05 : forall_Freescale_pseudo (λo. + (test_not_impl_pseudo HC05 o HC05_not_impl_pseudo ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count HC05 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC05)) ⊗ + (⊖ (test_not_impl_pseudo HC05 o HC05_not_impl_pseudo) ⊙ eq_w16 (get_pseudo_count HC05 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC05) 〈〈x0,x0〉:〈x0,x0〉〉)) + = true. napply refl_eq. -nqed.*) +nqed. -(* tutte im implementate *) -(* !!! per brevita... *) -(*nlemma ok_mode_table_HC05 : - forall_im HC05 (λi. - le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count HC05 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC05)) = true. +(* HC05: modalita' non implementate come da manuale *) +ndefinition HC05_not_impl_mode ≝ + [ MODE_INHH ; MODE_SP1 ; MODE_SP2 ; MODE_DIR1_to_DIR1 + ; MODE_IMM1_to_DIR1 ; MODE_IX0p_to_DIR1 ; MODE_DIR1_to_IX0p + ; MODE_INHA_and_IMM1 ; MODE_INHX_and_IMM1 ; MODE_IMM1_and_IMM1 + ; MODE_DIR1_and_IMM1 ; MODE_IX0_and_IMM1 ; MODE_IX0p_and_IMM1 + ; MODE_IX1_and_IMM1 ; MODE_IX1p_and_IMM1 ; MODE_SP1_and_IMM1 + ; MODE_TNY x0 ; MODE_TNY x1 ; MODE_TNY x2 ; MODE_TNY x3 + ; MODE_TNY x4 ; MODE_TNY x5 ; MODE_TNY x6 ; MODE_TNY x7 + ; MODE_TNY x8 ; MODE_TNY x9 ; MODE_TNY xA ; MODE_TNY xB + ; MODE_TNY xC ; MODE_TNY xD ; MODE_TNY xE ; MODE_TNY xF + ; MODE_SRT t00 ; MODE_SRT t01 ; MODE_SRT t02 ; MODE_SRT t03 + ; MODE_SRT t04 ; MODE_SRT t05 ; MODE_SRT t06 ; MODE_SRT t07 + ; MODE_SRT t08 ; MODE_SRT t09 ; MODE_SRT t0A ; MODE_SRT t0B + ; MODE_SRT t0C ; MODE_SRT t0D ; MODE_SRT t0E ; MODE_SRT t0F + ; MODE_SRT t10 ; MODE_SRT t11 ; MODE_SRT t12 ; MODE_SRT t13 + ; MODE_SRT t14 ; MODE_SRT t15 ; MODE_SRT t16 ; MODE_SRT t17 + ; MODE_SRT t18 ; MODE_SRT t19 ; MODE_SRT t1A ; MODE_SRT t1B + ; MODE_SRT t1C ; MODE_SRT t1D ; MODE_SRT t1E ; MODE_SRT t1F ]. + +nlemma ok_mode_table_HC05 : forall_Freescale_im (λi. + (test_not_impl_mode HC05 i HC05_not_impl_mode ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count HC05 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC05)) ⊗ + (⊖ (test_not_impl_mode HC05 i HC05_not_impl_mode) ⊙ eq_w16 (get_mode_count HC05 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC05) 〈〈x0,x0〉:〈x0,x0〉〉)) + = true. napply refl_eq. -nqed.*) +nqed. -(* nessuna ripetizione di combinazione op + imm *) -(* !!! per brevita... *) -(*nlemma ok_OpIm_table_HC05 : - forall_im HC05 (λi. - forall_op HC05 (λo. - le_w16 (get_OpIm_count HC05 o i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC05) 〈〈x0,x0〉:〈x0,x1〉〉)) = true. +nlemma ok_PsIm_table_HC05 : + forall_Freescale_im (λi:Freescale_instr_mode. + forall_Freescale_pseudo (λps:Freescale_pseudo. + le_w16 (get_PsIm_count HC05 ps i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC05) 〈〈x0,x0〉:〈x0,x1〉〉)) = true. napply refl_eq. -nqed.*) +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_instr_mode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_instr_mode.ma deleted file mode 100755 index 419c28c9f..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_instr_mode.ma +++ /dev/null @@ -1,175 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 HC08_instr_mode: Type ≝ - (* INHERENT = nessun operando *) - MODE_INH : HC08_instr_mode - (* INHERENT = nessun operando (A implicito) *) -| MODE_INHA : HC08_instr_mode - (* INHERENT = nessun operando (X implicito) *) -| MODE_INHX : HC08_instr_mode - (* INHERENT = nessun operando (H implicito) *) -| MODE_INHH : HC08_instr_mode - - (* INHERENT_ADDRESS = nessun operando (HX implicito) *) -| MODE_INHX0ADD : HC08_instr_mode - (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *) -| MODE_INHX1ADD : HC08_instr_mode - (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *) -| MODE_INHX2ADD : HC08_instr_mode - - (* IMMEDIATE = operando valore immediato byte = 0xbb *) -| MODE_IMM1 : HC08_instr_mode - (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *) -| MODE_IMM1EXT : HC08_instr_mode - (* IMMEDIATE = operando valore immediato word = 0xwwww *) -| MODE_IMM2 : HC08_instr_mode - (* DIRECT = operando offset byte = [0x00bb] *) -| MODE_DIR1 : HC08_instr_mode - (* DIRECT = operando offset word = [0xwwww] *) -| MODE_DIR2 : HC08_instr_mode - (* INDEXED = nessun operando (implicito [X] *) -| MODE_IX0 : HC08_instr_mode - (* INDEXED = operando offset relativo byte = [X+0x00bb] *) -| MODE_IX1 : HC08_instr_mode - (* INDEXED = operando offset relativo word = [X+0xwwww] *) -| MODE_IX2 : HC08_instr_mode - (* INDEXED = operando offset relativo byte = [SP+0x00bb] *) -| MODE_SP1 : HC08_instr_mode - (* INDEXED = operando offset relativo word = [SP+0xwwww] *) -| MODE_SP2 : HC08_instr_mode - - (* DIRECT → DIRECT = carica da diretto/scrive su diretto *) -| MODE_DIR1_to_DIR1 : HC08_instr_mode - (* IMMEDIATE → DIRECT = carica da immediato/scrive su diretto *) -| MODE_IMM1_to_DIR1 : HC08_instr_mode - (* INDEXED++ → DIRECT = carica da [X]/scrive su diretto/H:X++ *) -| MODE_IX0p_to_DIR1 : HC08_instr_mode - (* DIRECT → INDEXED++ = carica da diretto/scrive su [X]/H:X++ *) -| MODE_DIR1_to_IX0p : HC08_instr_mode - - (* INHERENT(A) + IMMEDIATE *) -| MODE_INHA_and_IMM1 : HC08_instr_mode - (* INHERENT(X) + IMMEDIATE *) -| MODE_INHX_and_IMM1 : HC08_instr_mode - (* IMMEDIATE + IMMEDIATE *) -| MODE_IMM1_and_IMM1 : HC08_instr_mode - (* DIRECT + IMMEDIATE *) -| MODE_DIR1_and_IMM1 : HC08_instr_mode - (* INDEXED + IMMEDIATE *) -| MODE_IX0_and_IMM1 : HC08_instr_mode - (* INDEXED++ + IMMEDIATE *) -| MODE_IX0p_and_IMM1 : HC08_instr_mode - (* INDEXED + IMMEDIATE *) -| MODE_IX1_and_IMM1 : HC08_instr_mode - (* INDEXED++ + IMMEDIATE *) -| MODE_IX1p_and_IMM1 : HC08_instr_mode - (* INDEXED + IMMEDIATE *) -| MODE_SP1_and_IMM1 : HC08_instr_mode - - (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *) - (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *) -| MODE_DIRn : oct → HC08_instr_mode - (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *) - (* + operando valore immediato byte *) - (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *) -| MODE_DIRn_and_IMM1 : oct → HC08_instr_mode -. - -ndefinition eq_HC08_im ≝ -λi1,i2:HC08_instr_mode. - match i1 with - [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ] - | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ] - | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ true | _ ⇒ false ] - | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ true | _ ⇒ false ] - | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ true | _ ⇒ false ] - | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ true | _ ⇒ false ] - | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ true | _ ⇒ false ] - | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ] - | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ true | _ ⇒ false ] - | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ] - | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ] - | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ true | _ ⇒ false ] - | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ true | _ ⇒ false ] - | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ true | _ ⇒ false ] - | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ true | _ ⇒ false ] - | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ true | _ ⇒ false ] - | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ true | _ ⇒ false ] - | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ true | _ ⇒ false ] - | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ true | _ ⇒ false ] - | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ true | _ ⇒ false ] - | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ true | _ ⇒ false ] - | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ] - | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eq_oct n1 n2 | _ ⇒ false ] - ]. - -(* iteratore sulle modalita' *) -ndefinition forall_HC08_im ≝ λP:HC08_instr_mode → bool. - P MODE_INH -⊗ P MODE_INHA -⊗ P MODE_INHX -⊗ P MODE_INHH -⊗ P MODE_INHX0ADD -⊗ P MODE_INHX1ADD -⊗ P MODE_INHX2ADD -⊗ P MODE_IMM1 -⊗ P MODE_IMM1EXT -⊗ P MODE_IMM2 -⊗ P MODE_DIR1 -⊗ P MODE_DIR2 -⊗ P MODE_IX0 -⊗ P MODE_IX1 -⊗ P MODE_IX2 -⊗ P MODE_SP1 -⊗ P MODE_SP2 -⊗ P MODE_DIR1_to_DIR1 -⊗ P MODE_IMM1_to_DIR1 -⊗ P MODE_IX0p_to_DIR1 -⊗ P MODE_DIR1_to_IX0p -⊗ P MODE_INHA_and_IMM1 -⊗ P MODE_INHX_and_IMM1 -⊗ P MODE_IMM1_and_IMM1 -⊗ P MODE_DIR1_and_IMM1 -⊗ P MODE_IX0_and_IMM1 -⊗ P MODE_IX0p_and_IMM1 -⊗ P MODE_IX1_and_IMM1 -⊗ P MODE_IX1p_and_IMM1 -⊗ P MODE_SP1_and_IMM1 -⊗ forall_oct (λo. P (MODE_DIRn o)) -⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o)). diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_instr_mode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_instr_mode_lemmas.ma deleted file mode 100755 index 100bcef31..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_instr_mode_lemmas.ma +++ /dev/null @@ -1,70 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_lemmas.ma". -include "emulator/opcodes/HC08_instr_mode.ma". -include "num/oct_lemmas.ma". - -nlemma eq_to_eqHC08im : ∀n1,n2.n1 = n2 → eq_HC08_im n1 n2 = true. - #n1; #n2; #H; - nrewrite > H; - nelim n2; - ##[ ##31,32: #o; nrewrite > (eq_to_eqoct … (refl_eq …)) ##] - nnormalize; - napply refl_eq. -nqed. - -nlemma neqHC08im_to_neq : ∀n1,n2.eq_HC08_im n1 n2 = false → n1 ≠ n2. - #n1; #n2; #H; - napply (not_to_not (n1 = n2) (eq_HC08_im n1 n2 = true) …); - ##[ ##1: napply (eq_to_eqHC08im n1 n2) - ##| ##2: napply (eqfalse_to_neqtrue … H) - ##] -nqed. - -(* !!! per brevita... *) -naxiom eqHC08im_to_eq : ∀c1,c2.eq_HC08_im c1 c2 = true → c1 = c2. - -nlemma neq_to_neqHC08im : ∀n1,n2.n1 ≠ n2 → eq_HC08_im n1 n2 = false. - #n1; #n2; #H; - napply (neqtrue_to_eqfalse (eq_HC08_im n1 n2)); - napply (not_to_not (eq_HC08_im n1 n2 = true) (n1 = n2) ? H); - napply (eqHC08im_to_eq n1 n2). -nqed. - -nlemma decidable_HC08im : ∀x,y:HC08_instr_mode.decidable (x = y). - #x; #y; nnormalize; - napply (or2_elim (eq_HC08_im x y = true) (eq_HC08_im x y = false) ? (decidable_bexpr ?)); - ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqHC08im_to_eq … H)) - ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqHC08im_to_neq … H)) - ##] -nqed. - -nlemma symmetric_eqHC08im : symmetricT HC08_instr_mode bool eq_HC08_im. - #n1; #n2; - napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_HC08im n1 n2)); - ##[ ##1: #H; nrewrite > H; napply refl_eq - ##| ##2: #H; nrewrite > (neq_to_neqHC08im n1 n2 H); - napply (symmetric_eq ? (eq_HC08_im n2 n1) false); - napply (neq_to_neqHC08im n2 n1 (symmetric_neq ? n1 n2 H)) - ##] -nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_opcode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_opcode.ma deleted file mode 100755 index a2a6e9295..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_opcode.ma +++ /dev/null @@ -1,182 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 HC08_opcode: Type ≝ - ADC : HC08_opcode (* add with carry *) -| ADD : HC08_opcode (* add *) -| AIS : HC08_opcode (* add immediate to SP *) -| AIX : HC08_opcode (* add immediate to X *) -| AND : HC08_opcode (* and *) -| ASL : HC08_opcode (* aritmetic shift left *) -| ASR : HC08_opcode (* aritmetic shift right *) -| BCC : HC08_opcode (* branch if C=0 *) -| BCLRn : HC08_opcode (* clear bit n *) -| BCS : HC08_opcode (* branch if C=1 *) -| BEQ : HC08_opcode (* branch if Z=1 *) -| BGE : HC08_opcode (* branch if N⊙V=0 (great or equal) *) -| BGT : HC08_opcode (* branch if Z|N⊙V=0 clear (great) *) -| BHCC : HC08_opcode (* branch if H=0 *) -| BHCS : HC08_opcode (* branch if H=1 *) -| BHI : HC08_opcode (* branch if C|Z=0, (higher) *) -| BIH : HC08_opcode (* branch if nIRQ=1 *) -| BIL : HC08_opcode (* branch if nIRQ=0 *) -| BIT : HC08_opcode (* flag = and (bit test) *) -| BLE : HC08_opcode (* branch if Z|N⊙V=1 (less or equal) *) -| BLS : HC08_opcode (* branch if C|Z=1 (lower or same) *) -| BLT : HC08_opcode (* branch if N⊙1=1 (less) *) -| BMC : HC08_opcode (* branch if I=0 (interrupt mask clear) *) -| BMI : HC08_opcode (* branch if N=1 (minus) *) -| BMS : HC08_opcode (* branch if I=1 (interrupt mask set) *) -| BNE : HC08_opcode (* branch if Z=0 *) -| BPL : HC08_opcode (* branch if N=0 (plus) *) -| BRA : HC08_opcode (* branch always *) -| BRCLRn : HC08_opcode (* branch if bit n clear *) -| BRN : HC08_opcode (* branch never (nop) *) -| BRSETn : HC08_opcode (* branch if bit n set *) -| BSETn : HC08_opcode (* set bit n *) -| BSR : HC08_opcode (* branch to subroutine *) -| CBEQA : HC08_opcode (* compare (A) and BEQ *) -| CBEQX : HC08_opcode (* compare (X) and BEQ *) -| CLC : HC08_opcode (* C=0 *) -| CLI : HC08_opcode (* I=0 *) -| CLR : HC08_opcode (* operand=0 *) -| CMP : HC08_opcode (* flag = sub (compare A) *) -| COM : HC08_opcode (* not (1 complement) *) -| CPHX : HC08_opcode (* flag = sub (compare H:X) *) -| CPX : HC08_opcode (* flag = sub (compare X) *) -| DAA : HC08_opcode (* decimal adjust A *) -| DBNZ : HC08_opcode (* dec and BNE *) -| DEC : HC08_opcode (* operand=operand-1 (decrement) *) -| DIV : HC08_opcode (* div *) -| EOR : HC08_opcode (* xor *) -| INC : HC08_opcode (* operand=operand+1 (increment) *) -| JMP : HC08_opcode (* jmp word [operand] *) -| JSR : HC08_opcode (* jmp to subroutine *) -| LDA : HC08_opcode (* load in A *) -| LDHX : HC08_opcode (* load in H:X *) -| LDX : HC08_opcode (* load in X *) -| LSR : HC08_opcode (* logical shift right *) -| MOV : HC08_opcode (* move *) -| MUL : HC08_opcode (* mul *) -| NEG : HC08_opcode (* neg (2 complement) *) -| NOP : HC08_opcode (* nop *) -| NSA : HC08_opcode (* nibble swap A (al:ah <- ah:al) *) -| ORA : HC08_opcode (* or *) -| PSHA : HC08_opcode (* push A *) -| PSHH : HC08_opcode (* push H *) -| PSHX : HC08_opcode (* push X *) -| PULA : HC08_opcode (* pop A *) -| PULH : HC08_opcode (* pop H *) -| PULX : HC08_opcode (* pop X *) -| ROL : HC08_opcode (* rotate left *) -| ROR : HC08_opcode (* rotate right *) -| RSP : HC08_opcode (* reset SP (0x00FF) *) -| RTI : HC08_opcode (* return from interrupt *) -| RTS : HC08_opcode (* return from subroutine *) -| SBC : HC08_opcode (* sub with carry*) -| SEC : HC08_opcode (* C=1 *) -| SEI : HC08_opcode (* I=1 *) -| STA : HC08_opcode (* store from A *) -| STHX : HC08_opcode (* store from H:X *) -| STOP : HC08_opcode (* !!stop mode!! *) -| STX : HC08_opcode (* store from X *) -| SUB : HC08_opcode (* sub *) -| SWI : HC08_opcode (* software interrupt *) -| TAP : HC08_opcode (* flag=A (transfer A to process status byte *) -| TAX : HC08_opcode (* X=A (transfer A to X) *) -| TPA : HC08_opcode (* A=flag (transfer process status byte to A) *) -| TST : HC08_opcode (* flag = sub (test) *) -| TSX : HC08_opcode (* X:H=SP (transfer SP to H:X) *) -| TXA : HC08_opcode (* A=X (transfer X to A) *) -| TXS : HC08_opcode (* SP=X:H (transfer H:X to SP) *) -| WAIT : HC08_opcode (* !!wait mode!! *) -. - -ndefinition eq_HC08_op ≝ -λop1,op2:HC08_opcode. - match op1 with - [ ADC ⇒ match op2 with [ ADC ⇒ true | _ ⇒ false ] | ADD ⇒ match op2 with [ ADD ⇒ true | _ ⇒ false ] - | AIS ⇒ match op2 with [ AIS ⇒ true | _ ⇒ false ] | AIX ⇒ match op2 with [ AIX ⇒ true | _ ⇒ false ] - | AND ⇒ match op2 with [ AND ⇒ true | _ ⇒ false ] | ASL ⇒ match op2 with [ ASL ⇒ true | _ ⇒ false ] - | ASR ⇒ match op2 with [ ASR ⇒ true | _ ⇒ false ] | BCC ⇒ match op2 with [ BCC ⇒ true | _ ⇒ false ] - | BCLRn ⇒ match op2 with [ BCLRn ⇒ true | _ ⇒ false ] | BCS ⇒ match op2 with [ BCS ⇒ true | _ ⇒ false ] - | BEQ ⇒ match op2 with [ BEQ ⇒ true | _ ⇒ false ] | BGE ⇒ match op2 with [ BGE ⇒ true | _ ⇒ false ] - | BGT ⇒ match op2 with [ BGT ⇒ true | _ ⇒ false ] | BHCC ⇒ match op2 with [ BHCC ⇒ true | _ ⇒ false ] - | BHCS ⇒ match op2 with [ BHCS ⇒ true | _ ⇒ false ] | BHI ⇒ match op2 with [ BHI ⇒ true | _ ⇒ false ] - | BIH ⇒ match op2 with [ BIH ⇒ true | _ ⇒ false ] | BIL ⇒ match op2 with [ BIL ⇒ true | _ ⇒ false ] - | BIT ⇒ match op2 with [ BIT ⇒ true | _ ⇒ false ] | BLE ⇒ match op2 with [ BLE ⇒ true | _ ⇒ false ] - | BLS ⇒ match op2 with [ BLS ⇒ true | _ ⇒ false ] | BLT ⇒ match op2 with [ BLT ⇒ true | _ ⇒ false ] - | BMC ⇒ match op2 with [ BMC ⇒ true | _ ⇒ false ] | BMI ⇒ match op2 with [ BMI ⇒ true | _ ⇒ false ] - | BMS ⇒ match op2 with [ BMS ⇒ true | _ ⇒ false ] | BNE ⇒ match op2 with [ BNE ⇒ true | _ ⇒ false ] - | BPL ⇒ match op2 with [ BPL ⇒ true | _ ⇒ false ] | BRA ⇒ match op2 with [ BRA ⇒ true | _ ⇒ false ] - | BRCLRn ⇒ match op2 with [ BRCLRn ⇒ true | _ ⇒ false ] | BRN ⇒ match op2 with [ BRN ⇒ true | _ ⇒ false ] - | BRSETn ⇒ match op2 with [ BRSETn ⇒ true | _ ⇒ false ] | BSETn ⇒ match op2 with [ BSETn ⇒ true | _ ⇒ false ] - | BSR ⇒ match op2 with [ BSR ⇒ true | _ ⇒ false ] | CBEQA ⇒ match op2 with [ CBEQA ⇒ true | _ ⇒ false ] - | CBEQX ⇒ match op2 with [ CBEQX ⇒ true | _ ⇒ false ] | CLC ⇒ match op2 with [ CLC ⇒ true | _ ⇒ false ] - | CLI ⇒ match op2 with [ CLI ⇒ true | _ ⇒ false ] | CLR ⇒ match op2 with [ CLR ⇒ true | _ ⇒ false ] - | CMP ⇒ match op2 with [ CMP ⇒ true | _ ⇒ false ] | COM ⇒ match op2 with [ COM ⇒ true | _ ⇒ false ] - | CPHX ⇒ match op2 with [ CPHX ⇒ true | _ ⇒ false ] | CPX ⇒ match op2 with [ CPX ⇒ true | _ ⇒ false ] - | DAA ⇒ match op2 with [ DAA ⇒ true | _ ⇒ false ] | DBNZ ⇒ match op2 with [ DBNZ ⇒ true | _ ⇒ false ] - | DEC ⇒ match op2 with [ DEC ⇒ true | _ ⇒ false ] | DIV ⇒ match op2 with [ DIV ⇒ true | _ ⇒ false ] - | EOR ⇒ match op2 with [ EOR ⇒ true | _ ⇒ false ] | INC ⇒ match op2 with [ INC ⇒ true | _ ⇒ false ] - | JMP ⇒ match op2 with [ JMP ⇒ true | _ ⇒ false ] | JSR ⇒ match op2 with [ JSR ⇒ true | _ ⇒ false ] - | LDA ⇒ match op2 with [ LDA ⇒ true | _ ⇒ false ] | LDHX ⇒ match op2 with [ LDHX ⇒ true | _ ⇒ false ] - | LDX ⇒ match op2 with [ LDX ⇒ true | _ ⇒ false ] | LSR ⇒ match op2 with [ LSR ⇒ true | _ ⇒ false ] - | MOV ⇒ match op2 with [ MOV ⇒ true | _ ⇒ false ] | MUL ⇒ match op2 with [ MUL ⇒ true | _ ⇒ false ] - | NEG ⇒ match op2 with [ NEG ⇒ true | _ ⇒ false ] | NOP ⇒ match op2 with [ NOP ⇒ true | _ ⇒ false ] - | NSA ⇒ match op2 with [ NSA ⇒ true | _ ⇒ false ] | ORA ⇒ match op2 with [ ORA ⇒ true | _ ⇒ false ] - | PSHA ⇒ match op2 with [ PSHA ⇒ true | _ ⇒ false ] | PSHH ⇒ match op2 with [ PSHH ⇒ true | _ ⇒ false ] - | PSHX ⇒ match op2 with [ PSHX ⇒ true | _ ⇒ false ] | PULA ⇒ match op2 with [ PULA ⇒ true | _ ⇒ false ] - | PULH ⇒ match op2 with [ PULH ⇒ true | _ ⇒ false ] | PULX ⇒ match op2 with [ PULX ⇒ true | _ ⇒ false ] - | ROL ⇒ match op2 with [ ROL ⇒ true | _ ⇒ false ] | ROR ⇒ match op2 with [ ROR ⇒ true | _ ⇒ false ] - | RSP ⇒ match op2 with [ RSP ⇒ true | _ ⇒ false ] | RTI ⇒ match op2 with [ RTI ⇒ true | _ ⇒ false ] - | RTS ⇒ match op2 with [ RTS ⇒ true | _ ⇒ false ] | SBC ⇒ match op2 with [ SBC ⇒ true | _ ⇒ false ] - | SEC ⇒ match op2 with [ SEC ⇒ true | _ ⇒ false ] | SEI ⇒ match op2 with [ SEI ⇒ true | _ ⇒ false ] - | STA ⇒ match op2 with [ STA ⇒ true | _ ⇒ false ] | STHX ⇒ match op2 with [ STHX ⇒ true | _ ⇒ false ] - | STOP ⇒ match op2 with [ STOP ⇒ true | _ ⇒ false ] | STX ⇒ match op2 with [ STX ⇒ true | _ ⇒ false ] - | SUB ⇒ match op2 with [ SUB ⇒ true | _ ⇒ false ] | SWI ⇒ match op2 with [ SWI ⇒ true | _ ⇒ false ] - | TAP ⇒ match op2 with [ TAP ⇒ true | _ ⇒ false ] | TAX ⇒ match op2 with [ TAX ⇒ true | _ ⇒ false ] - | TPA ⇒ match op2 with [ TPA ⇒ true | _ ⇒ false ] | TST ⇒ match op2 with [ TST ⇒ true | _ ⇒ false ] - | TSX ⇒ match op2 with [ TSX ⇒ true | _ ⇒ false ] | TXA ⇒ match op2 with [ TXA ⇒ true | _ ⇒ false ] - | TXS ⇒ match op2 with [ TXS ⇒ true | _ ⇒ false ] | WAIT ⇒ match op2 with [ WAIT ⇒ true | _ ⇒ false ] - ]. - -(* iteratore sugli opcode *) -ndefinition forall_HC08_op ≝ λP:HC08_opcode → bool. - P ADC ⊗ P ADD ⊗ P AIS ⊗ P AIX ⊗ P AND ⊗ P ASL ⊗ P ASR ⊗ P BCC ⊗ - P BCLRn ⊗ P BCS ⊗ P BEQ ⊗ P BGE ⊗ P BGT ⊗ P BHCC ⊗ P BHCS ⊗ P BHI ⊗ - P BIH ⊗ P BIL ⊗ P BIT ⊗ P BLE ⊗ P BLS ⊗ P BLT ⊗ P BMC ⊗ P BMI ⊗ - P BMS ⊗ P BNE ⊗ P BPL ⊗ P BRA ⊗ P BRCLRn ⊗ P BRN ⊗ P BRSETn ⊗ P BSETn ⊗ - P BSR ⊗ P CBEQA ⊗ P CBEQX ⊗ P CLC ⊗ P CLI ⊗ P CLR ⊗ P CMP ⊗ P COM ⊗ - P CPHX ⊗ P CPX ⊗ P DAA ⊗ P DBNZ ⊗ P DEC ⊗ P DIV ⊗ P EOR ⊗ P INC ⊗ - P JMP ⊗ P JSR ⊗ P LDA ⊗ P LDHX ⊗ P LDX ⊗ P LSR ⊗ P MOV ⊗ P MUL ⊗ - P NEG ⊗ P NOP ⊗ P NSA ⊗ P ORA ⊗ P PSHA ⊗ P PSHH ⊗ P PSHX ⊗ P PULA ⊗ - P PULH ⊗ P PULX ⊗ P ROL ⊗ P ROR ⊗ P RSP ⊗ P RTI ⊗ P RTS ⊗ P SBC ⊗ - P SEC ⊗ P SEI ⊗ P STA ⊗ P STHX ⊗ P STOP ⊗ P STX ⊗ P SUB ⊗ P SWI ⊗ - P TAP ⊗ P TAX ⊗ P TPA ⊗ P TST ⊗ P TSX ⊗ P TXA ⊗ P TXS ⊗ P WAIT. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_opcode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_opcode_lemmas.ma deleted file mode 100755 index e346c4890..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC08_opcode_lemmas.ma +++ /dev/null @@ -1,68 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_lemmas.ma". -include "emulator/opcodes/HC08_opcode.ma". - -nlemma eq_to_eqHC08op : ∀n1,n2.n1 = n2 → eq_HC08_op n1 n2 = true. - #n1; #n2; #H; - nrewrite > H; - nelim n2; - nnormalize; - napply refl_eq. -nqed. - -nlemma neqHC08op_to_neq : ∀n1,n2.eq_HC08_op n1 n2 = false → n1 ≠ n2. - #n1; #n2; #H; - napply (not_to_not (n1 = n2) (eq_HC08_op n1 n2 = true) …); - ##[ ##1: napply (eq_to_eqHC08op n1 n2) - ##| ##2: napply (eqfalse_to_neqtrue … H) - ##] -nqed. - -(* !!! per brevita... *) -naxiom eqHC08op_to_eq : ∀c1,c2.eq_HC08_op c1 c2 = true → c1 = c2. - -nlemma neq_to_neqHC08op : ∀n1,n2.n1 ≠ n2 → eq_HC08_op n1 n2 = false. - #n1; #n2; #H; - napply (neqtrue_to_eqfalse (eq_HC08_op n1 n2)); - napply (not_to_not (eq_HC08_op n1 n2 = true) (n1 = n2) ? H); - napply (eqHC08op_to_eq n1 n2). -nqed. - -nlemma decidable_HC08op : ∀x,y:HC08_opcode.decidable (x = y). - #x; #y; nnormalize; - napply (or2_elim (eq_HC08_op x y = true) (eq_HC08_op x y = false) ? (decidable_bexpr ?)); - ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqHC08op_to_eq … H)) - ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqHC08op_to_neq … H)) - ##] -nqed. - -nlemma symmetric_eqHC08op : symmetricT HC08_opcode bool eq_HC08_op. - #n1; #n2; - napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_HC08op n1 n2)); - ##[ ##1: #H; nrewrite > H; napply refl_eq - ##| ##2: #H; nrewrite > (neq_to_neqHC08op n1 n2 H); - napply (symmetric_eq ? (eq_HC08_op n2 n1) false); - napply (neq_to_neqHC08op n2 n1 (symmetric_neq ? n1 n2 H)) - ##] -nqed. 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 9a0ec7478..a0a7300f5 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 @@ -20,8 +20,8 @@ (* *) (* ********************************************************************** *) -include "emulator/opcodes/HC08_opcode.ma". -include "emulator/opcodes/HC08_instr_mode.ma". +include "emulator/opcodes/Freescale_pseudo.ma". +include "emulator/opcodes/Freescale_instr_mode.ma". include "emulator/opcodes/byte_or_word.ma". include "common/list.ma". 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 4e29e87fc..7c02884ee 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 @@ -20,7 +20,7 @@ (* *) (* ********************************************************************** *) -include "emulator/opcodes/opcode.ma". +include "emulator/opcodes/pseudo.ma". include "emulator/opcodes/HC08_table.ma". (* ***************** *) @@ -35,14 +35,12 @@ ndefinition HC08_not_impl_byte ≝ ;〈xA,xC〉 ]. -(* test bytecode non implementati *) -(* !!! per brevita... *) -(*nlemma ok_byte_table_HC08 : forall_b8 (λb. +nlemma ok_byte_table_HC08 : forall_b8 (λb. (test_not_impl_byte b HC08_not_impl_byte ⊙ eq_w16 (get_byte_count HC08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗ (⊖ (test_not_impl_byte b HC08_not_impl_byte) ⊙ eq_w16 (get_byte_count HC08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x0〉〉)) = true. napply refl_eq. -nqed.*) +nqed. (* HC08: opcode non implementati come da manuale (0x9E+byte) *) ndefinition HC08_not_impl_word ≝ @@ -77,36 +75,49 @@ ndefinition HC08_not_impl_word ≝ ;〈xF,x8〉;〈xF,x9〉;〈xF,xA〉;〈xF,xB〉;〈xF,xC〉;〈xF,xD〉;〈xF,xE〉;〈xF,xF〉 ]. -(* test bytecode non implementati *) -(* !!! per brevita... *) -(*nlemma ok_word_table_HC08 : forall_b8 (λb. +nlemma ok_word_table_HC08 : forall_b8 (λb. (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.*) +nqed. -(* tutti op implementati *) -(* !!! per brevita... *) -(*nlemma ok_pseudo_table_HC08 : - forall_op HC08 (λo. - le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count HC08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08)) = true. +(* HC08: pseudocodici non implementati come da manuale *) +ndefinition HC08_not_impl_pseudo ≝ + [ BGND ; SHA ; SLA ]. + +nlemma ok_pseudo_table_HC08 : forall_Freescale_pseudo (λo. + (test_not_impl_pseudo HC08 o HC08_not_impl_pseudo ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count HC08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08)) ⊗ + (⊖ (test_not_impl_pseudo HC08 o HC08_not_impl_pseudo) ⊙ eq_w16 (get_pseudo_count HC08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x0〉〉)) + = true. napply refl_eq. -nqed.*) +nqed. -(* tutte im implementate *) -(* !!! per brevita... *) -(*nlemma ok_mode_table_HC08 : - forall_im HC08 (λi. - le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count HC08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08)) = true. +(* HC08: modalita' non implementate come da manuale *) +ndefinition HC08_not_impl_mode ≝ + [ MODE_TNY x0 ; MODE_TNY x1 ; MODE_TNY x2 ; MODE_TNY x3 + ; MODE_TNY x4 ; MODE_TNY x5 ; MODE_TNY x6 ; MODE_TNY x7 + ; MODE_TNY x8 ; MODE_TNY x9 ; MODE_TNY xA ; MODE_TNY xB + ; MODE_TNY xC ; MODE_TNY xD ; MODE_TNY xE ; MODE_TNY xF + ; MODE_SRT t00 ; MODE_SRT t01 ; MODE_SRT t02 ; MODE_SRT t03 + ; MODE_SRT t04 ; MODE_SRT t05 ; MODE_SRT t06 ; MODE_SRT t07 + ; MODE_SRT t08 ; MODE_SRT t09 ; MODE_SRT t0A ; MODE_SRT t0B + ; MODE_SRT t0C ; MODE_SRT t0D ; MODE_SRT t0E ; MODE_SRT t0F + ; MODE_SRT t10 ; MODE_SRT t11 ; MODE_SRT t12 ; MODE_SRT t13 + ; MODE_SRT t14 ; MODE_SRT t15 ; MODE_SRT t16 ; MODE_SRT t17 + ; MODE_SRT t18 ; MODE_SRT t19 ; MODE_SRT t1A ; MODE_SRT t1B + ; MODE_SRT t1C ; MODE_SRT t1D ; MODE_SRT t1E ; MODE_SRT t1F ]. + +nlemma ok_mode_table_HC08 : forall_Freescale_im (λi. + (test_not_impl_mode HC08 i HC08_not_impl_mode ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count HC08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08)) ⊗ + (⊖ (test_not_impl_mode HC08 i HC08_not_impl_mode) ⊙ eq_w16 (get_mode_count HC08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x0〉〉)) + = true. napply refl_eq. -nqed.*) +nqed. -(* nessuna ripetizione di combinazione op + imm *) -(* !!! per brevita... *) -(*nlemma ok_OpIm_table_HC08 : - forall_im HC08 (λi. - forall_op HC08 (λo. - le_w16 (get_OpIm_count HC08 o i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x1〉〉)) = true. +nlemma ok_PsIm_table_HC08 : + forall_Freescale_im (λi:Freescale_instr_mode. + forall_Freescale_pseudo (λps:Freescale_pseudo. + le_w16 (get_PsIm_count HC08 ps i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x1〉〉)) = true. napply refl_eq. -nqed.*) +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_opcode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_opcode.ma deleted file mode 100755 index 2ccf39272..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_opcode.ma +++ /dev/null @@ -1,185 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 HCS08_opcode: Type ≝ - ADC : HCS08_opcode (* add with carry *) -| ADD : HCS08_opcode (* add *) -| AIS : HCS08_opcode (* add immediate to SP *) -| AIX : HCS08_opcode (* add immediate to X *) -| AND : HCS08_opcode (* and *) -| ASL : HCS08_opcode (* aritmetic shift left *) -| ASR : HCS08_opcode (* aritmetic shift right *) -| BCC : HCS08_opcode (* branch if C=0 *) -| BCLRn : HCS08_opcode (* clear bit n *) -| BCS : HCS08_opcode (* branch if C=1 *) -| BEQ : HCS08_opcode (* branch if Z=1 *) -| BGE : HCS08_opcode (* branch if N⊙V=0 (great or equal) *) -| BGND : HCS08_opcode (* !!background mode!! *) -| BGT : HCS08_opcode (* branch if Z|N⊙V=0 clear (great) *) -| BHCC : HCS08_opcode (* branch if H=0 *) -| BHCS : HCS08_opcode (* branch if H=1 *) -| BHI : HCS08_opcode (* branch if C|Z=0, (higher) *) -| BIH : HCS08_opcode (* branch if nIRQ=1 *) -| BIL : HCS08_opcode (* branch if nIRQ=0 *) -| BIT : HCS08_opcode (* flag = and (bit test) *) -| BLE : HCS08_opcode (* branch if Z|N⊙V=1 (less or equal) *) -| BLS : HCS08_opcode (* branch if C|Z=1 (lower or same) *) -| BLT : HCS08_opcode (* branch if N⊙1=1 (less) *) -| BMC : HCS08_opcode (* branch if I=0 (interrupt mask clear) *) -| BMI : HCS08_opcode (* branch if N=1 (minus) *) -| BMS : HCS08_opcode (* branch if I=1 (interrupt mask set) *) -| BNE : HCS08_opcode (* branch if Z=0 *) -| BPL : HCS08_opcode (* branch if N=0 (plus) *) -| BRA : HCS08_opcode (* branch always *) -| BRCLRn : HCS08_opcode (* branch if bit n clear *) -| BRN : HCS08_opcode (* branch never (nop) *) -| BRSETn : HCS08_opcode (* branch if bit n set *) -| BSETn : HCS08_opcode (* set bit n *) -| BSR : HCS08_opcode (* branch to subroutine *) -| CBEQA : HCS08_opcode (* compare (A) and BEQ *) -| CBEQX : HCS08_opcode (* compare (X) and BEQ *) -| CLC : HCS08_opcode (* C=0 *) -| CLI : HCS08_opcode (* I=0 *) -| CLR : HCS08_opcode (* operand=0 *) -| CMP : HCS08_opcode (* flag = sub (compare A) *) -| COM : HCS08_opcode (* not (1 complement) *) -| CPHX : HCS08_opcode (* flag = sub (compare H:X) *) -| CPX : HCS08_opcode (* flag = sub (compare X) *) -| DAA : HCS08_opcode (* decimal adjust A *) -| DBNZ : HCS08_opcode (* dec and BNE *) -| DEC : HCS08_opcode (* operand=operand-1 (decrement) *) -| DIV : HCS08_opcode (* div *) -| EOR : HCS08_opcode (* xor *) -| INC : HCS08_opcode (* operand=operand+1 (increment) *) -| JMP : HCS08_opcode (* jmp word [operand] *) -| JSR : HCS08_opcode (* jmp to subroutine *) -| LDA : HCS08_opcode (* load in A *) -| LDHX : HCS08_opcode (* load in H:X *) -| LDX : HCS08_opcode (* load in X *) -| LSR : HCS08_opcode (* logical shift right *) -| MOV : HCS08_opcode (* move *) -| MUL : HCS08_opcode (* mul *) -| NEG : HCS08_opcode (* neg (2 complement) *) -| NOP : HCS08_opcode (* nop *) -| NSA : HCS08_opcode (* nibble swap A (al:ah <- ah:al) *) -| ORA : HCS08_opcode (* or *) -| PSHA : HCS08_opcode (* push A *) -| PSHH : HCS08_opcode (* push H *) -| PSHX : HCS08_opcode (* push X *) -| PULA : HCS08_opcode (* pop A *) -| PULH : HCS08_opcode (* pop H *) -| PULX : HCS08_opcode (* pop X *) -| ROL : HCS08_opcode (* rotate left *) -| ROR : HCS08_opcode (* rotate right *) -| RSP : HCS08_opcode (* reset SP (0x00FF) *) -| RTI : HCS08_opcode (* return from interrupt *) -| RTS : HCS08_opcode (* return from subroutine *) -| SBC : HCS08_opcode (* sub with carry*) -| SEC : HCS08_opcode (* C=1 *) -| SEI : HCS08_opcode (* I=1 *) -| STA : HCS08_opcode (* store from A *) -| STHX : HCS08_opcode (* store from H:X *) -| STOP : HCS08_opcode (* !!stop mode!! *) -| STX : HCS08_opcode (* store from X *) -| SUB : HCS08_opcode (* sub *) -| SWI : HCS08_opcode (* software interrupt *) -| TAP : HCS08_opcode (* flag=A (transfer A to process status byte *) -| TAX : HCS08_opcode (* X=A (transfer A to X) *) -| TPA : HCS08_opcode (* A=flag (transfer process status byte to A) *) -| TST : HCS08_opcode (* flag = sub (test) *) -| TSX : HCS08_opcode (* X:H=SP (transfer SP to H:X) *) -| TXA : HCS08_opcode (* A=X (transfer X to A) *) -| TXS : HCS08_opcode (* SP=X:H (transfer H:X to SP) *) -| WAIT : HCS08_opcode (* !!wait mode!! *) -. - -ndefinition eq_HCS08_op ≝ -λop1,op2:HCS08_opcode. - match op1 with - [ ADC ⇒ match op2 with [ ADC ⇒ true | _ ⇒ false ] | ADD ⇒ match op2 with [ ADD ⇒ true | _ ⇒ false ] - | AIS ⇒ match op2 with [ AIS ⇒ true | _ ⇒ false ] | AIX ⇒ match op2 with [ AIX ⇒ true | _ ⇒ false ] - | AND ⇒ match op2 with [ AND ⇒ true | _ ⇒ false ] | ASL ⇒ match op2 with [ ASL ⇒ true | _ ⇒ false ] - | ASR ⇒ match op2 with [ ASR ⇒ true | _ ⇒ false ] | BCC ⇒ match op2 with [ BCC ⇒ true | _ ⇒ false ] - | BCLRn ⇒ match op2 with [ BCLRn ⇒ true | _ ⇒ false ] | BCS ⇒ match op2 with [ BCS ⇒ true | _ ⇒ false ] - | BEQ ⇒ match op2 with [ BEQ ⇒ true | _ ⇒ false ] | BGE ⇒ match op2 with [ BGE ⇒ true | _ ⇒ false ] - | BGND ⇒ match op2 with [ BGND ⇒ true | _ ⇒ false ] | BGT ⇒ match op2 with [ BGT ⇒ true | _ ⇒ false ] - | BHCC ⇒ match op2 with [ BHCC ⇒ true | _ ⇒ false ] | BHCS ⇒ match op2 with [ BHCS ⇒ true | _ ⇒ false ] - | BHI ⇒ match op2 with [ BHI ⇒ true | _ ⇒ false ] | BIH ⇒ match op2 with [ BIH ⇒ true | _ ⇒ false ] - | BIL ⇒ match op2 with [ BIL ⇒ true | _ ⇒ false ] | BIT ⇒ match op2 with [ BIT ⇒ true | _ ⇒ false ] - | BLE ⇒ match op2 with [ BLE ⇒ true | _ ⇒ false ] | BLS ⇒ match op2 with [ BLS ⇒ true | _ ⇒ false ] - | BLT ⇒ match op2 with [ BLT ⇒ true | _ ⇒ false ] | BMC ⇒ match op2 with [ BMC ⇒ true | _ ⇒ false ] - | BMI ⇒ match op2 with [ BMI ⇒ true | _ ⇒ false ] | BMS ⇒ match op2 with [ BMS ⇒ true | _ ⇒ false ] - | BNE ⇒ match op2 with [ BNE ⇒ true | _ ⇒ false ] | BPL ⇒ match op2 with [ BPL ⇒ true | _ ⇒ false ] - | BRA ⇒ match op2 with [ BRA ⇒ true | _ ⇒ false ] | BRCLRn ⇒ match op2 with [ BRCLRn ⇒ true | _ ⇒ false ] - | BRN ⇒ match op2 with [ BRN ⇒ true | _ ⇒ false ] | BRSETn ⇒ match op2 with [ BRSETn ⇒ true | _ ⇒ false ] - | BSETn ⇒ match op2 with [ BSETn ⇒ true | _ ⇒ false ] | BSR ⇒ match op2 with [ BSR ⇒ true | _ ⇒ false ] - | CBEQA ⇒ match op2 with [ CBEQA ⇒ true | _ ⇒ false ] | CBEQX ⇒ match op2 with [ CBEQX ⇒ true | _ ⇒ false ] - | CLC ⇒ match op2 with [ CLC ⇒ true | _ ⇒ false ] | CLI ⇒ match op2 with [ CLI ⇒ true | _ ⇒ false ] - | CLR ⇒ match op2 with [ CLR ⇒ true | _ ⇒ false ] | CMP ⇒ match op2 with [ CMP ⇒ true | _ ⇒ false ] - | COM ⇒ match op2 with [ COM ⇒ true | _ ⇒ false ] | CPHX ⇒ match op2 with [ CPHX ⇒ true | _ ⇒ false ] - | CPX ⇒ match op2 with [ CPX ⇒ true | _ ⇒ false ] | DAA ⇒ match op2 with [ DAA ⇒ true | _ ⇒ false ] - | DBNZ ⇒ match op2 with [ DBNZ ⇒ true | _ ⇒ false ] | DEC ⇒ match op2 with [ DEC ⇒ true | _ ⇒ false ] - | DIV ⇒ match op2 with [ DIV ⇒ true | _ ⇒ false ] | EOR ⇒ match op2 with [ EOR ⇒ true | _ ⇒ false ] - | INC ⇒ match op2 with [ INC ⇒ true | _ ⇒ false ] | JMP ⇒ match op2 with [ JMP ⇒ true | _ ⇒ false ] - | JSR ⇒ match op2 with [ JSR ⇒ true | _ ⇒ false ] | LDA ⇒ match op2 with [ LDA ⇒ true | _ ⇒ false ] - | LDHX ⇒ match op2 with [ LDHX ⇒ true | _ ⇒ false ] | LDX ⇒ match op2 with [ LDX ⇒ true | _ ⇒ false ] - | LSR ⇒ match op2 with [ LSR ⇒ true | _ ⇒ false ] | MOV ⇒ match op2 with [ MOV ⇒ true | _ ⇒ false ] - | MUL ⇒ match op2 with [ MUL ⇒ true | _ ⇒ false ] | NEG ⇒ match op2 with [ NEG ⇒ true | _ ⇒ false ] - | NOP ⇒ match op2 with [ NOP ⇒ true | _ ⇒ false ] | NSA ⇒ match op2 with [ NSA ⇒ true | _ ⇒ false ] - | ORA ⇒ match op2 with [ ORA ⇒ true | _ ⇒ false ] | PSHA ⇒ match op2 with [ PSHA ⇒ true | _ ⇒ false ] - | PSHH ⇒ match op2 with [ PSHH ⇒ true | _ ⇒ false ] | PSHX ⇒ match op2 with [ PSHX ⇒ true | _ ⇒ false ] - | PULA ⇒ match op2 with [ PULA ⇒ true | _ ⇒ false ] | PULH ⇒ match op2 with [ PULH ⇒ true | _ ⇒ false ] - | PULX ⇒ match op2 with [ PULX ⇒ true | _ ⇒ false ] | ROL ⇒ match op2 with [ ROL ⇒ true | _ ⇒ false ] - | ROR ⇒ match op2 with [ ROR ⇒ true | _ ⇒ false ] | RSP ⇒ match op2 with [ RSP ⇒ true | _ ⇒ false ] - | RTI ⇒ match op2 with [ RTI ⇒ true | _ ⇒ false ] | RTS ⇒ match op2 with [ RTS ⇒ true | _ ⇒ false ] - | SBC ⇒ match op2 with [ SBC ⇒ true | _ ⇒ false ] | SEC ⇒ match op2 with [ SEC ⇒ true | _ ⇒ false ] - | SEI ⇒ match op2 with [ SEI ⇒ true | _ ⇒ false ] | STA ⇒ match op2 with [ STA ⇒ true | _ ⇒ false ] - | STHX ⇒ match op2 with [ STHX ⇒ true | _ ⇒ false ] | STOP ⇒ match op2 with [ STOP ⇒ true | _ ⇒ false ] - | STX ⇒ match op2 with [ STX ⇒ true | _ ⇒ false ] | SUB ⇒ match op2 with [ SUB ⇒ true | _ ⇒ false ] - | SWI ⇒ match op2 with [ SWI ⇒ true | _ ⇒ false ] | TAP ⇒ match op2 with [ TAP ⇒ true | _ ⇒ false ] - | TAX ⇒ match op2 with [ TAX ⇒ true | _ ⇒ false ] | TPA ⇒ match op2 with [ TPA ⇒ true | _ ⇒ false ] - | TST ⇒ match op2 with [ TST ⇒ true | _ ⇒ false ] | TSX ⇒ match op2 with [ TSX ⇒ true | _ ⇒ false ] - | TXA ⇒ match op2 with [ TXA ⇒ true | _ ⇒ false ] | TXS ⇒ match op2 with [ TXS ⇒ true | _ ⇒ false ] - | WAIT ⇒ match op2 with [ WAIT ⇒ true | _ ⇒ false ] - ]. - -(* iteratore sugli opcode *) -ndefinition forall_HCS08_op ≝ λP:HCS08_opcode → bool. - P ADC ⊗ P ADD ⊗ P AIS ⊗ P AIX ⊗ P AND ⊗ P ASL ⊗ P ASR ⊗ P BCC ⊗ - P BCLRn ⊗ P BCS ⊗ P BEQ ⊗ P BGE ⊗ P BGND ⊗ P BGT ⊗ P BHCC ⊗ P BHCS ⊗ - P BHI ⊗ P BIH ⊗ P BIL ⊗ P BIT ⊗ P BLE ⊗ P BLS ⊗ P BLT ⊗ P BMC ⊗ - P BMI ⊗ P BMS ⊗ P BNE ⊗ P BPL ⊗ P BRA ⊗ P BRCLRn ⊗ P BRN ⊗ P BRSETn ⊗ - P BSETn ⊗ P BSR ⊗ P CBEQA ⊗ P CBEQX ⊗ P CLC ⊗ P CLI ⊗ P CLR ⊗ P CMP ⊗ - P COM ⊗ P CPHX ⊗ P CPX ⊗ P DAA ⊗ P DBNZ ⊗ P DEC ⊗ P DIV ⊗ P EOR ⊗ - P INC ⊗ P JMP ⊗ P JSR ⊗ P LDA ⊗ P LDHX ⊗ P LDX ⊗ P LSR ⊗ P MOV ⊗ - P MUL ⊗ P NEG ⊗ P NOP ⊗ P NSA ⊗ P ORA ⊗ P PSHA ⊗ P PSHH ⊗ P PSHX ⊗ - P PULA ⊗ P PULH ⊗ P PULX ⊗ P ROL ⊗ P ROR ⊗ P RSP ⊗ P RTI ⊗ P RTS ⊗ - P SBC ⊗ P SEC ⊗ P SEI ⊗ P STA ⊗ P STHX ⊗ P STOP ⊗ P STX ⊗ P SUB ⊗ - P SWI ⊗ P TAP ⊗ P TAX ⊗ P TPA ⊗ P TST ⊗ P TSX ⊗ P TXA ⊗ P TXS ⊗ - P WAIT. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_opcode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_opcode_lemmas.ma deleted file mode 100755 index a4b1b95e2..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/HCS08_opcode_lemmas.ma +++ /dev/null @@ -1,68 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_lemmas.ma". -include "emulator/opcodes/HCS08_opcode.ma". - -nlemma eq_to_eqHCS08op : ∀n1,n2.n1 = n2 → eq_HCS08_op n1 n2 = true. - #n1; #n2; #H; - nrewrite > H; - nelim n2; - nnormalize; - napply refl_eq. -nqed. - -nlemma neqHCS08op_to_neq : ∀n1,n2.eq_HCS08_op n1 n2 = false → n1 ≠ n2. - #n1; #n2; #H; - napply (not_to_not (n1 = n2) (eq_HCS08_op n1 n2 = true) …); - ##[ ##1: napply (eq_to_eqHCS08op n1 n2) - ##| ##2: napply (eqfalse_to_neqtrue … H) - ##] -nqed. - -(* !!! per brevita... *) -naxiom eqHCS08op_to_eq : ∀c1,c2.eq_HCS08_op c1 c2 = true → c1 = c2. - -nlemma neq_to_neqHCS08op : ∀n1,n2.n1 ≠ n2 → eq_HCS08_op n1 n2 = false. - #n1; #n2; #H; - napply (neqtrue_to_eqfalse (eq_HCS08_op n1 n2)); - napply (not_to_not (eq_HCS08_op n1 n2 = true) (n1 = n2) ? H); - napply (eqHCS08op_to_eq n1 n2). -nqed. - -nlemma decidable_HCS08op : ∀x,y:HCS08_opcode.decidable (x = y). - #x; #y; nnormalize; - napply (or2_elim (eq_HCS08_op x y = true) (eq_HCS08_op x y = false) ? (decidable_bexpr ?)); - ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqHCS08op_to_eq … H)) - ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqHCS08op_to_neq … H)) - ##] -nqed. - -nlemma symmetric_eqHCS08op : symmetricT HCS08_opcode bool eq_HCS08_op. - #n1; #n2; - napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_HCS08op n1 n2)); - ##[ ##1: #H; nrewrite > H; napply refl_eq - ##| ##2: #H; nrewrite > (neq_to_neqHCS08op n1 n2 H); - napply (symmetric_eq ? (eq_HCS08_op n2 n1) false); - napply (neq_to_neqHCS08op n2 n1 (symmetric_neq ? n1 n2 H)) - ##] -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 742e8b8ee..04f3b0890 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 @@ -20,8 +20,8 @@ (* *) (* ********************************************************************** *) -include "emulator/opcodes/HCS08_opcode.ma". -include "emulator/opcodes/HC08_instr_mode.ma". +include "emulator/opcodes/Freescale_pseudo.ma". +include "emulator/opcodes/Freescale_instr_mode.ma". include "emulator/opcodes/byte_or_word.ma". include "common/list.ma". 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 e51b236a3..343f9864d 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 @@ -20,7 +20,7 @@ (* *) (* ********************************************************************** *) -include "emulator/opcodes/opcode.ma". +include "emulator/opcodes/pseudo.ma". include "emulator/opcodes/HCS08_table.ma". (* ****************** *) @@ -34,14 +34,12 @@ ndefinition HCS08_not_impl_byte ≝ ;〈xA,xC〉 ]. -(* test bytecode non implementati *) -(* !!! per brevita... *) -(*nlemma ok_byte_table_HCS08 : forall_b8 (λb. +nlemma ok_byte_table_HCS08 : forall_b8 (λb. (test_not_impl_byte b HCS08_not_impl_byte ⊙ eq_w16 (get_byte_count HCS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗ (⊖ (test_not_impl_byte b HCS08_not_impl_byte) ⊙ eq_w16 (get_byte_count HCS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉)) = true. napply refl_eq. -nqed.*) +nqed. (* HCS08: opcode non implementati come da manuale (0x9E+byte) *) ndefinition HCS08_not_impl_word ≝ @@ -72,36 +70,49 @@ ndefinition HCS08_not_impl_word ≝ ;〈xF,x0〉;〈xF,x1〉;〈xF,x2〉;〈xF,x4〉;〈xF,x5〉;〈xF,x6〉;〈xF,x7〉;〈xF,x8〉;〈xF,x9〉;〈xF,xA〉;〈xF,xB〉;〈xF,xC〉;〈xF,xD〉 ]. -(* test bytecode non implementati *) -(* !!! per brevita... *) -(*nlemma ok_word_table_HCS08 : forall_b8 (λb. +nlemma ok_word_table_HCS08 : forall_b8 (λb. (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.*) +nqed. -(* tutti op implementati *) -(* !!! per brevita... *) -(*nlemma ok_pseudo_table_HCS08 : - forall_op HCS08 (λo. - le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count HCS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08)) = true. +(* HCS08: pseudocodici non implementati come da manuale *) +ndefinition HCS08_not_impl_pseudo ≝ + [ SHA ; SLA ]. + +nlemma ok_pseudo_table_HCS08 : forall_Freescale_pseudo (λo. + (test_not_impl_pseudo HCS08 o HCS08_not_impl_pseudo ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count HCS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08)) ⊗ + (⊖ (test_not_impl_pseudo HCS08 o HCS08_not_impl_pseudo) ⊙ eq_w16 (get_pseudo_count HCS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉)) + = true. napply refl_eq. -nqed.*) +nqed. -(* tutte im implementate *) -(* !!! per brevita... *) -(*nlemma ok_mode_table_HCS08 : - forall_im HCS08 (λi. - le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count HCS08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08)) = true. +(* HCS08: modalita' non implementate come da manuale *) +ndefinition HCS08_not_impl_mode ≝ + [ MODE_TNY x0 ; MODE_TNY x1 ; MODE_TNY x2 ; MODE_TNY x3 + ; MODE_TNY x4 ; MODE_TNY x5 ; MODE_TNY x6 ; MODE_TNY x7 + ; MODE_TNY x8 ; MODE_TNY x9 ; MODE_TNY xA ; MODE_TNY xB + ; MODE_TNY xC ; MODE_TNY xD ; MODE_TNY xE ; MODE_TNY xF + ; MODE_SRT t00 ; MODE_SRT t01 ; MODE_SRT t02 ; MODE_SRT t03 + ; MODE_SRT t04 ; MODE_SRT t05 ; MODE_SRT t06 ; MODE_SRT t07 + ; MODE_SRT t08 ; MODE_SRT t09 ; MODE_SRT t0A ; MODE_SRT t0B + ; MODE_SRT t0C ; MODE_SRT t0D ; MODE_SRT t0E ; MODE_SRT t0F + ; MODE_SRT t10 ; MODE_SRT t11 ; MODE_SRT t12 ; MODE_SRT t13 + ; MODE_SRT t14 ; MODE_SRT t15 ; MODE_SRT t16 ; MODE_SRT t17 + ; MODE_SRT t18 ; MODE_SRT t19 ; MODE_SRT t1A ; MODE_SRT t1B + ; MODE_SRT t1C ; MODE_SRT t1D ; MODE_SRT t1E ; MODE_SRT t1F ]. + +nlemma ok_mode_table_HCS08 : forall_Freescale_im (λi. + (test_not_impl_mode HCS08 i HCS08_not_impl_mode ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count HCS08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08)) ⊗ + (⊖ (test_not_impl_mode HCS08 i HCS08_not_impl_mode) ⊙ eq_w16 (get_mode_count HCS08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉)) + = true. napply refl_eq. -nqed.*) +nqed. -(* nessuna ripetizione di combinazione op + imm *) -(* !!! per brevita... *) -(*nlemma ok_OpIm_table_HCS08 : - forall_im HCS08 (λi. - forall_op HCS08 (λo. - le_w16 (get_OpIm_count HCS08 o i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉)) = true. +nlemma ok_PsIm_table_HCS08 : + forall_Freescale_im (λi:Freescale_instr_mode. + forall_Freescale_pseudo (λps:Freescale_pseudo. + le_w16 (get_PsIm_count HCS08 ps i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉)) = true. napply refl_eq. -nqed.*) +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 index 45548e7b1..a12114d80 100755 --- 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 @@ -68,7 +68,6 @@ ndefinition eq_IP2022_im ≝ | 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)) 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 deleted file mode 100755 index 315862e7d..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_opcode.ma +++ /dev/null @@ -1,126 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_opcode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_opcode_lemmas.ma deleted file mode 100755 index 427bfa177..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_opcode_lemmas.ma +++ /dev/null @@ -1,68 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_lemmas.ma". -include "emulator/opcodes/IP2022_opcode.ma". - -nlemma eq_to_eqIP2022op : ∀n1,n2.n1 = n2 → eq_IP2022_op n1 n2 = true. - #n1; #n2; #H; - nrewrite > H; - nelim n2; - nnormalize; - napply refl_eq. -nqed. - -nlemma neqIP2022op_to_neq : ∀n1,n2.eq_IP2022_op n1 n2 = false → n1 ≠ n2. - #n1; #n2; #H; - napply (not_to_not (n1 = n2) (eq_IP2022_op n1 n2 = true) …); - ##[ ##1: napply (eq_to_eqIP2022op n1 n2) - ##| ##2: napply (eqfalse_to_neqtrue … H) - ##] -nqed. - -(* !!! per brevita... *) -naxiom eqIP2022op_to_eq : ∀c1,c2.eq_IP2022_op c1 c2 = true → c1 = c2. - -nlemma neq_to_neqIP2022op : ∀n1,n2.n1 ≠ n2 → eq_IP2022_op n1 n2 = false. - #n1; #n2; #H; - napply (neqtrue_to_eqfalse (eq_IP2022_op n1 n2)); - napply (not_to_not (eq_IP2022_op n1 n2 = true) (n1 = n2) ? H); - napply (eqIP2022op_to_eq n1 n2). -nqed. - -nlemma decidable_IP2022op : ∀x,y:IP2022_opcode.decidable (x = y). - #x; #y; nnormalize; - napply (or2_elim (eq_IP2022_op x y = true) (eq_IP2022_op x y = false) ? (decidable_bexpr ?)); - ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqIP2022op_to_eq … H)) - ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqIP2022op_to_neq … H)) - ##] -nqed. - -nlemma symmetric_eqIP2022op : symmetricT IP2022_opcode bool eq_IP2022_op. - #n1; #n2; - napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_IP2022op n1 n2)); - ##[ ##1: #H; nrewrite > H; napply refl_eq - ##| ##2: #H; nrewrite > (neq_to_neqIP2022op n1 n2 H); - napply (symmetric_eq ? (eq_IP2022_op n2 n1) false); - napply (neq_to_neqIP2022op n2 n1 (symmetric_neq ? n1 n2 H)) - ##] -nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.ma new file mode 100755 index 000000000..9aa26cfdb --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.ma @@ -0,0 +1,125 @@ +(**************************************************************************) +(* ___ *) +(* ||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_pseudo: Type ≝ + ADD : IP2022_pseudo (* add *) +| ADDC : IP2022_pseudo (* add with carry *) +| AND : IP2022_pseudo (* and *) +| BREAK : IP2022_pseudo (* enter break mode *) +| BREAKX : IP2022_pseudo (* enter break mode, after skip *) +| CALL : IP2022_pseudo (* subroutine call *) +| CLR : IP2022_pseudo (* clear *) +| CLRB : IP2022_pseudo (* clear bit *) +| CMP : IP2022_pseudo (* set flags according to sub *) +| CSE : IP2022_pseudo (* confront & skip if equal *) +| CSNE : IP2022_pseudo (* confront & skip if not equal *) +| CWDT : IP2022_pseudo (* clear watch dog -- not impl. ERR *) +| DEC : IP2022_pseudo (* decrement *) +| DECSNZ : IP2022_pseudo (* decrement & skip if not zero *) +| DECSZ : IP2022_pseudo (* decrement & skip if zero *) +| FERASE : IP2022_pseudo (* flash erase -- not impl. ERR *) +| FREAD : IP2022_pseudo (* flash read -- not impl. ERR *) +| FWRITE : IP2022_pseudo (* flash write -- not impl. ERR *) +| INC : IP2022_pseudo (* increment *) +| INCSNZ : IP2022_pseudo (* increment & skip if not zero *) +| INCSZ : IP2022_pseudo (* increment & skip if zero *) +| INT : IP2022_pseudo (* interrupt -- not impl. ERR *) +| IREAD : IP2022_pseudo (* memory read *) +| IREADI : IP2022_pseudo (* memory read & inc *) +| IWRITE : IP2022_pseudo (* memory write *) +| IWRITEI : IP2022_pseudo (* memory write & inc *) +| JMP : IP2022_pseudo (* jump *) +| LOADH : IP2022_pseudo (* load Data Pointer High *) +| LOADL : IP2022_pseudo (* load Data Pointer Low *) +| MOV : IP2022_pseudo (* move *) +| MULS : IP2022_pseudo (* signed mul *) +| MULU : IP2022_pseudo (* unsigned mul *) +| NOP : IP2022_pseudo (* nop *) +| NOT : IP2022_pseudo (* not *) +| OR : IP2022_pseudo (* or *) +| PAGE : IP2022_pseudo (* set Page Register *) +| POP : IP2022_pseudo (* pop *) +| PUSH : IP2022_pseudo (* push *) +| RET : IP2022_pseudo (* subroutine ret *) +| RETI : IP2022_pseudo (* interrupt ret -- not impl. ERR *) +| RETNP : IP2022_pseudo (* subroutine ret & don't restore Page Register *) +| RETW : IP2022_pseudo (* subroutine ret & load W Register *) +| RL : IP2022_pseudo (* rotate left *) +| RR : IP2022_pseudo (* rotate right *) +| SB : IP2022_pseudo (* skip if bit set *) +| SETB : IP2022_pseudo (* set bit *) +| SNB : IP2022_pseudo (* skip if bit not set *) +| SPEED : IP2022_pseudo (* set Speed Register *) +| SUB : IP2022_pseudo (* sub *) +| SUBC : IP2022_pseudo (* sub with carry *) +| SWAP : IP2022_pseudo (* swap xxxxyyyy → yyyyxxxx *) +| TEST : IP2022_pseudo (* set flags according to zero test *) +| XOR : IP2022_pseudo (* xor *) +. + +ndefinition eq_IP2022_pseudo ≝ +λps1,ps2:IP2022_pseudo. + match ps1 with + [ ADD ⇒ match ps2 with [ ADD ⇒ true | _ ⇒ false ] | ADDC ⇒ match ps2 with [ ADDC ⇒ true | _ ⇒ false ] + | AND ⇒ match ps2 with [ AND ⇒ true | _ ⇒ false ] | BREAK ⇒ match ps2 with [ BREAK ⇒ true | _ ⇒ false ] + | BREAKX ⇒ match ps2 with [ BREAKX ⇒ true | _ ⇒ false ] | CALL ⇒ match ps2 with [ CALL ⇒ true | _ ⇒ false ] + | CLR ⇒ match ps2 with [ CLR ⇒ true | _ ⇒ false ] | CLRB ⇒ match ps2 with [ CLRB ⇒ true | _ ⇒ false ] + | CMP ⇒ match ps2 with [ CMP ⇒ true | _ ⇒ false ] | CSE ⇒ match ps2 with [ CSE ⇒ true | _ ⇒ false ] + | CSNE ⇒ match ps2 with [ CSNE ⇒ true | _ ⇒ false ] | CWDT ⇒ match ps2 with [ CWDT ⇒ true | _ ⇒ false ] + | DEC ⇒ match ps2 with [ DEC ⇒ true | _ ⇒ false ] | DECSNZ ⇒ match ps2 with [ DECSNZ ⇒ true | _ ⇒ false ] + | DECSZ ⇒ match ps2 with [ DECSZ ⇒ true | _ ⇒ false ] | FERASE ⇒ match ps2 with [ FERASE ⇒ true | _ ⇒ false ] + | FREAD ⇒ match ps2 with [ FREAD ⇒ true | _ ⇒ false ] | FWRITE ⇒ match ps2 with [ FWRITE ⇒ true | _ ⇒ false ] + | INC ⇒ match ps2 with [ INC ⇒ true | _ ⇒ false ] | INCSNZ ⇒ match ps2 with [ INCSNZ ⇒ true | _ ⇒ false ] + | INCSZ ⇒ match ps2 with [ INCSZ ⇒ true | _ ⇒ false ] | INT ⇒ match ps2 with [ INT ⇒ true | _ ⇒ false ] + | IREAD ⇒ match ps2 with [ IREAD ⇒ true | _ ⇒ false ] | IREADI ⇒ match ps2 with [ IREADI ⇒ true | _ ⇒ false ] + | IWRITE ⇒ match ps2 with [ IWRITE ⇒ true | _ ⇒ false ] | IWRITEI ⇒ match ps2 with [ IWRITEI ⇒ true | _ ⇒ false ] + | JMP ⇒ match ps2 with [ JMP ⇒ true | _ ⇒ false ] | LOADH ⇒ match ps2 with [ LOADH ⇒ true | _ ⇒ false ] + | LOADL ⇒ match ps2 with [ LOADL ⇒ true | _ ⇒ false ] | MOV ⇒ match ps2 with [ MOV ⇒ true | _ ⇒ false ] + | MULS ⇒ match ps2 with [ MULS ⇒ true | _ ⇒ false ] | MULU ⇒ match ps2 with [ MULU ⇒ true | _ ⇒ false ] + | NOP ⇒ match ps2 with [ NOP ⇒ true | _ ⇒ false ] | NOT ⇒ match ps2 with [ NOT ⇒ true | _ ⇒ false ] + | OR ⇒ match ps2 with [ OR ⇒ true | _ ⇒ false ] | PAGE ⇒ match ps2 with [ PAGE ⇒ true | _ ⇒ false ] + | POP ⇒ match ps2 with [ POP ⇒ true | _ ⇒ false ] | PUSH ⇒ match ps2 with [ PUSH ⇒ true | _ ⇒ false ] + | RET ⇒ match ps2 with [ RET ⇒ true | _ ⇒ false ] | RETI ⇒ match ps2 with [ RETI ⇒ true | _ ⇒ false ] + | RETNP ⇒ match ps2 with [ RETNP ⇒ true | _ ⇒ false ] | RETW ⇒ match ps2 with [ RETW ⇒ true | _ ⇒ false ] + | RL ⇒ match ps2 with [ RL ⇒ true | _ ⇒ false ] | RR ⇒ match ps2 with [ RR ⇒ true | _ ⇒ false ] + | SB ⇒ match ps2 with [ SB ⇒ true | _ ⇒ false ] | SETB ⇒ match ps2 with [ SETB ⇒ true | _ ⇒ false ] + | SNB ⇒ match ps2 with [ SNB ⇒ true | _ ⇒ false ] | SPEED ⇒ match ps2 with [ SPEED ⇒ true | _ ⇒ false ] + | SUB ⇒ match ps2 with [ SUB ⇒ true | _ ⇒ false ] | SUBC ⇒ match ps2 with [ SUBC ⇒ true | _ ⇒ false ] + | SWAP ⇒ match ps2 with [ SWAP ⇒ true | _ ⇒ false ] | TEST ⇒ match ps2 with [ TEST ⇒ true | _ ⇒ false ] + | XOR ⇒ match ps2 with [ XOR ⇒ true | _ ⇒ false ] + ]. + +ndefinition forall_IP2022_pseudo ≝ λP:IP2022_pseudo → 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_pseudo_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo_lemmas.ma new file mode 100644 index 000000000..2bf69d98d --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo_lemmas.ma @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lemmas.ma". +include "emulator/opcodes/IP2022_pseudo.ma". + +nlemma eq_to_eqIP2022pseudo : ∀n1,n2.n1 = n2 → eq_IP2022_pseudo n1 n2 = true. + #n1; #n2; #H; + nrewrite > H; + nelim n2; + nnormalize; + napply refl_eq. +nqed. + +nlemma neqIP2022pseudo_to_neq : ∀n1,n2.eq_IP2022_pseudo n1 n2 = false → n1 ≠ n2. + #n1; #n2; #H; + napply (not_to_not (n1 = n2) (eq_IP2022_pseudo n1 n2 = true) …); + ##[ ##1: napply (eq_to_eqIP2022pseudo n1 n2) + ##| ##2: napply (eqfalse_to_neqtrue … H) + ##] +nqed. + +(* !!! per brevita... *) +naxiom eqIP2022pseudo_to_eq : ∀c1,c2.eq_IP2022_pseudo c1 c2 = true → c1 = c2. + +nlemma neq_to_neqIP2022pseudo : ∀n1,n2.n1 ≠ n2 → eq_IP2022_pseudo n1 n2 = false. + #n1; #n2; #H; + napply (neqtrue_to_eqfalse (eq_IP2022_pseudo n1 n2)); + napply (not_to_not (eq_IP2022_pseudo n1 n2 = true) (n1 = n2) ? H); + napply (eqIP2022pseudo_to_eq n1 n2). +nqed. + +nlemma decidable_IP2022pseudo : ∀x,y:IP2022_pseudo.decidable (x = y). + #x; #y; nnormalize; + napply (or2_elim (eq_IP2022_pseudo x y = true) (eq_IP2022_pseudo x y = false) ? (decidable_bexpr ?)); + ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqIP2022pseudo_to_eq … H)) + ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqIP2022pseudo_to_neq … H)) + ##] +nqed. + +nlemma symmetric_eqIP2022pseudo : symmetricT IP2022_pseudo bool eq_IP2022_pseudo. + #n1; #n2; + napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_IP2022pseudo n1 n2)); + ##[ ##1: #H; nrewrite > H; napply refl_eq + ##| ##2: #H; nrewrite > (neq_to_neqIP2022pseudo n1 n2 H); + napply (symmetric_eq ? (eq_IP2022_pseudo n2 n1) false); + napply (neq_to_neqIP2022pseudo n2 n1 (symmetric_neq ? n1 n2 H)) + ##] +nqed. 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 index 0cddf72bc..0125d0506 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table.ma @@ -20,7 +20,7 @@ (* *) (* ********************************************************************** *) -include "emulator/opcodes/IP2022_opcode.ma". +include "emulator/opcodes/IP2022_pseudo.ma". include "emulator/opcodes/IP2022_instr_mode.ma". include "emulator/opcodes/byte_or_word.ma". include "common/list.ma". 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 index 798d25f99..3640054ac 100755 --- 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 @@ -20,7 +20,7 @@ (* *) (* ********************************************************************** *) -include "emulator/opcodes/opcode.ma". +include "emulator/opcodes/pseudo.ma". include "emulator/opcodes/IP2022_table.ma". (* ******************* *) @@ -33,8 +33,6 @@ ndefinition IP2022_not_impl_byte ≝ ;〈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 *) -(* !!! per brevita... *) (*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〉〉)) @@ -75,36 +73,30 @@ ndefinition IP2022_not_impl_word ≝ ;〈xF,x8〉;〈xF,x9〉;〈xF,xA〉;〈xF,xB〉;〈xF,xC〉;〈xF,xD〉;〈xF,xE〉;〈xF,xF〉 ]. -(* test bytecode non implementati *) -(* !!! per brevita... *) -(*nlemma ok_word_table_IP2022 : forall_b8 (λb. +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.*) +nqed. -(* tutti op implementati *) -(* !!! per brevita... *) -(*nlemma ok_pseudo_table_IP2022 : - forall_op IP2022 (λo. +(* tutti gli pseudo implementati *) +nlemma ok_pseudo_table_IP2022 : + forall_IP2022_pseudo (λo. le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count IP2022 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022)) = true. napply refl_eq. -nqed.*) +nqed. -(* tutte im implementate *) -(* !!! per brevita... *) -(*nlemma ok_mode_table_IP2022 : - forall_im IP2022 (λi. +(* tutte le modalita' implementate *) +nlemma ok_mode_table_IP2022 : + forall_IP2022_im (λi. le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count IP2022 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022)) = true. napply refl_eq. -nqed.*) +nqed. -(* nessuna ripetizione di combinazione op + imm *) -(* !!! per brevita... *) -(*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. +nlemma ok_PsIm_table_IP2022 : + forall_IP2022_im (λi. + forall_IP2022_pseudo (λps. + le_w16 (get_PsIm_count IP2022 ps i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022) 〈〈x0,x0〉:〈x0,x1〉〉)) = true. napply refl_eq. -nqed.*) +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_instr_mode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_instr_mode.ma deleted file mode 100755 index 0d5a311b3..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_instr_mode.ma +++ /dev/null @@ -1,102 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 RS08_instr_mode: Type ≝ - (* INHERENT = nessun operando *) - MODE_INH : RS08_instr_mode - (* INHERENT = nessun operando (A implicito) *) -| MODE_INHA : RS08_instr_mode - - (* IMMEDIATE = operando valore immediato byte = 0xbb *) -| MODE_IMM1 : RS08_instr_mode - (* IMMEDIATE = operando valore immediato word = 0xwwww *) -| MODE_IMM2 : RS08_instr_mode - (* DIRECT = operando offset byte = [0x00bb] *) -| MODE_DIR1 : RS08_instr_mode - - (* DIRECT → DIRECT = carica da diretto/scrive su diretto *) -| MODE_DIR1_to_DIR1 : RS08_instr_mode - (* IMMEDIATE → DIRECT = carica da immediato/scrive su diretto *) -| MODE_IMM1_to_DIR1 : RS08_instr_mode - - (* INHERENT(A) + IMMEDIATE *) -| MODE_INHA_and_IMM1 : RS08_instr_mode - (* IMMEDIATE + IMMEDIATE *) -| MODE_IMM1_and_IMM1 : RS08_instr_mode - (* DIRECT + IMMEDIATE *) -| MODE_DIR1_and_IMM1 : RS08_instr_mode - - (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *) - (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *) -| MODE_DIRn : oct → RS08_instr_mode - (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *) - (* + operando valore immediato byte *) - (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *) -| MODE_DIRn_and_IMM1 : oct → RS08_instr_mode - (* TINY = nessun operando (diretto implicito 4bit = [0x00000000:0000iiii]) *) -| MODE_TNY : exadecim → RS08_instr_mode - (* SHORT = nessun operando (diretto implicito 5bit = [0x00000000:000iiiii]) *) -| MODE_SRT : bitrigesim → RS08_instr_mode -. - -ndefinition eq_RS08_im ≝ -λi1,i2:RS08_instr_mode. - match i1 with - [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ] - | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ] - | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ] - | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ] - | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ] - | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ true | _ ⇒ false ] - | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ true | _ ⇒ false ] - | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ true | _ ⇒ false ] - | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ] - | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eq_oct n1 n2 | _ ⇒ false ] - | MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eq_ex e1 e2 | _ ⇒ false ] - | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bit t1 t2 | _ ⇒ false ] - ]. - -(* iteratore sulle modalita' *) -ndefinition forall_RS08_im ≝ λP:RS08_instr_mode → bool. - P MODE_INH -⊗ P MODE_INHA -⊗ P MODE_IMM1 -⊗ P MODE_IMM2 -⊗ P MODE_DIR1 -⊗ P MODE_DIR1_to_DIR1 -⊗ P MODE_IMM1_to_DIR1 -⊗ P MODE_INHA_and_IMM1 -⊗ P MODE_IMM1_and_IMM1 -⊗ P MODE_DIR1_and_IMM1 -⊗ forall_oct (λo. P (MODE_DIRn o)) -⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o)) -⊗ forall_ex (λe. P (MODE_TNY e)) -⊗ forall_bit (λt. P (MODE_SRT t)). diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_instr_mode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_instr_mode_lemmas.ma deleted file mode 100755 index aa834fbb7..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_instr_mode_lemmas.ma +++ /dev/null @@ -1,74 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_lemmas.ma". -include "emulator/opcodes/RS08_instr_mode.ma". -include "num/oct_lemmas.ma". -include "num/exadecim_lemmas.ma". -include "num/bitrigesim_lemmas.ma". - -nlemma eq_to_eqRS08im : ∀n1,n2.n1 = n2 → eq_RS08_im n1 n2 = true. - #n1; #n2; #H; - nrewrite > H; - nelim n2; - ##[ ##11,12: #o; nrewrite > (eq_to_eqoct … (refl_eq …)) - ##| ##13: #e; nrewrite > (eq_to_eqex … (refl_eq …)) - ##| ##14: #t; nrewrite > (eq_to_eqbit … (refl_eq …)) ##] - nnormalize; - napply refl_eq. -nqed. - -nlemma neqRS08im_to_neq : ∀n1,n2.eq_RS08_im n1 n2 = false → n1 ≠ n2. - #n1; #n2; #H; - napply (not_to_not (n1 = n2) (eq_RS08_im n1 n2 = true) …); - ##[ ##1: napply (eq_to_eqRS08im n1 n2) - ##| ##2: napply (eqfalse_to_neqtrue … H) - ##] -nqed. - -(* !!! per brevita... *) -naxiom eqRS08im_to_eq : ∀c1,c2.eq_RS08_im c1 c2 = true → c1 = c2. - -nlemma neq_to_neqRS08im : ∀n1,n2.n1 ≠ n2 → eq_RS08_im n1 n2 = false. - #n1; #n2; #H; - napply (neqtrue_to_eqfalse (eq_RS08_im n1 n2)); - napply (not_to_not (eq_RS08_im n1 n2 = true) (n1 = n2) ? H); - napply (eqRS08im_to_eq n1 n2). -nqed. - -nlemma decidable_RS08im : ∀x,y:RS08_instr_mode.decidable (x = y). - #x; #y; nnormalize; - napply (or2_elim (eq_RS08_im x y = true) (eq_RS08_im x y = false) ? (decidable_bexpr ?)); - ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqRS08im_to_eq … H)) - ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqRS08im_to_neq … H)) - ##] -nqed. - -nlemma symmetric_eqRS08im : symmetricT RS08_instr_mode bool eq_RS08_im. - #n1; #n2; - napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_RS08im n1 n2)); - ##[ ##1: #H; nrewrite > H; napply refl_eq - ##| ##2: #H; nrewrite > (neq_to_neqRS08im n1 n2 H); - napply (symmetric_eq ? (eq_RS08_im n2 n1) false); - napply (neq_to_neqRS08im n2 n1 (symmetric_neq ? n1 n2 H)) - ##] -nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_opcode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_opcode.ma deleted file mode 100755 index 9bdb8f42d..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_opcode.ma +++ /dev/null @@ -1,108 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 RS08_opcode: Type ≝ - ADC : RS08_opcode (* add with carry *) -| ADD : RS08_opcode (* add *) -| AND : RS08_opcode (* and *) -| ASL : RS08_opcode (* aritmetic shift left *) -| BCC : RS08_opcode (* branch if C=0 *) -| BCLRn : RS08_opcode (* clear bit n *) -| BCS : RS08_opcode (* branch if C=1 *) -| BEQ : RS08_opcode (* branch if Z=1 *) -| BGND : RS08_opcode (* !!background mode!! *) -| BNE : RS08_opcode (* branch if Z=0 *) -| BRA : RS08_opcode (* branch always *) -| BRCLRn : RS08_opcode (* branch if bit n clear *) -| BRSETn : RS08_opcode (* branch if bit n set *) -| BSETn : RS08_opcode (* set bit n *) -| BSR : RS08_opcode (* branch to subroutine *) -| CBEQA : RS08_opcode (* compare (A) and BEQ *) -| CLC : RS08_opcode (* C=0 *) -| CLR : RS08_opcode (* operand=0 *) -| CMP : RS08_opcode (* flag = sub (compare A) *) -| COM : RS08_opcode (* not (1 complement) *) -| DBNZ : RS08_opcode (* dec and BNE *) -| DEC : RS08_opcode (* operand=operand-1 (decrement) *) -| EOR : RS08_opcode (* xor *) -| INC : RS08_opcode (* operand=operand+1 (increment) *) -| JMP : RS08_opcode (* jmp word [operand] *) -| JSR : RS08_opcode (* jmp to subroutine *) -| LDA : RS08_opcode (* load in A *) -| LSR : RS08_opcode (* logical shift right *) -| MOV : RS08_opcode (* move *) -| NOP : RS08_opcode (* nop *) -| ORA : RS08_opcode (* or *) -| ROL : RS08_opcode (* rotate left *) -| ROR : RS08_opcode (* rotate right *) -| RTS : RS08_opcode (* return from subroutine *) -| SBC : RS08_opcode (* sub with carry*) -| SEC : RS08_opcode (* C=1 *) -| SHA : RS08_opcode (* swap spc_high,A *) -| SLA : RS08_opcode (* swap spc_low,A *) -| STA : RS08_opcode (* store from A *) -| STOP : RS08_opcode (* !!stop mode!! *) -| SUB : RS08_opcode (* sub *) -| WAIT : RS08_opcode (* !!wait mode!! *) -. - -ndefinition eq_RS08_op ≝ -λop1,op2:RS08_opcode. - match op1 with - [ ADC ⇒ match op2 with [ ADC ⇒ true | _ ⇒ false ] | ADD ⇒ match op2 with [ ADD ⇒ true | _ ⇒ false ] - | AND ⇒ match op2 with [ AND ⇒ true | _ ⇒ false ] | ASL ⇒ match op2 with [ ASL ⇒ true | _ ⇒ false ] - | BCC ⇒ match op2 with [ BCC ⇒ true | _ ⇒ false ] | BCLRn ⇒ match op2 with [ BCLRn ⇒ true | _ ⇒ false ] - | BCS ⇒ match op2 with [ BCS ⇒ true | _ ⇒ false ] | BEQ ⇒ match op2 with [ BEQ ⇒ true | _ ⇒ false ] - | BGND ⇒ match op2 with [ BGND ⇒ true | _ ⇒ false ] | BNE ⇒ match op2 with [ BNE ⇒ true | _ ⇒ false ] - | BRA ⇒ match op2 with [ BRA ⇒ true | _ ⇒ false ] | BRCLRn ⇒ match op2 with [ BRCLRn ⇒ true | _ ⇒ false ] - | BRSETn ⇒ match op2 with [ BRSETn ⇒ true | _ ⇒ false ] | BSETn ⇒ match op2 with [ BSETn ⇒ true | _ ⇒ false ] - | BSR ⇒ match op2 with [ BSR ⇒ true | _ ⇒ false ] | CBEQA ⇒ match op2 with [ CBEQA ⇒ true | _ ⇒ false ] - | CLC ⇒ match op2 with [ CLC ⇒ true | _ ⇒ false ] | CLR ⇒ match op2 with [ CLR ⇒ true | _ ⇒ false ] - | CMP ⇒ match op2 with [ CMP ⇒ true | _ ⇒ false ] | COM ⇒ match op2 with [ COM ⇒ true | _ ⇒ false ] - | DBNZ ⇒ match op2 with [ DBNZ ⇒ true | _ ⇒ false ] | DEC ⇒ match op2 with [ DEC ⇒ true | _ ⇒ false ] - | EOR ⇒ match op2 with [ EOR ⇒ true | _ ⇒ false ] | INC ⇒ match op2 with [ INC ⇒ true | _ ⇒ false ] - | JMP ⇒ match op2 with [ JMP ⇒ true | _ ⇒ false ] | JSR ⇒ match op2 with [ JSR ⇒ true | _ ⇒ false ] - | LDA ⇒ match op2 with [ LDA ⇒ true | _ ⇒ false ] | LSR ⇒ match op2 with [ LSR ⇒ true | _ ⇒ false ] - | MOV ⇒ match op2 with [ MOV ⇒ true | _ ⇒ false ] | NOP ⇒ match op2 with [ NOP ⇒ true | _ ⇒ false ] - | ORA ⇒ match op2 with [ ORA ⇒ true | _ ⇒ false ] | ROL ⇒ match op2 with [ ROL ⇒ true | _ ⇒ false ] - | ROR ⇒ match op2 with [ ROR ⇒ true | _ ⇒ false ] | RTS ⇒ match op2 with [ RTS ⇒ true | _ ⇒ false ] - | SBC ⇒ match op2 with [ SBC ⇒ true | _ ⇒ false ] | SEC ⇒ match op2 with [ SEC ⇒ true | _ ⇒ false ] - | SHA ⇒ match op2 with [ SHA ⇒ true | _ ⇒ false ] | SLA ⇒ match op2 with [ SLA ⇒ true | _ ⇒ false ] - | STA ⇒ match op2 with [ STA ⇒ true | _ ⇒ false ] | STOP ⇒ match op2 with [ STOP ⇒ true | _ ⇒ false ] - | SUB ⇒ match op2 with [ SUB ⇒ true | _ ⇒ false ] | WAIT ⇒ match op2 with [ WAIT ⇒ true | _ ⇒ false ] - ]. - -(* iteratore sugli opcode *) -ndefinition forall_RS08_op ≝ λP:RS08_opcode → bool. - P ADC ⊗ P ADD ⊗ P AND ⊗ P ASL ⊗ P BCC ⊗ P BCLRn ⊗ P BCS ⊗ P BEQ ⊗ - P BGND ⊗ P BNE ⊗ P BRA ⊗ P BRCLRn ⊗ P BRSETn ⊗ P BSETn ⊗ P BSR ⊗ P CBEQA ⊗ - P CLC ⊗ P CLR ⊗ P CMP ⊗ P COM ⊗ P DBNZ ⊗ P DEC ⊗ P EOR ⊗ P INC ⊗ - P JMP ⊗ P JSR ⊗ P LDA ⊗ P LSR ⊗ P MOV ⊗ P NOP ⊗ P ORA ⊗ P ROL ⊗ - P ROR ⊗ P RTS ⊗ P SBC ⊗ P SEC ⊗ P SHA ⊗ P SLA ⊗ P STA ⊗ P STOP ⊗ - P SUB ⊗ P WAIT. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_opcode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_opcode_lemmas.ma deleted file mode 100755 index 0046e1094..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_opcode_lemmas.ma +++ /dev/null @@ -1,68 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_lemmas.ma". -include "emulator/opcodes/RS08_opcode.ma". - -nlemma eq_to_eqRS08op : ∀n1,n2.n1 = n2 → eq_RS08_op n1 n2 = true. - #n1; #n2; #H; - nrewrite > H; - nelim n2; - nnormalize; - napply refl_eq. -nqed. - -nlemma neqRS08op_to_neq : ∀n1,n2.eq_RS08_op n1 n2 = false → n1 ≠ n2. - #n1; #n2; #H; - napply (not_to_not (n1 = n2) (eq_RS08_op n1 n2 = true) …); - ##[ ##1: napply (eq_to_eqRS08op n1 n2) - ##| ##2: napply (eqfalse_to_neqtrue … H) - ##] -nqed. - -(* !!! per brevita... *) -naxiom eqRS08op_to_eq : ∀c1,c2.eq_RS08_op c1 c2 = true → c1 = c2. - -nlemma neq_to_neqRS08op : ∀n1,n2.n1 ≠ n2 → eq_RS08_op n1 n2 = false. - #n1; #n2; #H; - napply (neqtrue_to_eqfalse (eq_RS08_op n1 n2)); - napply (not_to_not (eq_RS08_op n1 n2 = true) (n1 = n2) ? H); - napply (eqRS08op_to_eq n1 n2). -nqed. - -nlemma decidable_RS08op : ∀x,y:RS08_opcode.decidable (x = y). - #x; #y; nnormalize; - napply (or2_elim (eq_RS08_op x y = true) (eq_RS08_op x y = false) ? (decidable_bexpr ?)); - ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqRS08op_to_eq … H)) - ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqRS08op_to_neq … H)) - ##] -nqed. - -nlemma symmetric_eqRS08op : symmetricT RS08_opcode bool eq_RS08_op. - #n1; #n2; - napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_RS08op n1 n2)); - ##[ ##1: #H; nrewrite > H; napply refl_eq - ##| ##2: #H; nrewrite > (neq_to_neqRS08op n1 n2 H); - napply (symmetric_eq ? (eq_RS08_op n2 n1) false); - napply (neq_to_neqRS08op n2 n1 (symmetric_neq ? n1 n2 H)) - ##] -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 56fa8b5fa..5640c506a 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 @@ -20,8 +20,8 @@ (* *) (* ********************************************************************** *) -include "emulator/opcodes/RS08_opcode.ma". -include "emulator/opcodes/RS08_instr_mode.ma". +include "emulator/opcodes/Freescale_pseudo.ma". +include "emulator/opcodes/Freescale_instr_mode.ma". include "emulator/opcodes/byte_or_word.ma". include "common/list.ma". diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_table_tests.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_table_tests.ma index 73f1c0ad2..143724ca3 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_table_tests.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_table_tests.ma @@ -20,7 +20,7 @@ (* *) (* ********************************************************************** *) -include "emulator/opcodes/opcode.ma". +include "emulator/opcodes/pseudo.ma". include "emulator/opcodes/RS08_table.ma". (* ***************** *) @@ -35,36 +35,44 @@ ndefinition RS08_not_impl_byte ≝ ;〈xB,x3〉;〈xB,x5〉 ]. -(* test bytecode non implementati *) -(* !!! per brevita... *) -(*nlemma ok_byte_table_RS08 : forall_b8 (λb. +nlemma ok_byte_table_RS08 : forall_b8 (λb. (test_not_impl_byte b RS08_not_impl_byte ⊙ eq_w16 (get_byte_count RS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗ (⊖ (test_not_impl_byte b RS08_not_impl_byte) ⊙ eq_w16 (get_byte_count RS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08) 〈〈x0,x0〉:〈x0,x0〉〉)) = true. napply refl_eq. -nqed.*) +nqed. -(* tutti op implementati *) -(* !!! per brevita... *) -(*nlemma ok_pseudo_table_RS08 : - forall_op RS08 (λo. - le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count RS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08)) = true. +(* RS08: pseudocodici non implementati come da manuale *) +ndefinition RS08_not_impl_pseudo ≝ + [ AIS ; AIX ; ASR ; BGE ; BGT ; BHCC ; BHCS ; BHI ; BIH ; BIL ; BIT ; BLE ; BLS + ; BLT ; BMC ; BMI ; BMS ; BPL ; BRN ; CBEQX ; CLI ; CPHX ; CPX ; DAA ; DIV + ; LDHX ; LDX ; MUL ; NEG ; NSA ; PSHA ; PSHH ; PSHX ; PULA ; PULH ; PULX ; RSP + ; RTI ; SEI ; STHX ; STX ; SWI ; TAP ; TAX ; TPA ; TST ; TSX ; TXA ; TXS ]. + +nlemma ok_pseudo_table_RS08 : forall_Freescale_pseudo (λo. + (test_not_impl_pseudo RS08 o RS08_not_impl_pseudo ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count RS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08)) ⊗ + (⊖ (test_not_impl_pseudo RS08 o RS08_not_impl_pseudo) ⊙ eq_w16 (get_pseudo_count RS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08) 〈〈x0,x0〉:〈x0,x0〉〉)) + = true. napply refl_eq. -nqed.*) +nqed. -(* tutte im implementate *) -(* !!! per brevita... *) -(*nlemma ok_mode_table_RS08 : - forall_im RS08 (λi. - le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count RS08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08)) = true. +(* RS08: modalita' non implementate come da manuale *) +ndefinition RS08_not_impl_mode ≝ + [ MODE_INHX ; MODE_INHH ; MODE_INHX0ADD ; MODE_INHX1ADD ; MODE_INHX2ADD ; MODE_IMM1EXT + ; MODE_DIR2 ; MODE_IX0 ; MODE_IX1 ; MODE_IX2 ; MODE_SP1 ; MODE_SP2 + ; MODE_IX0p_to_DIR1 ; MODE_DIR1_to_IX0p ; MODE_INHX_and_IMM1 ; MODE_IX0_and_IMM1 + ; MODE_IX0p_and_IMM1 ; MODE_IX1_and_IMM1 ; MODE_IX1p_and_IMM1 ; MODE_SP1_and_IMM1 ]. + +nlemma ok_mode_table_RS08 : forall_Freescale_im (λi. + (test_not_impl_mode RS08 i RS08_not_impl_mode ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count RS08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08)) ⊗ + (⊖ (test_not_impl_mode RS08 i RS08_not_impl_mode) ⊙ eq_w16 (get_mode_count RS08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08) 〈〈x0,x0〉:〈x0,x0〉〉)) + = true. napply refl_eq. -nqed.*) +nqed. -(* nessuna ripetizione di combinazione op + imm *) -(* !!! per brevita... *) -(*nlemma ok_OpIm_table_RS08 : - forall_im RS08 (λi. - forall_op RS08 (λo. - le_w16 (get_OpIm_count RS08 o i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08) 〈〈x0,x0〉:〈x0,x1〉〉)) = true. +nlemma ok_PsIm_table_RS08 : + forall_Freescale_im (λi:Freescale_instr_mode. + forall_Freescale_pseudo (λps:Freescale_pseudo. + le_w16 (get_PsIm_count RS08 ps i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_RS08) 〈〈x0,x0〉:〈x0,x1〉〉)) = true. napply refl_eq. -nqed.*) +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode.ma deleted file mode 100755 index 4c3f8c849..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode.ma +++ /dev/null @@ -1,195 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/HC05_opcode.ma". -include "emulator/opcodes/HC05_instr_mode.ma". -include "emulator/opcodes/HC08_opcode.ma". -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". - -(* ********************************************** *) -(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *) -(* ********************************************** *) - -(* enumerazione delle ALU *) -ninductive mcu_type: Type ≝ - HC05 : mcu_type -| HC08 : mcu_type -| HCS08 : mcu_type -| RS08 : mcu_type -| IP2022 : mcu_type. - -ndefinition eq_mcutype ≝ -λm1,m2:mcu_type. - match m1 with - [ HC05 ⇒ match m2 with [ HC05 ⇒ true | _ ⇒ false ] - | 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 ≝ -λmcu:mcu_type.match mcu with - [ HC05 ⇒ HC05_opcode - | HC08 ⇒ HC08_opcode - | HCS08 ⇒ HCS08_opcode - | RS08 ⇒ RS08_opcode - | IP2022 ⇒ IP2022_opcode - ]. - -ndefinition aux_im_type ≝ -λmcu:mcu_type.match mcu with - [ HC05 ⇒ HC05_instr_mode - | HC08 ⇒ HC08_instr_mode - | HCS08 ⇒ HC08_instr_mode - | RS08 ⇒ RS08_instr_mode - | IP2022 ⇒ IP2022_instr_mode - ]. - -ndefinition eq_op ≝ -λmcu:mcu_type. - match mcu - return λm.aux_op_type m → aux_op_type m → bool - with - [ HC05 ⇒ eq_HC05_op - | HC08 ⇒ eq_HC08_op - | HCS08 ⇒ eq_HCS08_op - | RS08 ⇒ eq_RS08_op - | IP2022 ⇒ eq_IP2022_op - ]. - -ndefinition eq_im ≝ -λmcu:mcu_type. - match mcu - return λm.aux_im_type m → aux_im_type m → bool - with - [ HC05 ⇒ eq_HC05_im - | HC08 ⇒ eq_HC08_im - | HCS08 ⇒ eq_HC08_im - | RS08 ⇒ eq_RS08_im - | IP2022 ⇒ eq_IP2022_im - ]. - -ndefinition forall_op ≝ -λmcu:mcu_type. - match mcu - return λm.(aux_op_type m → bool) → bool - with - [ HC05 ⇒ forall_HC05_op - | HC08 ⇒ forall_HC08_op - | HCS08 ⇒ forall_HCS08_op - | RS08 ⇒ forall_RS08_op - | IP2022 ⇒ forall_IP2022_op - ]. - -ndefinition forall_im ≝ -λmcu:mcu_type. - match mcu - return λm.(aux_im_type m → bool) → bool - with - [ HC05 ⇒ forall_HC05_im - | HC08 ⇒ forall_HC08_im - | HCS08 ⇒ forall_HC08_im - | RS08 ⇒ forall_RS08_im - | IP2022 ⇒ forall_IP2022_im - ]. - -(* ********************************************* *) -(* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *) -(* ********************************************* *) - -ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_op_type mcu) (aux_im_type mcu) byte8_or_word16 byte8. - -(* su tutta la lista quante volte compare il byte *) -nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝ - match l with - [ nil ⇒ c - | cons hd tl ⇒ match thd4T … hd with - [ Byte b' ⇒ match eq_b8 b b' with - [ true ⇒ get_byte_count m b (succ_w16 c) tl - | false ⇒ get_byte_count m b c tl - ] - | Word _ ⇒ get_byte_count m b c tl - ] - ]. - -(* 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 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 - ] - ] - ]. - -(* su tutta la lista quante volte compare lo pseudocodice *) -nlet rec get_pseudo_count (m:mcu_type) (o:aux_op_type m) (c:word16) (l:list (aux_table_type m)) on l ≝ - match l with - [ nil ⇒ c - | cons hd tl ⇒ match eq_op m o (fst4T … hd) with - [ true ⇒ get_pseudo_count m o (succ_w16 c) tl - | false ⇒ get_pseudo_count m o c tl - ] - ]. - -(* su tutta la lista quante volte compare la modalita' *) -nlet rec get_mode_count (m:mcu_type) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝ - match l with - [ nil ⇒ c - | cons hd tl ⇒ match eq_im m i (snd4T … hd) with - [ true ⇒ get_mode_count m i (succ_w16 c) tl - | false ⇒ get_mode_count m i c tl - ] - ]. - -(* b e' non implementato? *) -nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝ - match l with - [ nil ⇒ false - | cons hd tl ⇒ match eq_b8 b hd with - [ true ⇒ true - | false ⇒ test_not_impl_byte b 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 - [ nil ⇒ c - | cons hd tl ⇒ - match (eq_op m o (fst4T … hd)) ⊗ - (eq_im m i (snd4T … hd)) with - [ true ⇒ get_OpIm_count m o i (succ_w16 c) tl - | false ⇒ get_OpIm_count m o i c tl - ] - ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode_lemmas.ma deleted file mode 100755 index bb12d86a0..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode_lemmas.ma +++ /dev/null @@ -1,152 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/HC05_opcode_lemmas.ma". -include "emulator/opcodes/HC05_instr_mode_lemmas.ma". -include "emulator/opcodes/HC08_opcode_lemmas.ma". -include "emulator/opcodes/HC08_instr_mode_lemmas.ma". -include "emulator/opcodes/HCS08_opcode_lemmas.ma". -include "emulator/opcodes/RS08_opcode_lemmas.ma". -include "emulator/opcodes/RS08_instr_mode_lemmas.ma". -include "emulator/opcodes/IP2022_opcode_lemmas.ma". -include "emulator/opcodes/IP2022_instr_mode_lemmas.ma". -include "emulator/opcodes/opcode.ma". - -nlemma eq_to_eqop : ∀m.∀n1,n2.(n1 = n2) → (eq_op m n1 n2 = true). - #m; nelim m; - ##[ ##1: napply eq_to_eqHC05op - ##| ##2: napply eq_to_eqHC08op - ##| ##3: napply eq_to_eqHCS08op - ##| ##4: napply eq_to_eqRS08op - ##| ##5: napply eq_to_eqIP2022op - ##] -nqed. - -nlemma neqop_to_neq : ∀m.∀n1,n2.(eq_op m n1 n2 = false) → (n1 ≠ n2). - #m; nelim m; - ##[ ##1: napply neqHC05op_to_neq - ##| ##2: napply neqHC08op_to_neq - ##| ##3: napply neqHCS08op_to_neq - ##| ##4: napply neqRS08op_to_neq - ##| ##5: napply neqIP2022op_to_neq - ##] -nqed. - -nlemma eqop_to_eq : ∀m.∀n1,n2.(eq_op m n1 n2 = true) → (n1 = n2). - #m; nelim m; - ##[ ##1: napply eqHC05op_to_eq - ##| ##2: napply eqHC08op_to_eq - ##| ##3: napply eqHCS08op_to_eq - ##| ##4: napply eqRS08op_to_eq - ##| ##5: napply eqIP2022op_to_eq - ##] -nqed. - -nlemma neq_to_neqop : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_op m n1 n2 = false). - #m; nelim m; - ##[ ##1: napply neq_to_neqHC05op - ##| ##2: napply neq_to_neqHC08op - ##| ##3: napply neq_to_neqHCS08op - ##| ##4: napply neq_to_neqRS08op - ##| ##5: napply neq_to_neqIP2022op - ##] -nqed. - -nlemma decidable_op : ∀m.∀x,y:aux_op_type m.decidable (x = y). - #m; nelim m; - ##[ ##1: napply decidable_HC05op - ##| ##2: napply decidable_HC08op - ##| ##3: napply decidable_HCS08op - ##| ##4: napply decidable_RS08op - ##| ##5: napply decidable_IP2022op - ##] -nqed. - -nlemma symmetric_eqop : ∀m.symmetricT (aux_op_type m) bool (eq_op m). - #m; nelim m; - ##[ ##1: napply symmetric_eqHC05op - ##| ##2: napply symmetric_eqHC08op - ##| ##3: napply symmetric_eqHCS08op - ##| ##4: napply symmetric_eqRS08op - ##| ##5: napply symmetric_eqIP2022op - ##] -nqed. - -nlemma eq_to_eqim : ∀m.∀n1,n2.(n1 = n2) → (eq_im m n1 n2 = true). - #m; nelim m; - ##[ ##1: napply eq_to_eqHC05im - ##| ##2: napply eq_to_eqHC08im - ##| ##3: napply eq_to_eqHC08im - ##| ##4: napply eq_to_eqRS08im - ##| ##5: napply eq_to_eqIP2022im - ##] -nqed. - -nlemma neqim_to_neq : ∀m.∀n1,n2.(eq_im m n1 n2 = false) → (n1 ≠ n2). - #m; nelim m; - ##[ ##1: napply neqHC05im_to_neq - ##| ##2: napply neqHC08im_to_neq - ##| ##3: napply neqHC08im_to_neq - ##| ##4: napply neqRS08im_to_neq - ##| ##5: napply neqIP2022im_to_neq - ##] -nqed. - -nlemma eqim_to_eq : ∀m.∀n1,n2.(eq_im m n1 n2 = true) → (n1 = n2). - #m; nelim m; - ##[ ##1: napply eqHC05im_to_eq - ##| ##2: napply eqHC08im_to_eq - ##| ##3: napply eqHC08im_to_eq - ##| ##4: napply eqRS08im_to_eq - ##| ##5: napply eqIP2022im_to_eq - ##] -nqed. - -nlemma neq_to_neqim : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_im m n1 n2 = false). - #m; nelim m; - ##[ ##1: napply neq_to_neqHC05im - ##| ##2: napply neq_to_neqHC08im - ##| ##3: napply neq_to_neqHC08im - ##| ##4: napply neq_to_neqRS08im - ##| ##5: napply neq_to_neqIP2022im - ##] -nqed. - -nlemma decidable_im : ∀m.∀x,y:aux_im_type m.decidable (x = y). - #m; nelim m; - ##[ ##1: napply decidable_HC05im - ##| ##2: napply decidable_HC08im - ##| ##3: napply decidable_HC08im - ##| ##4: napply decidable_RS08im - ##| ##5: napply decidable_IP2022im - ##] -nqed. - -nlemma symmetric_eqim : ∀m.symmetricT (aux_im_type m) bool (eq_im m). - #m; nelim m; - ##[ ##1: napply symmetric_eqHC05im - ##| ##2: napply symmetric_eqHC08im - ##| ##3: napply symmetric_eqHC08im - ##| ##4: napply symmetric_eqRS08im - ##| ##5: napply symmetric_eqIP2022im - ##] -nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/pseudo.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/pseudo.ma new file mode 100755 index 000000000..8e583418b --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/pseudo.ma @@ -0,0 +1,210 @@ +(**************************************************************************) +(* ___ *) +(* ||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/Freescale_pseudo.ma". +include "emulator/opcodes/Freescale_instr_mode.ma". +include "emulator/opcodes/IP2022_pseudo.ma". +include "emulator/opcodes/IP2022_instr_mode.ma". +include "emulator/opcodes/byte_or_word.ma". +include "common/list.ma". + +(* ********************************************** *) +(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *) +(* ********************************************** *) + +(* enumerazione delle ALU *) +ninductive mcu_type: Type ≝ + HC05 : mcu_type +| HC08 : mcu_type +| HCS08 : mcu_type +| RS08 : mcu_type +| IP2022 : mcu_type. + +ndefinition eq_mcutype ≝ +λm1,m2:mcu_type. + match m1 with + [ HC05 ⇒ match m2 with [ HC05 ⇒ true | _ ⇒ false ] + | 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_pseudo_type ≝ +λmcu:mcu_type.match mcu with + [ HC05 ⇒ Freescale_pseudo + | HC08 ⇒ Freescale_pseudo + | HCS08 ⇒ Freescale_pseudo + | RS08 ⇒ Freescale_pseudo + | IP2022 ⇒ IP2022_pseudo + ]. + +ndefinition aux_im_type ≝ +λmcu:mcu_type.match mcu with + [ HC05 ⇒ Freescale_instr_mode + | HC08 ⇒ Freescale_instr_mode + | HCS08 ⇒ Freescale_instr_mode + | RS08 ⇒ Freescale_instr_mode + | IP2022 ⇒ IP2022_instr_mode + ]. + +ndefinition eq_pseudo ≝ +λmcu:mcu_type. + match mcu + return λm.aux_pseudo_type m → aux_pseudo_type m → bool + with + [ HC05 ⇒ eq_Freescale_pseudo + | HC08 ⇒ eq_Freescale_pseudo + | HCS08 ⇒ eq_Freescale_pseudo + | RS08 ⇒ eq_Freescale_pseudo + | IP2022 ⇒ eq_IP2022_pseudo + ]. + +ndefinition eq_im ≝ +λmcu:mcu_type. + match mcu + return λm.aux_im_type m → aux_im_type m → bool + with + [ HC05 ⇒ eq_Freescale_im + | HC08 ⇒ eq_Freescale_im + | HCS08 ⇒ eq_Freescale_im + | RS08 ⇒ eq_Freescale_im + | IP2022 ⇒ eq_IP2022_im + ]. + +ndefinition forall_pseudo ≝ +λmcu:mcu_type. + match mcu + return λm.(aux_pseudo_type m → bool) → bool + with + [ HC05 ⇒ forall_Freescale_pseudo + | HC08 ⇒ forall_Freescale_pseudo + | HCS08 ⇒ forall_Freescale_pseudo + | RS08 ⇒ forall_Freescale_pseudo + | IP2022 ⇒ forall_IP2022_pseudo + ]. + +ndefinition forall_im ≝ +λmcu:mcu_type. + match mcu + return λm.(aux_im_type m → bool) → bool + with + [ HC05 ⇒ forall_Freescale_im + | HC08 ⇒ forall_Freescale_im + | HCS08 ⇒ forall_Freescale_im + | RS08 ⇒ forall_Freescale_im + | IP2022 ⇒ forall_IP2022_im + ]. + +(* ********************************************* *) +(* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *) +(* ********************************************* *) + +ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 byte8. + +(* su tutta la lista quante volte compare il byte *) +nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝ + match l with + [ nil ⇒ c + | cons hd tl ⇒ match thd4T … hd with + [ Byte b' ⇒ match eq_b8 b b' with + [ true ⇒ get_byte_count m b (succ_w16 c) tl + | false ⇒ get_byte_count m b c tl + ] + | Word _ ⇒ get_byte_count m b c tl + ] + ]. + +(* 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 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 + ] + ] + ]. + +(* su tutta la lista quante volte compare lo pseudocodice *) +nlet rec get_pseudo_count (m:mcu_type) (o:aux_pseudo_type m) (c:word16) (l:list (aux_table_type m)) on l ≝ + match l with + [ nil ⇒ c + | cons hd tl ⇒ match eq_pseudo m o (fst4T … hd) with + [ true ⇒ get_pseudo_count m o (succ_w16 c) tl + | false ⇒ get_pseudo_count m o c tl + ] + ]. + +(* su tutta la lista quante volte compare la modalita' *) +nlet rec get_mode_count (m:mcu_type) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝ + match l with + [ nil ⇒ c + | cons hd tl ⇒ match eq_im m i (snd4T … hd) with + [ true ⇒ get_mode_count m i (succ_w16 c) tl + | false ⇒ get_mode_count m i c tl + ] + ]. + +(* b e' non implementato? *) +nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝ + match l with + [ nil ⇒ false + | cons hd tl ⇒ match eq_b8 b hd with + [ true ⇒ true + | false ⇒ test_not_impl_byte b tl + ] + ]. + +(* su tutta la lista quante volte compare la coppia pseudo,instr_mode *) +nlet rec get_PsIm_count (m:mcu_type) (o:aux_pseudo_type m) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝ + match l with + [ nil ⇒ c + | cons hd tl ⇒ + match (eq_pseudo m o (fst4T … hd)) ⊗ + (eq_im m i (snd4T … hd)) with + [ true ⇒ get_PsIm_count m o i (succ_w16 c) tl + | false ⇒ get_PsIm_count m o i c tl + ] + ]. + +(* o e' non implementato? *) +nlet rec test_not_impl_pseudo (m:mcu_type) (o:aux_pseudo_type m) (l:list (aux_pseudo_type m)) on l ≝ + match l with + [ nil ⇒ false + | cons hd tl ⇒ match eq_pseudo 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 + ] + ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/pseudo_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/pseudo_lemmas.ma new file mode 100755 index 000000000..2506560f2 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/pseudo_lemmas.ma @@ -0,0 +1,111 @@ +(**************************************************************************) +(* ___ *) +(* ||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/Freescale_pseudo_lemmas.ma". +include "emulator/opcodes/Freescale_instr_mode_lemmas.ma". +include "emulator/opcodes/IP2022_pseudo_lemmas.ma". +include "emulator/opcodes/IP2022_instr_mode_lemmas.ma". +include "emulator/opcodes/pseudo.ma". + +nlemma eq_to_eqpseudo : ∀m.∀n1,n2.(n1 = n2) → (eq_pseudo m n1 n2 = true). + #m; nelim m; + ##[ ##1,2,3,4: napply eq_to_eqFreescalepseudo + ##| ##5: napply eq_to_eqIP2022pseudo + ##] +nqed. + +nlemma neqpseudo_to_neq : ∀m.∀n1,n2.(eq_pseudo m n1 n2 = false) → (n1 ≠ n2). + #m; nelim m; + ##[ ##1,2,3,4: napply neqFreescalepseudo_to_neq + ##| ##5: napply neqIP2022pseudo_to_neq + ##] +nqed. + +nlemma eqpseudo_to_eq : ∀m.∀n1,n2.(eq_pseudo m n1 n2 = true) → (n1 = n2). + #m; nelim m; + ##[ ##1,2,3,4: napply eqFreescalepseudo_to_eq + ##| ##5: napply eqIP2022pseudo_to_eq + ##] +nqed. + +nlemma neq_to_neqpseudo : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_pseudo m n1 n2 = false). + #m; nelim m; + ##[ ##1,2,3,4: napply neq_to_neqFreescalepseudo + ##| ##5: napply neq_to_neqIP2022pseudo + ##] +nqed. + +nlemma decidable_pseudo : ∀m.∀x,y:aux_pseudo_type m.decidable (x = y). + #m; nelim m; + ##[ ##1,2,3,4: napply decidable_Freescalepseudo + ##| ##5: napply decidable_IP2022pseudo + ##] +nqed. + +nlemma symmetric_eqpseudo : ∀m.symmetricT (aux_pseudo_type m) bool (eq_pseudo m). + #m; nelim m; + ##[ ##1,2,3,4: napply symmetric_eqFreescalepseudo + ##| ##5: napply symmetric_eqIP2022pseudo + ##] +nqed. + +nlemma eq_to_eqim : ∀m.∀n1,n2.(n1 = n2) → (eq_im m n1 n2 = true). + #m; nelim m; + ##[ ##1,2,3,4: napply eq_to_eqFreescaleim + ##| ##5: napply eq_to_eqIP2022im + ##] +nqed. + +nlemma neqim_to_neq : ∀m.∀n1,n2.(eq_im m n1 n2 = false) → (n1 ≠ n2). + #m; nelim m; + ##[ ##1,2,3,4: napply neqFreescaleim_to_neq + ##| ##5: napply neqIP2022im_to_neq + ##] +nqed. + +nlemma eqim_to_eq : ∀m.∀n1,n2.(eq_im m n1 n2 = true) → (n1 = n2). + #m; nelim m; + ##[ ##1,2,3,4: napply eqFreescaleim_to_eq + ##| ##5: napply eqIP2022im_to_eq + ##] +nqed. + +nlemma neq_to_neqim : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_im m n1 n2 = false). + #m; nelim m; + ##[ ##1,2,3,4: napply neq_to_neqFreescaleim + ##| ##5: napply neq_to_neqIP2022im + ##] +nqed. + +nlemma decidable_im : ∀m.∀x,y:aux_im_type m.decidable (x = y). + #m; nelim m; + ##[ ##1,2,3,4: napply decidable_Freescaleim + ##| ##5: napply decidable_IP2022im + ##] +nqed. + +nlemma symmetric_eqim : ∀m.symmetricT (aux_im_type m) bool (eq_im m). + #m; nelim m; + ##[ ##1,2,3,4: napply symmetric_eqFreescaleim + ##| ##5: napply symmetric_eqIP2022im + ##] +nqed. 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 index bec7454a4..08beb8b21 100755 --- 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 @@ -61,13 +61,13 @@ ndefinition RS08_memory_filter_read_aux ≝ (* 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))〉〉 + [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) (ext_word32 〈〈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〉〉))〉) + (ext_word32 (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 ]]]]]. @@ -121,14 +121,14 @@ ndefinition RS08_memory_filter_write_aux ≝ (* 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))〉〉) + [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) (ext_word32 〈〈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〉〉))〉)) + (ext_word32 (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) diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma index 9462c455b..0456997fc 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma @@ -25,7 +25,7 @@ include "emulator/status/HC05_status.ma". include "emulator/status/HC08_status.ma". include "emulator/status/RS08_status.ma". include "emulator/status/IP2022_status.ma". -include "emulator/opcodes/opcode.ma". +include "emulator/opcodes/pseudo.ma". (* *********************************** *) (* STATUS INTERNO DEL PROCESSORE (ALU) *) diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma index aee06a2f0..48d10ecf6 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma @@ -27,7 +27,7 @@ include "emulator/status/IP2022_status_lemmas.ma". include "emulator/status/status.ma". include "common/option_lemmas.ma". include "common/prod_lemmas.ma". -include "emulator/opcodes/opcode_lemmas.ma". +include "emulator/opcodes/pseudo_lemmas.ma". (* *********************************** *) (* STATUS INTERNO DEL PROCESSORE (ALU) *) 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 8548eb583..d24a7cf44 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 @@ -20,7 +20,7 @@ (* *) (* ********************************************************************** *) -include "emulator/opcodes/opcode.ma". +include "emulator/opcodes/pseudo.ma". include "common/option.ma". include "emulator/opcodes/HC05_table.ma". include "emulator/opcodes/HC08_table.ma". diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma index b2ad856f0..9cf490eab 100755 --- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma +++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma @@ -71,6 +71,14 @@ ndefinition setMSB_b8 ≝ setOPH_cn ? setMSB_ex. ndefinition getLSB_b8 ≝ getOPL_cn ? getLSB_ex. ndefinition setLSB_b8 ≝ setOPL_cn ? setLSB_ex. +(* operatore estensione unsigned *) +ndefinition extu_b8 ≝ λe2.〈x0,e2〉. + +(* operatore estensione signed *) +ndefinition exts_b8 ≝ +λe2.〈(match getMSB_ex e2 with + [ true ⇒ xF | false ⇒ x0 ]),e2〉. + (* operatore rotazione destra con carry *) ndefinition rcr_b8 ≝ opcr_cn ? rcr_ex. diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma index df45e02a7..a6c12ec9e 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word16.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma @@ -28,6 +28,8 @@ include "num/byte8.ma". ndefinition word16 ≝ comp_num byte8. ndefinition mk_word16 ≝ λb1,b2.mk_comp_num byte8 b1 b2. +ndefinition ext_word16 ≝ λb2.mk_comp_num byte8 〈x0,x0〉 b2. +ndefinition ext2_word16 ≝ λe2.mk_comp_num byte8 〈x0,x0〉 〈x0,e2〉. (* \langle \rangle *) notation "〈x:y〉" non associative with precedence 80 @@ -68,6 +70,18 @@ ndefinition setMSB_w16 ≝ setOPH_cn ? setMSB_b8. ndefinition getLSB_w16 ≝ getOPL_cn ? getLSB_b8. ndefinition setLSB_w16 ≝ setOPL_cn ? setLSB_b8. +(* operatore estensione unsigned *) +ndefinition extu_w16 ≝ λb2.〈〈x0,x0〉:b2〉. +ndefinition extu2_w16 ≝ λe2.〈〈x0,x0〉:〈x0,e2〉〉. + +(* operatore estensione signed *) +ndefinition exts_w16 ≝ +λb2.〈(match getMSB_b8 b2 with + [ true ⇒ 〈xF,xF〉 | false ⇒ 〈x0,x0〉 ]):b2〉. +ndefinition exts2_w16 ≝ +λe2.(match getMSB_ex e2 with + [ true ⇒ 〈〈xF,xF〉:〈xF,e2〉〉 | false ⇒ 〈〈x0,x0〉:〈x0,e2〉〉 ]). + (* operatore rotazione destra con carry *) ndefinition rcr_w16 ≝ opcr_cn ? rcr_b8. diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma index 4c6d8101b..7be3a53c5 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word32.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma @@ -28,6 +28,7 @@ include "num/word16.ma". ndefinition word32 ≝ comp_num word16. ndefinition mk_word32 ≝ λw1,w2.mk_comp_num word16 w1 w2. +ndefinition ext_word32 ≝ λw2.mk_comp_num word16 〈〈x0,x0〉:〈x0,x0〉〉 w2. (* \langle \rangle *) notation "〈x.y〉" non associative with precedence 80 @@ -68,6 +69,22 @@ ndefinition setMSB_w32 ≝ setOPH_cn ? setMSB_w16. ndefinition getLSB_w32 ≝ getOPL_cn ? getLSB_w16. ndefinition setLSB_w32 ≝ setOPL_cn ? setLSB_w16. +(* operatore estensione unsigned *) +ndefinition extu_w32 ≝ λw2.〈〈〈x0,x0〉:〈x0,x0〉〉.w2〉. +ndefinition extu2_w32 ≝ λb2.〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:b2〉〉. +ndefinition extu3_w32 ≝ λe2.〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,e2〉〉〉. + +(* operatore estensione signed *) +ndefinition exts_w32 ≝ +λw2.〈(match getMSB_w16 w2 with + [ true ⇒ 〈〈xF,xF〉:〈xF,xF〉〉 | false ⇒ 〈〈x0,x0〉:〈x0,x0〉〉 ]).w2〉. +ndefinition exts2_w32 ≝ +λb2.(match getMSB_b8 b2 with + [ true ⇒ 〈〈〈xF,xF〉:〈xF,xF〉〉.〈〈xF,xF〉:b2〉〉 | false ⇒ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:b2〉〉 ]). +ndefinition exts3_w32 ≝ +λe2.(match getMSB_ex e2 with + [ true ⇒ 〈〈〈xF,xF〉:〈xF,xF〉〉.〈〈xF,xF〉:〈xF,e2〉〉〉 | false ⇒ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,e2〉〉〉 ]). + (* operatore rotazione destra con carry *) ndefinition rcr_w32 ≝ opcr_cn ? rcr_w16.