helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.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 IP2022_pseudo: Type ≝
  31   ADD     : IP2022_pseudo (* add *)
  32 | ADDC    : IP2022_pseudo (* add with carry *)
  33 | AND     : IP2022_pseudo (* and *)
  34 | BREAK   : IP2022_pseudo (* enter break mode *)
  35 | BREAKX  : IP2022_pseudo (* enter break mode, after skip *)
  36 | CALL    : IP2022_pseudo (* subroutine call *)
  37 | CLR     : IP2022_pseudo (* clear *)
  38 | CLRB    : IP2022_pseudo (* clear bit *)
  39 | CMP     : IP2022_pseudo (* set flags according to sub *)
  40 | CSE     : IP2022_pseudo (* confront & skip if equal *)
  41 | CSNE    : IP2022_pseudo (* confront & skip if not equal *)
  42 | CWDT    : IP2022_pseudo (* clear watch dog -- not impl. ERR *)
  43 | DEC     : IP2022_pseudo (* decrement *)
  44 | DECSNZ  : IP2022_pseudo (* decrement & skip if not zero *)
  45 | DECSZ   : IP2022_pseudo (* decrement & skip if zero *)
  46 | FERASE  : IP2022_pseudo (* flash erase -- not impl. ERR *)
  47 | FREAD   : IP2022_pseudo (* flash read -- not impl. ERR *)
  48 | FWRITE  : IP2022_pseudo (* flash write -- not impl. ERR *)
  49 | INC     : IP2022_pseudo (* increment *)
  50 | INCSNZ  : IP2022_pseudo (* increment & skip if not zero *)
  51 | INCSZ   : IP2022_pseudo (* increment & skip if zero *)
  52 | INT     : IP2022_pseudo (* interrupt -- not impl. ERR *)
  53 | IREAD   : IP2022_pseudo (* memory read *)
  54 | IREADI  : IP2022_pseudo (* memory read & inc *)
  55 | IWRITE  : IP2022_pseudo (* memory write *)
  56 | IWRITEI : IP2022_pseudo (* memory write & inc *)
  57 | JMP     : IP2022_pseudo (* jump *)
  58 | LOADH   : IP2022_pseudo (* load Data Pointer High *)
  59 | LOADL   : IP2022_pseudo (* load Data Pointer Low *)
  60 | MOV     : IP2022_pseudo (* move *)
  61 | MULS    : IP2022_pseudo (* signed mul *)
  62 | MULU    : IP2022_pseudo (* unsigned mul *)
  63 | NOP     : IP2022_pseudo (* nop *)
  64 | NOT     : IP2022_pseudo (* not *)
  65 | OR      : IP2022_pseudo (* or *)
  66 | PAGE    : IP2022_pseudo (* set Page Register *)
  67 | POP     : IP2022_pseudo (* pop *)
  68 | PUSH    : IP2022_pseudo (* push *)
  69 | RET     : IP2022_pseudo (* subroutine ret *)
  70 | RETI    : IP2022_pseudo (* interrupt ret -- not impl. ERR *)
  71 | RETNP   : IP2022_pseudo (* subroutine ret & don't restore Page Register *)
  72 | RETW    : IP2022_pseudo (* subroutine ret & load W Register *)
  73 | RL      : IP2022_pseudo (* rotate left *)
  74 | RR      : IP2022_pseudo (* rotate right *)
  75 | SB      : IP2022_pseudo (* skip if bit set *)
  76 | SETB    : IP2022_pseudo (* set bit *)
  77 | SNB     : IP2022_pseudo (* skip if bit not set *)
  78 | SPEED   : IP2022_pseudo (* set Speed Register *)
  79 | SUB     : IP2022_pseudo (* sub *)
  80 | SUBC    : IP2022_pseudo (* sub with carry *)
  81 | SWAP    : IP2022_pseudo (* swap xxxxyyyy → yyyyxxxx *)
  82 | TEST    : IP2022_pseudo (* set flags according to zero test *)
  83 | XOR     : IP2022_pseudo (* xor *)
  84 .
  85
  86 ndefinition eq_IP2022_pseudo ≝
  87 λps1,ps2:IP2022_pseudo.
  88  match ps1 with
  89   [ ADD ⇒ match ps2 with [ ADD ⇒ true | _ ⇒ false ]       | ADDC ⇒ match ps2 with [ ADDC ⇒ true | _ ⇒ false ]
  90   | AND ⇒ match ps2 with [ AND ⇒ true | _ ⇒ false ]       | BREAK ⇒ match ps2 with [ BREAK ⇒ true | _ ⇒ false ]
  91   | BREAKX ⇒ match ps2 with [ BREAKX ⇒ true | _ ⇒ false ] | CALL ⇒ match ps2 with [ CALL ⇒ true | _ ⇒ false ]
  92   | CLR ⇒ match ps2 with [ CLR ⇒ true | _ ⇒ false ]       | CLRB ⇒ match ps2 with [ CLRB ⇒ true | _ ⇒ false ]
  93   | CMP ⇒ match ps2 with [ CMP ⇒ true | _ ⇒ false ]       | CSE ⇒ match ps2 with [ CSE ⇒ true | _ ⇒ false ]
  94   | CSNE ⇒ match ps2 with [ CSNE ⇒ true | _ ⇒ false ]     | CWDT ⇒ match ps2 with [ CWDT ⇒ true | _ ⇒ false ]
  95   | DEC ⇒ match ps2 with [ DEC ⇒ true | _ ⇒ false ]       | DECSNZ ⇒ match ps2 with [ DECSNZ ⇒ true | _ ⇒ false ]
  96   | DECSZ ⇒ match ps2 with [ DECSZ ⇒ true | _ ⇒ false ]   | FERASE ⇒ match ps2 with [ FERASE ⇒ true | _ ⇒ false ]
  97   | FREAD ⇒ match ps2 with [ FREAD ⇒ true | _ ⇒ false ]   | FWRITE ⇒ match ps2 with [ FWRITE ⇒ true | _ ⇒ false ]
  98   | INC ⇒ match ps2 with [ INC ⇒ true | _ ⇒ false ]       | INCSNZ ⇒ match ps2 with [ INCSNZ ⇒ true | _ ⇒ false ]
  99   | INCSZ ⇒ match ps2 with [ INCSZ ⇒ true | _ ⇒ false ]   | INT ⇒ match ps2 with [ INT ⇒ true | _ ⇒ false ]
 100   | IREAD ⇒ match ps2 with [ IREAD ⇒ true | _ ⇒ false ]   | IREADI ⇒ match ps2 with [ IREADI ⇒ true | _ ⇒ false ]
 101   | IWRITE ⇒ match ps2 with [ IWRITE ⇒ true | _ ⇒ false ] | IWRITEI ⇒ match ps2 with [ IWRITEI ⇒ true | _ ⇒ false ]
 102   | JMP ⇒ match ps2 with [ JMP ⇒ true | _ ⇒ false ]       | LOADH ⇒ match ps2 with [ LOADH ⇒ true | _ ⇒ false ]
 103   | LOADL ⇒ match ps2 with [ LOADL ⇒ true | _ ⇒ false ]   | MOV ⇒ match ps2 with [ MOV ⇒ true | _ ⇒ false ]
 104   | MULS ⇒ match ps2 with [ MULS ⇒ true | _ ⇒ false ]     | MULU ⇒ match ps2 with [ MULU ⇒ true | _ ⇒ false ]
 105   | NOP ⇒ match ps2 with [ NOP ⇒ true | _ ⇒ false ]       | NOT ⇒ match ps2 with [ NOT ⇒ true | _ ⇒ false ]
 106   | OR ⇒ match ps2 with [ OR ⇒ true | _ ⇒ false ]         | PAGE ⇒ match ps2 with [ PAGE ⇒ true | _ ⇒ false ]
 107   | POP ⇒ match ps2 with [ POP ⇒ true | _ ⇒ false ]       | PUSH ⇒ match ps2 with [ PUSH ⇒ true | _ ⇒ false ]
 108   | RET ⇒ match ps2 with [ RET ⇒ true | _ ⇒ false ]       | RETI ⇒ match ps2 with [ RETI ⇒ true | _ ⇒ false ]
 109   | RETNP ⇒ match ps2 with [ RETNP ⇒ true | _ ⇒ false ]   | RETW ⇒ match ps2 with [ RETW ⇒ true | _ ⇒ false ]
 110   | RL ⇒ match ps2 with [ RL ⇒ true | _ ⇒ false ]         | RR ⇒ match ps2 with [ RR ⇒ true | _ ⇒ false ]
 111   | SB ⇒ match ps2 with [ SB ⇒ true | _ ⇒ false ]         | SETB ⇒ match ps2 with [ SETB ⇒ true | _ ⇒ false ]
 112   | SNB ⇒ match ps2 with [ SNB ⇒ true | _ ⇒ false ]       | SPEED ⇒ match ps2 with [ SPEED ⇒ true | _ ⇒ false ]
 113   | SUB ⇒ match ps2 with [ SUB ⇒ true | _ ⇒ false ]       | SUBC ⇒ match ps2 with [ SUBC ⇒ true | _ ⇒ false ]
 114   | SWAP ⇒ match ps2 with [ SWAP ⇒ true | _ ⇒ false ]     | TEST ⇒ match ps2 with [ TEST ⇒ true | _ ⇒ false ]
 115   | XOR ⇒ match ps2 with [ XOR ⇒ true | _ ⇒ false ]
 116   ].
 117
 118 ndefinition forall_IP2022_pseudo ≝ λP:IP2022_pseudo → bool.
 119  P ADD     ⊗ P ADDC    ⊗ P AND     ⊗ P BREAK   ⊗ P BREAKX  ⊗ P CALL    ⊗ P CLR    ⊗ P CLRB    ⊗
 120  P CMP     ⊗ P CSE     ⊗ P CSNE    ⊗ P CWDT    ⊗ P DEC     ⊗ P DECSNZ  ⊗ P DECSZ  ⊗ P FERASE  ⊗
 121  P FREAD   ⊗ P FWRITE  ⊗ P INC     ⊗ P INCSNZ  ⊗ P INCSZ   ⊗ P INT     ⊗ P IREAD  ⊗ P IREADI  ⊗
 122  P IWRITE  ⊗ P IWRITEI ⊗ P JMP     ⊗ P LOADH   ⊗ P LOADL   ⊗ P MOV     ⊗ P MULS   ⊗ P MULU    ⊗
 123  P NOP     ⊗ P NOT     ⊗ P OR      ⊗ P PAGE    ⊗ P POP     ⊗ P PUSH    ⊗ P RET    ⊗ P RETI    ⊗
 124  P RETNP   ⊗ P RETW    ⊗ P RL      ⊗ P RR      ⊗ P SB      ⊗ P SETB    ⊗ P SNB    ⊗ P SPEED   ⊗
 125  P SUB     ⊗ P SUBC    ⊗ P SWAP    ⊗ P TEST    ⊗ P XOR.