X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fmultivm%2FIP2022_multivm.ma;fp=matitaB%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fmultivm%2FIP2022_multivm.ma;h=e5201540f62dea3dd3cdb5f4798078cb240320ef;hb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;hp=0000000000000000000000000000000000000000;hpb=f04a064bb34aabaf91dc0c48e3b08b37ecd7b0a2;p=helm.git

diff --git a/matitaB/matita/contribs/ng_assembly/emulator/multivm/IP2022_multivm.ma b/matitaB/matita/contribs/ng_assembly/emulator/multivm/IP2022_multivm.ma
new file mode 100755
index 000000000..e5201540f
--- /dev/null
+++ b/matitaB/matita/contribs/ng_assembly/emulator/multivm/IP2022_multivm.ma
@@ -0,0 +1,109 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
+(*                                                                        *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Sviluppo: 2008-2010                                                  *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "emulator/multivm/multivm_base.ma".
+include "emulator/read_write/load_write.ma".
+
+(* ************************************************ *)
+(* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
+(* ************************************************ *)
+
+(* **************** *)
+(* LOGICA DELLA ALU *)
+(* **************** *)
+
+ndefinition execute_NO ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
+ None (ProdT (any_status m t) word16).
+
+(* raccordo *)
+ndefinition IP2022_execute_any ≝
+λps:IP2022_pseudo.match ps with
+  [ ADD    ⇒ execute_NO (* add *)
+  | ADDC   ⇒ execute_NO (* add with carry *)
+  | AND    ⇒ execute_NO (* and *)
+  | BREAK  ⇒ execute_NO (* enter break mode *)
+  | BREAKX ⇒ execute_NO (* enter break mode, after skip *)
+  | CALL   ⇒ execute_NO (* subroutine call *)
+  | CLR    ⇒ execute_NO (* clear *)
+  | CLRB   ⇒ execute_NO (* clear bit *)
+  | CMP    ⇒ execute_NO (* set flags according to sub *)
+  | CSE    ⇒ execute_NO (* confront & skip if equal *)
+  | CSNE   ⇒ execute_NO (* confront & skip if not equal *)
+  | CWDT   ⇒ execute_NO (* clear watch dog -- not impl. ERR *)
+  | DEC    ⇒ execute_NO (* decrement *)
+  | DECSNZ ⇒ execute_NO (* decrement & skip if not zero *)
+  | DECSZ  ⇒ execute_NO (* decrement & skip if zero *)
+  | FERASE ⇒ execute_NO (* flash erase -- not impl. ERR *)
+  | FREAD  ⇒ execute_NO (* flash read -- not impl. ERR *)
+  | FWRITE ⇒ execute_NO (* flash write -- not impl. ERR *)
+  | INC    ⇒ execute_NO (* increment *)
+  | INCSNZ ⇒ execute_NO (* increment & skip if not zero *)
+  | INCSZ  ⇒ execute_NO (* increment & skip if zero *)
+  | INT    ⇒ execute_NO (* interrupt -- not impl. ERR *)
+  | IREAD  ⇒ execute_NO (* memory read *)
+  | IWRITE ⇒ execute_NO (* memory write *)
+  | JMP    ⇒ execute_NO (* jump *)
+  | LOADH  ⇒ execute_NO (* load Data Pointer High *)
+  | LOADL  ⇒ execute_NO (* load Data Pointer Low *)
+  | MOV    ⇒ execute_NO (* move *)
+  | MULS   ⇒ execute_NO (* signed mul *)
+  | MULU   ⇒ execute_NO (* unsigned mul *)
+  | NOP    ⇒ execute_NO (* nop *)
+  | NOT    ⇒ execute_NO (* not *)
+  | OR     ⇒ execute_NO (* or *)
+  | PAGE   ⇒ execute_NO (* set Page Register *)
+  | POP    ⇒ execute_NO (* pop *)
+  | PUSH   ⇒ execute_NO (* push *)
+  | RET    ⇒ execute_NO (* subroutine ret *)
+  | RETI   ⇒ execute_NO (* interrupt ret -- not impl. ERR *)
+  | RETNP  ⇒ execute_NO (* subroutine ret & don't restore Page Register *)
+  | RETW   ⇒ execute_NO (* subroutine ret & load W Register *)
+  | RL     ⇒ execute_NO (* rotate left *)
+  | RR     ⇒ execute_NO (* rotate right *)
+  | SB     ⇒ execute_NO (* skip if bit set *)
+  | SETB   ⇒ execute_NO (* set bit *)
+  | SNB    ⇒ execute_NO (* skip if bit not set *)
+  | SPEED  ⇒ execute_NO (* set Speed Register *)
+  | SUB    ⇒ execute_NO (* sub *)
+  | SUBC   ⇒ execute_NO (* sub with carry *)
+  | SWAP   ⇒ execute_NO (* swap xxxxyyyy → yyyyxxxx *)
+  | TEST   ⇒ execute_NO (* set flags according to zero test *)
+  | XOR    ⇒ execute_NO (* xor *)
+  ].
+
+(* stati speciali di esecuzione *)
+ndefinition IP2022_check_susp ≝
+λps:IP2022_pseudo.match ps with
+ [ BREAK ⇒ Some ? BGND_MODE
+ | BREAKX ⇒ Some ? BGND_MODE
+ | _ ⇒ None ?
+ ].
+
+(* istruzioni speciali per skip *)
+ndefinition IP2022_check_skip ≝
+λps:IP2022_pseudo.match ps with
+ [ LOADH ⇒ true
+ | LOADL ⇒ true
+ | PAGE ⇒ true
+ | _ ⇒ false
+ ].