matita/matita/contribs/ng_assembly2/emulator/opcodes/Freescale_instr_mode_base.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/exadecim.ma".
  24 include "num/bitrigesim.ma".
  25
  26 (* ********************************************** *)
  27 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  28 (* ********************************************** *)
  29
  30 (* enumerazione delle modalita' di indirizzamento = caricamento degli operandi *)
  31 ninductive Freescale_instr_mode: Type ≝
  32   (* INHERENT = nessun operando *)
  33   MODE_INH  : Freescale_instr_mode
  34   (* INHERENT = nessun operando (A implicito) *)
  35 | MODE_INHA : Freescale_instr_mode
  36   (* INHERENT = nessun operando (X implicito) *)
  37 | MODE_INHX : Freescale_instr_mode
  38   (* INHERENT = nessun operando (H implicito) *)
  39 | MODE_INHH : Freescale_instr_mode
  40
  41   (* INHERENT_ADDRESS = nessun operando (HX implicito) *)
  42 | MODE_INHX0ADD : Freescale_instr_mode
  43   (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *)
  44 | MODE_INHX1ADD : Freescale_instr_mode
  45   (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *)
  46 | MODE_INHX2ADD : Freescale_instr_mode
  47
  48   (* IMMEDIATE = operando valore immediato byte = 0xbb *)
  49 | MODE_IMM1 : Freescale_instr_mode
  50   (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *)
  51 | MODE_IMM1EXT : Freescale_instr_mode
  52   (* IMMEDIATE = operando valore immediato word = 0xwwww *)
  53 | MODE_IMM2 : Freescale_instr_mode
  54   (* DIRECT = operando offset byte = [0x00bb] *)
  55 | MODE_DIR1 : Freescale_instr_mode
  56   (* DIRECT = operando offset word = [0xwwww] *)
  57 | MODE_DIR2 : Freescale_instr_mode
  58   (* INDEXED = nessun operando (implicito [X] *)
  59 | MODE_IX0  : Freescale_instr_mode
  60   (* INDEXED = operando offset relativo byte = [X+0x00bb] *)
  61 | MODE_IX1  : Freescale_instr_mode
  62   (* INDEXED = operando offset relativo word = [X+0xwwww] *)
  63 | MODE_IX2  : Freescale_instr_mode
  64   (* INDEXED = operando offset relativo byte = [SP+0x00bb] *)
  65 | MODE_SP1  : Freescale_instr_mode
  66   (* INDEXED = operando offset relativo word = [SP+0xwwww] *)
  67 | MODE_SP2  : Freescale_instr_mode
  68
  69   (* DIRECT → DIRECT = carica da diretto/scrive su diretto *)
  70 | MODE_DIR1_to_DIR1 : Freescale_instr_mode
  71   (* IMMEDIATE → DIRECT = carica da immediato/scrive su diretto *)
  72 | MODE_IMM1_to_DIR1 : Freescale_instr_mode
  73   (* INDEXED++ → DIRECT = carica da [X]/scrive su diretto/H:X++ *)
  74 | MODE_IX0p_to_DIR1 : Freescale_instr_mode
  75   (* DIRECT → INDEXED++ = carica da diretto/scrive su [X]/H:X++ *)
  76 | MODE_DIR1_to_IX0p : Freescale_instr_mode
  77
  78   (* INHERENT(A) + IMMEDIATE *)
  79 | MODE_INHA_and_IMM1 : Freescale_instr_mode
  80   (* INHERENT(X) + IMMEDIATE *)
  81 | MODE_INHX_and_IMM1 : Freescale_instr_mode
  82   (* IMMEDIATE + IMMEDIATE *)
  83 | MODE_IMM1_and_IMM1 : Freescale_instr_mode
  84   (* DIRECT + IMMEDIATE *)
  85 | MODE_DIR1_and_IMM1 : Freescale_instr_mode
  86   (* INDEXED + IMMEDIATE *)
  87 | MODE_IX0_and_IMM1  : Freescale_instr_mode
  88   (* INDEXED++ + IMMEDIATE *)
  89 | MODE_IX0p_and_IMM1 : Freescale_instr_mode
  90   (* INDEXED + IMMEDIATE *)
  91 | MODE_IX1_and_IMM1  : Freescale_instr_mode
  92   (* INDEXED++ + IMMEDIATE *)
  93 | MODE_IX1p_and_IMM1 : Freescale_instr_mode
  94   (* INDEXED + IMMEDIATE *)
  95 | MODE_SP1_and_IMM1  : Freescale_instr_mode
  96
  97   (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *)
  98   (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *)
  99 | MODE_DIRn          : oct → Freescale_instr_mode
 100   (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *)
 101   (*                            + operando valore immediato byte  *)
 102   (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *)
 103 | MODE_DIRn_and_IMM1 : oct → Freescale_instr_mode
 104   (* TINY = nessun operando (diretto implicito 4bit = [0x00000000:0000iiii]) *)
 105 | MODE_TNY           : exadecim → Freescale_instr_mode
 106   (* SHORT = nessun operando (diretto implicito 5bit = [0x00000000:000iiiii]) *)
 107 | MODE_SRT           : bitrigesim → Freescale_instr_mode
 108 .
 109
 110 ndefinition eq_Freescale_im ≝
 111 λi1,i2:Freescale_instr_mode.
 112  match i1 with
 113   [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
 114   | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ]
 115   | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ true | _ ⇒ false ]
 116   | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ true | _ ⇒ false ]
 117   | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ true | _ ⇒ false ]
 118   | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ true | _ ⇒ false ]
 119   | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ true | _ ⇒ false ]
 120   | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ]
 121   | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ true | _ ⇒ false ]
 122   | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ]
 123   | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ]
 124   | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ true | _ ⇒ false ]
 125   | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ true | _ ⇒ false ]
 126   | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ true | _ ⇒ false ]
 127   | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ true | _ ⇒ false ]
 128   | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ true | _ ⇒ false ]
 129   | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ true | _ ⇒ false ]
 130   | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ true | _ ⇒ false ]
 131   | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ true | _ ⇒ false ]
 132   | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ true | _ ⇒ false ]
 133   | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ true | _ ⇒ false ]
 134   | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ true | _ ⇒ false ]
 135   | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ true | _ ⇒ false ]
 136   | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ true | _ ⇒ false ]
 137   | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ true | _ ⇒ false ]
 138   | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ true | _ ⇒ false ]
 139   | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ true | _ ⇒ false ]
 140   | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ true | _ ⇒ false ]
 141   | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ true | _ ⇒ false ]
 142   | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ true | _ ⇒ false ]
 143   | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eqc ? n1 n2 | _ ⇒ false ]
 144   | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2  ⇒ eqc ? n1 n2 | _ ⇒ false ]
 145   | MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eqc ? e1 e2 | _ ⇒ false ]
 146   | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eqc ? t1 t2 | _ ⇒ false ]
 147   ].
 148
 149 ndefinition forall_Freescale_im ≝ λP:Freescale_instr_mode → bool.
 150   P MODE_INH
 151 ⊗ P MODE_INHA
 152 ⊗ P MODE_INHX
 153 ⊗ P MODE_INHH
 154
 155 ⊗ P MODE_INHX0ADD
 156 ⊗ P MODE_INHX1ADD
 157 ⊗ P MODE_INHX2ADD
 158
 159 ⊗ P MODE_IMM1
 160 ⊗ P MODE_IMM1EXT
 161 ⊗ P MODE_IMM2
 162 ⊗ P MODE_DIR1
 163 ⊗ P MODE_DIR2
 164 ⊗ P MODE_IX0
 165 ⊗ P MODE_IX1
 166 ⊗ P MODE_IX2
 167 ⊗ P MODE_SP1
 168 ⊗ P MODE_SP2
 169
 170 ⊗ P MODE_DIR1_to_DIR1
 171 ⊗ P MODE_IMM1_to_DIR1
 172 ⊗ P MODE_IX0p_to_DIR1
 173 ⊗ P MODE_DIR1_to_IX0p
 174
 175 ⊗ P MODE_INHA_and_IMM1
 176 ⊗ P MODE_INHX_and_IMM1
 177 ⊗ P MODE_IMM1_and_IMM1
 178 ⊗ P MODE_DIR1_and_IMM1
 179 ⊗ P MODE_IX0_and_IMM1
 180 ⊗ P MODE_IX0p_and_IMM1
 181 ⊗ P MODE_IX1_and_IMM1
 182 ⊗ P MODE_IX1p_and_IMM1
 183 ⊗ P MODE_SP1_and_IMM1
 184
 185 ⊗ forallc ? (λo. P (MODE_DIRn o))
 186 ⊗ forallc ? (λo. P (MODE_DIRn_and_IMM1 o))
 187 ⊗ forallc ? (λe. P (MODE_TNY e))
 188 ⊗ forallc ? (λt. P (MODE_SRT t)).