-freescale/multivm_lemmas.ma common/nat_lemmas.ma freescale/multivm.ma
-freescale/status.ma freescale/opcode_base.ma memory/memory_abs.ma
common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma
-opcodes/RS08_table.ma common/list.ma opcodes/RS08_opcode_base.ma opcodes/byte_or_word.ma
+emulator/opcodes/HC05_table_tests.ma emulator/opcodes/HC05_table.ma emulator/opcodes/opcode.ma
num/bool.ma common/theory.ma
-freescale_tests/micro_tests10.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
-freescale/table_HCS08_tests.ma freescale/opcode.ma freescale/table_HCS08.ma
compiler/preast_tree.ma common/string.ma compiler/ast_type.ma num/word32.ma
-opcodes/HCS08_opcode_base.ma num/word16.ma
-freescale/multivm.ma freescale/load_write.ma
-freescale_tests/medium_tests_tools.ma freescale/multivm.ma
-freescale/opcode_base_lemmas.ma freescale/opcode_base.ma num/bool_lemmas.ma
+emulator/status/HC08_status.ma num/word16.ma
+common/nat.ma num/bool.ma
common/nat_to_num.ma common/nat.ma num/word32.ma
common/string_lemmas.ma common/ascii_lemmas.ma common/list_utility_lemmas.ma common/string.ma
-common/nat.ma num/bool.ma
compiler/ast_type_lemmas.ma common/list_utility_lemmas.ma compiler/ast_type.ma
-freescale_tests/micro_tests3.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
-memory/memory_bits.ma memory/memory_trees.ma
num/quatern.ma num/bool.ma
num/exadecim.ma common/nat.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma
-freescale/table_HC05_tests.ma freescale/opcode.ma freescale/table_HC05.ma
-opcodes/opcode.ma common/list.ma opcodes/HC05_opcode_base.ma opcodes/HC08_opcode_base.ma opcodes/HCS08_opcode_base.ma opcodes/RS08_opcode_base.ma opcodes/byte_or_word.ma
num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma
+emulator/status/status.ma emulator/memory/memory_abs.ma emulator/opcodes/opcode.ma emulator/status/HC05_status.ma emulator/status/HC08_status.ma emulator/status/RS08_status.ma
num/byte8.ma num/bitrigesim.ma num/exadecim.ma
-opcodes/HC08_opcode_base.ma num/word16.ma
-freescale_tests/micro_tests4bis.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
-freescale/load_write.ma freescale/model.ma freescale/translation.ma
-freescale/table_RS08.ma common/list.ma freescale/opcode_base.ma
+emulator/opcodes/HC08_table.ma common/list.ma emulator/opcodes/HC08_instr_mode.ma emulator/opcodes/HC08_opcode.ma emulator/opcodes/byte_or_word.ma
common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma
-freescale_tests/micro_tests6.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
+emulator/opcodes/HC05_table.ma common/list.ma emulator/opcodes/HC05_instr_mode.ma emulator/opcodes/HC05_opcode.ma emulator/opcodes/byte_or_word.ma
common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma
-opcodes/RS08_opcode_base.ma num/word16.ma
-opcodes/HC05_opcode_base.ma num/word16.ma
-freescale/table_RS08_tests.ma freescale/opcode.ma freescale/table_RS08.ma
-freescale/translation.ma common/option.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma
-freescale/translation_lemmas.ma freescale/translation.ma num/byte8_lemmas.ma
-memory/memory_func.ma common/list.ma common/option.ma memory/memory_struct.ma num/word32.ma
+emulator/translation/HCS08_translation.ma emulator/translation/translation_base.ma
+emulator/memory/memory_trees.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma
+emulator/opcodes/IP2022_opcode.ma num/bool.ma
num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma
-freescale_tests/micro_tests9.ma common/nat_to_num.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
-opcodes/HCS08_table_tests.ma freescale/opcode.ma
+emulator/opcodes/RS08_table_tests.ma emulator/opcodes/RS08_table.ma emulator/opcodes/opcode.ma
test_errori.ma
-freescale_tests/micro_tests2.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
compiler/environment.ma common/string.ma compiler/ast_type.ma
+emulator/translation/translation_base.ma common/option.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/opcode.ma
common/ascii_lemmas.ma common/ascii.ma num/bool_lemmas.ma
-freescale/model.ma freescale/status.ma
-freescale/table_HC05.ma common/list.ma freescale/opcode_base.ma
-opcodes/HC08_table.ma common/list.ma opcodes/HC08_opcode_base.ma opcodes/byte_or_word.ma
-opcodes/HC08_table_tests.ma opcodes/opcode.ma
+emulator/opcodes/IP2022_table.ma common/list.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_opcode.ma emulator/opcodes/byte_or_word.ma
+emulator/status/HC05_status.ma num/word16.ma
+emulator/memory/memory_bits.ma emulator/memory/memory_trees.ma
common/string.ma common/ascii.ma common/list_utility.ma
common/theory.ma
+emulator/opcodes/byte_or_word.ma num/word16.ma
compiler/ast_type.ma common/list_utility.ma
num/word16.ma num/byte8.ma
-freescale_tests/micro_tests5.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
+emulator/opcodes/IP2022_instr_mode.ma num/word16.ma
+emulator/translation/HC08_translation.ma emulator/translation/translation_base.ma
common/prod.ma num/bool.ma
+emulator/opcodes/HCS08_opcode.ma num/bool.ma
+emulator/opcodes/HC08_opcode.ma num/bool.ma
num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma
num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma
-freescale_tests/medium_tests.ma common/list_utility.ma common/nat_to_num.ma freescale_tests/medium_tests_tools.ma
-memory/memory_trees.ma common/list.ma common/option.ma memory/memory_struct.ma num/word32.ma
+emulator/status/status_getter.ma emulator/status/status.ma
num/bool_lemmas.ma num/bool.ma
-freescale/opcode_base_lemmas1.ma freescale/opcode_base_lemmas_instrmode.ma freescale/opcode_base_lemmas_opcode.ma num/word16_lemmas.ma
-freescale/table_HC08.ma common/list.ma freescale/opcode_base.ma
-opcodes/HC05_table_tests.ma opcodes/opcode.ma
-memory/memory_struct.ma num/byte8.ma num/oct.ma
+emulator/memory/memory_abs.ma emulator/memory/memory_bits.ma emulator/memory/memory_func.ma emulator/memory/memory_trees.ma
+emulator/opcodes/RS08_opcode.ma num/bool.ma
num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma
-freescale/table_HCS08.ma common/list.ma freescale/opcode_base.ma
-memory/memory_abs.ma memory/memory_bits.ma memory/memory_func.ma memory/memory_trees.ma
+emulator/memory/memory_struct.ma num/byte8.ma num/oct.ma
+emulator/translation/RS08_translation.ma emulator/translation/translation_base.ma
+emulator/status/status_setter.ma emulator/status/status.ma
+emulator/translation/HC05_translation.ma emulator/translation/translation_base.ma
num/word32.ma num/word16.ma
common/ascii.ma num/bool.ma
-freescale_tests/micro_tests8.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
-freescale/opcode_base.ma num/word16.ma
-freescale/status_lemmas.ma common/option_lemmas.ma common/prod_lemmas.ma freescale/opcode_base_lemmas1.ma freescale/status.ma num/word16_lemmas.ma
-freescale_tests/micro_tests_tools.ma common/list.ma num/word16.ma
+emulator/opcodes/HCS08_table_tests.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/opcode.ma
+emulator/opcodes/HC05_instr_mode.ma num/word16.ma
+emulator/opcodes/IP2022_table_tests.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/opcode.ma
num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma
-freescale_tests/micro_tests1.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
-opcodes/HCS08_table.ma common/list.ma opcodes/HCS08_opcode_base.ma opcodes/byte_or_word.ma
-freescale/table_HC08_tests.ma freescale/opcode.ma freescale/table_HC08.ma
+emulator/memory/memory_func.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma
+emulator/opcodes/RS08_instr_mode.ma num/word16.ma
+emulator/status/RS08_status.ma num/word16.ma
+emulator/opcodes/HC08_instr_mode.ma num/word16.ma
+emulator/opcodes/opcode.ma common/list.ma emulator/opcodes/HC05_instr_mode.ma emulator/opcodes/HC05_opcode.ma emulator/opcodes/HC08_instr_mode.ma emulator/opcodes/HC08_opcode.ma emulator/opcodes/HCS08_opcode.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_opcode.ma emulator/opcodes/RS08_instr_mode.ma emulator/opcodes/RS08_opcode.ma emulator/opcodes/byte_or_word.ma
common/option.ma num/bool.ma
common/option_lemmas.ma common/option.ma num/bool_lemmas.ma
num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma
-freescale/opcode_base_lemmas_opcode.ma freescale/opcode_base.ma num/bool_lemmas.ma
-freescale_tests/micro_tests4.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
+emulator/opcodes/RS08_table.ma common/list.ma emulator/opcodes/RS08_instr_mode.ma emulator/opcodes/RS08_opcode.ma emulator/opcodes/byte_or_word.ma
common/sigma.ma common/theory.ma
common/list_lemmas.ma common/list.ma
+emulator/opcodes/HCS08_table.ma common/list.ma emulator/opcodes/HC08_instr_mode.ma emulator/opcodes/HCS08_opcode.ma emulator/opcodes/byte_or_word.ma
+emulator/translation/IP2022_translation.ma emulator/translation/translation_base.ma
universe/universe.ma common/list.ma common/nat_lemmas.ma common/prod.ma
num/bitrigesim.ma num/bool.ma
-opcodes/byte_or_word.ma num/word16.ma
-opcodes/HC05_table.ma common/list.ma opcodes/HC05_opcode_base.ma opcodes/byte_or_word.ma
-freescale/opcode_base_lemmas_instrmode.ma freescale/opcode_base.ma num/bitrigesim_lemmas.ma num/exadecim_lemmas.ma num/oct_lemmas.ma
common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma
+emulator/translation/translation.ma emulator/translation/HC05_translation.ma emulator/translation/HC08_translation.ma emulator/translation/HCS08_translation.ma emulator/translation/IP2022_translation.ma emulator/translation/RS08_translation.ma
num/oct.ma num/bool.ma
common/list.ma common/theory.ma
-freescale/opcode.ma common/list.ma freescale/opcode_base.ma
-freescale_tests/micro_tests7.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma
-opcodes/RS08_table_tests.ma freescale/opcode.ma
+emulator/opcodes/HC08_table_tests.ma emulator/opcodes/HC08_table.ma emulator/opcodes/opcode.ma
+emulator/opcodes/HC05_opcode.ma num/bool.ma
(* ***************** *)
(* definizione come concatenazione finale di liste per velocizzare il parsing *)
-(* ogni riga e' (any_opcode m) (instr_mode) (opcode esadecimale) (#cicli esecuzione) *)
-(* NB: l'uso di any_opcode m + concatenazione finale tutte liste
- impedisce di introdurre opcode disomogenei (per mcu) *)
+(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *)
ndefinition opcode_table_HC05_1 ≝
[
(* ***************** *)
(* definizione come concatenazione finale di liste per velocizzare il parsing *)
-(* ogni riga e' (any_opcode m) (instr_mode) (opcode esadecimale) (#cicli esecuzione) *)
-(* NB: l'uso di any_opcode m + concatenazione finale tutte liste
- impedisce di introdurre opcode disomogenei (per mcu) *)
+(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *)
ndefinition opcode_table_HC08_1 ≝
[
(* test bytecode non implementati *)
nlemma ok_word_table_HC08 : forall_b8 (λb.
- (test_not_impl_byte b HC08_not_impl_word ⊙ eq_w16 (get_word_count HC08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
- (⊖ (test_not_impl_byte b HC08_not_impl_word) ⊙ eq_w16 (get_word_count HC08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x0〉〉))
+ (test_not_impl_byte b HC08_not_impl_word ⊙ eq_w16 (get_word_count HC08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
+ (⊖ (test_not_impl_byte b HC08_not_impl_word) ⊙ eq_w16 (get_word_count HC08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HC08) 〈〈x0,x0〉:〈x0,x0〉〉))
= true.
napply refl_eq.
nqed.
(* ****************** *)
(* definizione come concatenazione finale di liste per velocizzare il parsing *)
-(* ogni riga e' (any_opcode m) (instr_mode) (opcode esadecimale) (#cicli esecuzione) *)
-(* NB: l'uso di any_opcode m + concatenazione finale tutte liste
- impedisce di introdurre opcode disomogenei (per mcu) *)
+(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *)
ndefinition opcode_table_HCS08_1 ≝
[
(* test bytecode non implementati *)
nlemma ok_word_table_HCS08 : forall_b8 (λb.
- (test_not_impl_byte b HCS08_not_impl_word ⊙ eq_w16 (get_word_count HCS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
- (⊖ (test_not_impl_byte b HCS08_not_impl_word) ⊙ eq_w16 (get_word_count HCS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉))
+ (test_not_impl_byte b HCS08_not_impl_word ⊙ eq_w16 (get_word_count HCS08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
+ (⊖ (test_not_impl_byte b HCS08_not_impl_word) ⊙ eq_w16 (get_word_count HCS08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉))
= true.
napply refl_eq.
nqed.
--- /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 IP2022_instr_mode: Type ≝
+ (* nessun operando : formato xxxxxxxx xxxxxxxx *)
+ MODE_INH : IP2022_instr_mode
+
+ (* #lit3 → / : formato xxxxxxxx xxxxxkkk *)
+| MODE_IMM3 : oct → IP2022_instr_mode
+ (* W, #lit8 → W : formato xxxxxxxx kkkkkkkk [load 1 byte arg] *)
+| MODE_IMM8 : IP2022_instr_mode
+ (* #lit13 → / : formato xxxkkkkk kkkkkkkk [load 1 byte arg] *)
+| MODE_IMM13 : bitrigesim → IP2022_instr_mode
+
+ (* FR, W → FR : formato xxxxxxx0 ffffffff [load 1 byte arg] *)
+| MODE_FR0_and_W : IP2022_instr_mode
+ (* FR, W → FR : formato xxxxxxx1 ffffffff [load 1 byte arg] *)
+| MODE_FR1_and_W : IP2022_instr_mode
+ (* W, FR → W : formato xxxxxxx0 ffffffff [load 1 byte arg] *)
+| MODE_W_and_FR0 : IP2022_instr_mode
+ (* W, FR → W : formato xxxxxxx1 ffffffff [load 1 byte arg] *)
+| MODE_W_and_FR1 : IP2022_instr_mode
+
+ (* FR(bitN) → FR(bitN) : formato xxxxbbb0 ffffffff [load 1 byte arg] *)
+| MODE_FR0n : oct → IP2022_instr_mode
+ (* FR(bitN) → FR(bitN) : formato xxxxbbb1 ffffffff [load 1 byte arg] *)
+| MODE_FR1n : oct → IP2022_instr_mode
+.
+
+ndefinition eq_IP2022_im ≝
+λi1,i2:IP2022_instr_mode.
+ match i1 with
+ [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
+ | MODE_IMM3 o1 ⇒ match i2 with [ MODE_IMM3 o2 ⇒ eq_oct o1 o2 | _ ⇒ false ]
+ | MODE_IMM8 ⇒ match i2 with [ MODE_IMM8 ⇒ true | _ ⇒ false ]
+ | MODE_IMM13 t1 ⇒ match i2 with [ MODE_IMM13 t2 ⇒ eq_bit t1 t2 | _ ⇒ false ]
+ | MODE_FR0_and_W ⇒ match i2 with [ MODE_FR0_and_W ⇒ true | _ ⇒ false ]
+ | MODE_FR1_and_W ⇒ match i2 with [ MODE_FR1_and_W ⇒ true | _ ⇒ false ]
+ | MODE_W_and_FR0 ⇒ match i2 with [ MODE_W_and_FR0 ⇒ true | _ ⇒ false ]
+ | MODE_W_and_FR1 ⇒ match i2 with [ MODE_W_and_FR1 ⇒ true | _ ⇒ false ]
+ | MODE_FR0n o1 ⇒ match i2 with [ MODE_FR0n o2 ⇒ eq_oct o1 o2 | _ ⇒ false ]
+ | MODE_FR1n o1 ⇒ match i2 with [ MODE_FR1n o2 ⇒ eq_oct o1 o2 | _ ⇒ false ]
+ ].
+
+(* iteratore sulle modalita' *)
+ndefinition forall_IP2022_im ≝ λP:IP2022_instr_mode → bool.
+ P MODE_INH
+⊗ forall_oct (λo.P (MODE_IMM3 o))
+⊗ P MODE_IMM8
+⊗ forall_bit (λt.P (MODE_IMM13 t))
+⊗ P MODE_FR0_and_W
+⊗ P MODE_FR1_and_W
+⊗ P MODE_W_and_FR0
+⊗ P MODE_W_and_FR1
+⊗ forall_oct (λo.P (MODE_FR0n o))
+⊗ forall_oct (λo.P (MODE_FR1n o)).
--- /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 "emulator/opcodes/IP2022_opcode.ma".
+include "emulator/opcodes/IP2022_instr_mode.ma".
+include "emulator/opcodes/byte_or_word.ma".
+include "common/list.ma".
+
+(* ******************* *)
+(* TABELLA DELL'IP2022 *)
+(* ******************* *)
+
+(* definizione come concatenazione finale di liste per velocizzare il parsing *)
+(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *)
+
+ndefinition opcode_table_IP2022_1 ≝
+[
+ quadruple … ADD MODE_FR0_and_W (Byte 〈x1,xE〉) 〈x0,x1〉
+; quadruple … ADD MODE_FR1_and_W (Byte 〈x1,xF〉) 〈x0,x1〉
+; quadruple … ADD MODE_W_and_FR0 (Byte 〈x1,xC〉) 〈x0,x1〉
+; quadruple … ADD MODE_W_and_FR1 (Byte 〈x1,xD〉) 〈x0,x1〉
+; quadruple … ADD MODE_IMM8 (Byte 〈x7,xB〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_2 ≝
+[
+ quadruple … ADDC MODE_FR0_and_W (Byte 〈x5,xE〉) 〈x0,x1〉
+; quadruple … ADDC MODE_FR1_and_W (Byte 〈x5,xF〉) 〈x0,x1〉
+; quadruple … ADDC MODE_W_and_FR0 (Byte 〈x5,xC〉) 〈x0,x1〉
+; quadruple … ADDC MODE_W_and_FR1 (Byte 〈x5,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_3 ≝
+[
+ quadruple … AND MODE_FR0_and_W (Byte 〈x1,x6〉) 〈x0,x1〉
+; quadruple … AND MODE_FR1_and_W (Byte 〈x1,x7〉) 〈x0,x1〉
+; quadruple … AND MODE_W_and_FR0 (Byte 〈x1,x4〉) 〈x0,x1〉
+; quadruple … AND MODE_W_and_FR1 (Byte 〈x1,x5〉) 〈x0,x1〉
+; quadruple … AND MODE_IMM8 (Byte 〈x7,xE〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_4 ≝
+[
+ quadruple … BREAK MODE_INH (Word 〈〈x0,x0〉:〈x0,x1〉〉) 〈x0,x1〉
+; quadruple … BREAKX MODE_INH (Word 〈〈x0,x0〉:〈x0,x5〉〉) 〈x0,x1〉
+; quadruple … CWDT MODE_INH (Word 〈〈x0,x0〉:〈x0,x4〉〉) 〈x0,x1〉
+; quadruple … FERASE MODE_INH (Word 〈〈x0,x0〉:〈x0,x3〉〉) 〈x0,x1〉
+; quadruple … FREAD MODE_INH (Word 〈〈x0,x0〉:〈x1,xB〉〉) 〈x0,x1〉
+; quadruple … FWRITE MODE_INH (Word 〈〈x0,x0〉:〈x1,xA〉〉) 〈x0,x1〉
+; quadruple … INT MODE_INH (Word 〈〈x0,x0〉:〈x0,x6〉〉) 〈x0,x3〉
+; quadruple … IREAD MODE_INH (Word 〈〈x0,x0〉:〈x1,x9〉〉) 〈x0,x4〉 (* blocking *)
+; quadruple … IREADI MODE_INH (Word 〈〈x0,x0〉:〈x1,xD〉〉) 〈x0,x4〉 (* blocking *)
+; quadruple … IWRITE MODE_INH (Word 〈〈x0,x0〉:〈x1,x8〉〉) 〈x0,x4〉 (* blocking *)
+; quadruple … IWRITEI MODE_INH (Word 〈〈x0,x0〉:〈x1,xC〉〉) 〈x0,x4〉 (* blocking *)
+; quadruple … NOP MODE_INH (Word 〈〈x0,x0〉:〈x0,x0〉〉) 〈x0,x1〉
+; quadruple … RET MODE_INH (Word 〈〈x0,x0〉:〈x0,x7〉〉) 〈x0,x3〉
+; quadruple … RETNP MODE_INH (Word 〈〈x0,x0〉:〈x0,x2〉〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_IP2022_5 ≝
+[
+ quadruple … CALL (MODE_IMM13 t00) (Byte 〈xC,x0〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t01) (Byte 〈xC,x1〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t02) (Byte 〈xC,x2〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t03) (Byte 〈xC,x3〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t04) (Byte 〈xC,x4〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t05) (Byte 〈xC,x5〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t06) (Byte 〈xC,x6〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t07) (Byte 〈xC,x7〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t08) (Byte 〈xC,x8〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t09) (Byte 〈xC,x9〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0A) (Byte 〈xC,xA〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0B) (Byte 〈xC,xB〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0C) (Byte 〈xC,xC〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0D) (Byte 〈xC,xD〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0E) (Byte 〈xC,xE〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0F) (Byte 〈xC,xF〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t10) (Byte 〈xD,x0〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t11) (Byte 〈xD,x1〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t12) (Byte 〈xD,x2〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t13) (Byte 〈xD,x3〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t14) (Byte 〈xD,x4〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t15) (Byte 〈xD,x5〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t16) (Byte 〈xD,x6〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t17) (Byte 〈xD,x7〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t18) (Byte 〈xD,x8〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t19) (Byte 〈xD,x9〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1A) (Byte 〈xD,xA〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1B) (Byte 〈xD,xB〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1C) (Byte 〈xD,xC〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1D) (Byte 〈xD,xD〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1E) (Byte 〈xD,xE〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1F) (Byte 〈xD,xF〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_IP2022_6 ≝
+[
+ quadruple … CLR MODE_FR0_and_W (Byte 〈x0,x6〉) 〈x0,x1〉
+; quadruple … CLR MODE_FR1_and_W (Byte 〈x0,x7〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_7 ≝
+[
+ quadruple … CLRB (MODE_FR0n o0) (Byte 〈x8,x0〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o0) (Byte 〈x8,x1〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o1) (Byte 〈x8,x2〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o1) (Byte 〈x8,x3〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o2) (Byte 〈x8,x4〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o2) (Byte 〈x8,x5〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o3) (Byte 〈x8,x6〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o3) (Byte 〈x8,x7〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o4) (Byte 〈x8,x8〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o4) (Byte 〈x8,x9〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o5) (Byte 〈x8,xA〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o5) (Byte 〈x8,xB〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o6) (Byte 〈x8,xC〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o6) (Byte 〈x8,xD〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o7) (Byte 〈x8,xE〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o7) (Byte 〈x8,xF〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_8 ≝
+[
+ quadruple … CMP MODE_W_and_FR0 (Byte 〈x0,x4〉) 〈x0,x1〉
+; quadruple … CMP MODE_W_and_FR1 (Byte 〈x0,x5〉) 〈x0,x1〉
+; quadruple … CMP MODE_IMM8 (Byte 〈x7,x9〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_9 ≝
+[
+ quadruple … CSE MODE_W_and_FR0 (Byte 〈x4,x2〉) 〈x0,x1〉
+; quadruple … CSE MODE_W_and_FR1 (Byte 〈x4,x3〉) 〈x0,x1〉
+; quadruple … CSE MODE_IMM8 (Byte 〈x7,x7〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_10 ≝
+[
+ quadruple … CSNE MODE_W_and_FR0 (Byte 〈x4,x0〉) 〈x0,x1〉
+; quadruple … CSNE MODE_W_and_FR1 (Byte 〈x4,x1〉) 〈x0,x1〉
+; quadruple … CSNE MODE_IMM8 (Byte 〈x7,x6〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_11 ≝
+[
+ quadruple … DEC MODE_FR0_and_W (Byte 〈x0,xE〉) 〈x0,x1〉
+; quadruple … DEC MODE_FR1_and_W (Byte 〈x0,xF〉) 〈x0,x1〉
+; quadruple … DEC MODE_W_and_FR0 (Byte 〈x0,xC〉) 〈x0,x1〉
+; quadruple … DEC MODE_W_and_FR1 (Byte 〈x0,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_12 ≝
+[
+ quadruple … DECSNZ MODE_FR0_and_W (Byte 〈x4,xE〉) 〈x0,x1〉
+; quadruple … DECSNZ MODE_FR1_and_W (Byte 〈x4,xF〉) 〈x0,x1〉
+; quadruple … DECSNZ MODE_W_and_FR0 (Byte 〈x4,xC〉) 〈x0,x1〉
+; quadruple … DECSNZ MODE_W_and_FR1 (Byte 〈x4,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_13 ≝
+[
+ quadruple … DECSZ MODE_FR0_and_W (Byte 〈x2,xE〉) 〈x0,x1〉
+; quadruple … DECSZ MODE_FR1_and_W (Byte 〈x2,xF〉) 〈x0,x1〉
+; quadruple … DECSZ MODE_W_and_FR0 (Byte 〈x2,xC〉) 〈x0,x1〉
+; quadruple … DECSZ MODE_W_and_FR1 (Byte 〈x2,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_14 ≝
+[
+ quadruple … INC MODE_FR0_and_W (Byte 〈x2,xA〉) 〈x0,x1〉
+; quadruple … INC MODE_FR1_and_W (Byte 〈x2,xB〉) 〈x0,x1〉
+; quadruple … INC MODE_W_and_FR0 (Byte 〈x2,x8〉) 〈x0,x1〉
+; quadruple … INC MODE_W_and_FR1 (Byte 〈x2,x9〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_15 ≝
+[
+ quadruple … INCSNZ MODE_FR0_and_W (Byte 〈x5,xA〉) 〈x0,x1〉
+; quadruple … INCSNZ MODE_FR1_and_W (Byte 〈x5,xB〉) 〈x0,x1〉
+; quadruple … INCSNZ MODE_W_and_FR0 (Byte 〈x5,x8〉) 〈x0,x1〉
+; quadruple … INCSNZ MODE_W_and_FR1 (Byte 〈x5,x9〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_16 ≝
+[
+ quadruple … INCSZ MODE_FR0_and_W (Byte 〈x3,xE〉) 〈x0,x1〉
+; quadruple … INCSZ MODE_FR1_and_W (Byte 〈x3,xF〉) 〈x0,x1〉
+; quadruple … INCSZ MODE_W_and_FR0 (Byte 〈x3,xC〉) 〈x0,x1〉
+; quadruple … INCSZ MODE_W_and_FR1 (Byte 〈x3,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_17 ≝
+[
+ quadruple … JMP (MODE_IMM13 t00) (Byte 〈xE,x0〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t01) (Byte 〈xE,x1〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t02) (Byte 〈xE,x2〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t03) (Byte 〈xE,x3〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t04) (Byte 〈xE,x4〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t05) (Byte 〈xE,x5〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t06) (Byte 〈xE,x6〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t07) (Byte 〈xE,x7〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t08) (Byte 〈xE,x8〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t09) (Byte 〈xE,x9〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0A) (Byte 〈xE,xA〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0B) (Byte 〈xE,xB〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0C) (Byte 〈xE,xC〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0D) (Byte 〈xE,xD〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0E) (Byte 〈xE,xE〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0F) (Byte 〈xE,xF〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t10) (Byte 〈xF,x0〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t11) (Byte 〈xF,x1〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t12) (Byte 〈xF,x2〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t13) (Byte 〈xF,x3〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t14) (Byte 〈xF,x4〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t15) (Byte 〈xF,x5〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t16) (Byte 〈xF,x6〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t17) (Byte 〈xF,x7〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t18) (Byte 〈xF,x8〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t19) (Byte 〈xF,x9〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1A) (Byte 〈xF,xA〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1B) (Byte 〈xF,xB〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1C) (Byte 〈xF,xC〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1D) (Byte 〈xF,xD〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1E) (Byte 〈xF,xE〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1F) (Byte 〈xF,xF〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_IP2022_18 ≝
+[
+ quadruple … LOADH MODE_IMM8 (Byte 〈x7,x0〉) 〈x0,x1〉
+; quadruple … LOADL MODE_IMM8 (Byte 〈x7,x1〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_19 ≝
+[
+ quadruple … MOV MODE_FR0_and_W (Byte 〈x0,x2〉) 〈x0,x1〉
+; quadruple … MOV MODE_FR1_and_W (Byte 〈x0,x3〉) 〈x0,x1〉
+; quadruple … MOV MODE_W_and_FR0 (Byte 〈x2,x0〉) 〈x0,x1〉
+; quadruple … MOV MODE_W_and_FR1 (Byte 〈x2,x1〉) 〈x0,x1〉
+; quadruple … MOV MODE_IMM8 (Byte 〈x7,xC〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_20 ≝
+[
+ quadruple … MULS MODE_W_and_FR0 (Byte 〈x5,x4〉) 〈x0,x1〉
+; quadruple … MULS MODE_W_and_FR1 (Byte 〈x5,x5〉) 〈x0,x1〉
+; quadruple … MULS MODE_IMM8 (Byte 〈x7,x3〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_21 ≝
+[
+ quadruple … MULU MODE_W_and_FR0 (Byte 〈x5,x0〉) 〈x0,x1〉
+; quadruple … MULU MODE_W_and_FR1 (Byte 〈x5,x1〉) 〈x0,x1〉
+; quadruple … MULU MODE_IMM8 (Byte 〈x7,x2〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_22 ≝
+[
+ quadruple … NOT MODE_FR0_and_W (Byte 〈x2,x6〉) 〈x0,x1〉
+; quadruple … NOT MODE_FR1_and_W (Byte 〈x2,x7〉) 〈x0,x1〉
+; quadruple … NOT MODE_W_and_FR0 (Byte 〈x2,x4〉) 〈x0,x1〉
+; quadruple … NOT MODE_W_and_FR1 (Byte 〈x2,x5〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_23 ≝
+[
+ quadruple … OR MODE_FR0_and_W (Byte 〈x1,x2〉) 〈x0,x1〉
+; quadruple … OR MODE_FR1_and_W (Byte 〈x1,x3〉) 〈x0,x1〉
+; quadruple … OR MODE_W_and_FR0 (Byte 〈x1,x0〉) 〈x0,x1〉
+; quadruple … OR MODE_W_and_FR1 (Byte 〈x1,x1〉) 〈x0,x1〉
+; quadruple … OR MODE_IMM8 (Byte 〈x7,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_24 ≝
+[
+ quadruple … PAGE (MODE_IMM3 o0) (Word 〈〈x0,x0〉:〈x1,x0〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o1) (Word 〈〈x0,x0〉:〈x1,x1〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o2) (Word 〈〈x0,x0〉:〈x1,x2〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o3) (Word 〈〈x0,x0〉:〈x1,x3〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o4) (Word 〈〈x0,x0〉:〈x1,x4〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o5) (Word 〈〈x0,x0〉:〈x1,x5〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o6) (Word 〈〈x0,x0〉:〈x1,x6〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o7) (Word 〈〈x0,x0〉:〈x1,x7〉〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_25 ≝
+[
+ quadruple … POP MODE_FR0_and_W (Byte 〈x4,x6〉) 〈x0,x1〉
+; quadruple … POP MODE_FR1_and_W (Byte 〈x4,x7〉) 〈x0,x1〉
+; quadruple … PUSH MODE_W_and_FR0 (Byte 〈x4,x4〉) 〈x0,x1〉
+; quadruple … PUSH MODE_W_and_FR1 (Byte 〈x4,x5〉) 〈x0,x1〉
+; quadruple … PUSH MODE_IMM8 (Byte 〈x7,x4〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_26 ≝
+[
+ quadruple … RETI (MODE_IMM3 o0) (Word 〈〈x0,x0〉:〈x0,x8〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o1) (Word 〈〈x0,x0〉:〈x0,x9〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o2) (Word 〈〈x0,x0〉:〈x0,xA〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o3) (Word 〈〈x0,x0〉:〈x0,xB〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o4) (Word 〈〈x0,x0〉:〈x0,xC〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o5) (Word 〈〈x0,x0〉:〈x0,xD〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o6) (Word 〈〈x0,x0〉:〈x0,xE〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o7) (Word 〈〈x0,x0〉:〈x0,xF〉〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_IP2022_27 ≝
+[ quadruple … RETW MODE_IMM8 (Byte 〈x7,x8〉) 〈x0,x3〉 ].
+
+ndefinition opcode_table_IP2022_28 ≝
+[
+ quadruple … RL MODE_FR0_and_W (Byte 〈x3,x6〉) 〈x0,x1〉
+; quadruple … RL MODE_FR1_and_W (Byte 〈x3,x7〉) 〈x0,x1〉
+; quadruple … RL MODE_W_and_FR0 (Byte 〈x3,x4〉) 〈x0,x1〉
+; quadruple … RL MODE_W_and_FR1 (Byte 〈x3,x5〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_29 ≝
+[
+ quadruple … RR MODE_FR0_and_W (Byte 〈x3,x2〉) 〈x0,x1〉
+; quadruple … RR MODE_FR1_and_W (Byte 〈x3,x3〉) 〈x0,x1〉
+; quadruple … RR MODE_W_and_FR0 (Byte 〈x3,x0〉) 〈x0,x1〉
+; quadruple … RR MODE_W_and_FR1 (Byte 〈x3,x1〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_30 ≝
+[
+ quadruple … SB (MODE_FR0n o0) (Byte 〈xB,x0〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o0) (Byte 〈xB,x1〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o1) (Byte 〈xB,x2〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o1) (Byte 〈xB,x3〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o2) (Byte 〈xB,x4〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o2) (Byte 〈xB,x5〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o3) (Byte 〈xB,x6〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o3) (Byte 〈xB,x7〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o4) (Byte 〈xB,x8〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o4) (Byte 〈xB,x9〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o5) (Byte 〈xB,xA〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o5) (Byte 〈xB,xB〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o6) (Byte 〈xB,xC〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o6) (Byte 〈xB,xD〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o7) (Byte 〈xB,xE〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o7) (Byte 〈xB,xF〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_31 ≝
+[
+ quadruple … SETB (MODE_FR0n o0) (Byte 〈x9,x0〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o0) (Byte 〈x9,x1〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o1) (Byte 〈x9,x2〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o1) (Byte 〈x9,x3〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o2) (Byte 〈x9,x4〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o2) (Byte 〈x9,x5〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o3) (Byte 〈x9,x6〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o3) (Byte 〈x9,x7〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o4) (Byte 〈x9,x8〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o4) (Byte 〈x9,x9〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o5) (Byte 〈x9,xA〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o5) (Byte 〈x9,xB〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o6) (Byte 〈x9,xC〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o6) (Byte 〈x9,xD〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o7) (Byte 〈x9,xE〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o7) (Byte 〈x9,xF〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_32 ≝
+[
+ quadruple … SNB (MODE_FR0n o0) (Byte 〈xA,x0〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o0) (Byte 〈xA,x1〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o1) (Byte 〈xA,x2〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o1) (Byte 〈xA,x3〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o2) (Byte 〈xA,x4〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o2) (Byte 〈xA,x5〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o3) (Byte 〈xA,x6〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o3) (Byte 〈xA,x7〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o4) (Byte 〈xA,x8〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o4) (Byte 〈xA,x9〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o5) (Byte 〈xA,xA〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o5) (Byte 〈xA,xB〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o6) (Byte 〈xA,xC〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o6) (Byte 〈xA,xD〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o7) (Byte 〈xA,xE〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o7) (Byte 〈xA,xF〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_33 ≝
+[ quadruple … SPEED MODE_IMM8 (Byte 〈x0,x1〉) 〈x0,x1〉 ].
+
+ndefinition opcode_table_IP2022_34 ≝
+[
+ quadruple … SUB MODE_FR0_and_W (Byte 〈x0,xA〉) 〈x0,x1〉
+; quadruple … SUB MODE_FR1_and_W (Byte 〈x0,xB〉) 〈x0,x1〉
+; quadruple … SUB MODE_W_and_FR0 (Byte 〈x0,x8〉) 〈x0,x1〉
+; quadruple … SUB MODE_W_and_FR1 (Byte 〈x0,x9〉) 〈x0,x1〉
+; quadruple … SUB MODE_IMM8 (Byte 〈x7,xA〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_35 ≝
+[
+ quadruple … SUBC MODE_FR0_and_W (Byte 〈x4,xA〉) 〈x0,x1〉
+; quadruple … SUBC MODE_FR1_and_W (Byte 〈x4,xB〉) 〈x0,x1〉
+; quadruple … SUBC MODE_W_and_FR0 (Byte 〈x4,x8〉) 〈x0,x1〉
+; quadruple … SUBC MODE_W_and_FR1 (Byte 〈x4,x9〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_36 ≝
+[
+ quadruple … SWAP MODE_FR0_and_W (Byte 〈x3,xA〉) 〈x0,x1〉
+; quadruple … SWAP MODE_FR1_and_W (Byte 〈x3,xB〉) 〈x0,x1〉
+; quadruple … SWAP MODE_W_and_FR0 (Byte 〈x3,x8〉) 〈x0,x1〉
+; quadruple … SWAP MODE_W_and_FR1 (Byte 〈x3,x9〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_37 ≝
+[
+ quadruple … TEST MODE_FR0_and_W (Byte 〈x2,x2〉) 〈x0,x1〉
+; quadruple … TEST MODE_FR1_and_W (Byte 〈x2,x3〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_38 ≝
+[
+ quadruple … XOR MODE_FR0_and_W (Byte 〈x1,xA〉) 〈x0,x1〉
+; quadruple … XOR MODE_FR1_and_W (Byte 〈x1,xB〉) 〈x0,x1〉
+; quadruple … XOR MODE_W_and_FR0 (Byte 〈x1,x8〉) 〈x0,x1〉
+; quadruple … XOR MODE_W_and_FR1 (Byte 〈x1,x9〉) 〈x0,x1〉
+; quadruple … XOR MODE_IMM8 (Byte 〈x7,xF〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022 ≝
+ opcode_table_IP2022_1 @ opcode_table_IP2022_2 @ opcode_table_IP2022_3 @ opcode_table_IP2022_4 @
+ opcode_table_IP2022_5 @ opcode_table_IP2022_6 @ opcode_table_IP2022_7 @ opcode_table_IP2022_8 @
+ opcode_table_IP2022_9 @ opcode_table_IP2022_10 @ opcode_table_IP2022_11 @ opcode_table_IP2022_12 @
+ opcode_table_IP2022_13 @ opcode_table_IP2022_14 @ opcode_table_IP2022_15 @ opcode_table_IP2022_16 @
+ opcode_table_IP2022_17 @ opcode_table_IP2022_18 @ opcode_table_IP2022_19 @ opcode_table_IP2022_20 @
+ opcode_table_IP2022_21 @ opcode_table_IP2022_22 @ opcode_table_IP2022_23 @ opcode_table_IP2022_24 @
+ opcode_table_IP2022_25 @ opcode_table_IP2022_26 @ opcode_table_IP2022_27 @ opcode_table_IP2022_28 @
+ opcode_table_IP2022_29 @ opcode_table_IP2022_30 @ opcode_table_IP2022_31 @ opcode_table_IP2022_32 @
+ opcode_table_IP2022_33 @ opcode_table_IP2022_34 @ opcode_table_IP2022_35 @ opcode_table_IP2022_36 @
+ opcode_table_IP2022_37 @ opcode_table_IP2022_38.
--- /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/opcode.ma".
+include "emulator/opcodes/IP2022_table.ma".
+
+(* ******************* *)
+(* TABELLA DELL'IP2022 *)
+(* ******************* *)
+
+(* IP2022: opcode non implementati come da manuale (byte) *)
+ndefinition IP2022_not_impl_byte ≝
+ [〈x0,x0〉;〈x5,x2〉;〈x5,x3〉;〈x5,x6〉;〈x5,x7〉;〈x6,x0〉;〈x6,x1〉;〈x6,x2〉
+ ;〈x6,x3〉;〈x6,x4〉;〈x6,x5〉;〈x6,x6〉;〈x6,x7〉;〈x6,x8〉;〈x6,x9〉;〈x6,xA〉
+ ;〈x6,xB〉;〈x6,xC〉;〈x6,xD〉;〈x6,xE〉;〈x6,xF〉;〈x7,x5〉 ].
+
+(* test bytecode non implementati *)
+nlemma ok_byte_table_IP2022 : forall_b8 (λb.
+ (test_not_impl_byte b IP2022_not_impl_byte ⊙ eq_w16 (get_byte_count IP2022 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
+ (⊖ (test_not_impl_byte b IP2022_not_impl_byte) ⊙ eq_w16 (get_byte_count IP2022 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022) 〈〈x0,x0〉:〈x0,x0〉〉))
+ = true.
+ napply refl_eq.
+nqed.
+
+(* IP2022: opcode non implementati come da manuale (0x00+byte) *)
+ndefinition IP2022_not_impl_word ≝
+ [〈x1,xE〉;〈x1,xF〉
+ ;〈x2,x0〉;〈x2,x1〉;〈x2,x2〉;〈x2,x3〉;〈x2,x4〉;〈x2,x5〉;〈x2,x6〉;〈x2,x7〉
+ ;〈x2,x8〉;〈x2,x9〉;〈x2,xA〉;〈x2,xB〉;〈x2,xC〉;〈x2,xD〉;〈x2,xE〉;〈x2,xF〉
+ ;〈x3,x0〉;〈x3,x1〉;〈x3,x2〉;〈x3,x3〉;〈x3,x4〉;〈x3,x5〉;〈x3,x6〉;〈x3,x7〉
+ ;〈x3,x8〉;〈x3,x9〉;〈x3,xA〉;〈x3,xB〉;〈x3,xC〉;〈x3,xD〉;〈x3,xE〉;〈x3,xF〉
+ ;〈x4,x0〉;〈x4,x1〉;〈x4,x2〉;〈x4,x3〉;〈x4,x4〉;〈x4,x5〉;〈x4,x6〉;〈x4,x7〉
+ ;〈x4,x8〉;〈x4,x9〉;〈x4,xA〉;〈x4,xB〉;〈x4,xC〉;〈x4,xD〉;〈x4,xE〉;〈x4,xF〉
+ ;〈x5,x0〉;〈x5,x1〉;〈x5,x2〉;〈x5,x3〉;〈x5,x4〉;〈x5,x5〉;〈x5,x6〉;〈x5,x7〉
+ ;〈x5,x8〉;〈x5,x9〉;〈x5,xA〉;〈x5,xB〉;〈x5,xC〉;〈x5,xD〉;〈x5,xE〉;〈x5,xF〉
+ ;〈x6,x0〉;〈x6,x1〉;〈x6,x2〉;〈x6,x3〉;〈x6,x4〉;〈x6,x5〉;〈x6,x6〉;〈x6,x7〉
+ ;〈x6,x8〉;〈x6,x9〉;〈x6,xA〉;〈x6,xB〉;〈x6,xC〉;〈x6,xD〉;〈x6,xE〉;〈x6,xF〉
+ ;〈x7,x0〉;〈x7,x1〉;〈x7,x2〉;〈x7,x3〉;〈x7,x4〉;〈x7,x5〉;〈x7,x6〉;〈x7,x7〉
+ ;〈x7,x8〉;〈x7,x9〉;〈x7,xA〉;〈x7,xB〉;〈x7,xC〉;〈x7,xD〉;〈x7,xE〉;〈x7,xF〉
+ ;〈x8,x0〉;〈x8,x1〉;〈x8,x2〉;〈x8,x3〉;〈x8,x4〉;〈x8,x5〉;〈x8,x6〉;〈x8,x7〉
+ ;〈x8,x8〉;〈x8,x9〉;〈x8,xA〉;〈x8,xB〉;〈x8,xC〉;〈x8,xD〉;〈x8,xE〉;〈x8,xF〉
+ ;〈x9,x0〉;〈x9,x1〉;〈x9,x2〉;〈x9,x3〉;〈x9,x4〉;〈x9,x5〉;〈x9,x6〉;〈x9,x7〉
+ ;〈x9,x8〉;〈x9,x9〉;〈x9,xA〉;〈x9,xB〉;〈x9,xC〉;〈x9,xD〉;〈x9,xE〉;〈x9,xF〉
+ ;〈xA,x0〉;〈xA,x1〉;〈xA,x2〉;〈xA,x3〉;〈xA,x4〉;〈xA,x5〉;〈xA,x6〉;〈xA,x7〉
+ ;〈xA,x8〉;〈xA,x9〉;〈xA,xA〉;〈xA,xB〉;〈xA,xC〉;〈xA,xD〉;〈xA,xE〉;〈xA,xF〉
+ ;〈xB,x0〉;〈xB,x1〉;〈xB,x2〉;〈xB,x3〉;〈xB,x4〉;〈xB,x5〉;〈xB,x6〉;〈xB,x7〉
+ ;〈xB,x8〉;〈xB,x9〉;〈xB,xA〉;〈xB,xB〉;〈xB,xC〉;〈xB,xD〉;〈xB,xE〉;〈xB,xF〉
+ ;〈xC,x0〉;〈xC,x1〉;〈xC,x2〉;〈xC,x3〉;〈xC,x4〉;〈xC,x5〉;〈xC,x6〉;〈xC,x7〉
+ ;〈xC,x8〉;〈xC,x9〉;〈xC,xA〉;〈xC,xB〉;〈xC,xC〉;〈xC,xD〉;〈xC,xE〉;〈xC,xF〉
+ ;〈xD,x0〉;〈xD,x1〉;〈xD,x2〉;〈xD,x3〉;〈xD,x4〉;〈xD,x5〉;〈xD,x6〉;〈xD,x7〉
+ ;〈xD,x8〉;〈xD,x9〉;〈xD,xA〉;〈xD,xB〉;〈xD,xC〉;〈xD,xD〉;〈xD,xE〉;〈xD,xF〉
+ ;〈xE,x0〉;〈xE,x1〉;〈xE,x2〉;〈xE,x3〉;〈xE,x4〉;〈xE,x5〉;〈xE,x6〉;〈xE,x7〉
+ ;〈xE,x8〉;〈xE,x9〉;〈xE,xA〉;〈xE,xB〉;〈xE,xC〉;〈xE,xD〉;〈xE,xE〉;〈xE,xF〉
+ ;〈xF,x0〉;〈xF,x1〉;〈xF,x2〉;〈xF,x3〉;〈xF,x4〉;〈xF,x5〉;〈xF,x6〉;〈xF,x7〉
+ ;〈xF,x8〉;〈xF,x9〉;〈xF,xA〉;〈xF,xB〉;〈xF,xC〉;〈xF,xD〉;〈xF,xE〉;〈xF,xF〉
+ ].
+
+(* test bytecode non implementati *)
+nlemma ok_word_table_IP2022 : forall_b8 (λb.
+ (test_not_impl_byte b IP2022_not_impl_word ⊙ eq_w16 (get_word_count IP2022 〈〈x0,x0〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
+ (⊖ (test_not_impl_byte b IP2022_not_impl_word) ⊙ eq_w16 (get_word_count IP2022 〈〈x0,x0〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022) 〈〈x0,x0〉:〈x0,x0〉〉))
+ = true.
+ napply refl_eq.
+nqed.
+
+(* tutti op implementati *)
+nlemma ok_pseudo_table_IP2022 :
+ forall_op IP2022 (λo.
+ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count IP2022 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022)) = true.
+ napply refl_eq.
+nqed.
+
+(* tutte im implementate *)
+nlemma ok_mode_table_IP2022 :
+ forall_im IP2022 (λi.
+ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count IP2022 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022)) = true.
+ napply refl_eq.
+nqed.
+
+(* nessuna ripetizione di combinazione op + imm *)
+nlemma ok_OpIm_table_IP2022 :
+ forall_im IP2022 (λi.
+ forall_op IP2022 (λo.
+ le_w16 (get_OpIm_count IP2022 o i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_IP2022) 〈〈x0,x0〉:〈x0,x1〉〉)) = true.
+ napply refl_eq.
+nqed.
(* ***************** *)
(* definizione come concatenazione finale di liste per velocizzare il parsing *)
-(* ogni riga e' (any_opcode m) (instr_mode) (opcode esadecimale) (#cicli esecuzione) *)
-(* NB: l'uso di any_opcode m + concatenazione finale tutte liste
- impedisce di introdurre opcode disomogenei (per mcu) *)
+(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *)
ndefinition opcode_table_RS08_1 ≝
[
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".
(* enumerazione delle ALU *)
ninductive mcu_type: Type ≝
- HC05 : mcu_type
-| HC08 : mcu_type
-| HCS08 : mcu_type
-| RS08 : mcu_type.
+ HC05 : mcu_type
+| HC08 : mcu_type
+| HCS08 : mcu_type
+| RS08 : mcu_type
+| IP2022 : mcu_type.
ndefinition eq_mcutype ≝
λm1,m2:mcu_type.
| 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 ≝
| HC08 ⇒ HC08_opcode
| HCS08 ⇒ HCS08_opcode
| RS08 ⇒ RS08_opcode
+ | IP2022 ⇒ IP2022_opcode
].
ndefinition aux_im_type ≝
| HC08 ⇒ HC08_instr_mode
| HCS08 ⇒ HC08_instr_mode
| RS08 ⇒ RS08_instr_mode
+ | IP2022 ⇒ IP2022_instr_mode
].
ndefinition eq_op ≝
| HC08 ⇒ eq_HC08_op
| HCS08 ⇒ eq_HCS08_op
| RS08 ⇒ eq_RS08_op
+ | IP2022 ⇒ eq_IP2022_op
].
ndefinition eq_im ≝
| HC08 ⇒ eq_HC08_im
| HCS08 ⇒ eq_HC08_im
| RS08 ⇒ eq_RS08_im
+ | IP2022 ⇒ eq_IP2022_im
].
ndefinition forall_op ≝
| HC08 ⇒ forall_HC08_op
| HCS08 ⇒ forall_HCS08_op
| RS08 ⇒ forall_RS08_op
+ | IP2022 ⇒ forall_IP2022_op
].
ndefinition forall_im ≝
| HC08 ⇒ forall_HC08_im
| HCS08 ⇒ forall_HC08_im
| RS08 ⇒ forall_RS08_im
+ | IP2022 ⇒ forall_IP2022_im
].
(* ********************************************* *)
]
].
-(* su tutta la lista quante volte compare la word (0x9E+byte) *)
-nlet rec get_word_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝
+(* su tutta la lista quante volte compare la word *)
+nlet rec get_word_count (m:mcu_type) (w:word16) (c:word16) (l:list (aux_table_type m)) on l ≝
match l with
[ nil ⇒ c
| cons hd tl ⇒ match thd4T … hd with
- [ Byte _ ⇒ get_word_count m b c tl
- | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
- [ true ⇒ get_word_count m b (succ_w16 c) tl
- | false ⇒ get_word_count m b c tl
+ [ Byte _ ⇒ get_word_count m w c tl
+ | Word w' ⇒ match eq_w16 w w' with
+ [ true ⇒ get_word_count m w (succ_w16 c) tl
+ | false ⇒ get_word_count m w c tl
]
]
].
]
].
-(* o e' non implementato? *)
-nlet rec test_not_impl_pseudo (m:mcu_type) (o:aux_op_type m) (l:list (aux_op_type m)) on l ≝
- match l with
- [ nil ⇒ false
- | cons hd tl ⇒ match eq_op m o hd with
- [ true ⇒ true
- | false ⇒ test_not_impl_pseudo m o tl
- ]
- ].
-
-(* i e' non implementato? *)
-nlet rec test_not_impl_mode (m:mcu_type) (i:aux_im_type m) (l:list (aux_im_type m)) on l ≝
- match l with
- [ nil ⇒ false
- | cons hd tl ⇒ match eq_im m i hd with
- [ true ⇒ true
- | false ⇒ test_not_impl_mode m i tl
- ]
- ].
-
(* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
nlet rec get_OpIm_count (m:mcu_type) (o:aux_op_type m) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
match l with
--- /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/translation/translation_base.ma".
+
+(* ******************************************************* *)
+(* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
+(* ******************************************************* *)
+
+(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
+ninductive IP2022_MA_check : IP2022_instr_mode → Type ≝
+ maINH : IP2022_MA_check MODE_INH
+| maIMM3 : ∀n.IP2022_MA_check (MODE_IMM3 n)
+| maIMM8 : byte8 → IP2022_MA_check MODE_IMM8
+| maIMM13 : ∀t.byte8 → IP2022_MA_check (MODE_IMM13 t)
+| maFR0_and_W : byte8 → IP2022_MA_check MODE_FR0_and_W
+| maFR1_and_W : byte8 → IP2022_MA_check MODE_FR1_and_W
+| maW_and_FR0 : byte8 → IP2022_MA_check MODE_W_and_FR0
+| maW_and_FR1 : byte8 → IP2022_MA_check MODE_W_and_FR1
+| maFR0n : ∀n.byte8 → IP2022_MA_check (MODE_FR0n n)
+| maFR1n : ∀n.byte8 → IP2022_MA_check (MODE_FR1n n)
+.
+
+(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
+ MA_check i → list (t_byte8 m) *)
+ndefinition IP2022_args_picker ≝
+λi:aux_im_type IP2022.λargs:IP2022_MA_check i.
+ match args with
+ [ maINH ⇒ nil ?
+ | maIMM3 _ ⇒ nil ?
+ | maIMM8 b ⇒ [ TByte IP2022 b ]
+ | maIMM13 _ b ⇒ [ TByte IP2022 b ]
+ | maFR0_and_W b ⇒ [ TByte IP2022 b ]
+ | maFR1_and_W b ⇒ [ TByte IP2022 b ]
+ | maW_and_FR0 b ⇒ [ TByte IP2022 b ]
+ | maW_and_FR1 b ⇒ [ TByte IP2022 b ]
+ | maFR0n _ b ⇒ [ TByte IP2022 b ]
+ | maFR1n _ b ⇒ [ TByte IP2022 b ]
+ ].
include "emulator/translation/HC08_translation.ma".
include "emulator/translation/HCS08_translation.ma".
include "emulator/translation/RS08_translation.ma".
+include "emulator/translation/IP2022_translation.ma".
(* ******************************************************* *)
(* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
| HC08 ⇒ HC08_MA_check
| HCS08 ⇒ HCS08_MA_check
| RS08 ⇒ RS08_MA_check
+ | IP2022 ⇒ IP2022_MA_check
].
(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
| HC08 ⇒ HC08_args_picker
| HCS08 ⇒ HCS08_args_picker
| RS08 ⇒ RS08_args_picker
+ | IP2022 ⇒ IP2022_args_picker
].
(* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
].
(* detipatore del compilato: (t_byte8 m) → byte8 *)
-nlet rec source_to_byte8_HC05_aux (p1:list (t_byte8 HC05)) (p2:list byte8) ≝
+nlet rec source_to_byte8_aux (m:mcu_type) (p2:list byte8) (p1:list (t_byte8 m)) on p1 ≝
match p1 with
[ nil ⇒ p2
- | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC05_aux tl (p2@[b]) ]
+ | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_aux m (p2@[b]) tl ]
].
-nlet rec source_to_byte8_HC08_aux (p1:list (t_byte8 HC08)) (p2:list byte8) ≝
- match p1 with
- [ nil ⇒ p2
- | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC08_aux tl (p2@[b]) ]
- ].
-
-nlet rec source_to_byte8_HCS08_aux (p1:list (t_byte8 HCS08)) (p2:list byte8) ≝
- match p1 with
- [ nil ⇒ p2
- | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HCS08_aux tl (p2@[b]) ]
- ].
-
-nlet rec source_to_byte8_RS08_aux (p1:list (t_byte8 RS08)) (p2:list byte8) ≝
- match p1 with
- [ nil ⇒ p2
- | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_RS08_aux tl (p2@[b]) ]
- ].
-
-ndefinition source_to_byte8 ≝
-λm:mcu_type.
- match m
- return λm:mcu_type.list (t_byte8 m) → list byte8
- with
- [ HC05 ⇒ λl:list (t_byte8 HC05).source_to_byte8_HC05_aux l []
- | HC08 ⇒ λl:list (t_byte8 HC08).source_to_byte8_HC08_aux l []
- | HCS08 ⇒ λl:list (t_byte8 HCS08).source_to_byte8_HCS08_aux l []
- | RS08 ⇒ λl:list (t_byte8 RS08).source_to_byte8_RS08_aux l []
- ].
+ndefinition source_to_byte8 ≝ λm:mcu_type.source_to_byte8_aux m [].
include "emulator/opcodes/HC08_table.ma".
include "emulator/opcodes/HCS08_table.ma".
include "emulator/opcodes/RS08_table.ma".
+include "emulator/opcodes/IP2022_table.ma".
(* ***************************** *)
(* TRADUZIONE ESADECIMALE → INFO *)
| HC08 ⇒ opcode_table_HC08
| HCS08 ⇒ opcode_table_HCS08
| RS08 ⇒ opcode_table_RS08
+ | IP2022 ⇒ opcode_table_IP2022
].
(* traduzione mcu+esadecimale → info *)
projects / helm.git / commitdiff