helm/software/matita/contribs/ng_assembly/emulator/opcodes/HC05_instr_mode.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/word16.ma".
  24
  25 (* ********************************************** *)
  26 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  27 (* ********************************************** *)
  28
  29 (* enumerazione delle modalita' di indirizzamento = caricamento degli operandi *)
  30 ninductive HC05_instr_mode: Type ≝
  31   (* INHERENT = nessun operando *)
  32   MODE_INH  : HC05_instr_mode
  33   (* INHERENT = nessun operando (A implicito) *)
  34 | MODE_INHA : HC05_instr_mode
  35   (* INHERENT = nessun operando (X implicito) *)
  36 | MODE_INHX : HC05_instr_mode
  37
  38   (* INHERENT_ADDRESS = nessun operando (HX implicito) *)
  39 | MODE_INHX0ADD : HC05_instr_mode
  40   (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *)
  41 | MODE_INHX1ADD : HC05_instr_mode
  42   (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *)
  43 | MODE_INHX2ADD : HC05_instr_mode
  44
  45   (* IMMEDIATE = operando valore immediato byte = 0xbb *)
  46 | MODE_IMM1 : HC05_instr_mode
  47   (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *)
  48 | MODE_IMM1EXT : HC05_instr_mode
  49   (* IMMEDIATE = operando valore immediato word = 0xwwww *)
  50 | MODE_IMM2 : HC05_instr_mode
  51   (* DIRECT = operando offset byte = [0x00bb] *)
  52 | MODE_DIR1 : HC05_instr_mode
  53   (* DIRECT = operando offset word = [0xwwww] *)
  54 | MODE_DIR2 : HC05_instr_mode
  55   (* INDEXED = nessun operando (implicito [X] *)
  56 | MODE_IX0  : HC05_instr_mode
  57   (* INDEXED = operando offset relativo byte = [X+0x00bb] *)
  58 | MODE_IX1  : HC05_instr_mode
  59   (* INDEXED = operando offset relativo word = [X+0xwwww] *)
  60 | MODE_IX2  : HC05_instr_mode
  61
  62   (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *)
  63   (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *)
  64 | MODE_DIRn          : oct → HC05_instr_mode
  65   (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *)
  66   (*                            + operando valore immediato byte  *)
  67   (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *)
  68 | MODE_DIRn_and_IMM1 : oct → HC05_instr_mode
  69 .
  70
  71 ndefinition eq_HC05_im ≝
  72 λi1,i2:HC05_instr_mode.
  73  match i1 with
  74   [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
  75   | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ]
  76   | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ true | _ ⇒ false ]
  77   | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ true | _ ⇒ false ]
  78   | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ true | _ ⇒ false ]
  79   | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ true | _ ⇒ false ]
  80   | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ]
  81   | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ true | _ ⇒ false ]
  82   | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ]
  83   | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ]
  84   | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ true | _ ⇒ false ]
  85   | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ true | _ ⇒ false ]
  86   | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ true | _ ⇒ false ]
  87   | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ true | _ ⇒ false ]
  88   | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
  89   | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2  ⇒ eq_oct n1 n2 | _ ⇒ false ]
  90   ].
  91
  92 (* iteratore sulle modalita' *)
  93 ndefinition forall_HC05_im ≝ λP:HC05_instr_mode → bool.
  94   P MODE_INH
  95 ⊗ P MODE_INHA
  96 ⊗ P MODE_INHX
  97 ⊗ P MODE_INHX0ADD
  98 ⊗ P MODE_INHX1ADD
  99 ⊗ P MODE_INHX2ADD
 100 ⊗ P MODE_IMM1
 101 ⊗ P MODE_IMM1EXT
 102 ⊗ P MODE_IMM2
 103 ⊗ P MODE_DIR1
 104 ⊗ P MODE_DIR2
 105 ⊗ P MODE_IX0
 106 ⊗ P MODE_IX1
 107 ⊗ P MODE_IX2
 108 ⊗ forall_oct (λo. P (MODE_DIRn o))
 109 ⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o)).