mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / opcodes / IP2022_pseudo.ma

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.ma
old mode 100755 (executable)
new mode 100644 (file)
index 9aa26cf..9a29506
--- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.ma
@@ -51,9 +51,13 @@ ninductive IP2022_pseudo: Type ≝
 | INCSZ   : IP2022_pseudo (* increment & skip if zero *)
 | INT     : IP2022_pseudo (* interrupt -- not impl. ERR *)
 | IREAD   : IP2022_pseudo (* memory read *)
-| IREADI  : IP2022_pseudo (* memory read & inc *)
+(* NB: ignorata la differenza IREAD/IREADI perche' non e' implementata EXT_MEM
+       IREAD → ADDRX= 0x00 ram, 0x01 flash, 0x80 0x81 ext_mem
+       IREADI → ADDRX= 0x00 ram, 0x01 flash *)
 | IWRITE  : IP2022_pseudo (* memory write *)
-| IWRITEI : IP2022_pseudo (* memory write & inc *)
+(* NB: ignorata la differenza IWRITE/IWRITEI perche' non e' implementata EXT_MEM
+       IREAD → ADDRX= 0x00 ram, 0x80 0x81 ext_mem
+       IREADI → ADDRX= 0x00 ram *)
 | JMP     : IP2022_pseudo (* jump *)
 | LOADH   : IP2022_pseudo (* load Data Pointer High *)
 | LOADL   : IP2022_pseudo (* load Data Pointer Low *)
@@ -97,8 +101,7 @@ ndefinition eq_IP2022_pseudo ≝
   | FREAD ⇒ match ps2 with [ FREAD ⇒ true | _ ⇒ false ]   | FWRITE ⇒ match ps2 with [ FWRITE ⇒ true | _ ⇒ false ]
   | INC ⇒ match ps2 with [ INC ⇒ true | _ ⇒ false ]       | INCSNZ ⇒ match ps2 with [ INCSNZ ⇒ true | _ ⇒ false ]
   | INCSZ ⇒ match ps2 with [ INCSZ ⇒ true | _ ⇒ false ]   | INT ⇒ match ps2 with [ INT ⇒ true | _ ⇒ false ]
-  | IREAD ⇒ match ps2 with [ IREAD ⇒ true | _ ⇒ false ]   | IREADI ⇒ match ps2 with [ IREADI ⇒ true | _ ⇒ false ]
-  | IWRITE ⇒ match ps2 with [ IWRITE ⇒ true | _ ⇒ false ] | IWRITEI ⇒ match ps2 with [ IWRITEI ⇒ true | _ ⇒ false ]
+  | IREAD ⇒ match ps2 with [ IREAD ⇒ true | _ ⇒ false ]   | IWRITE ⇒ match ps2 with [ IWRITE ⇒ true | _ ⇒ false ]
   | JMP ⇒ match ps2 with [ JMP ⇒ true | _ ⇒ false ]       | LOADH ⇒ match ps2 with [ LOADH ⇒ true | _ ⇒ false ]
   | LOADL ⇒ match ps2 with [ LOADL ⇒ true | _ ⇒ false ]   | MOV ⇒ match ps2 with [ MOV ⇒ true | _ ⇒ false ]
   | MULS ⇒ match ps2 with [ MULS ⇒ true | _ ⇒ false ]     | MULU ⇒ match ps2 with [ MULU ⇒ true | _ ⇒ false ] 
@@ -118,8 +121,8 @@ ndefinition eq_IP2022_pseudo ≝
 ndefinition forall_IP2022_pseudo ≝ λP:IP2022_pseudo → bool.
  P ADD     ⊗ P ADDC    ⊗ P AND     ⊗ P BREAK   ⊗ P BREAKX  ⊗ P CALL    ⊗ P CLR    ⊗ P CLRB    ⊗
  P CMP     ⊗ P CSE     ⊗ P CSNE    ⊗ P CWDT    ⊗ P DEC     ⊗ P DECSNZ  ⊗ P DECSZ  ⊗ P FERASE  ⊗
- P FREAD   ⊗ P FWRITE  ⊗ P INC     ⊗ P INCSNZ  ⊗ P INCSZ   ⊗ P INT     ⊗ P IREAD  ⊗ P IREADI  ⊗
- P IWRITE  ⊗ P IWRITEI ⊗ P JMP     ⊗ P LOADH   ⊗ P LOADL   ⊗ P MOV     ⊗ P MULS   ⊗ P MULU    ⊗
- P NOP     ⊗ P NOT     ⊗ P OR      ⊗ P PAGE    ⊗ P POP     ⊗ P PUSH    ⊗ P RET    ⊗ P RETI    ⊗
- P RETNP   ⊗ P RETW    ⊗ P RL      ⊗ P RR      ⊗ P SB      ⊗ P SETB    ⊗ P SNB    ⊗ P SPEED   ⊗
- P SUB     ⊗ P SUBC    ⊗ P SWAP    ⊗ P TEST    ⊗ P XOR.
+ P FREAD   ⊗ P FWRITE  ⊗ P INC     ⊗ P INCSNZ  ⊗ P INCSZ   ⊗ P INT     ⊗ P IREAD  ⊗ P IWRITE  ⊗
+ P JMP     ⊗ P LOADH   ⊗ P LOADL   ⊗ P MOV     ⊗ P MULS    ⊗ P MULU    ⊗ P NOP    ⊗ P NOT     ⊗
+ P OR      ⊗ P PAGE    ⊗ P POP     ⊗ P PUSH    ⊗ P RET     ⊗ P RETI    ⊗ P RETNP  ⊗ P RETW    ⊗
+ P RL      ⊗ P RR      ⊗ P SB      ⊗ P SETB    ⊗ P SNB     ⊗ P SPEED   ⊗ P SUB    ⊗ P SUBC    ⊗
+ P SWAP    ⊗ P TEST    ⊗ P XOR.