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 RS08_instr_mode: Type ≝
31 (* INHERENT = nessun operando *)
32 MODE_INH : RS08_instr_mode
33 (* INHERENT = nessun operando (A implicito) *)
34 | MODE_INHA : RS08_instr_mode
36 (* IMMEDIATE = operando valore immediato byte = 0xbb *)
37 | MODE_IMM1 : RS08_instr_mode
38 (* IMMEDIATE = operando valore immediato word = 0xwwww *)
39 | MODE_IMM2 : RS08_instr_mode
40 (* DIRECT = operando offset byte = [0x00bb] *)
41 | MODE_DIR1 : RS08_instr_mode
43 (* DIRECT → DIRECT = carica da diretto/scrive su diretto *)
44 | MODE_DIR1_to_DIR1 : RS08_instr_mode
45 (* IMMEDIATE → DIRECT = carica da immediato/scrive su diretto *)
46 | MODE_IMM1_to_DIR1 : RS08_instr_mode
48 (* INHERENT(A) + IMMEDIATE *)
49 | MODE_INHA_and_IMM1 : RS08_instr_mode
50 (* IMMEDIATE + IMMEDIATE *)
51 | MODE_IMM1_and_IMM1 : RS08_instr_mode
52 (* DIRECT + IMMEDIATE *)
53 | MODE_DIR1_and_IMM1 : RS08_instr_mode
55 (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *)
56 (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *)
57 | MODE_DIRn : oct → RS08_instr_mode
58 (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *)
59 (* + operando valore immediato byte *)
60 (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *)
61 | MODE_DIRn_and_IMM1 : oct → RS08_instr_mode
62 (* TINY = nessun operando (diretto implicito 4bit = [0x00000000:0000iiii]) *)
63 | MODE_TNY : exadecim → RS08_instr_mode
64 (* SHORT = nessun operando (diretto implicito 5bit = [0x00000000:000iiiii]) *)
65 | MODE_SRT : bitrigesim → RS08_instr_mode
68 ndefinition eq_RS08_im ≝
69 λi1,i2:RS08_instr_mode.
71 [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
72 | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ]
73 | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ]
74 | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ]
75 | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ]
76 | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ true | _ ⇒ false ]
77 | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ true | _ ⇒ false ]
78 | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ true | _ ⇒ false ]
79 | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ true | _ ⇒ false ]
80 | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ true | _ ⇒ false ]
81 | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
82 | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
83 | MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eq_ex e1 e2 | _ ⇒ false ]
84 | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bit t1 t2 | _ ⇒ false ]
87 (* iteratore sulle modalita' *)
88 ndefinition forall_RS08_im ≝ λP:RS08_instr_mode → bool.
96 ⊗ P MODE_INHA_and_IMM1
97 ⊗ P MODE_IMM1_and_IMM1
98 ⊗ P MODE_DIR1_and_IMM1
99 ⊗ forall_oct (λo. P (MODE_DIRn o))
100 ⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o))
101 ⊗ forall_ex (λe. P (MODE_TNY e))
102 ⊗ forall_bit (λt. P (MODE_SRT t)).