1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "num/bool.ma".
25 (* ********************************************** *)
26 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
27 (* ********************************************** *)
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 *)
90 ndefinition eq_IP2022_pseudo ≝
91 λps1,ps2:IP2022_pseudo.
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 ]
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.