helm/software/matita/contribs/ng_assembly/emulator/opcodes/RS08_opcode.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/bool.ma".
  24
  25 (* ********************************************** *)
  26 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  27 (* ********************************************** *)
  28
  29 (* enumerazione delle istruzioni *)
  30 ninductive RS08_opcode: Type ≝
  31   ADC    : RS08_opcode (* add with carry *)
  32 | ADD    : RS08_opcode (* add *)
  33 | AND    : RS08_opcode (* and *)
  34 | ASL    : RS08_opcode (* aritmetic shift left *)
  35 | BCC    : RS08_opcode (* branch if C=0 *)
  36 | BCLRn  : RS08_opcode (* clear bit n *)
  37 | BCS    : RS08_opcode (* branch if C=1 *)
  38 | BEQ    : RS08_opcode (* branch if Z=1 *)
  39 | BGND   : RS08_opcode (* !!background mode!! *)
  40 | BNE    : RS08_opcode (* branch if Z=0 *)
  41 | BRA    : RS08_opcode (* branch always *)
  42 | BRCLRn : RS08_opcode (* branch if bit n clear *)
  43 | BRSETn : RS08_opcode (* branch if bit n set *)
  44 | BSETn  : RS08_opcode (* set bit n *)
  45 | BSR    : RS08_opcode (* branch to subroutine *)
  46 | CBEQA  : RS08_opcode (* compare (A) and BEQ *)
  47 | CLC    : RS08_opcode (* C=0 *)
  48 | CLR    : RS08_opcode (* operand=0 *)
  49 | CMP    : RS08_opcode (* flag = sub (compare A) *)
  50 | COM    : RS08_opcode (* not (1 complement) *)
  51 | DBNZ   : RS08_opcode (* dec and BNE *)
  52 | DEC    : RS08_opcode (* operand=operand-1 (decrement) *)
  53 | EOR    : RS08_opcode (* xor *)
  54 | INC    : RS08_opcode (* operand=operand+1 (increment) *)
  55 | JMP    : RS08_opcode (* jmp word [operand] *)
  56 | JSR    : RS08_opcode (* jmp to subroutine *)
  57 | LDA    : RS08_opcode (* load in A *)
  58 | LSR    : RS08_opcode (* logical shift right *)
  59 | MOV    : RS08_opcode (* move *)
  60 | NOP    : RS08_opcode (* nop *)
  61 | ORA    : RS08_opcode (* or *)
  62 | ROL    : RS08_opcode (* rotate left *)
  63 | ROR    : RS08_opcode (* rotate right *)
  64 | RTS    : RS08_opcode (* return from subroutine *)
  65 | SBC    : RS08_opcode (* sub with carry*)
  66 | SEC    : RS08_opcode (* C=1 *)
  67 | SHA    : RS08_opcode (* swap spc_high,A *)
  68 | SLA    : RS08_opcode (* swap spc_low,A *)
  69 | STA    : RS08_opcode (* store from A *)
  70 | STOP   : RS08_opcode (* !!stop mode!! *)
  71 | SUB    : RS08_opcode (* sub *)
  72 | WAIT   : RS08_opcode (* !!wait mode!! *)
  73 .
  74
  75 ndefinition eq_RS08_op ≝
  76 λop1,op2:RS08_opcode.
  77  match op1 with
  78   [ ADC ⇒ match op2 with [ ADC ⇒ true | _ ⇒ false ]       | ADD ⇒ match op2 with [ ADD ⇒ true | _ ⇒ false ]
  79   | AND ⇒ match op2 with [ AND ⇒ true | _ ⇒ false ]       | ASL ⇒ match op2 with [ ASL ⇒ true | _ ⇒ false ]
  80   | BCC ⇒ match op2 with [ BCC ⇒ true | _ ⇒ false ]       | BCLRn ⇒ match op2 with [ BCLRn ⇒ true | _ ⇒ false ]
  81   | BCS ⇒ match op2 with [ BCS ⇒ true | _ ⇒ false ]       | BEQ ⇒ match op2 with [ BEQ ⇒ true | _ ⇒ false ]
  82   | BGND ⇒ match op2 with [ BGND ⇒ true | _ ⇒ false ]     | BNE ⇒ match op2 with [ BNE ⇒ true | _ ⇒ false ]
  83   | BRA ⇒ match op2 with [ BRA ⇒ true | _ ⇒ false ]       | BRCLRn ⇒ match op2 with [ BRCLRn ⇒ true | _ ⇒ false ]
  84   | BRSETn ⇒ match op2 with [ BRSETn ⇒ true | _ ⇒ false ] | BSETn ⇒ match op2 with [ BSETn ⇒ true | _ ⇒ false ]
  85   | BSR ⇒ match op2 with [ BSR ⇒ true | _ ⇒ false ]       | CBEQA ⇒ match op2 with [ CBEQA ⇒ true | _ ⇒ false ]
  86   | CLC ⇒ match op2 with [ CLC ⇒ true | _ ⇒ false ]       | CLR ⇒ match op2 with [ CLR ⇒ true | _ ⇒ false ]
  87   | CMP ⇒ match op2 with [ CMP ⇒ true | _ ⇒ false ]       | COM ⇒ match op2 with [ COM ⇒ true | _ ⇒ false ]
  88   | DBNZ ⇒ match op2 with [ DBNZ ⇒ true | _ ⇒ false ]     | DEC ⇒ match op2 with [ DEC ⇒ true | _ ⇒ false ]
  89   | EOR ⇒ match op2 with [ EOR ⇒ true | _ ⇒ false ]       | INC ⇒ match op2 with [ INC ⇒ true | _ ⇒ false ]
  90   | JMP ⇒ match op2 with [ JMP ⇒ true | _ ⇒ false ]       | JSR ⇒ match op2 with [ JSR ⇒ true | _ ⇒ false ]
  91   | LDA ⇒ match op2 with [ LDA ⇒ true | _ ⇒ false ]       | LSR ⇒ match op2 with [ LSR ⇒ true | _ ⇒ false ]
  92   | MOV ⇒ match op2 with [ MOV ⇒ true | _ ⇒ false ]       | NOP ⇒ match op2 with [ NOP ⇒ true | _ ⇒ false ]
  93   | ORA ⇒ match op2 with [ ORA ⇒ true | _ ⇒ false ]       | ROL ⇒ match op2 with [ ROL ⇒ true | _ ⇒ false ]
  94   | ROR ⇒ match op2 with [ ROR ⇒ true | _ ⇒ false ]       | RTS ⇒ match op2 with [ RTS ⇒ true | _ ⇒ false ]
  95   | SBC ⇒ match op2 with [ SBC ⇒ true | _ ⇒ false ]       | SEC ⇒ match op2 with [ SEC ⇒ true | _ ⇒ false ]
  96   | SHA ⇒ match op2 with [ SHA ⇒ true | _ ⇒ false ]       | SLA ⇒ match op2 with [ SLA ⇒ true | _ ⇒ false ]
  97   | STA ⇒ match op2 with [ STA ⇒ true | _ ⇒ false ]       | STOP ⇒ match op2 with [ STOP ⇒ true | _ ⇒ false ]
  98   | SUB ⇒ match op2 with [ SUB ⇒ true | _ ⇒ false ]       | WAIT ⇒ match op2 with [ WAIT ⇒ true | _ ⇒ false ]
  99   ].
 100
 101 (* iteratore sugli opcode *)
 102 ndefinition forall_RS08_op ≝ λP:RS08_opcode → bool.
 103  P ADC    ⊗ P ADD    ⊗ P AND    ⊗ P ASL    ⊗ P BCC    ⊗ P BCLRn  ⊗ P BCS    ⊗ P BEQ    ⊗
 104  P BGND   ⊗ P BNE    ⊗ P BRA    ⊗ P BRCLRn ⊗ P BRSETn ⊗ P BSETn  ⊗ P BSR    ⊗ P CBEQA  ⊗
 105  P CLC    ⊗ P CLR    ⊗ P CMP    ⊗ P COM    ⊗ P DBNZ   ⊗ P DEC    ⊗ P EOR    ⊗ P INC    ⊗
 106  P JMP    ⊗ P JSR    ⊗ P LDA    ⊗ P LSR    ⊗ P MOV    ⊗ P NOP    ⊗ P ORA    ⊗ P ROL    ⊗
 107  P ROR    ⊗ P RTS    ⊗ P SBC    ⊗ P SEC    ⊗ P SHA    ⊗ P SLA    ⊗ P STA    ⊗ P STOP   ⊗
 108  P SUB    ⊗ P WAIT.