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 IP2022_instr_mode: Type ≝
31 (* nessun operando : formato xxxxxxxx xxxxxxxx *)
32 MODE_INH : IP2022_instr_mode
33 (* operando implicito [ADDR] : formato xxxxxxxx xxxxxxxx *)
34 | MODE_INHADDR : IP2022_instr_mode
35 (* operando implicito [ADDR]/ADDR+=2 : formato xxxxxxxx xxxxxxxx *)
36 | MODE_INHADDRpp : IP2022_instr_mode
38 (* #lit3 → / : formato xxxxxxxx xxxxxkkk *)
39 | MODE_IMM3 : oct → IP2022_instr_mode
40 (* W, #lit8 → W : formato xxxxxxxx kkkkkkkk [load 1 byte arg] *)
41 | MODE_IMM8 : IP2022_instr_mode
42 (* #lit13 → / : formato xxxkkkkk kkkkkkkk [load 1 byte arg] *)
43 | MODE_IMM13 : bitrigesim → IP2022_instr_mode
45 (* FR, W → FR : formato xxxxxxx0 ffffffff [load 1 byte arg] *)
46 | MODE_FR0_and_W : IP2022_instr_mode
47 (* FR, W → FR : formato xxxxxxx1 ffffffff [load 1 byte arg] *)
48 | MODE_FR1_and_W : IP2022_instr_mode
49 (* W, FR → W : formato xxxxxxx0 ffffffff [load 1 byte arg] *)
50 | MODE_W_and_FR0 : IP2022_instr_mode
51 (* W, FR → W : formato xxxxxxx1 ffffffff [load 1 byte arg] *)
52 | MODE_W_and_FR1 : IP2022_instr_mode
54 (* FR(bitN) → FR(bitN) : formato xxxxbbb0 ffffffff [load 1 byte arg] *)
55 | MODE_FR0n : oct → IP2022_instr_mode
56 (* FR(bitN) → FR(bitN) : formato xxxxbbb1 ffffffff [load 1 byte arg] *)
57 | MODE_FR1n : oct → IP2022_instr_mode
60 ndefinition eq_IP2022_im ≝
61 λi1,i2:IP2022_instr_mode.
63 [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
64 | MODE_INHADDR ⇒ match i2 with [ MODE_INHADDR ⇒ true | _ ⇒ false ]
65 | MODE_INHADDRpp ⇒ match i2 with [ MODE_INHADDRpp ⇒ true | _ ⇒ false ]
66 | MODE_IMM3 o1 ⇒ match i2 with [ MODE_IMM3 o2 ⇒ eq_oct o1 o2 | _ ⇒ false ]
67 | MODE_IMM8 ⇒ match i2 with [ MODE_IMM8 ⇒ true | _ ⇒ false ]
68 | MODE_IMM13 t1 ⇒ match i2 with [ MODE_IMM13 t2 ⇒ eq_bit t1 t2 | _ ⇒ false ]
69 | MODE_FR0_and_W ⇒ match i2 with [ MODE_FR0_and_W ⇒ true | _ ⇒ false ]
70 | MODE_FR1_and_W ⇒ match i2 with [ MODE_FR1_and_W ⇒ true | _ ⇒ false ]
71 | MODE_W_and_FR0 ⇒ match i2 with [ MODE_W_and_FR0 ⇒ true | _ ⇒ false ]
72 | MODE_W_and_FR1 ⇒ match i2 with [ MODE_W_and_FR1 ⇒ true | _ ⇒ false ]
73 | MODE_FR0n o1 ⇒ match i2 with [ MODE_FR0n o2 ⇒ eq_oct o1 o2 | _ ⇒ false ]
74 | MODE_FR1n o1 ⇒ match i2 with [ MODE_FR1n o2 ⇒ eq_oct o1 o2 | _ ⇒ false ]
77 ndefinition forall_IP2022_im ≝ λP:IP2022_instr_mode → bool.
81 ⊗ forall_oct (λo.P (MODE_IMM3 o))
83 ⊗ forall_bit (λt.P (MODE_IMM13 t))
88 ⊗ forall_oct (λo.P (MODE_FR0n o))
89 ⊗ forall_oct (λo.P (MODE_FR1n o)).