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 *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/exadecim.ma".
33 nrecord byte8 : Type ≝
39 ndefinition byte8_ind : ΠP:byte8 → Prop.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
40 λP:byte8 → Prop.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
41 match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
43 ndefinition byte8_rec : ΠP:byte8 → Set.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
44 λP:byte8 → Set.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
45 match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
47 ndefinition byte8_rect : ΠP:byte8 → Type.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
48 λP:byte8 → Type.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
49 match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
51 ndefinition b8h ≝ λb:byte8.match b with [ mk_byte8 x _ ⇒ x ].
52 ndefinition b8l ≝ λb:byte8.match b with [ mk_byte8 _ x ⇒ x ].
55 notation "〈x,y〉" non associative with precedence 80
56 for @{ 'mk_byte8 $x $y }.
57 interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
60 ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
64 λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with
66 | false ⇒ match gt_ex (b8h b1) (b8h b2) with
68 | false ⇒ lt_ex (b8l b1) (b8l b2) ]].
71 ndefinition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2).
74 ndefinition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2).
77 ndefinition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2).
81 λb1,b2:byte8.mk_byte8 (and_ex (b8h b1) (b8h b2)) (and_ex (b8l b1) (b8l b2)).
85 λb1,b2:byte8.mk_byte8 (or_ex (b8h b1) (b8h b2)) (or_ex (b8l b1) (b8l b2)).
89 λb1,b2:byte8.mk_byte8 (xor_ex (b8h b1) (b8h b2)) (xor_ex (b8l b1) (b8l b2)).
91 (* operatore rotazione destra con carry *)
93 λb:byte8.λc:bool.match rcr_ex (b8h b) c with
94 [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
95 [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
97 (* operatore shift destro *)
99 λb:byte8.match rcr_ex (b8h b) false with
100 [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
101 [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
103 (* operatore rotazione destra *)
105 λb:byte8.match rcr_ex (b8h b) false with
106 [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
107 [ pair bl' c'' ⇒ match c'' with
108 [ true ⇒ mk_byte8 (or_ex x8 bh') bl'
109 | false ⇒ mk_byte8 bh' bl' ]]].
111 (* operatore rotazione destra n-volte *)
112 nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
115 | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
117 (* operatore rotazione sinistra con carry *)
119 λb:byte8.λc:bool.match rcl_ex (b8l b) c with
120 [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
121 [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
123 (* operatore shift sinistro *)
125 λb:byte8.match rcl_ex (b8l b) false with
126 [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
127 [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
129 (* operatore rotazione sinistra *)
131 λb:byte8.match rcl_ex (b8l b) false with
132 [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
133 [ pair bh' c'' ⇒ match c'' with
134 [ true ⇒ mk_byte8 bh' (or_ex x1 bl')
135 | false ⇒ mk_byte8 bh' bl' ]]].
137 (* operatore rotazione sinistra n-volte *)
138 nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
141 | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
143 (* operatore not/complemento a 1 *)
145 λb:byte8.mk_byte8 (not_ex (b8h b)) (not_ex (b8l b)).
147 (* operatore somma con data+carry → data+carry *)
148 ndefinition plus_b8_dc_dc ≝
149 λb1,b2:byte8.λc:bool.
150 match plus_ex_dc_dc (b8l b1) (b8l b2) c with
151 [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
152 [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]].
154 (* operatore somma con data+carry → data *)
155 ndefinition plus_b8_dc_d ≝
156 λb1,b2:byte8.λc:bool.
157 match plus_ex_dc_dc (b8l b1) (b8l b2) c with
158 [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
160 (* operatore somma con data+carry → c *)
161 ndefinition plus_b8_dc_c ≝
162 λb1,b2:byte8.λc:bool.
163 plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_dc_c (b8l b1) (b8l b2) c).
165 (* operatore somma con data → data+carry *)
166 ndefinition plus_b8_d_dc ≝
168 match plus_ex_d_dc (b8l b1) (b8l b2) with
169 [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
170 [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]].
172 (* operatore somma con data → data *)
173 ndefinition plus_b8_d_d ≝
175 match plus_ex_d_dc (b8l b1) (b8l b2) with
176 [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
178 (* operatore somma con data → c *)
179 ndefinition plus_b8_d_c ≝
181 plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_d_c (b8l b1) (b8l b2)).
183 (* operatore Most Significant Bit *)
184 ndefinition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
186 (* byte → naturali *)
187 ndefinition nat_of_byte8 ≝ λb:byte8.(16*(nat_of_exadecim (b8h b))) + (nat_of_exadecim (b8l b)).
189 (* operatore predecessore *)
190 ndefinition pred_b8 ≝
191 λb:byte8.match eq_ex (b8l b) x0 with
192 [ true ⇒ mk_byte8 (pred_ex (b8h b)) (pred_ex (b8l b))
193 | false ⇒ mk_byte8 (b8h b) (pred_ex (b8l b)) ].
195 (* operatore successore *)
196 ndefinition succ_b8 ≝
197 λb:byte8.match eq_ex (b8l b) xF with
198 [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
199 | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ].
201 (* operatore neg/complemento a 2 *)
202 ndefinition compl_b8 ≝
203 λb:byte8.match MSB_b8 b with
204 [ true ⇒ succ_b8 (not_b8 b)
205 | false ⇒ not_b8 (pred_b8 b) ].
207 (* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
209 λe1,e2:exadecim.match e1 with
211 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x0〉 | x2 ⇒ 〈x0,x0〉 | x3 ⇒ 〈x0,x0〉
212 | x4 ⇒ 〈x0,x0〉 | x5 ⇒ 〈x0,x0〉 | x6 ⇒ 〈x0,x0〉 | x7 ⇒ 〈x0,x0〉
213 | x8 ⇒ 〈x0,x0〉 | x9 ⇒ 〈x0,x0〉 | xA ⇒ 〈x0,x0〉 | xB ⇒ 〈x0,x0〉
214 | xC ⇒ 〈x0,x0〉 | xD ⇒ 〈x0,x0〉 | xE ⇒ 〈x0,x0〉 | xF ⇒ 〈x0,x0〉 ]
216 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x1〉 | x2 ⇒ 〈x0,x2〉 | x3 ⇒ 〈x0,x3〉
217 | x4 ⇒ 〈x0,x4〉 | x5 ⇒ 〈x0,x5〉 | x6 ⇒ 〈x0,x6〉 | x7 ⇒ 〈x0,x7〉
218 | x8 ⇒ 〈x0,x8〉 | x9 ⇒ 〈x0,x9〉 | xA ⇒ 〈x0,xA〉 | xB ⇒ 〈x0,xB〉
219 | xC ⇒ 〈x0,xC〉 | xD ⇒ 〈x0,xD〉 | xE ⇒ 〈x0,xE〉 | xF ⇒ 〈x0,xF〉 ]
221 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x2〉 | x2 ⇒ 〈x0,x4〉 | x3 ⇒ 〈x0,x6〉
222 | x4 ⇒ 〈x0,x8〉 | x5 ⇒ 〈x0,xA〉 | x6 ⇒ 〈x0,xC〉 | x7 ⇒ 〈x0,xE〉
223 | x8 ⇒ 〈x1,x0〉 | x9 ⇒ 〈x1,x2〉 | xA ⇒ 〈x1,x4〉 | xB ⇒ 〈x1,x6〉
224 | xC ⇒ 〈x1,x8〉 | xD ⇒ 〈x1,xA〉 | xE ⇒ 〈x1,xC〉 | xF ⇒ 〈x1,xE〉 ]
226 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x3〉 | x2 ⇒ 〈x0,x6〉 | x3 ⇒ 〈x0,x9〉
227 | x4 ⇒ 〈x0,xC〉 | x5 ⇒ 〈x0,xF〉 | x6 ⇒ 〈x1,x2〉 | x7 ⇒ 〈x1,x5〉
228 | x8 ⇒ 〈x1,x8〉 | x9 ⇒ 〈x1,xB〉 | xA ⇒ 〈x1,xE〉 | xB ⇒ 〈x2,x1〉
229 | xC ⇒ 〈x2,x4〉 | xD ⇒ 〈x2,x7〉 | xE ⇒ 〈x2,xA〉 | xF ⇒ 〈x2,xD〉 ]
231 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x4〉 | x2 ⇒ 〈x0,x8〉 | x3 ⇒ 〈x0,xC〉
232 | x4 ⇒ 〈x1,x0〉 | x5 ⇒ 〈x1,x4〉 | x6 ⇒ 〈x1,x8〉 | x7 ⇒ 〈x1,xC〉
233 | x8 ⇒ 〈x2,x0〉 | x9 ⇒ 〈x2,x4〉 | xA ⇒ 〈x2,x8〉 | xB ⇒ 〈x2,xC〉
234 | xC ⇒ 〈x3,x0〉 | xD ⇒ 〈x3,x4〉 | xE ⇒ 〈x3,x8〉 | xF ⇒ 〈x3,xC〉 ]
236 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x5〉 | x2 ⇒ 〈x0,xA〉 | x3 ⇒ 〈x0,xF〉
237 | x4 ⇒ 〈x1,x4〉 | x5 ⇒ 〈x1,x9〉 | x6 ⇒ 〈x1,xE〉 | x7 ⇒ 〈x2,x3〉
238 | x8 ⇒ 〈x2,x8〉 | x9 ⇒ 〈x2,xD〉 | xA ⇒ 〈x3,x2〉 | xB ⇒ 〈x3,x7〉
239 | xC ⇒ 〈x3,xC〉 | xD ⇒ 〈x4,x1〉 | xE ⇒ 〈x4,x6〉 | xF ⇒ 〈x4,xB〉 ]
241 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x6〉 | x2 ⇒ 〈x0,xC〉 | x3 ⇒ 〈x1,x2〉
242 | x4 ⇒ 〈x1,x8〉 | x5 ⇒ 〈x1,xE〉 | x6 ⇒ 〈x2,x4〉 | x7 ⇒ 〈x2,xA〉
243 | x8 ⇒ 〈x3,x0〉 | x9 ⇒ 〈x3,x6〉 | xA ⇒ 〈x3,xC〉 | xB ⇒ 〈x4,x2〉
244 | xC ⇒ 〈x4,x8〉 | xD ⇒ 〈x4,xE〉 | xE ⇒ 〈x5,x4〉 | xF ⇒ 〈x5,xA〉 ]
246 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x7〉 | x2 ⇒ 〈x0,xE〉 | x3 ⇒ 〈x1,x5〉
247 | x4 ⇒ 〈x1,xC〉 | x5 ⇒ 〈x2,x3〉 | x6 ⇒ 〈x2,xA〉 | x7 ⇒ 〈x3,x1〉
248 | x8 ⇒ 〈x3,x8〉 | x9 ⇒ 〈x3,xF〉 | xA ⇒ 〈x4,x6〉 | xB ⇒ 〈x4,xD〉
249 | xC ⇒ 〈x5,x4〉 | xD ⇒ 〈x5,xB〉 | xE ⇒ 〈x6,x2〉 | xF ⇒ 〈x6,x9〉 ]
251 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x8〉 | x2 ⇒ 〈x1,x0〉 | x3 ⇒ 〈x1,x8〉
252 | x4 ⇒ 〈x2,x0〉 | x5 ⇒ 〈x2,x8〉 | x6 ⇒ 〈x3,x0〉 | x7 ⇒ 〈x3,x8〉
253 | x8 ⇒ 〈x4,x0〉 | x9 ⇒ 〈x4,x8〉 | xA ⇒ 〈x5,x0〉 | xB ⇒ 〈x5,x8〉
254 | xC ⇒ 〈x6,x0〉 | xD ⇒ 〈x6,x8〉 | xE ⇒ 〈x7,x0〉 | xF ⇒ 〈x7,x8〉 ]
256 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x9〉 | x2 ⇒ 〈x1,x2〉 | x3 ⇒ 〈x1,xB〉
257 | x4 ⇒ 〈x2,x4〉 | x5 ⇒ 〈x2,xD〉 | x6 ⇒ 〈x3,x6〉 | x7 ⇒ 〈x3,xF〉
258 | x8 ⇒ 〈x4,x8〉 | x9 ⇒ 〈x5,x1〉 | xA ⇒ 〈x5,xA〉 | xB ⇒ 〈x6,x3〉
259 | xC ⇒ 〈x6,xC〉 | xD ⇒ 〈x7,x5〉 | xE ⇒ 〈x7,xE〉 | xF ⇒ 〈x8,x7〉 ]
261 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xA〉 | x2 ⇒ 〈x1,x4〉 | x3 ⇒ 〈x1,xE〉
262 | x4 ⇒ 〈x2,x8〉 | x5 ⇒ 〈x3,x2〉 | x6 ⇒ 〈x3,xC〉 | x7 ⇒ 〈x4,x6〉
263 | x8 ⇒ 〈x5,x0〉 | x9 ⇒ 〈x5,xA〉 | xA ⇒ 〈x6,x4〉 | xB ⇒ 〈x6,xE〉
264 | xC ⇒ 〈x7,x8〉 | xD ⇒ 〈x8,x2〉 | xE ⇒ 〈x8,xC〉 | xF ⇒ 〈x9,x6〉 ]
266 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xB〉 | x2 ⇒ 〈x1,x6〉 | x3 ⇒ 〈x2,x1〉
267 | x4 ⇒ 〈x2,xC〉 | x5 ⇒ 〈x3,x7〉 | x6 ⇒ 〈x4,x2〉 | x7 ⇒ 〈x4,xD〉
268 | x8 ⇒ 〈x5,x8〉 | x9 ⇒ 〈x6,x3〉 | xA ⇒ 〈x6,xE〉 | xB ⇒ 〈x7,x9〉
269 | xC ⇒ 〈x8,x4〉 | xD ⇒ 〈x8,xF〉 | xE ⇒ 〈x9,xA〉 | xF ⇒ 〈xA,x5〉 ]
271 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xC〉 | x2 ⇒ 〈x1,x8〉 | x3 ⇒ 〈x2,x4〉
272 | x4 ⇒ 〈x3,x0〉 | x5 ⇒ 〈x3,xC〉 | x6 ⇒ 〈x4,x8〉 | x7 ⇒ 〈x5,x4〉
273 | x8 ⇒ 〈x6,x0〉 | x9 ⇒ 〈x6,xC〉 | xA ⇒ 〈x7,x8〉 | xB ⇒ 〈x8,x4〉
274 | xC ⇒ 〈x9,x0〉 | xD ⇒ 〈x9,xC〉 | xE ⇒ 〈xA,x8〉 | xF ⇒ 〈xB,x4〉 ]
276 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xD〉 | x2 ⇒ 〈x1,xA〉 | x3 ⇒ 〈x2,x7〉
277 | x4 ⇒ 〈x3,x4〉 | x5 ⇒ 〈x4,x1〉 | x6 ⇒ 〈x4,xE〉 | x7 ⇒ 〈x5,xB〉
278 | x8 ⇒ 〈x6,x8〉 | x9 ⇒ 〈x7,x5〉 | xA ⇒ 〈x8,x2〉 | xB ⇒ 〈x8,xF〉
279 | xC ⇒ 〈x9,xC〉 | xD ⇒ 〈xA,x9〉 | xE ⇒ 〈xB,x6〉 | xF ⇒ 〈xC,x3〉 ]
281 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xE〉 | x2 ⇒ 〈x1,xC〉 | x3 ⇒ 〈x2,xA〉
282 | x4 ⇒ 〈x3,x8〉 | x5 ⇒ 〈x4,x6〉 | x6 ⇒ 〈x5,x4〉 | x7 ⇒ 〈x6,x2〉
283 | x8 ⇒ 〈x7,x0〉 | x9 ⇒ 〈x7,xE〉 | xA ⇒ 〈x8,xC〉 | xB ⇒ 〈x9,xA〉
284 | xC ⇒ 〈xA,x8〉 | xD ⇒ 〈xB,x6〉 | xE ⇒ 〈xC,x4〉 | xF ⇒ 〈xD,x2〉 ]
286 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xF〉 | x2 ⇒ 〈x1,xE〉 | x3 ⇒ 〈x2,xD〉
287 | x4 ⇒ 〈x3,xC〉 | x5 ⇒ 〈x4,xB〉 | x6 ⇒ 〈x5,xA〉 | x7 ⇒ 〈x6,x9〉
288 | x8 ⇒ 〈x7,x8〉 | x9 ⇒ 〈x8,x7〉 | xA ⇒ 〈x9,x6〉 | xB ⇒ 〈xA,x5〉
289 | xC ⇒ 〈xB,x4〉 | xD ⇒ 〈xC,x3〉 | xE ⇒ 〈xD,x2〉 | xF ⇒ 〈xE,x1〉 ]
292 (* correzione per somma su BCD *)
293 (* input: halfcarry,carry,X(BCD+BCD) *)
294 (* output: X',carry' *)
297 match lt_b8 X 〈x9,xA〉 with
300 (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
301 [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
303 let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
305 | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
306 let X'' ≝ match c with
307 [ true ⇒ plus_b8_d_d X' 〈x6,x0〉
312 (* X' = [X:0x9A-0xFF]
313 [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
314 [(b16l X):0xA-0xF] X + 0x6 + 0x60 *)
316 let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
318 | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
319 let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in
323 (* iteratore sui byte *)
324 ndefinition forall_byte8 ≝
326 forall_exadecim (λbh.
327 forall_exadecim (λbl.
328 P (mk_byte8 bh bl))).