]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma
mod change (-x)
[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / status / RS08_status.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "num/word16.ma".
24
25 (* *********************************** *)
26 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
27 (* *********************************** *)
28
29 (* ALU dell'RS08 *)
30 nrecord alu_RS08: Type ≝
31  {
32  (* A: registo accumulatore *)
33  acc_low_reg_RS08 : byte8;
34  (* PC: registro program counter *)
35  pc_reg_RS08 : word16;
36  (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
37  (* la logica della sua costruzione e' quindi (PC∧mask) *)
38  (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
39  pc_mask_RS08 : word16;
40  (* SPC: registro shadow program counter *)
41  (* NB: il suo modificatore e' lo stesso di PC *)
42  spc_reg_RS08 : word16;
43
44  (* X: registro indice parte bassa *)
45  (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
46  (* la lettura/scrittura avviene tramite la locazione [0x000F] *)
47  x_map_RS08 : byte8;
48  (* PS: registro selezione di pagina *)
49  (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
50  (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
51  (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
52  (* la lettura/scrittura avviene tramite la locazione [0x001F] *)
53  ps_map_RS08 : byte8;
54  
55  (* Z: flag zero *)
56  z_flag_RS08 : bool;
57  (* C: flag carry *)
58  c_flag_RS08 : bool
59  }.
60
61 notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'Spc_Reg' ≝ spc ; break 'X_Map' ≝ xm ; break 'Ps_Map' ≝ psm ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl)}"
62  non associative with precedence 80 for
63  @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
64 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
65  (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
66
67 (* ****** *)
68 (* SETTER *)
69 (* ****** *)
70
71 (* setter specifico RS08 di A *)
72 ndefinition set_acc_8_low_reg_RS08 ≝ 
73 λalu.λacclow':byte8.
74  mk_alu_RS08
75   acclow'
76   (pc_reg_RS08 alu)
77   (pc_mask_RS08 alu)
78   (spc_reg_RS08 alu)
79   (x_map_RS08 alu)
80   (ps_map_RS08 alu)
81   (z_flag_RS08 alu)
82   (c_flag_RS08 alu).
83
84 (* setter specifico RS08 di PC, effettua PC∧mask *)
85 ndefinition set_pc_reg_RS08 ≝ 
86 λalu.λpc':word16.
87  mk_alu_RS08
88   (acc_low_reg_RS08 alu)
89   (and_w16 pc' (pc_mask_RS08 alu))
90   (pc_mask_RS08 alu)
91   (spc_reg_RS08 alu)
92   (x_map_RS08 alu)
93   (ps_map_RS08 alu)
94   (z_flag_RS08 alu)
95   (c_flag_RS08 alu).
96
97 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
98 ndefinition set_spc_reg_RS08 ≝ 
99 λalu.λspc':word16.
100  mk_alu_RS08
101   (acc_low_reg_RS08 alu)
102   (pc_reg_RS08 alu)
103   (pc_mask_RS08 alu)
104   (and_w16 spc' (pc_mask_RS08 alu))
105   (x_map_RS08 alu)
106   (ps_map_RS08 alu)
107   (z_flag_RS08 alu)
108   (c_flag_RS08 alu).
109
110 (* setter specifico RS08 di memory mapped X *)
111 ndefinition set_x_map_RS08 ≝ 
112 λalu.λxm':byte8.
113  mk_alu_RS08
114   (acc_low_reg_RS08 alu)
115   (pc_reg_RS08 alu)
116   (pc_mask_RS08 alu)
117   (spc_reg_RS08 alu)
118   xm'
119   (ps_map_RS08 alu)
120   (z_flag_RS08 alu)
121   (c_flag_RS08 alu).
122
123 (* setter specifico RS08 di memory mapped PS *)
124 ndefinition set_ps_map_RS08 ≝ 
125 λalu.λpsm':byte8.
126  mk_alu_RS08
127   (acc_low_reg_RS08 alu)
128   (pc_reg_RS08 alu)
129   (pc_mask_RS08 alu)
130   (spc_reg_RS08 alu)
131   (x_map_RS08 alu)
132   psm'
133   (z_flag_RS08 alu)
134   (c_flag_RS08 alu).
135
136 (* setter sprcifico RS08 di Z *)
137 ndefinition set_z_flag_RS08 ≝ 
138 λalu.λzfl':bool.
139  mk_alu_RS08
140   (acc_low_reg_RS08 alu)
141   (pc_reg_RS08 alu)
142   (pc_mask_RS08 alu)
143   (spc_reg_RS08 alu)
144   (x_map_RS08 alu)
145   (ps_map_RS08 alu)
146   zfl'
147   (c_flag_RS08 alu).
148
149 (* setter specifico RS08 di C *)
150 ndefinition set_c_flag_RS08 ≝ 
151 λalu.λcfl':bool.
152  mk_alu_RS08
153   (acc_low_reg_RS08 alu)
154   (pc_reg_RS08 alu)
155   (pc_mask_RS08 alu)
156   (spc_reg_RS08 alu)
157   (x_map_RS08 alu)
158   (ps_map_RS08 alu)
159   (z_flag_RS08 alu)
160   cfl'.
161
162 (* ***************** *)
163 (* CONFRONTO FRA ALU *)
164 (* ***************** *)
165
166 (* confronto registro per registro dell'RS08 *)
167 ndefinition eq_RS08_alu ≝
168 λalu1,alu2:alu_RS08.
169  (eq_b8 (acc_low_reg_RS08 alu1) (acc_low_reg_RS08 alu2)) ⊗
170  (eq_w16 (pc_reg_RS08 alu1) (pc_reg_RS08 alu2)) ⊗
171  (eq_w16 (pc_mask_RS08 alu1) (pc_mask_RS08 alu2)) ⊗
172  (eq_w16 (spc_reg_RS08 alu1) (spc_reg_RS08 alu2)) ⊗
173  (eq_b8 (x_map_RS08 alu1) (x_map_RS08 alu2)) ⊗
174  (eq_b8 (ps_map_RS08 alu1) (ps_map_RS08 alu2)) ⊗
175  (eq_bool (z_flag_RS08 alu1) (z_flag_RS08 alu2)) ⊗
176  (eq_bool (c_flag_RS08 alu1) (c_flag_RS08 alu2)).