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: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/aux_bases.ma".
24 include "freescale/word16.ma".
25 include "freescale/theory.ma".
27 (* ********************************************** *)
28 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
29 (* ********************************************** *)
31 (* enumerazione delle ALU *)
32 ninductive mcu_type: Type ≝
38 ndefinition mcu_type_ind : ΠP:mcu_type → Prop.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
39 λP:mcu_type → Prop.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type.
40 match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].
42 ndefinition mcu_type_rec : ΠP:mcu_type → Set.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
43 λP:mcu_type → Set.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type.
44 match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].
46 ndefinition mcu_type_rect : ΠP:mcu_type → Type.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
47 λP:mcu_type → Type.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type.
48 match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].
50 ndefinition eq_mcutype ≝
53 [ HC05 ⇒ match m2 with [ HC05 ⇒ true | _ ⇒ false ]
54 | HC08 ⇒ match m2 with [ HC08 ⇒ true | _ ⇒ false ]
55 | HCS08 ⇒ match m2 with [ HCS08 ⇒ true | _ ⇒ false ]
56 | RS08 ⇒ match m2 with [ RS08 ⇒ true | _ ⇒ false ]
59 (* enumerazione delle modalita' di indirizzamento = caricamento degli operandi *)
60 ninductive instr_mode: Type ≝
61 (* INHERENT = nessun operando *)
63 (* INHERENT = nessun operando (A implicito) *)
64 | MODE_INHA : instr_mode
65 (* INHERENT = nessun operando (X implicito) *)
66 | MODE_INHX : instr_mode
67 (* INHERENT = nessun operando (H implicito) *)
68 | MODE_INHH : instr_mode
70 (* INHERENT_ADDRESS = nessun operando (HX implicito) *)
71 | MODE_INHX0ADD : instr_mode
72 (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *)
73 | MODE_INHX1ADD : instr_mode
74 (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *)
75 | MODE_INHX2ADD : instr_mode
77 (* IMMEDIATE = operando valore immediato byte = 0xbb *)
78 | MODE_IMM1 : instr_mode
79 (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *)
80 | MODE_IMM1EXT : instr_mode
81 (* IMMEDIATE = operando valore immediato word = 0xwwww *)
82 | MODE_IMM2 : instr_mode
83 (* DIRECT = operando offset byte = [0x00bb] *)
84 | MODE_DIR1 : instr_mode
85 (* DIRECT = operando offset word = [0xwwww] *)
86 | MODE_DIR2 : instr_mode
87 (* INDEXED = nessun operando (implicito [X] *)
88 | MODE_IX0 : instr_mode
89 (* INDEXED = operando offset relativo byte = [X+0x00bb] *)
90 | MODE_IX1 : instr_mode
91 (* INDEXED = operando offset relativo word = [X+0xwwww] *)
92 | MODE_IX2 : instr_mode
93 (* INDEXED = operando offset relativo byte = [SP+0x00bb] *)
94 | MODE_SP1 : instr_mode
95 (* INDEXED = operando offset relativo word = [SP+0xwwww] *)
96 | MODE_SP2 : instr_mode
98 (* DIRECT → DIRECT = carica da diretto/scrive su diretto *)
99 | MODE_DIR1_to_DIR1 : instr_mode
100 (* IMMEDIATE → DIRECT = carica da immediato/scrive su diretto *)
101 | MODE_IMM1_to_DIR1 : instr_mode
102 (* INDEXED++ → DIRECT = carica da [X]/scrive su diretto/H:X++ *)
103 | MODE_IX0p_to_DIR1 : instr_mode
104 (* DIRECT → INDEXED++ = carica da diretto/scrive su [X]/H:X++ *)
105 | MODE_DIR1_to_IX0p : instr_mode
107 (* INHERENT(A) + IMMEDIATE *)
108 | MODE_INHA_and_IMM1 : instr_mode
109 (* INHERENT(X) + IMMEDIATE *)
110 | MODE_INHX_and_IMM1 : instr_mode
111 (* IMMEDIATE + IMMEDIATE *)
112 | MODE_IMM1_and_IMM1 : instr_mode
113 (* DIRECT + IMMEDIATE *)
114 | MODE_DIR1_and_IMM1 : instr_mode
115 (* INDEXED + IMMEDIATE *)
116 | MODE_IX0_and_IMM1 : instr_mode
117 (* INDEXED++ + IMMEDIATE *)
118 | MODE_IX0p_and_IMM1 : instr_mode
119 (* INDEXED + IMMEDIATE *)
120 | MODE_IX1_and_IMM1 : instr_mode
121 (* INDEXED++ + IMMEDIATE *)
122 | MODE_IX1p_and_IMM1 : instr_mode
123 (* INDEXED + IMMEDIATE *)
124 | MODE_SP1_and_IMM1 : instr_mode
126 (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *)
127 (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *)
128 | MODE_DIRn : oct → instr_mode
129 (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *)
130 (* + operando valore immediato byte *)
131 (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *)
132 | MODE_DIRn_and_IMM1 : oct → instr_mode
133 (* TINY = nessun operando (diretto implicito 4bit = [0x00000000:0000iiii]) *)
134 | MODE_TNY : exadecim → instr_mode
135 (* SHORT = nessun operando (diretto implicito 5bit = [0x00000000:000iiiii]) *)
136 | MODE_SRT : bitrigesim → instr_mode
139 ndefinition instr_mode_ind
140 : ΠP:instr_mode → Prop.
141 P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD →
142 P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 →
143 P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 →
144 P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 →
145 P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 →
146 P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 →
147 (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) →
148 (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝
149 λP:instr_mode → Prop.
150 λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD.
151 λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2.
152 λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1.
153 λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1.
154 λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1.
155 λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1.
156 λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d).
157 λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode.
159 [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4
160 | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8
161 | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13
162 | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17
163 | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20
164 | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23
165 | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26
166 | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29
167 | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d
168 | MODE_SRT (d:bitrigesim) ⇒ f3 d ].
170 ndefinition instr_mode_rec
171 : ΠP:instr_mode → Set.
172 P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD →
173 P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 →
174 P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 →
175 P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 →
176 P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 →
177 P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 →
178 (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) →
179 (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝
181 λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD.
182 λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2.
183 λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1.
184 λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1.
185 λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1.
186 λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1.
187 λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d).
188 λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode.
190 [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4
191 | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8
192 | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13
193 | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17
194 | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20
195 | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23
196 | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26
197 | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29
198 | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d
199 | MODE_SRT (d:bitrigesim) ⇒ f3 d ].
201 ndefinition instr_mode_rect
202 : ΠP:instr_mode → Type.
203 P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD →
204 P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 →
205 P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 →
206 P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 →
207 P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 →
208 P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 →
209 (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) →
210 (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝
211 λP:instr_mode → Type.
212 λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD.
213 λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2.
214 λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1.
215 λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1.
216 λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1.
217 λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1.
218 λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d).
219 λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode.
221 [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4
222 | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8
223 | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13
224 | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17
225 | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20
226 | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23
227 | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26
228 | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29
229 | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d
230 | MODE_SRT (d:bitrigesim) ⇒ f3 d ].
232 ndefinition eq_instrmode ≝
235 [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
236 | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ]
237 | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ true | _ ⇒ false ]
238 | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ true | _ ⇒ false ]
239 | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ true | _ ⇒ false ]
240 | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ true | _ ⇒ false ]
241 | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ true | _ ⇒ false ]
242 | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ]
243 | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ true | _ ⇒ false ]
244 | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ]
245 | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ]
246 | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ true | _ ⇒ false ]
247 | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ true | _ ⇒ false ]
248 | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ true | _ ⇒ false ]
249 | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ true | _ ⇒ false ]
250 | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ true | _ ⇒ false ]
251 | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ true | _ ⇒ false ]
252 | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ true | _ ⇒ false ]
253 | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ true | _ ⇒ false ]
254 | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ true | _ ⇒ false ]
255 | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ true | _ ⇒ false ]
256 | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ true | _ ⇒ false ]
257 | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ true | _ ⇒ false ]
258 | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ true | _ ⇒ false ]
259 | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ true | _ ⇒ false ]
260 | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ true | _ ⇒ false ]
261 | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ true | _ ⇒ false ]
262 | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ true | _ ⇒ false ]
263 | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ true | _ ⇒ false ]
264 | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ true | _ ⇒ false ]
265 | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
266 | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
267 | MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eq_ex e1 e2 | _ ⇒ false ]
268 | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bitrig t1 t2 | _ ⇒ false ]
271 (* enumerazione delle istruzioni di tutte le ALU *)
272 ninductive opcode: Type ≝
273 ADC : opcode (* add with carry *)
274 | ADD : opcode (* add *)
275 | AIS : opcode (* add immediate to SP *)
276 | AIX : opcode (* add immediate to X *)
277 | AND : opcode (* and *)
278 | ASL : opcode (* aritmetic shift left *)
279 | ASR : opcode (* aritmetic shift right *)
280 | BCC : opcode (* branch if C=0 *)
281 | BCLRn : opcode (* clear bit n *)
282 | BCS : opcode (* branch if C=1 *)
283 | BEQ : opcode (* branch if Z=1 *)
284 | BGE : opcode (* branch if N⊙V=0 (great or equal) *)
285 | BGND : opcode (* !!background mode!! *)
286 | BGT : opcode (* branch if Z|N⊙V=0 clear (great) *)
287 | BHCC : opcode (* branch if H=0 *)
288 | BHCS : opcode (* branch if H=1 *)
289 | BHI : opcode (* branch if C|Z=0, (higher) *)
290 | BIH : opcode (* branch if nIRQ=1 *)
291 | BIL : opcode (* branch if nIRQ=0 *)
292 | BIT : opcode (* flag = and (bit test) *)
293 | BLE : opcode (* branch if Z|N⊙V=1 (less or equal) *)
294 | BLS : opcode (* branch if C|Z=1 (lower or same) *)
295 | BLT : opcode (* branch if N⊙1=1 (less) *)
296 | BMC : opcode (* branch if I=0 (interrupt mask clear) *)
297 | BMI : opcode (* branch if N=1 (minus) *)
298 | BMS : opcode (* branch if I=1 (interrupt mask set) *)
299 | BNE : opcode (* branch if Z=0 *)
300 | BPL : opcode (* branch if N=0 (plus) *)
301 | BRA : opcode (* branch always *)
302 | BRCLRn : opcode (* branch if bit n clear *)
303 | BRN : opcode (* branch never (nop) *)
304 | BRSETn : opcode (* branch if bit n set *)
305 | BSETn : opcode (* set bit n *)
306 | BSR : opcode (* branch to subroutine *)
307 | CBEQA : opcode (* compare (A) and BEQ *)
308 | CBEQX : opcode (* compare (X) and BEQ *)
309 | CLC : opcode (* C=0 *)
310 | CLI : opcode (* I=0 *)
311 | CLR : opcode (* operand=0 *)
312 | CMP : opcode (* flag = sub (compare A) *)
313 | COM : opcode (* not (1 complement) *)
314 | CPHX : opcode (* flag = sub (compare H:X) *)
315 | CPX : opcode (* flag = sub (compare X) *)
316 | DAA : opcode (* decimal adjust A *)
317 | DBNZ : opcode (* dec and BNE *)
318 | DEC : opcode (* operand=operand-1 (decrement) *)
319 | DIV : opcode (* div *)
320 | EOR : opcode (* xor *)
321 | INC : opcode (* operand=operand+1 (increment) *)
322 | JMP : opcode (* jmp word [operand] *)
323 | JSR : opcode (* jmp to subroutine *)
324 | LDA : opcode (* load in A *)
325 | LDHX : opcode (* load in H:X *)
326 | LDX : opcode (* load in X *)
327 | LSR : opcode (* logical shift right *)
328 | MOV : opcode (* move *)
329 | MUL : opcode (* mul *)
330 | NEG : opcode (* neg (2 complement) *)
331 | NOP : opcode (* nop *)
332 | NSA : opcode (* nibble swap A (al:ah <- ah:al) *)
333 | ORA : opcode (* or *)
334 | PSHA : opcode (* push A *)
335 | PSHH : opcode (* push H *)
336 | PSHX : opcode (* push X *)
337 | PULA : opcode (* pop A *)
338 | PULH : opcode (* pop H *)
339 | PULX : opcode (* pop X *)
340 | ROL : opcode (* rotate left *)
341 | ROR : opcode (* rotate right *)
342 | RSP : opcode (* reset SP (0x00FF) *)
343 | RTI : opcode (* return from interrupt *)
344 | RTS : opcode (* return from subroutine *)
345 | SBC : opcode (* sub with carry*)
346 | SEC : opcode (* C=1 *)
347 | SEI : opcode (* I=1 *)
348 | SHA : opcode (* swap spc_high,A *)
349 | SLA : opcode (* swap spc_low,A *)
350 | STA : opcode (* store from A *)
351 | STHX : opcode (* store from H:X *)
352 | STOP : opcode (* !!stop mode!! *)
353 | STX : opcode (* store from X *)
354 | SUB : opcode (* sub *)
355 | SWI : opcode (* software interrupt *)
356 | TAP : opcode (* flag=A (transfer A to process status byte *)
357 | TAX : opcode (* X=A (transfer A to X) *)
358 | TPA : opcode (* A=flag (transfer process status byte to A) *)
359 | TST : opcode (* flag = sub (test) *)
360 | TSX : opcode (* X:H=SP (transfer SP to H:X) *)
361 | TXA : opcode (* A=X (transfer X to A) *)
362 | TXS : opcode (* SP=X:H (transfer H:X to SP) *)
363 | WAIT : opcode (* !!wait mode!! *)
366 ndefinition opcode_ind
368 P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ →
369 P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS →
370 P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn →
371 P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA →
372 P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV →
373 P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX →
374 P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX →
375 P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT →
378 λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS.
379 λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL.
380 λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL.
381 λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX.
382 λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ.
383 λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX.
384 λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH.
385 λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS.
386 λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX.
387 λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS.
388 λp90:P WAIT.λo:opcode.
390 [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8
391 | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16
392 | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24
393 | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32
394 | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40
395 | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48
396 | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56
397 | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64
398 | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72
399 | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80
400 | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88
401 | TXS ⇒ p89 | WAIT ⇒ p90 ].
403 ndefinition opcode_rec
405 P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ →
406 P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS →
407 P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn →
408 P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA →
409 P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV →
410 P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX →
411 P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX →
412 P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT →
415 λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS.
416 λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL.
417 λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL.
418 λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX.
419 λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ.
420 λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX.
421 λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH.
422 λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS.
423 λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX.
424 λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS.
425 λp90:P WAIT.λo:opcode.
427 [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8
428 | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16
429 | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24
430 | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32
431 | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40
432 | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48
433 | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56
434 | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64
435 | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72
436 | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80
437 | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88
438 | TXS ⇒ p89 | WAIT ⇒ p90 ].
440 ndefinition opcode_rect
442 P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ →
443 P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS →
444 P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn →
445 P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA →
446 P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV →
447 P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX →
448 P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX →
449 P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT →
452 λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS.
453 λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL.
454 λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL.
455 λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX.
456 λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ.
457 λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX.
458 λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH.
459 λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS.
460 λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX.
461 λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS.
462 λp90:P WAIT.λo:opcode.
464 [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8
465 | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16
466 | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24
467 | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32
468 | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40
469 | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48
470 | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56
471 | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64
472 | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72
473 | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80
474 | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88
475 | TXS ⇒ p89 | WAIT ⇒ p90 ].
480 [ ADC ⇒ match op2 with [ ADC ⇒ true | _ ⇒ false ] | ADD ⇒ match op2 with [ ADD ⇒ true | _ ⇒ false ]
481 | AIS ⇒ match op2 with [ AIS ⇒ true | _ ⇒ false ] | AIX ⇒ match op2 with [ AIX ⇒ true | _ ⇒ false ]
482 | AND ⇒ match op2 with [ AND ⇒ true | _ ⇒ false ] | ASL ⇒ match op2 with [ ASL ⇒ true | _ ⇒ false ]
483 | ASR ⇒ match op2 with [ ASR ⇒ true | _ ⇒ false ] | BCC ⇒ match op2 with [ BCC ⇒ true | _ ⇒ false ]
484 | BCLRn ⇒ match op2 with [ BCLRn ⇒ true | _ ⇒ false ] | BCS ⇒ match op2 with [ BCS ⇒ true | _ ⇒ false ]
485 | BEQ ⇒ match op2 with [ BEQ ⇒ true | _ ⇒ false ] | BGE ⇒ match op2 with [ BGE ⇒ true | _ ⇒ false ]
486 | BGND ⇒ match op2 with [ BGND ⇒ true | _ ⇒ false ] | BGT ⇒ match op2 with [ BGT ⇒ true | _ ⇒ false ]
487 | BHCC ⇒ match op2 with [ BHCC ⇒ true | _ ⇒ false ] | BHCS ⇒ match op2 with [ BHCS ⇒ true | _ ⇒ false ]
488 | BHI ⇒ match op2 with [ BHI ⇒ true | _ ⇒ false ] | BIH ⇒ match op2 with [ BIH ⇒ true | _ ⇒ false ]
489 | BIL ⇒ match op2 with [ BIL ⇒ true | _ ⇒ false ] | BIT ⇒ match op2 with [ BIT ⇒ true | _ ⇒ false ]
490 | BLE ⇒ match op2 with [ BLE ⇒ true | _ ⇒ false ] | BLS ⇒ match op2 with [ BLS ⇒ true | _ ⇒ false ]
491 | BLT ⇒ match op2 with [ BLT ⇒ true | _ ⇒ false ] | BMC ⇒ match op2 with [ BMC ⇒ true | _ ⇒ false ]
492 | BMI ⇒ match op2 with [ BMI ⇒ true | _ ⇒ false ] | BMS ⇒ match op2 with [ BMS ⇒ true | _ ⇒ false ]
493 | BNE ⇒ match op2 with [ BNE ⇒ true | _ ⇒ false ] | BPL ⇒ match op2 with [ BPL ⇒ true | _ ⇒ false ]
494 | BRA ⇒ match op2 with [ BRA ⇒ true | _ ⇒ false ] | BRCLRn ⇒ match op2 with [ BRCLRn ⇒ true | _ ⇒ false ]
495 | BRN ⇒ match op2 with [ BRN ⇒ true | _ ⇒ false ] | BRSETn ⇒ match op2 with [ BRSETn ⇒ true | _ ⇒ false ]
496 | BSETn ⇒ match op2 with [ BSETn ⇒ true | _ ⇒ false ] | BSR ⇒ match op2 with [ BSR ⇒ true | _ ⇒ false ]
497 | CBEQA ⇒ match op2 with [ CBEQA ⇒ true | _ ⇒ false ] | CBEQX ⇒ match op2 with [ CBEQX ⇒ true | _ ⇒ false ]
498 | CLC ⇒ match op2 with [ CLC ⇒ true | _ ⇒ false ] | CLI ⇒ match op2 with [ CLI ⇒ true | _ ⇒ false ]
499 | CLR ⇒ match op2 with [ CLR ⇒ true | _ ⇒ false ] | CMP ⇒ match op2 with [ CMP ⇒ true | _ ⇒ false ]
500 | COM ⇒ match op2 with [ COM ⇒ true | _ ⇒ false ] | CPHX ⇒ match op2 with [ CPHX ⇒ true | _ ⇒ false ]
501 | CPX ⇒ match op2 with [ CPX ⇒ true | _ ⇒ false ] | DAA ⇒ match op2 with [ DAA ⇒ true | _ ⇒ false ]
502 | DBNZ ⇒ match op2 with [ DBNZ ⇒ true | _ ⇒ false ] | DEC ⇒ match op2 with [ DEC ⇒ true | _ ⇒ false ]
503 | DIV ⇒ match op2 with [ DIV ⇒ true | _ ⇒ false ] | EOR ⇒ match op2 with [ EOR ⇒ true | _ ⇒ false ]
504 | INC ⇒ match op2 with [ INC ⇒ true | _ ⇒ false ] | JMP ⇒ match op2 with [ JMP ⇒ true | _ ⇒ false ]
505 | JSR ⇒ match op2 with [ JSR ⇒ true | _ ⇒ false ] | LDA ⇒ match op2 with [ LDA ⇒ true | _ ⇒ false ]
506 | LDHX ⇒ match op2 with [ LDHX ⇒ true | _ ⇒ false ] | LDX ⇒ match op2 with [ LDX ⇒ true | _ ⇒ false ]
507 | LSR ⇒ match op2 with [ LSR ⇒ true | _ ⇒ false ] | MOV ⇒ match op2 with [ MOV ⇒ true | _ ⇒ false ]
508 | MUL ⇒ match op2 with [ MUL ⇒ true | _ ⇒ false ] | NEG ⇒ match op2 with [ NEG ⇒ true | _ ⇒ false ]
509 | NOP ⇒ match op2 with [ NOP ⇒ true | _ ⇒ false ] | NSA ⇒ match op2 with [ NSA ⇒ true | _ ⇒ false ]
510 | ORA ⇒ match op2 with [ ORA ⇒ true | _ ⇒ false ] | PSHA ⇒ match op2 with [ PSHA ⇒ true | _ ⇒ false ]
511 | PSHH ⇒ match op2 with [ PSHH ⇒ true | _ ⇒ false ] | PSHX ⇒ match op2 with [ PSHX ⇒ true | _ ⇒ false ]
512 | PULA ⇒ match op2 with [ PULA ⇒ true | _ ⇒ false ] | PULH ⇒ match op2 with [ PULH ⇒ true | _ ⇒ false ]
513 | PULX ⇒ match op2 with [ PULX ⇒ true | _ ⇒ false ] | ROL ⇒ match op2 with [ ROL ⇒ true | _ ⇒ false ]
514 | ROR ⇒ match op2 with [ ROR ⇒ true | _ ⇒ false ] | RSP ⇒ match op2 with [ RSP ⇒ true | _ ⇒ false ]
515 | RTI ⇒ match op2 with [ RTI ⇒ true | _ ⇒ false ] | RTS ⇒ match op2 with [ RTS ⇒ true | _ ⇒ false ]
516 | SBC ⇒ match op2 with [ SBC ⇒ true | _ ⇒ false ] | SEC ⇒ match op2 with [ SEC ⇒ true | _ ⇒ false ]
517 | SEI ⇒ match op2 with [ SEI ⇒ true | _ ⇒ false ] | SHA ⇒ match op2 with [ SHA ⇒ true | _ ⇒ false ]
518 | SLA ⇒ match op2 with [ SLA ⇒ true | _ ⇒ false ] | STA ⇒ match op2 with [ STA ⇒ true | _ ⇒ false ]
519 | STHX ⇒ match op2 with [ STHX ⇒ true | _ ⇒ false ] | STOP ⇒ match op2 with [ STOP ⇒ true | _ ⇒ false ]
520 | STX ⇒ match op2 with [ STX ⇒ true | _ ⇒ false ] | SUB ⇒ match op2 with [ SUB ⇒ true | _ ⇒ false ]
521 | SWI ⇒ match op2 with [ SWI ⇒ true | _ ⇒ false ] | TAP ⇒ match op2 with [ TAP ⇒ true | _ ⇒ false ]
522 | TAX ⇒ match op2 with [ TAX ⇒ true | _ ⇒ false ] | TPA ⇒ match op2 with [ TPA ⇒ true | _ ⇒ false ]
523 | TST ⇒ match op2 with [ TST ⇒ true | _ ⇒ false ] | TSX ⇒ match op2 with [ TSX ⇒ true | _ ⇒ false ]
524 | TXA ⇒ match op2 with [ TXA ⇒ true | _ ⇒ false ] | TXS ⇒ match op2 with [ TXS ⇒ true | _ ⇒ false ]
525 | WAIT ⇒ match op2 with [ WAIT ⇒ true | _ ⇒ false ]
528 (* introduzione di un tipo opcode dipendente dall'mcu_type (phantom type) *)
529 ninductive any_opcode (m:mcu_type) : Type ≝
530 anyOP : opcode → any_opcode m.
532 ndefinition any_opcode_ind
533 : Πm:mcu_type.ΠP:any_opcode m → Prop.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝
534 λm:mcu_type.λP:any_opcode m → Prop.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m.
535 match a with [ anyOP (o:opcode) ⇒ f o ].
537 ndefinition any_opcode_rec
538 : Πm:mcu_type.ΠP:any_opcode m → Set.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝
539 λm:mcu_type.λP:any_opcode m → Set.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m.
540 match a with [ anyOP (o:opcode) ⇒ f o ].
542 ndefinition any_opcode_rect
543 : Πm:mcu_type.ΠP:any_opcode m → Type.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝
544 λm:mcu_type.λP:any_opcode m → Type.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m.
545 match a with [ anyOP (o:opcode) ⇒ f o ].
547 ndefinition eq_anyop ≝
548 λm:mcu_type.λop1,op2:any_opcode m.
549 match op1 with [ anyOP op1' ⇒
550 match op2 with [ anyOP op2' ⇒
553 (* raggruppamento di byte e word in un tipo unico *)
554 ninductive byte8_or_word16 : Type ≝
555 Byte: byte8 → byte8_or_word16
556 | Word: word16 → byte8_or_word16.
558 ndefinition byte8_or_word16_ind
559 : ΠP:byte8_or_word16 → Prop.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝
560 λP:byte8_or_word16 → Prop.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16.
561 match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].
563 ndefinition byte8_or_word16_rec
564 : ΠP:byte8_or_word16 → Set.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝
565 λP:byte8_or_word16 → Set.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16.
566 match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].
568 ndefinition byte8_or_word16_rect
569 : ΠP:byte8_or_word16 → Type.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝
570 λP:byte8_or_word16 → Type.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16.
571 match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].
573 ndefinition eq_b8w16 ≝
574 λbw1,bw2:byte8_or_word16.
576 [ Byte b1 ⇒ match bw2 with [ Byte b2 ⇒ eq_b8 b1 b2 | Word _ ⇒ false ]
577 | Word w1 ⇒ match bw2 with [ Byte _ ⇒ false | Word w2 ⇒ eq_w16 w1 w2 ]