helm/software/matita/contribs/assembly/freescale/word32.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 (*                                                                        *)
  17 (* Sviluppato da:                                                         *)
  18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  19 (*                                                                        *)
  20 (* ********************************************************************** *)
  21
  22 include "freescale/word16.ma".
  23
  24 (* *********************** *)
  25 (* DEFINIZIONE DELLE DWORD *)
  26 (* *********************** *)
  27
  28 record word32 : Type ≝
  29  {
  30  w32h: word16;
  31  w32l: word16
  32  }.
  33
  34 (* \langle \rangle *)
  35 notation "〈x.y〉" non associative with precedence 80
  36  for @{ 'mk_word32 $x $y }.
  37 interpretation "mk_word32" 'mk_word32 x y = (mk_word32 x y).
  38
  39 (* operatore = *)
  40 definition eq_w32 ≝ λw1,w2.(eq_w16 (w32h w1) (w32h w2)) ⊗ (eq_w16 (w32l w1) (w32l w2)).
  41
  42 (* operatore < *)
  43 definition lt_w32 ≝
  44 λw1,w2:word32.match lt_w16 (w32h w1) (w32h w2) with
  45  [ true ⇒ true
  46  | false ⇒ match gt_w16 (w32h w1) (w32h w2) with
  47   [ true ⇒ false
  48   | false ⇒ lt_w16 (w32l w1) (w32l w2) ]].
  49
  50 (* operatore ≤ *)
  51 definition le_w32 ≝ λw1,w2:word32.(eq_w32 w1 w2) ⊕ (lt_w32 w1 w2).
  52
  53 (* operatore > *)
  54 definition gt_w32 ≝ λw1,w2:word32.⊖ (le_w32 w1 w2).
  55
  56 (* operatore ≥ *)
  57 definition ge_w32 ≝ λw1,w2:word32.⊖ (lt_w32 w1 w2).
  58
  59 (* operatore and *)
  60 definition and_w32 ≝
  61 λw1,w2:word32.mk_word32 (and_w16 (w32h w1) (w32h w2)) (and_w16 (w32l w1) (w32l w2)).
  62
  63 (* operatore or *)
  64 definition or_w32 ≝
  65 λw1,w2:word32.mk_word32 (or_w16 (w32h w1) (w32h w2)) (or_w16 (w32l w1) (w32l w2)).
  66
  67 (* operatore xor *)
  68 definition xor_w32 ≝
  69 λw1,w2:word32.mk_word32 (xor_w16 (w32h w1) (w32h w2)) (xor_w16 (w32l w1) (w32l w2)).
  70
  71 (* operatore rotazione destra con carry *)
  72 definition rcr_w32 ≝
  73 λw:word32.λc:bool.match rcr_w16 (w32h w) c with
  74  [ pair wh' c' ⇒ match rcr_w16 (w32l w) c' with
  75   [ pair wl' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]].
  76
  77 (* operatore shift destro *)
  78 definition shr_w32 ≝
  79 λw:word32.match rcr_w16 (w32h w) false with
  80  [ pair wh' c' ⇒ match rcr_w16 (w32l w) c' with
  81   [ pair wl' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]].
  82
  83 (* operatore rotazione destra *)
  84 definition ror_w32 ≝
  85 λw:word32.match rcr_w16 (w32h w) false with
  86  [ pair wh' c' ⇒ match rcr_w16 (w32l w) c' with
  87   [ pair wl' c'' ⇒ match c'' with
  88    [ true ⇒ mk_word32 (or_w16 (mk_word16 (mk_byte8 x8 x0) (mk_byte8 x0 x0)) wh') wl'
  89    | false ⇒ mk_word32 wh' wl' ]]].
  90
  91 (* operatore rotazione destra n-volte *)
  92 let rec ror_w32_n (w:word32) (n:nat) on n ≝
  93  match n with
  94   [ O ⇒ w
  95   | S n' ⇒ ror_w32_n (ror_w32 w) n' ].
  96
  97 (* operatore rotazione sinistra con carry *)
  98 definition rcl_w32 ≝
  99 λw:word32.λc:bool.match rcl_w16 (w32l w) c with
 100  [ pair wl' c' ⇒ match rcl_w16 (w32h w) c' with
 101   [ pair wh' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]].
 102
 103 (* operatore shift sinistro *)
 104 definition shl_w32 ≝
 105 λw:word32.match rcl_w16 (w32l w) false with
 106  [ pair wl' c' ⇒ match rcl_w16 (w32h w) c' with
 107   [ pair wh' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]].
 108
 109 (* operatore rotazione sinistra *)
 110 definition rol_w32 ≝
 111 λw:word32.match rcl_w16 (w32l w) false with
 112  [ pair wl' c' ⇒ match rcl_w16 (w32h w) c' with
 113   [ pair wh' c'' ⇒ match c'' with
 114    [ true ⇒ mk_word32 wh' (or_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x1)) wl')
 115    | false ⇒ mk_word32 wh' wl' ]]].
 116
 117 (* operatore rotazione sinistra n-volte *)
 118 let rec rol_w32_n (w:word32) (n:nat) on n ≝
 119  match n with
 120   [ O ⇒ w
 121   | S n' ⇒ rol_w32_n (rol_w32 w) n' ].
 122
 123 (* operatore not/complemento a 1 *)
 124 definition not_w32 ≝
 125 λw:word32.mk_word32 (not_w16 (w32h w)) (not_w16 (w32l w)).
 126
 127 (* operatore somma con carry *)
 128 definition plus_w32 ≝
 129 λw1,w2:word32.λc:bool.
 130  match plus_w16 (w32l w1) (w32l w2) c with
 131   [ pair l c' ⇒ match plus_w16 (w32h w1) (w32h w2) c' with
 132    [ pair h c'' ⇒ pair ?? (mk_word32 h l) c'' ]].
 133
 134 (* operatore somma senza carry *)
 135 definition plus_w32nc ≝
 136 λw1,w2:word32.fst ?? (plus_w32 w1 w2 false).
 137
 138 (* operatore carry della somma *)
 139 definition plus_w32c ≝
 140 λw1,w2:word32.snd ?? (plus_w32 w1 w2 false).
 141
 142 (* operatore Most Significant Bit *)
 143 definition MSB_w32 ≝ λw:word32.eq_ex x8 (and_ex x8 (b8h (w16h (w32h w)))).
 144
 145 (* word → naturali *)
 146 definition nat_of_word32 ≝ λw:word32. (256 * 256 * (w32h w)) + (nat_of_word16 (w32l w)).
 147
 148 coercion nat_of_word32.
 149
 150 (* naturali → word *)
 151 definition word32_of_nat ≝
 152  λn.mk_word32 (word16_of_nat (n / (256*256))) (word16_of_nat n).
 153
 154 (* operatore predecessore *)
 155 definition pred_w32 ≝
 156 λw:word32.match eq_w16 (w32l w) (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) with
 157  [ true ⇒ mk_word32 (pred_w16 (w32h w)) (pred_w16 (w32l w))
 158  | false ⇒ mk_word32 (w32h w) (pred_w16 (w32l w)) ].
 159
 160 (* operatore successore *)
 161 definition succ_w32 ≝
 162 λw:word32.match eq_w16 (w32l w) (mk_word16 (mk_byte8 xF xF) (mk_byte8 xF xF)) with
 163  [ true ⇒ mk_word32 (succ_w16 (w32h w)) (succ_w16 (w32l w))
 164  | false ⇒ mk_word32 (w32h w) (succ_w16 (w32l w)) ].
 165
 166 (* operatore neg/complemento a 2 *)
 167 definition compl_w32 ≝
 168 λw:word32.match MSB_w32 w with
 169  [ true ⇒ succ_w32 (not_w32 w)
 170  | false ⇒ not_w32 (pred_w32 w) ].
 171
 172 (*
 173    operatore moltiplicazione senza segno: b*b=[0x00000000,0xFFFE0001]
 174    ... in pratica (〈a:b〉*〈c:d〉) = (a*c)<<16+(a*d)<<8+(b*c)<<8+(b*d)
 175 *)
 176 definition mul_w16 ≝
 177 λb1,b2:word16.match b1 with
 178 [ mk_word16 b1h b1l ⇒ match b2 with
 179 [ mk_word16 b2h b2l ⇒ match mul_b8 b1l b2l with
 180 [ mk_word16 t1_h t1_l ⇒ match mul_b8 b1h b2l with
 181 [ mk_word16 t2_h t2_l ⇒ match mul_b8 b2h b1l with
 182 [ mk_word16 t3_h t3_l ⇒ match mul_b8 b1h b2h with
 183 [ mk_word16 t4_h t4_l ⇒
 184  plus_w32nc
 185   (plus_w32nc
 186    (plus_w32nc 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉) 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉
 187 ]]]]]].
 188
 189 (* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
 190 definition div_w16 ≝
 191 λw:word32.λb:word16.match eq_w16 b 〈〈x0,x0〉:〈x0,x0〉〉 with
 192 (*
 193    la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
 194 *)
 195  [ true ⇒ tripleT ??? 〈〈xF,xF〉:〈xF,xF〉〉 (w32l w) true
 196  | false ⇒ match eq_w32 w 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 with
 197 (* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
 198   [ true ⇒ tripleT ??? 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 false
 199 (* 1) e' una divisione sensata che produrra' overflow/risultato *)
 200 (* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *)
 201 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
 202 (* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
 203 (*    puo' essere sottratto al dividendo *)
 204   | false ⇒ let rec aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:nat) on c ≝
 205   let w' ≝ plus_w32nc divd (compl_w32 divs) in
 206    match c with
 207    [ O ⇒ match le_w32 divs divd with
 208     [ true ⇒ tripleT ??? (or_w16 molt q) (w32l w') (⊖ (eq_w16 (w32h w') 〈〈x0,x0〉:〈x0,x0〉〉))
 209     | false ⇒ tripleT ??? q (w32l divd) (⊖ (eq_w16 (w32h divd) 〈〈x0,x0〉:〈x0,x0〉〉)) ]
 210    | S c' ⇒ match le_w32 divs divd with
 211     [ true ⇒ aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) c'
 212     | false ⇒ aux divd (ror_w32 divs) (ror_w16 molt) q c' ]]
 213   in aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 15) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 15 ]].
 214
 215 (* operatore x in [inf,sup] *)
 216 definition in_range ≝
 217 λx,inf,sup:word32.(le_w32 inf sup) ⊗ (ge_w32 x inf) ⊗ (le_w32 x sup).
 218
 219 (* iteratore sulle word *)
 220 definition forall_word32 ≝
 221  λP.
 222   forall_word16 (λbh.
 223   forall_word16 (λbl.
 224    P (mk_word32 bh bl ))).