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/exadecim.ma".
24 include "num/bitrigesim.ma".
26 (* ********************************************** *)
27 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
28 (* ********************************************** *)
30 (* enumerazione delle modalita' di indirizzamento = caricamento degli operandi *)
31 ninductive Freescale_instr_mode: Type ≝
32 (* INHERENT = nessun operando *)
33 MODE_INH : Freescale_instr_mode
34 (* INHERENT = nessun operando (A implicito) *)
35 | MODE_INHA : Freescale_instr_mode
36 (* INHERENT = nessun operando (X implicito) *)
37 | MODE_INHX : Freescale_instr_mode
38 (* INHERENT = nessun operando (H implicito) *)
39 | MODE_INHH : Freescale_instr_mode
41 (* INHERENT_ADDRESS = nessun operando (HX implicito) *)
42 | MODE_INHX0ADD : Freescale_instr_mode
43 (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *)
44 | MODE_INHX1ADD : Freescale_instr_mode
45 (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *)
46 | MODE_INHX2ADD : Freescale_instr_mode
48 (* IMMEDIATE = operando valore immediato byte = 0xbb *)
49 | MODE_IMM1 : Freescale_instr_mode
50 (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *)
51 | MODE_IMM1EXT : Freescale_instr_mode
52 (* IMMEDIATE = operando valore immediato word = 0xwwww *)
53 | MODE_IMM2 : Freescale_instr_mode
54 (* DIRECT = operando offset byte = [0x00bb] *)
55 | MODE_DIR1 : Freescale_instr_mode
56 (* DIRECT = operando offset word = [0xwwww] *)
57 | MODE_DIR2 : Freescale_instr_mode
58 (* INDEXED = nessun operando (implicito [X] *)
59 | MODE_IX0 : Freescale_instr_mode
60 (* INDEXED = operando offset relativo byte = [X+0x00bb] *)
61 | MODE_IX1 : Freescale_instr_mode
62 (* INDEXED = operando offset relativo word = [X+0xwwww] *)
63 | MODE_IX2 : Freescale_instr_mode
64 (* INDEXED = operando offset relativo byte = [SP+0x00bb] *)
65 | MODE_SP1 : Freescale_instr_mode
66 (* INDEXED = operando offset relativo word = [SP+0xwwww] *)
67 | MODE_SP2 : Freescale_instr_mode
69 (* DIRECT → DIRECT = carica da diretto/scrive su diretto *)
70 | MODE_DIR1_to_DIR1 : Freescale_instr_mode
71 (* IMMEDIATE → DIRECT = carica da immediato/scrive su diretto *)
72 | MODE_IMM1_to_DIR1 : Freescale_instr_mode
73 (* INDEXED++ → DIRECT = carica da [X]/scrive su diretto/H:X++ *)
74 | MODE_IX0p_to_DIR1 : Freescale_instr_mode
75 (* DIRECT → INDEXED++ = carica da diretto/scrive su [X]/H:X++ *)
76 | MODE_DIR1_to_IX0p : Freescale_instr_mode
78 (* INHERENT(A) + IMMEDIATE *)
79 | MODE_INHA_and_IMM1 : Freescale_instr_mode
80 (* INHERENT(X) + IMMEDIATE *)
81 | MODE_INHX_and_IMM1 : Freescale_instr_mode
82 (* IMMEDIATE + IMMEDIATE *)
83 | MODE_IMM1_and_IMM1 : Freescale_instr_mode
84 (* DIRECT + IMMEDIATE *)
85 | MODE_DIR1_and_IMM1 : Freescale_instr_mode
86 (* INDEXED + IMMEDIATE *)
87 | MODE_IX0_and_IMM1 : Freescale_instr_mode
88 (* INDEXED++ + IMMEDIATE *)
89 | MODE_IX0p_and_IMM1 : Freescale_instr_mode
90 (* INDEXED + IMMEDIATE *)
91 | MODE_IX1_and_IMM1 : Freescale_instr_mode
92 (* INDEXED++ + IMMEDIATE *)
93 | MODE_IX1p_and_IMM1 : Freescale_instr_mode
94 (* INDEXED + IMMEDIATE *)
95 | MODE_SP1_and_IMM1 : Freescale_instr_mode
97 (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *)
98 (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *)
99 | MODE_DIRn : oct → Freescale_instr_mode
100 (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *)
101 (* + operando valore immediato byte *)
102 (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *)
103 | MODE_DIRn_and_IMM1 : oct → Freescale_instr_mode
104 (* TINY = nessun operando (diretto implicito 4bit = [0x00000000:0000iiii]) *)
105 | MODE_TNY : exadecim → Freescale_instr_mode
106 (* SHORT = nessun operando (diretto implicito 5bit = [0x00000000:000iiiii]) *)
107 | MODE_SRT : bitrigesim → Freescale_instr_mode
110 ndefinition eq_Freescale_im ≝
111 λi1,i2:Freescale_instr_mode.
113 [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
114 | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ]
115 | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ true | _ ⇒ false ]
116 | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ true | _ ⇒ false ]
117 | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ true | _ ⇒ false ]
118 | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ true | _ ⇒ false ]
119 | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ true | _ ⇒ false ]
120 | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ]
121 | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ true | _ ⇒ false ]
122 | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ]
123 | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ]
124 | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ true | _ ⇒ false ]
125 | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ true | _ ⇒ false ]
126 | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ true | _ ⇒ false ]
127 | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ true | _ ⇒ false ]
128 | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ true | _ ⇒ false ]
129 | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ true | _ ⇒ false ]
130 | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ true | _ ⇒ false ]
131 | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ true | _ ⇒ false ]
132 | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ true | _ ⇒ false ]
133 | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ true | _ ⇒ false ]
134 | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ true | _ ⇒ false ]
135 | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ true | _ ⇒ false ]
136 | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ true | _ ⇒ false ]
137 | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ true | _ ⇒ false ]
138 | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ true | _ ⇒ false ]
139 | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ true | _ ⇒ false ]
140 | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ true | _ ⇒ false ]
141 | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ true | _ ⇒ false ]
142 | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ true | _ ⇒ false ]
143 | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eqc ? n1 n2 | _ ⇒ false ]
144 | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eqc ? n1 n2 | _ ⇒ false ]
145 | MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eqc ? e1 e2 | _ ⇒ false ]
146 | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eqc ? t1 t2 | _ ⇒ false ]
149 ndefinition forall_Freescale_im ≝ λP:Freescale_instr_mode → bool.
170 ⊗ P MODE_DIR1_to_DIR1
171 ⊗ P MODE_IMM1_to_DIR1
172 ⊗ P MODE_IX0p_to_DIR1
173 ⊗ P MODE_DIR1_to_IX0p
175 ⊗ P MODE_INHA_and_IMM1
176 ⊗ P MODE_INHX_and_IMM1
177 ⊗ P MODE_IMM1_and_IMM1
178 ⊗ P MODE_DIR1_and_IMM1
179 ⊗ P MODE_IX0_and_IMM1
180 ⊗ P MODE_IX0p_and_IMM1
181 ⊗ P MODE_IX1_and_IMM1
182 ⊗ P MODE_IX1p_and_IMM1
183 ⊗ P MODE_SP1_and_IMM1
185 ⊗ forallc ? (λo. P (MODE_DIRn o))
186 ⊗ forallc ? (λo. P (MODE_DIRn_and_IMM1 o))
187 ⊗ forallc ? (λe. P (MODE_TNY e))
188 ⊗ forallc ? (λt. P (MODE_SRT t)).