helm/software/matita/contribs/ng_assembly/opcodes/HC05_opcode_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/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)).
 110
 111 (* enumerazione delle istruzioni *)
 112 ninductive HC05_opcode: Type ≝
 113   ADC    : HC05_opcode (* add with carry *)
 114 | ADD    : HC05_opcode (* add *)
 115 | AND    : HC05_opcode (* and *)
 116 | ASL    : HC05_opcode (* aritmetic shift left *)
 117 | ASR    : HC05_opcode (* aritmetic shift right *)
 118 | BCC    : HC05_opcode (* branch if C=0 *)
 119 | BCLRn  : HC05_opcode (* clear bit n *)
 120 | BCS    : HC05_opcode (* branch if C=1 *)
 121 | BEQ    : HC05_opcode (* branch if Z=1 *)
 122 | BHCC   : HC05_opcode (* branch if H=0 *)
 123 | BHCS   : HC05_opcode (* branch if H=1 *)
 124 | BHI    : HC05_opcode (* branch if C|Z=0, (higher) *)
 125 | BIH    : HC05_opcode (* branch if nIRQ=1 *)
 126 | BIL    : HC05_opcode (* branch if nIRQ=0 *)
 127 | BIT    : HC05_opcode (* flag = and (bit test) *)
 128 | BLS    : HC05_opcode (* branch if C|Z=1 (lower or same) *)
 129 | BMC    : HC05_opcode (* branch if I=0 (interrupt mask clear) *)
 130 | BMI    : HC05_opcode (* branch if N=1 (minus) *)
 131 | BMS    : HC05_opcode (* branch if I=1 (interrupt mask set) *)
 132 | BNE    : HC05_opcode (* branch if Z=0 *)
 133 | BPL    : HC05_opcode (* branch if N=0 (plus) *)
 134 | BRA    : HC05_opcode (* branch always *)
 135 | BRCLRn : HC05_opcode (* branch if bit n clear *)
 136 | BRN    : HC05_opcode (* branch never (nop) *)
 137 | BRSETn : HC05_opcode (* branch if bit n set *)
 138 | BSETn  : HC05_opcode (* set bit n *)
 139 | BSR    : HC05_opcode (* branch to subroutine *)
 140 | CLC    : HC05_opcode (* C=0 *)
 141 | CLI    : HC05_opcode (* I=0 *)
 142 | CLR    : HC05_opcode (* operand=0 *)
 143 | CMP    : HC05_opcode (* flag = sub (compare A) *)
 144 | COM    : HC05_opcode (* not (1 complement) *)
 145 | CPX    : HC05_opcode (* flag = sub (compare X) *)
 146 | DEC    : HC05_opcode (* operand=operand-1 (decrement) *)
 147 | EOR    : HC05_opcode (* xor *)
 148 | INC    : HC05_opcode (* operand=operand+1 (increment) *)
 149 | JMP    : HC05_opcode (* jmp word [operand] *)
 150 | JSR    : HC05_opcode (* jmp to subroutine *)
 151 | LDA    : HC05_opcode (* load in A *)
 152 | LDX    : HC05_opcode (* load in X *)
 153 | LSR    : HC05_opcode (* logical shift right *)
 154 | MUL    : HC05_opcode (* mul *)
 155 | NEG    : HC05_opcode (* neg (2 complement) *)
 156 | NOP    : HC05_opcode (* nop *)
 157 | ORA    : HC05_opcode (* or *)
 158 | ROL    : HC05_opcode (* rotate left *)
 159 | ROR    : HC05_opcode (* rotate right *)
 160 | RSP    : HC05_opcode (* reset SP (0x00FF) *)
 161 | RTI    : HC05_opcode (* return from interrupt *)
 162 | RTS    : HC05_opcode (* return from subroutine *)
 163 | SBC    : HC05_opcode (* sub with carry*)
 164 | SEC    : HC05_opcode (* C=1 *)
 165 | SEI    : HC05_opcode (* I=1 *)
 166 | STA    : HC05_opcode (* store from A *)
 167 | STOP   : HC05_opcode (* !!stop mode!! *)
 168 | STX    : HC05_opcode (* store from X *)
 169 | SUB    : HC05_opcode (* sub *)
 170 | SWI    : HC05_opcode (* software interrupt *)
 171 | TAX    : HC05_opcode (* X=A (transfer A to X) *)
 172 | TST    : HC05_opcode (* flag = sub (test) *)
 173 | TXA    : HC05_opcode (* A=X (transfer X to A) *)
 174 | WAIT   : HC05_opcode (* !!wait mode!! *)
 175 .
 176
 177 ndefinition eq_HC05_op ≝
 178 λop1,op2:HC05_opcode.
 179  match op1 with
 180   [ ADC ⇒ match op2 with [ ADC ⇒ true | _ ⇒ false ]       | ADD ⇒ match op2 with [ ADD ⇒ true | _ ⇒ false ]
 181   | AND ⇒ match op2 with [ AND ⇒ true | _ ⇒ false ]       | ASL ⇒ match op2 with [ ASL ⇒ true | _ ⇒ false ]
 182   | ASR ⇒ match op2 with [ ASR ⇒ true | _ ⇒ false ]       | BCC ⇒ match op2 with [ BCC ⇒ true | _ ⇒ false ]
 183   | BCLRn ⇒ match op2 with [ BCLRn ⇒ true | _ ⇒ false ]   | BCS ⇒ match op2 with [ BCS ⇒ true | _ ⇒ false ]
 184   | BEQ ⇒ match op2 with [ BEQ ⇒ true | _ ⇒ false ]       | BHCC ⇒ match op2 with [ BHCC ⇒ true | _ ⇒ false ]
 185   | BHCS ⇒ match op2 with [ BHCS ⇒ true | _ ⇒ false ]     | BHI ⇒ match op2 with [ BHI ⇒ true | _ ⇒ false ]
 186   | BIH ⇒ match op2 with [ BIH ⇒ true | _ ⇒ false ]       | BIL ⇒ match op2 with [ BIL ⇒ true | _ ⇒ false ]
 187   | BIT ⇒ match op2 with [ BIT ⇒ true | _ ⇒ false ]       | BLS ⇒ match op2 with [ BLS ⇒ true | _ ⇒ false ]
 188   | BMC ⇒ match op2 with [ BMC ⇒ true | _ ⇒ false ]       | BMI ⇒ match op2 with [ BMI ⇒ true | _ ⇒ false ]
 189   | BMS ⇒ match op2 with [ BMS ⇒ true | _ ⇒ false ]       | BNE ⇒ match op2 with [ BNE ⇒ true | _ ⇒ false ]
 190   | BPL ⇒ match op2 with [ BPL ⇒ true | _ ⇒ false ]       | BRA ⇒ match op2 with [ BRA ⇒ true | _ ⇒ false ]
 191   | BRCLRn ⇒ match op2 with [ BRCLRn ⇒ true | _ ⇒ false ] | BRN ⇒ match op2 with [ BRN ⇒ true | _ ⇒ false ]
 192   | BRSETn ⇒ match op2 with [ BRSETn ⇒ true | _ ⇒ false ] | BSETn ⇒ match op2 with [ BSETn ⇒ true | _ ⇒ false ]
 193   | BSR ⇒ match op2 with [ BSR ⇒ true | _ ⇒ false ]       | CLC ⇒ match op2 with [ CLC ⇒ true | _ ⇒ false ]
 194   | CLI ⇒ match op2 with [ CLI ⇒ true | _ ⇒ false ]       | CLR ⇒ match op2 with [ CLR ⇒ true | _ ⇒ false ]
 195   | CMP ⇒ match op2 with [ CMP ⇒ true | _ ⇒ false ]       | COM ⇒ match op2 with [ COM ⇒ true | _ ⇒ false ]
 196   | CPX ⇒ match op2 with [ CPX ⇒ true | _ ⇒ false ]       | DEC ⇒ match op2 with [ DEC ⇒ true | _ ⇒ false ]
 197   | EOR ⇒ match op2 with [ EOR ⇒ true | _ ⇒ false ]       | INC ⇒ match op2 with [ INC ⇒ true | _ ⇒ false ]
 198   | JMP ⇒ match op2 with [ JMP ⇒ true | _ ⇒ false ]       | JSR ⇒ match op2 with [ JSR ⇒ true | _ ⇒ false ]
 199   | LDA ⇒ match op2 with [ LDA ⇒ true | _ ⇒ false ]       | LDX ⇒ match op2 with [ LDX ⇒ true | _ ⇒ false ]
 200   | LSR ⇒ match op2 with [ LSR ⇒ true | _ ⇒ false ]       | MUL ⇒ match op2 with [ MUL ⇒ true | _ ⇒ false ]
 201   | NEG ⇒ match op2 with [ NEG ⇒ true | _ ⇒ false ]       | NOP ⇒ match op2 with [ NOP ⇒ true | _ ⇒ false ]
 202   | ORA ⇒ match op2 with [ ORA ⇒ true | _ ⇒ false ]       | ROL ⇒ match op2 with [ ROL ⇒ true | _ ⇒ false ]
 203   | ROR ⇒ match op2 with [ ROR ⇒ true | _ ⇒ false ]       | RSP ⇒ match op2 with [ RSP ⇒ true | _ ⇒ false ]
 204   | RTI ⇒ match op2 with [ RTI ⇒ true | _ ⇒ false ]       | RTS ⇒ match op2 with [ RTS ⇒ true | _ ⇒ false ]
 205   | SBC ⇒ match op2 with [ SBC ⇒ true | _ ⇒ false ]       | SEC ⇒ match op2 with [ SEC ⇒ true | _ ⇒ false ]
 206   | SEI ⇒ match op2 with [ SEI ⇒ true | _ ⇒ false ]       | STA ⇒ match op2 with [ STA ⇒ true | _ ⇒ false ]
 207   | STOP ⇒ match op2 with [ STOP ⇒ true | _ ⇒ false ]     | STX ⇒ match op2 with [ STX ⇒ true | _ ⇒ false ]
 208   | SUB ⇒ match op2 with [ SUB ⇒ true | _ ⇒ false ]       | SWI ⇒ match op2 with [ SWI ⇒ true | _ ⇒ false ]
 209   | TAX ⇒ match op2 with [ TAX ⇒ true | _ ⇒ false ]       | TST ⇒ match op2 with [ TST ⇒ true | _ ⇒ false ]
 210   | TXA ⇒ match op2 with [ TXA ⇒ true | _ ⇒ false ]       | WAIT ⇒ match op2 with [ WAIT ⇒ true | _ ⇒ false ]
 211   ].
 212
 213 (* iteratore sugli opcode *)
 214 ndefinition forall_HC05_op ≝ λP:HC05_opcode → bool.
 215  P ADC    ⊗ P ADD    ⊗ P AND    ⊗ P ASL    ⊗ P ASR    ⊗ P BCC    ⊗ P BCLRn  ⊗ P BCS    ⊗
 216  P BEQ    ⊗ P BHCC   ⊗ P BHCS   ⊗ P BHI    ⊗ P BIH    ⊗ P BIL    ⊗ P BIT    ⊗ P BLS    ⊗
 217  P BMC    ⊗ P BMI    ⊗ P BMS    ⊗ P BNE    ⊗ P BPL    ⊗ P BRA    ⊗ P BRCLRn ⊗ P BRN    ⊗
 218  P BRSETn ⊗ P BSETn  ⊗ P BSR    ⊗ P CLC    ⊗ P CLI    ⊗ P CLR    ⊗ P CMP    ⊗ P COM    ⊗
 219  P CPX    ⊗ P DEC    ⊗ P EOR    ⊗ P INC    ⊗ P JMP    ⊗ P JSR    ⊗ P LDA    ⊗ P LDX    ⊗
 220  P LSR    ⊗ P MUL    ⊗ P NEG    ⊗ P NOP    ⊗ P ORA    ⊗ P ROL    ⊗ P ROR    ⊗ P RSP    ⊗
 221  P RTI    ⊗ P RTS    ⊗ P SBC    ⊗ P SEC    ⊗ P SEI    ⊗ P STA    ⊗ P STOP   ⊗ P STX    ⊗
 222  P SUB    ⊗ P SWI    ⊗ P TAX    ⊗ P TST    ⊗ P TXA    ⊗ P WAIT.