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
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
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
(* (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 ].
(* 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
]
].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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)).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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)).
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
(* *)
(* ********************************************************************** *)
-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".
(* *)
(* ********************************************************************** *)
-include "emulator/opcodes/opcode.ma".
+include "emulator/opcodes/pseudo.ma".
include "emulator/opcodes/HC05_table.ma".
(* ***************** *)
;〈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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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)).
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
(* *)
(* ********************************************************************** *)
-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".
(* *)
(* ********************************************************************** *)
-include "emulator/opcodes/opcode.ma".
+include "emulator/opcodes/pseudo.ma".
include "emulator/opcodes/HC08_table.ma".
(* ***************** *)
;〈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 ≝
;〈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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
(* *)
(* ********************************************************************** *)
-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".
(* *)
(* ********************************************************************** *)
-include "emulator/opcodes/opcode.ma".
+include "emulator/opcodes/pseudo.ma".
include "emulator/opcodes/HCS08_table.ma".
(* ****************** *)
;〈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 ≝
;〈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.
| 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))
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
(* *)
(* ********************************************************************** *)
-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".
(* *)
(* ********************************************************************** *)
-include "emulator/opcodes/opcode.ma".
+include "emulator/opcodes/pseudo.ma".
include "emulator/opcodes/IP2022_table.ma".
(* ******************* *)
;〈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〉〉))
;〈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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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)).
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
(* *)
(* ********************************************************************** *)
-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".
(* *)
(* ********************************************************************** *)
-include "emulator/opcodes/opcode.ma".
+include "emulator/opcodes/pseudo.ma".
include "emulator/opcodes/RS08_table.ma".
(* ***************** *)
;〈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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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
- ]
- ].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
+ ]
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
(* 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 ]]]]].
(* 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)
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) *)
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) *)
(* *)
(* ********************************************************************** *)
-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".
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.
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
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.
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
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.
projects / helm.git / commitdiff