helm/software/matita/contribs/ng_assembly2/emulator/opcodes/IP2022_pseudo_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/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 (* NB: ignorata la differenza IREAD/IREADI perche' non e' implementata EXT_MEM
  55        IREAD → ADDRX= 0x00 ram, 0x01 flash, 0x80 0x81 ext_mem
  56        IREADI → ADDRX= 0x00 ram, 0x01 flash *)
  57 | IWRITE  : IP2022_pseudo (* memory write *)
  58 (* NB: ignorata la differenza IWRITE/IWRITEI perche' non e' implementata EXT_MEM
  59        IREAD → ADDRX= 0x00 ram, 0x80 0x81 ext_mem
  60        IREADI → ADDRX= 0x00 ram *)
  61 | JMP     : IP2022_pseudo (* jump *)
  62 | LOADH   : IP2022_pseudo (* load Data Pointer High *)
  63 | LOADL   : IP2022_pseudo (* load Data Pointer Low *)
  64 | MOV     : IP2022_pseudo (* move *)
  65 | MULS    : IP2022_pseudo (* signed mul *)
  66 | MULU    : IP2022_pseudo (* unsigned mul *)
  67 | NOP     : IP2022_pseudo (* nop *)
  68 | NOT     : IP2022_pseudo (* not *)
  69 | OR      : IP2022_pseudo (* or *)
  70 | PAGE    : IP2022_pseudo (* set Page Register *)
  71 | POP     : IP2022_pseudo (* pop *)
  72 | PUSH    : IP2022_pseudo (* push *)
  73 | RET     : IP2022_pseudo (* subroutine ret *)
  74 | RETI    : IP2022_pseudo (* interrupt ret -- not impl. ERR *)
  75 | RETNP   : IP2022_pseudo (* subroutine ret & don't restore Page Register *)
  76 | RETW    : IP2022_pseudo (* subroutine ret & load W Register *)
  77 | RL      : IP2022_pseudo (* rotate left *)
  78 | RR      : IP2022_pseudo (* rotate right *)
  79 | SB      : IP2022_pseudo (* skip if bit set *)
  80 | SETB    : IP2022_pseudo (* set bit *)
  81 | SNB     : IP2022_pseudo (* skip if bit not set *)
  82 | SPEED   : IP2022_pseudo (* set Speed Register *)
  83 | SUB     : IP2022_pseudo (* sub *)
  84 | SUBC    : IP2022_pseudo (* sub with carry *)
  85 | SWAP    : IP2022_pseudo (* swap xxxxyyyy → yyyyxxxx *)
  86 | TEST    : IP2022_pseudo (* set flags according to zero test *)
  87 | XOR     : IP2022_pseudo (* xor *)
  88 .
  89
  90 ndefinition eq_IP2022_pseudo ≝
  91 λps1,ps2:IP2022_pseudo.
  92  match ps1 with
  93   [ ADD ⇒ match ps2 with [ ADD ⇒ true | _ ⇒ false ]       | ADDC ⇒ match ps2 with [ ADDC ⇒ true | _ ⇒ false ]
  94   | AND ⇒ match ps2 with [ AND ⇒ true | _ ⇒ false ]       | BREAK ⇒ match ps2 with [ BREAK ⇒ true | _ ⇒ false ]
  95   | BREAKX ⇒ match ps2 with [ BREAKX ⇒ true | _ ⇒ false ] | CALL ⇒ match ps2 with [ CALL ⇒ true | _ ⇒ false ]
  96   | CLR ⇒ match ps2 with [ CLR ⇒ true | _ ⇒ false ]       | CLRB ⇒ match ps2 with [ CLRB ⇒ true | _ ⇒ false ]
  97   | CMP ⇒ match ps2 with [ CMP ⇒ true | _ ⇒ false ]       | CSE ⇒ match ps2 with [ CSE ⇒ true | _ ⇒ false ]
  98   | CSNE ⇒ match ps2 with [ CSNE ⇒ true | _ ⇒ false ]     | CWDT ⇒ match ps2 with [ CWDT ⇒ true | _ ⇒ false ]
  99   | DEC ⇒ match ps2 with [ DEC ⇒ true | _ ⇒ false ]       | DECSNZ ⇒ match ps2 with [ DECSNZ ⇒ true | _ ⇒ false ]
 100   | DECSZ ⇒ match ps2 with [ DECSZ ⇒ true | _ ⇒ false ]   | FERASE ⇒ match ps2 with [ FERASE ⇒ true | _ ⇒ false ]
 101   | FREAD ⇒ match ps2 with [ FREAD ⇒ true | _ ⇒ false ]   | FWRITE ⇒ match ps2 with [ FWRITE ⇒ true | _ ⇒ false ]
 102   | INC ⇒ match ps2 with [ INC ⇒ true | _ ⇒ false ]       | INCSNZ ⇒ match ps2 with [ INCSNZ ⇒ true | _ ⇒ false ]
 103   | INCSZ ⇒ match ps2 with [ INCSZ ⇒ true | _ ⇒ false ]   | INT ⇒ match ps2 with [ INT ⇒ true | _ ⇒ false ]
 104   | IREAD ⇒ match ps2 with [ IREAD ⇒ true | _ ⇒ false ]   | IWRITE ⇒ match ps2 with [ IWRITE ⇒ true | _ ⇒ false ]
 105   | JMP ⇒ match ps2 with [ JMP ⇒ true | _ ⇒ false ]       | LOADH ⇒ match ps2 with [ LOADH ⇒ true | _ ⇒ false ]
 106   | LOADL ⇒ match ps2 with [ LOADL ⇒ true | _ ⇒ false ]   | MOV ⇒ match ps2 with [ MOV ⇒ true | _ ⇒ false ]
 107   | MULS ⇒ match ps2 with [ MULS ⇒ true | _ ⇒ false ]     | MULU ⇒ match ps2 with [ MULU ⇒ true | _ ⇒ false ]
 108   | NOP ⇒ match ps2 with [ NOP ⇒ true | _ ⇒ false ]       | NOT ⇒ match ps2 with [ NOT ⇒ true | _ ⇒ false ]
 109   | OR ⇒ match ps2 with [ OR ⇒ true | _ ⇒ false ]         | PAGE ⇒ match ps2 with [ PAGE ⇒ true | _ ⇒ false ]
 110   | POP ⇒ match ps2 with [ POP ⇒ true | _ ⇒ false ]       | PUSH ⇒ match ps2 with [ PUSH ⇒ true | _ ⇒ false ]
 111   | RET ⇒ match ps2 with [ RET ⇒ true | _ ⇒ false ]       | RETI ⇒ match ps2 with [ RETI ⇒ true | _ ⇒ false ]
 112   | RETNP ⇒ match ps2 with [ RETNP ⇒ true | _ ⇒ false ]   | RETW ⇒ match ps2 with [ RETW ⇒ true | _ ⇒ false ]
 113   | RL ⇒ match ps2 with [ RL ⇒ true | _ ⇒ false ]         | RR ⇒ match ps2 with [ RR ⇒ true | _ ⇒ false ]
 114   | SB ⇒ match ps2 with [ SB ⇒ true | _ ⇒ false ]         | SETB ⇒ match ps2 with [ SETB ⇒ true | _ ⇒ false ]
 115   | SNB ⇒ match ps2 with [ SNB ⇒ true | _ ⇒ false ]       | SPEED ⇒ match ps2 with [ SPEED ⇒ true | _ ⇒ false ]
 116   | SUB ⇒ match ps2 with [ SUB ⇒ true | _ ⇒ false ]       | SUBC ⇒ match ps2 with [ SUBC ⇒ true | _ ⇒ false ]
 117   | SWAP ⇒ match ps2 with [ SWAP ⇒ true | _ ⇒ false ]     | TEST ⇒ match ps2 with [ TEST ⇒ true | _ ⇒ false ]
 118   | XOR ⇒ match ps2 with [ XOR ⇒ true | _ ⇒ false ]
 119   ].
 120
 121 ndefinition forall_IP2022_pseudo ≝ λP:IP2022_pseudo → bool.
 122  P ADD     ⊗ P ADDC    ⊗ P AND     ⊗ P BREAK   ⊗ P BREAKX  ⊗ P CALL    ⊗ P CLR    ⊗ P CLRB    ⊗
 123  P CMP     ⊗ P CSE     ⊗ P CSNE    ⊗ P CWDT    ⊗ P DEC     ⊗ P DECSNZ  ⊗ P DECSZ  ⊗ P FERASE  ⊗
 124  P FREAD   ⊗ P FWRITE  ⊗ P INC     ⊗ P INCSNZ  ⊗ P INCSZ   ⊗ P INT     ⊗ P IREAD  ⊗ P IWRITE  ⊗
 125  P JMP     ⊗ P LOADH   ⊗ P LOADL   ⊗ P MOV     ⊗ P MULS    ⊗ P MULU    ⊗ P NOP    ⊗ P NOT     ⊗
 126  P OR      ⊗ P PAGE    ⊗ P POP     ⊗ P PUSH    ⊗ P RET     ⊗ P RETI    ⊗ P RETNP  ⊗ P RETW    ⊗
 127  P RL      ⊗ P RR      ⊗ P SB      ⊗ P SETB    ⊗ P SNB     ⊗ P SPEED   ⊗ P SUB    ⊗ P SUBC    ⊗
 128  P SWAP    ⊗ P TEST    ⊗ P XOR.