]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/ng_assembly/emulator/status/HC05_status.ma
mod change (-x)
[helm.git] / matitaB / matita / contribs / ng_assembly / emulator / status / HC05_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'HC05 *)
30 nrecord alu_HC05: Type ≝
31  {
32  (* A: registo accumulatore *)
33  acc_low_reg_HC05 : byte8;
34  (* X: registro indice *)
35  indX_low_reg_HC05 : byte8;
36  (* SP: registo stack pointer *)
37  sp_reg_HC05 : word16;
38  (* modificatori di SP: per esempio e' definito come 0000000011xxxxxxb *)
39  (* la logica della sua costruzione e' quindi (SP∧mask)∨fix *)
40  (* totalmente racchiusa nella ALU, bastera' fare get(set(SP)) *)
41  sp_mask_HC05 : word16;
42  sp_fix_HC05 : word16;
43  (* PC: registro program counter *)
44  pc_reg_HC05 : word16;
45  (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
46  (* la logica della sua costruzione e' quindi (PC∧mask) *)
47  (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
48  pc_mask_HC05 : word16;
49  
50  (* H: flag semi-carry (somma nibble basso) *)
51  h_flag_HC05 : bool;
52  (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
53  i_flag_HC05 : bool;
54  (* N: flag segno/negativita' *)
55  n_flag_HC05 : bool;
56  (* Z: flag zero *)
57  z_flag_HC05 : bool;
58  (* C: flag carry *)
59  c_flag_HC05 : bool;
60  
61  (* IRQ: flag che simula il pin esterno IRQ *)
62  irq_flag_HC05 : bool
63  }.
64
65 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg' ≝ sp ; break 'Sp_Mask' ≝ spm ; break 'Sp_Fix' ≝ spf ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
66  non associative with precedence 80 for
67  @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
68 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
69  (mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
70
71 (* ****** *)
72 (* SETTER *)
73 (* ****** *)
74
75 (* setter specifico HC05 di A *)
76 ndefinition set_acc_8_low_reg_HC05 ≝
77 λalu.λacclow':byte8.
78  mk_alu_HC05
79   acclow'
80   (indX_low_reg_HC05 alu)
81   (sp_reg_HC05 alu)
82   (sp_mask_HC05 alu)
83   (sp_fix_HC05 alu)
84   (pc_reg_HC05 alu)
85   (pc_mask_HC05 alu)
86   (h_flag_HC05 alu)
87   (i_flag_HC05 alu)
88   (n_flag_HC05 alu)
89   (z_flag_HC05 alu)
90   (c_flag_HC05 alu)
91   (irq_flag_HC05 alu).
92
93 (* setter specifico HC05 di X *)
94 ndefinition set_indX_8_low_reg_HC05 ≝
95 λalu.λindxlow':byte8.
96  mk_alu_HC05
97   (acc_low_reg_HC05 alu)
98   indxlow'
99   (sp_reg_HC05 alu)
100   (sp_mask_HC05 alu)
101   (sp_fix_HC05 alu)
102   (pc_reg_HC05 alu)
103   (pc_mask_HC05 alu)
104   (h_flag_HC05 alu)
105   (i_flag_HC05 alu)
106   (n_flag_HC05 alu)
107   (z_flag_HC05 alu)
108   (c_flag_HC05 alu)
109   (irq_flag_HC05 alu).
110
111 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
112 ndefinition set_sp_reg_HC05 ≝
113 λalu.λsp':word16.
114  mk_alu_HC05
115   (acc_low_reg_HC05 alu)
116   (indX_low_reg_HC05 alu)
117   (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
118   (sp_mask_HC05 alu)
119   (sp_fix_HC05 alu)
120   (pc_reg_HC05 alu)
121   (pc_mask_HC05 alu)
122   (h_flag_HC05 alu)
123   (i_flag_HC05 alu)
124   (n_flag_HC05 alu)
125   (z_flag_HC05 alu)
126   (c_flag_HC05 alu)
127   (irq_flag_HC05 alu).
128
129 (* setter specifico HC05 di PC, effettua PC∧mask *)
130 ndefinition set_pc_reg_HC05 ≝
131 λalu.λpc':word16.
132  mk_alu_HC05
133   (acc_low_reg_HC05 alu)
134   (indX_low_reg_HC05 alu)
135   (sp_reg_HC05 alu)
136   (sp_mask_HC05 alu)
137   (sp_fix_HC05 alu)
138   (and_w16 pc' (pc_mask_HC05 alu))
139   (pc_mask_HC05 alu)
140   (h_flag_HC05 alu)
141   (i_flag_HC05 alu)
142   (n_flag_HC05 alu)
143   (z_flag_HC05 alu)
144   (c_flag_HC05 alu)
145   (irq_flag_HC05 alu).
146
147 (* setter specifico HC05 di H *)
148 ndefinition set_h_flag_HC05 ≝
149 λalu.λhfl':bool.
150  mk_alu_HC05
151   (acc_low_reg_HC05 alu)
152   (indX_low_reg_HC05 alu)
153   (sp_reg_HC05 alu)
154   (sp_mask_HC05 alu)
155   (sp_fix_HC05 alu)
156   (pc_reg_HC05 alu)
157   (pc_mask_HC05 alu)
158   hfl'
159   (i_flag_HC05 alu)
160   (n_flag_HC05 alu)
161   (z_flag_HC05 alu)
162   (c_flag_HC05 alu)
163   (irq_flag_HC05 alu).
164
165 (* setter specifico HC05 di I *)
166 ndefinition set_i_flag_HC05 ≝
167 λalu.λifl':bool.
168  mk_alu_HC05
169   (acc_low_reg_HC05 alu)
170   (indX_low_reg_HC05 alu)
171   (sp_reg_HC05 alu)
172   (sp_mask_HC05 alu)
173   (sp_fix_HC05 alu)
174   (pc_reg_HC05 alu)
175   (pc_mask_HC05 alu)
176   (h_flag_HC05 alu)
177   ifl'
178   (n_flag_HC05 alu)
179   (z_flag_HC05 alu)
180   (c_flag_HC05 alu)
181   (irq_flag_HC05 alu).
182
183 (* setter specifico HC05 di N *)
184 ndefinition set_n_flag_HC05 ≝
185 λalu.λnfl':bool.
186  mk_alu_HC05
187   (acc_low_reg_HC05 alu)
188   (indX_low_reg_HC05 alu)
189   (sp_reg_HC05 alu)
190   (sp_mask_HC05 alu)
191   (sp_fix_HC05 alu)
192   (pc_reg_HC05 alu)
193   (pc_mask_HC05 alu)
194   (h_flag_HC05 alu)
195   (i_flag_HC05 alu)
196   nfl'
197   (z_flag_HC05 alu)
198   (c_flag_HC05 alu)
199   (irq_flag_HC05 alu).
200
201 (* setter specifico HC05 di Z *)
202 ndefinition set_z_flag_HC05 ≝
203 λalu.λzfl':bool.
204  mk_alu_HC05
205   (acc_low_reg_HC05 alu)
206   (indX_low_reg_HC05 alu)
207   (sp_reg_HC05 alu)
208   (sp_mask_HC05 alu)
209   (sp_fix_HC05 alu)
210   (pc_reg_HC05 alu)
211   (pc_mask_HC05 alu)
212   (h_flag_HC05 alu)
213   (i_flag_HC05 alu)
214   (n_flag_HC05 alu)
215   zfl'
216   (c_flag_HC05 alu)
217   (irq_flag_HC05 alu).
218
219 (* setter specifico HC05 di C *)
220 ndefinition set_c_flag_HC05 ≝
221 λalu.λcfl':bool.
222  mk_alu_HC05
223   (acc_low_reg_HC05 alu)
224   (indX_low_reg_HC05 alu)
225   (sp_reg_HC05 alu)
226   (sp_mask_HC05 alu)
227   (sp_fix_HC05 alu)
228   (pc_reg_HC05 alu)
229   (pc_mask_HC05 alu)
230   (h_flag_HC05 alu)
231   (i_flag_HC05 alu)
232   (n_flag_HC05 alu)
233   (z_flag_HC05 alu)
234   cfl'
235   (irq_flag_HC05 alu).
236
237 (* setter specifico HC05 di IRQ *)
238 ndefinition set_irq_flag_HC05 ≝
239 λalu.λirqfl':bool.
240  mk_alu_HC05
241   (acc_low_reg_HC05 alu)
242   (indX_low_reg_HC05 alu)
243   (sp_reg_HC05 alu)
244   (sp_mask_HC05 alu)
245   (sp_fix_HC05 alu)
246   (pc_reg_HC05 alu)
247   (pc_mask_HC05 alu)
248   (h_flag_HC05 alu)
249   (i_flag_HC05 alu)
250   (n_flag_HC05 alu)
251   (z_flag_HC05 alu)
252   (c_flag_HC05 alu)
253   irqfl'.
254
255 (* ***************** *)
256 (* CONFRONTO FRA ALU *)
257 (* ***************** *)
258
259 (* confronto registro per registro dell'HC05 *)
260 ndefinition eq_HC05_alu ≝
261 λalu1,alu2:alu_HC05.
262  (eq_b8 (acc_low_reg_HC05 alu1) (acc_low_reg_HC05 alu2)) ⊗
263  (eq_b8 (indX_low_reg_HC05 alu1) (indX_low_reg_HC05 alu2)) ⊗
264  (eq_w16 (sp_reg_HC05 alu1) (sp_reg_HC05 alu2)) ⊗
265  (eq_w16 (sp_mask_HC05 alu1) (sp_mask_HC05 alu2)) ⊗
266  (eq_w16 (sp_fix_HC05 alu1) (sp_fix_HC05 alu2)) ⊗
267  (eq_w16 (pc_reg_HC05 alu1) (pc_reg_HC05 alu2)) ⊗
268  (eq_w16 (pc_mask_HC05 alu1) (pc_mask_HC05 alu2)) ⊗
269  (eq_bool (h_flag_HC05 alu1) (h_flag_HC05 alu2)) ⊗
270  (eq_bool (i_flag_HC05 alu1) (i_flag_HC05 alu2)) ⊗
271  (eq_bool (n_flag_HC05 alu1) (n_flag_HC05 alu2)) ⊗
272  (eq_bool (z_flag_HC05 alu1) (z_flag_HC05 alu2)) ⊗
273  (eq_bool (c_flag_HC05 alu1) (c_flag_HC05 alu2)) ⊗
274  (eq_bool (irq_flag_HC05 alu1) (irq_flag_HC05 alu2)).