Tests enabled again.

[helm.git] / helm / software / matita / library / freescale / table_HC05.ma

diff --git a/helm/software/matita/library/freescale/table_HC05.ma b/helm/software/matita/library/freescale/table_HC05.ma
index 57a6bf42a50cfe262b8890daa5c01e8aac696b4e..6938cd3e67da4da6fb181a09de9fac379801195b 100644 (file)
--- a/helm/software/matita/library/freescale/table_HC05.ma
+++ b/helm/software/matita/library/freescale/table_HC05.ma
@@ -24,9 +24,6 @@
 (*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-set "baseuri" "cic:/matita/freescale/table_HC05/".
-
-(*include "/media/VIRTUOSO/freescale/opcode.ma".*)
 include "freescale/opcode.ma".
 
 (* ***************** *)
@@ -242,21 +239,21 @@ definition opcode_table_HC05_17 ≝
 
 definition opcode_table_HC05_18 ≝
 [
-  quadrupleT ???? (anyOP HC05 JMP) MODE_DIR1 (Byte 〈xB,xC〉) 〈x0,x2〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_DIR2 (Byte 〈xC,xC〉) 〈x0,x3〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_IX2  (Byte 〈xD,xC〉) 〈x0,x4〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_IX1  (Byte 〈xE,xC〉) 〈x0,x3〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_IX0  (Byte 〈xF,xC〉) 〈x0,x2〉
+  quadrupleT ???? (anyOP HC05 JMP) MODE_IMM1EXT  (Byte 〈xB,xC〉) 〈x0,x2〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_IMM2     (Byte 〈xC,xC〉) 〈x0,x3〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_INHX2ADD (Byte 〈xD,xC〉) 〈x0,x4〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_INHX1ADD (Byte 〈xE,xC〉) 〈x0,x3〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_INHX0ADD (Byte 〈xF,xC〉) 〈x0,x2〉
 ].
 
 definition opcode_table_HC05_19 ≝
 [
-  quadrupleT ???? (anyOP HC05 BSR) MODE_IMM1 (Byte 〈xA,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_DIR1 (Byte 〈xB,xD〉) 〈x0,x5〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_DIR2 (Byte 〈xC,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_IX2  (Byte 〈xD,xD〉) 〈x0,x7〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_IX1  (Byte 〈xE,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_IX0  (Byte 〈xF,xD〉) 〈x0,x5〉
+  quadrupleT ???? (anyOP HC05 BSR) MODE_IMM1     (Byte 〈xA,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_IMM1EXT  (Byte 〈xB,xD〉) 〈x0,x5〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_IMM2     (Byte 〈xC,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_INHX2ADD (Byte 〈xD,xD〉) 〈x0,x7〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_INHX1ADD (Byte 〈xE,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_INHX0ADD (Byte 〈xF,xD〉) 〈x0,x5〉
 ].
 
 definition opcode_table_HC05_20 ≝
@@ -381,33 +378,3 @@ definition opcode_table_HC05 ≝
  opcode_table_HC05_21 @ opcode_table_HC05_22 @ opcode_table_HC05_23 @ opcode_table_HC05_24 @
  opcode_table_HC05_25 @ opcode_table_HC05_26 @ opcode_table_HC05_27 @ opcode_table_HC05_28 @
  opcode_table_HC05_29 @ opcode_table_HC05_30 @ opcode_table_HC05_31.
-
-(* CORRETTEZZA *)
-
-(* HC05: opcode non implementati come da manuale *)
-definition HC05_not_impl ≝
- [〈x3,x1〉;〈x3,x2〉;〈x3,x5〉;〈x3,xB〉;〈x3,xE〉
- ;〈x4,x1〉;〈x4,x5〉;〈x4,xB〉;〈x4,xE〉
- ;〈x5,x1〉;〈x5,x2〉;〈x5,x5〉;〈x5,xB〉;〈x5,xE〉
- ;〈x6,x1〉;〈x6,x2〉;〈x6,x5〉;〈x6,xB〉;〈x6,xE〉
- ;〈x7,x1〉;〈x7,x2〉;〈x7,x5〉;〈x7,xB〉;〈x7,xE〉
- ;〈x8,x2〉;〈x8,x4〉;〈x8,x5〉;〈x8,x6〉;〈x8,x7〉;〈x8,x8〉;〈x8,x9〉;〈x8,xA〉;〈x8,xB〉;〈x8,xC〉;〈x8,xD〉
- ;〈x9,x0〉;〈x9,x1〉;〈x9,x2〉;〈x9,x3〉;〈x9,x4〉;〈x9,x5〉;〈x9,x6〉;〈x9,xE〉
- ;〈xA,x7〉;〈xA,xC〉;〈xA,xF〉
- ].
-
-lemma ok_byte_table_HC05 : forall_byte8 (λb.
- (test_not_impl b HC05_not_impl     ⊕ eqb (get_byte_count HC05 b 0 opcode_table_HC05) 1) ⊗
- (⊖ (test_not_impl b HC05_not_impl) ⊕ eqb (get_byte_count HC05 b 0 opcode_table_HC05) 0))
- = true.
- reflexivity.
-qed.
-
-(*
-lemma ok_OpIm_table_HC05 :
- forall_instr_mode (λi:instr_mode.
- forall_opcode     (λop:opcode.
-  leb (get_OpIm_count HC05 (anyOP HC05 op) i 0 opcode_table_HC05) 1)) = true.
- reflexivity.
-qed.
-*)