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 HC05_instr_mode: Type ≝
31 (* INHERENT = nessun operando *)
32 MODE_INH : HC05_instr_mode
33 (* INHERENT = nessun operando (A implicito) *)
34 | MODE_INHA : HC05_instr_mode
35 (* INHERENT = nessun operando (X implicito) *)
36 | MODE_INHX : HC05_instr_mode
38 (* INHERENT_ADDRESS = nessun operando (HX implicito) *)
39 | MODE_INHX0ADD : HC05_instr_mode
40 (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *)
41 | MODE_INHX1ADD : HC05_instr_mode
42 (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *)
43 | MODE_INHX2ADD : HC05_instr_mode
45 (* IMMEDIATE = operando valore immediato byte = 0xbb *)
46 | MODE_IMM1 : HC05_instr_mode
47 (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *)
48 | MODE_IMM1EXT : HC05_instr_mode
49 (* IMMEDIATE = operando valore immediato word = 0xwwww *)
50 | MODE_IMM2 : HC05_instr_mode
51 (* DIRECT = operando offset byte = [0x00bb] *)
52 | MODE_DIR1 : HC05_instr_mode
53 (* DIRECT = operando offset word = [0xwwww] *)
54 | MODE_DIR2 : HC05_instr_mode
55 (* INDEXED = nessun operando (implicito [X] *)
56 | MODE_IX0 : HC05_instr_mode
57 (* INDEXED = operando offset relativo byte = [X+0x00bb] *)
58 | MODE_IX1 : HC05_instr_mode
59 (* INDEXED = operando offset relativo word = [X+0xwwww] *)
60 | MODE_IX2 : HC05_instr_mode
62 (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *)
63 (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *)
64 | MODE_DIRn : oct → HC05_instr_mode
65 (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *)
66 (* + operando valore immediato byte *)
67 (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *)
68 | MODE_DIRn_and_IMM1 : oct → HC05_instr_mode
71 ndefinition eq_HC05_im ≝
72 λi1,i2:HC05_instr_mode.
74 [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
75 | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ]
76 | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ true | _ ⇒ false ]
77 | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ true | _ ⇒ false ]
78 | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ true | _ ⇒ false ]
79 | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ true | _ ⇒ false ]
80 | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ]
81 | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ true | _ ⇒ false ]
82 | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ]
83 | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ]
84 | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ true | _ ⇒ false ]
85 | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ true | _ ⇒ false ]
86 | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ true | _ ⇒ false ]
87 | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ true | _ ⇒ false ]
88 | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
89 | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
92 (* iteratore sulle modalita' *)
93 ndefinition forall_HC05_im ≝ λP:HC05_instr_mode → bool.
108 ⊗ forall_oct (λo. P (MODE_DIRn o))
109 ⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o)).