]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/ng_assembly2/emulator/status/HC08_status_base.ma
wip ....
[helm.git] / matitaB / matita / contribs / ng_assembly2 / emulator / status / HC08_status_base.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'HC08/HCS08 *) 
30 nrecord alu_HC08: Type ≝
31  {
32  (* A: registo accumulatore *)
33  acc_low_reg_HC08 : byte8;
34  (* X: registro indice parte bassa *)
35  indX_low_reg_HC08 : byte8;
36  (* H: registro indice parte alta *)
37  indX_high_reg_HC08 : byte8;
38  (* SP: registo stack pointer *)
39  sp_reg_HC08 : word16;
40  (* PC: registro program counter *)
41  pc_reg_HC08 : word16;
42  
43  (* V: flag overflow *)
44  v_flag_HC08 : bool;
45  (* H: flag semi-carry (somma nibble basso) *)
46  h_flag_HC08 : bool;
47  (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
48  i_flag_HC08 : bool;
49  (* N: flag segno/negativita' *)
50  n_flag_HC08 : bool;
51  (* Z: flag zero *)
52  z_flag_HC08 : bool;
53  (* C: flag carry *)
54  c_flag_HC08 : bool;
55  
56  (* IRQ: flag che simula il pin esterno IRQ *)
57  irq_flag_HC08 : bool
58  }.
59
60 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg' ≝ indxhigh ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'V_Flag' ≝ vfl ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
61  non associative with precedence 80 for
62  @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
63 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
64  (mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
65
66 (* ****** *)
67 (* SETTER *)
68 (* ****** *)
69
70 (* setter specifico HC08/HCS08 di A *)
71 ndefinition set_acc_8_low_reg_HC08 ≝
72 λalu.λacclow':byte8.
73  mk_alu_HC08
74   acclow'
75   (indX_low_reg_HC08 alu)
76   (indX_high_reg_HC08 alu)
77   (sp_reg_HC08 alu)
78   (pc_reg_HC08 alu)
79   (v_flag_HC08 alu)
80   (h_flag_HC08 alu)
81   (i_flag_HC08 alu)
82   (n_flag_HC08 alu)
83   (z_flag_HC08 alu)
84   (c_flag_HC08 alu)
85   (irq_flag_HC08 alu).
86
87 (* setter specifico HC08/HCS08 di X *)
88 ndefinition set_indX_8_low_reg_HC08 ≝
89 λalu.λindxlow':byte8.
90  mk_alu_HC08
91   (acc_low_reg_HC08 alu)
92   indxlow'
93   (indX_high_reg_HC08 alu)
94   (sp_reg_HC08 alu)
95   (pc_reg_HC08 alu)
96   (v_flag_HC08 alu)
97   (h_flag_HC08 alu)
98   (i_flag_HC08 alu)
99   (n_flag_HC08 alu)
100   (z_flag_HC08 alu)
101   (c_flag_HC08 alu)
102   (irq_flag_HC08 alu).
103
104 (* setter specifico HC08/HCS08 di H *)
105 ndefinition set_indX_8_high_reg_HC08 ≝
106 λalu.λindxhigh':byte8.
107  mk_alu_HC08
108   (acc_low_reg_HC08 alu)
109   (indX_low_reg_HC08 alu)
110   indxhigh'
111   (sp_reg_HC08 alu)
112   (pc_reg_HC08 alu)
113   (v_flag_HC08 alu)
114   (h_flag_HC08 alu)
115   (i_flag_HC08 alu)
116   (n_flag_HC08 alu)
117   (z_flag_HC08 alu)
118   (c_flag_HC08 alu)
119   (irq_flag_HC08 alu).
120
121 (* setter specifico HC08/HCS08 di H:X *)
122 ndefinition set_indX_16_reg_HC08 ≝
123 λalu.λindx16:word16.
124  mk_alu_HC08
125   (acc_low_reg_HC08 alu)
126   (cnL ? indx16)
127   (cnH ? indx16)
128   (sp_reg_HC08 alu)
129   (pc_reg_HC08 alu)
130   (v_flag_HC08 alu)
131   (h_flag_HC08 alu)
132   (i_flag_HC08 alu)
133   (n_flag_HC08 alu)
134   (z_flag_HC08 alu)
135   (c_flag_HC08 alu)
136   (irq_flag_HC08 alu).
137
138 (* setter specifico HC08/HCS08 di SP *)
139 ndefinition set_sp_reg_HC08 ≝
140 λalu.λsp':word16.
141  mk_alu_HC08
142   (acc_low_reg_HC08 alu)
143   (indX_low_reg_HC08 alu)
144   (indX_high_reg_HC08 alu)
145   sp'
146   (pc_reg_HC08 alu)
147   (v_flag_HC08 alu)
148   (h_flag_HC08 alu)
149   (i_flag_HC08 alu)
150   (n_flag_HC08 alu)
151   (z_flag_HC08 alu)
152   (c_flag_HC08 alu)
153   (irq_flag_HC08 alu).
154
155 (* setter specifico HC08/HCS08 di PC *)
156 ndefinition set_pc_reg_HC08 ≝
157 λalu.λpc':word16.
158  mk_alu_HC08
159   (acc_low_reg_HC08 alu)
160   (indX_low_reg_HC08 alu)
161   (indX_high_reg_HC08 alu)
162   (sp_reg_HC08 alu)
163   pc'
164   (v_flag_HC08 alu)
165   (h_flag_HC08 alu)
166   (i_flag_HC08 alu)
167   (n_flag_HC08 alu)
168   (z_flag_HC08 alu)
169   (c_flag_HC08 alu)
170   (irq_flag_HC08 alu).
171
172 (* setter specifico HC08/HCS08 di V *)
173 ndefinition set_v_flag_HC08 ≝
174 λalu.λvfl':bool.
175  mk_alu_HC08
176   (acc_low_reg_HC08 alu)
177   (indX_low_reg_HC08 alu)
178   (indX_high_reg_HC08 alu)
179   (sp_reg_HC08 alu)
180   (pc_reg_HC08 alu)
181   vfl'
182   (h_flag_HC08 alu)
183   (i_flag_HC08 alu)
184   (n_flag_HC08 alu)
185   (z_flag_HC08 alu)
186   (c_flag_HC08 alu)
187   (irq_flag_HC08 alu).
188
189 (* setter specifico HC08/HCS08 di H *)
190 ndefinition set_h_flag_HC08 ≝
191 λalu.λhfl':bool.
192  mk_alu_HC08
193   (acc_low_reg_HC08 alu)
194   (indX_low_reg_HC08 alu)
195   (indX_high_reg_HC08 alu)
196   (sp_reg_HC08 alu)
197   (pc_reg_HC08 alu)
198   (v_flag_HC08 alu)
199   hfl'
200   (i_flag_HC08 alu)
201   (n_flag_HC08 alu)
202   (z_flag_HC08 alu)
203   (c_flag_HC08 alu)
204   (irq_flag_HC08 alu).
205
206 (* setter specifico HC08/HCS08 di I *)
207 ndefinition set_i_flag_HC08 ≝
208 λalu.λifl':bool.
209  mk_alu_HC08
210   (acc_low_reg_HC08 alu)
211   (indX_low_reg_HC08 alu)
212   (indX_high_reg_HC08 alu)
213   (sp_reg_HC08 alu)
214   (pc_reg_HC08 alu)
215   (v_flag_HC08 alu)
216   (h_flag_HC08 alu)
217   ifl'
218   (n_flag_HC08 alu)
219   (z_flag_HC08 alu)
220   (c_flag_HC08 alu)
221   (irq_flag_HC08 alu).
222
223 (* setter specifico HC08/HCS08 di N *)
224 ndefinition set_n_flag_HC08 ≝
225 λalu.λnfl':bool.
226  mk_alu_HC08
227   (acc_low_reg_HC08 alu)
228   (indX_low_reg_HC08 alu)
229   (indX_high_reg_HC08 alu)
230   (sp_reg_HC08 alu)
231   (pc_reg_HC08 alu)
232   (v_flag_HC08 alu)
233   (h_flag_HC08 alu)
234   (i_flag_HC08 alu)
235   nfl'
236   (z_flag_HC08 alu)
237   (c_flag_HC08 alu)
238   (irq_flag_HC08 alu).
239
240 (* setter specifico HC08/HCS08 di Z *)
241 ndefinition set_z_flag_HC08 ≝
242 λalu.λzfl':bool.
243  mk_alu_HC08
244   (acc_low_reg_HC08 alu)
245   (indX_low_reg_HC08 alu)
246   (indX_high_reg_HC08 alu)
247   (sp_reg_HC08 alu)
248   (pc_reg_HC08 alu)
249   (v_flag_HC08 alu)
250   (h_flag_HC08 alu)
251   (i_flag_HC08 alu)
252   (n_flag_HC08 alu)
253   zfl'
254   (c_flag_HC08 alu)
255   (irq_flag_HC08 alu).
256
257 (* setter specifico HC08/HCS08 di C *)
258 ndefinition set_c_flag_HC08 ≝
259 λalu.λcfl':bool.
260  mk_alu_HC08
261   (acc_low_reg_HC08 alu)
262   (indX_low_reg_HC08 alu)
263   (indX_high_reg_HC08 alu)
264   (sp_reg_HC08 alu)
265   (pc_reg_HC08 alu)
266   (v_flag_HC08 alu)
267   (h_flag_HC08 alu)
268   (i_flag_HC08 alu)
269   (n_flag_HC08 alu)
270   (z_flag_HC08 alu)
271   cfl'
272   (irq_flag_HC08 alu).
273
274 (* setter specifico HC08/HCS08 di IRQ *)
275 ndefinition set_irq_flag_HC08 ≝
276 λalu.λirqfl':bool.
277  mk_alu_HC08
278   (acc_low_reg_HC08 alu)
279   (indX_low_reg_HC08 alu)
280   (indX_high_reg_HC08 alu)
281   (sp_reg_HC08 alu)
282   (pc_reg_HC08 alu)
283   (v_flag_HC08 alu)
284   (h_flag_HC08 alu)
285   (i_flag_HC08 alu)
286   (n_flag_HC08 alu)
287   (z_flag_HC08 alu)
288   (c_flag_HC08 alu)
289   irqfl'.
290
291 (* ***************** *)
292 (* CONFRONTO FRA ALU *)
293 (* ***************** *)
294
295 (* confronto registro per registro dell'HC08 *)
296 ndefinition eq_HC08_alu ≝
297 λalu1,alu2:alu_HC08.
298  (eqc ? (acc_low_reg_HC08 alu1) (acc_low_reg_HC08 alu2)) ⊗
299  (eqc ? (indX_low_reg_HC08 alu1) (indX_low_reg_HC08 alu2)) ⊗
300  (eqc ? (indX_high_reg_HC08 alu1) (indX_high_reg_HC08 alu2)) ⊗
301  (eqc ? (sp_reg_HC08 alu1) (sp_reg_HC08 alu2)) ⊗
302  (eqc ? (pc_reg_HC08 alu1) (pc_reg_HC08 alu2)) ⊗
303  (eqc ? (v_flag_HC08 alu1) (v_flag_HC08 alu2)) ⊗
304  (eqc ? (h_flag_HC08 alu1) (h_flag_HC08 alu2)) ⊗
305  (eqc ? (i_flag_HC08 alu1) (i_flag_HC08 alu2)) ⊗
306  (eqc ? (n_flag_HC08 alu1) (n_flag_HC08 alu2)) ⊗
307  (eqc ? (z_flag_HC08 alu1) (z_flag_HC08 alu2)) ⊗
308  (eqc ? (c_flag_HC08 alu1) (c_flag_HC08 alu2)) ⊗
309  (eqc ? (irq_flag_HC08 alu1) (irq_flag_HC08 alu2)).
310
311 ndefinition forall_HC08_alu ≝ λP:alu_HC08 → bool.
312  forallc ? (λr1.forallc ? (λr2.
313  forallc ? (λr3.forallc ? (λr4.
314  forallc ? (λr5.forallc ? (λr6.
315  forallc ? (λr7.forallc ? (λr8.
316  forallc ? (λr9.forallc ? (λr10.
317  forallc ? (λr11.forallc ? (λr12.
318  P (mk_alu_HC08 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12))))))))))))).