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