matita/matita/contribs/ng_assembly/emulator/multivm/IP2022_multivm.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 "emulator/multivm/multivm_base.ma".
  24 include "emulator/read_write/load_write.ma".
  25
  26 (* ************************************************ *)
  27 (* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
  28 (* ************************************************ *)
  29
  30 (* **************** *)
  31 (* LOGICA DELLA ALU *)
  32 (* **************** *)
  33
  34 ndefinition execute_NO ≝
  35 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
  36  None (ProdT (any_status m t) word16).
  37
  38 (* raccordo *)
  39 ndefinition IP2022_execute_any ≝
  40 λps:IP2022_pseudo.match ps with
  41   [ ADD    ⇒ execute_NO (* add *)
  42   | ADDC   ⇒ execute_NO (* add with carry *)
  43   | AND    ⇒ execute_NO (* and *)
  44   | BREAK  ⇒ execute_NO (* enter break mode *)
  45   | BREAKX ⇒ execute_NO (* enter break mode, after skip *)
  46   | CALL   ⇒ execute_NO (* subroutine call *)
  47   | CLR    ⇒ execute_NO (* clear *)
  48   | CLRB   ⇒ execute_NO (* clear bit *)
  49   | CMP    ⇒ execute_NO (* set flags according to sub *)
  50   | CSE    ⇒ execute_NO (* confront & skip if equal *)
  51   | CSNE   ⇒ execute_NO (* confront & skip if not equal *)
  52   | CWDT   ⇒ execute_NO (* clear watch dog -- not impl. ERR *)
  53   | DEC    ⇒ execute_NO (* decrement *)
  54   | DECSNZ ⇒ execute_NO (* decrement & skip if not zero *)
  55   | DECSZ  ⇒ execute_NO (* decrement & skip if zero *)
  56   | FERASE ⇒ execute_NO (* flash erase -- not impl. ERR *)
  57   | FREAD  ⇒ execute_NO (* flash read -- not impl. ERR *)
  58   | FWRITE ⇒ execute_NO (* flash write -- not impl. ERR *)
  59   | INC    ⇒ execute_NO (* increment *)
  60   | INCSNZ ⇒ execute_NO (* increment & skip if not zero *)
  61   | INCSZ  ⇒ execute_NO (* increment & skip if zero *)
  62   | INT    ⇒ execute_NO (* interrupt -- not impl. ERR *)
  63   | IREAD  ⇒ execute_NO (* memory read *)
  64   | IWRITE ⇒ execute_NO (* memory write *)
  65   | JMP    ⇒ execute_NO (* jump *)
  66   | LOADH  ⇒ execute_NO (* load Data Pointer High *)
  67   | LOADL  ⇒ execute_NO (* load Data Pointer Low *)
  68   | MOV    ⇒ execute_NO (* move *)
  69   | MULS   ⇒ execute_NO (* signed mul *)
  70   | MULU   ⇒ execute_NO (* unsigned mul *)
  71   | NOP    ⇒ execute_NO (* nop *)
  72   | NOT    ⇒ execute_NO (* not *)
  73   | OR     ⇒ execute_NO (* or *)
  74   | PAGE   ⇒ execute_NO (* set Page Register *)
  75   | POP    ⇒ execute_NO (* pop *)
  76   | PUSH   ⇒ execute_NO (* push *)
  77   | RET    ⇒ execute_NO (* subroutine ret *)
  78   | RETI   ⇒ execute_NO (* interrupt ret -- not impl. ERR *)
  79   | RETNP  ⇒ execute_NO (* subroutine ret & don't restore Page Register *)
  80   | RETW   ⇒ execute_NO (* subroutine ret & load W Register *)
  81   | RL     ⇒ execute_NO (* rotate left *)
  82   | RR     ⇒ execute_NO (* rotate right *)
  83   | SB     ⇒ execute_NO (* skip if bit set *)
  84   | SETB   ⇒ execute_NO (* set bit *)
  85   | SNB    ⇒ execute_NO (* skip if bit not set *)
  86   | SPEED  ⇒ execute_NO (* set Speed Register *)
  87   | SUB    ⇒ execute_NO (* sub *)
  88   | SUBC   ⇒ execute_NO (* sub with carry *)
  89   | SWAP   ⇒ execute_NO (* swap xxxxyyyy → yyyyxxxx *)
  90   | TEST   ⇒ execute_NO (* set flags according to zero test *)
  91   | XOR    ⇒ execute_NO (* xor *)
  92   ].
  93
  94 (* stati speciali di esecuzione *)
  95 ndefinition IP2022_check_susp ≝
  96 λps:IP2022_pseudo.match ps with
  97  [ BREAK ⇒ Some ? BGND_MODE
  98  | BREAKX ⇒ Some ? BGND_MODE
  99  | _ ⇒ None ?
 100  ].
 101
 102 (* istruzioni speciali per skip *)
 103 ndefinition IP2022_check_skip ≝
 104 λps:IP2022_pseudo.match ps with
 105  [ LOADH ⇒ true
 106  | LOADL ⇒ true
 107  | PAGE ⇒ true
 108  | _ ⇒ false
 109  ].