helm/software/matita/contribs/ng_assembly/opcodes/opcode.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 "opcodes/HC05_opcode_base.ma".
  24 include "opcodes/HC08_opcode_base.ma".
  25 include "opcodes/HCS08_opcode_base.ma".
  26 include "opcodes/RS08_opcode_base.ma".
  27 include "opcodes/byte_or_word.ma".
  28 include "common/list.ma".
  29
  30 (* ********************************************** *)
  31 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  32 (* ********************************************** *)
  33
  34 (* enumerazione delle ALU *)
  35 ninductive mcu_type: Type ≝
  36   HC05  : mcu_type
  37 | HC08  : mcu_type
  38 | HCS08 : mcu_type
  39 | RS08  : mcu_type.
  40
  41 ndefinition eq_mcutype ≝
  42 λm1,m2:mcu_type.
  43  match m1 with
  44   [ HC05 ⇒ match m2 with [ HC05 ⇒ true | _ ⇒ false ]
  45   | HC08 ⇒ match m2 with [ HC08 ⇒ true | _ ⇒ false ]
  46   | HCS08 ⇒ match m2 with [ HCS08 ⇒ true | _ ⇒ false ]
  47   | RS08 ⇒ match m2 with [ RS08 ⇒ true | _ ⇒ false ]
  48   ].
  49
  50 ndefinition aux_op_type ≝
  51 λmcu:mcu_type.match mcu with
  52  [ HC05 ⇒ HC05_opcode
  53  | HC08 ⇒ HC08_opcode
  54  | HCS08 ⇒ HCS08_opcode
  55  | RS08 ⇒ RS08_opcode
  56  ].
  57
  58 ndefinition aux_im_type ≝
  59 λmcu:mcu_type.match mcu with
  60  [ HC05 ⇒ HC05_instr_mode
  61  | HC08 ⇒ HC08_instr_mode
  62  | HCS08 ⇒ HCS08_instr_mode
  63  | RS08 ⇒ RS08_instr_mode
  64  ].
  65
  66 ndefinition eq_op ≝
  67 λmcu:mcu_type.
  68  match mcu
  69   return λm.aux_op_type m → aux_op_type m → bool
  70  with
  71   [ HC05 ⇒ eq_HC05_op
  72   | HC08 ⇒ eq_HC08_op
  73   | HCS08 ⇒ eq_HCS08_op
  74   | RS08 ⇒ eq_RS08_op
  75   ].
  76
  77 ndefinition eq_im ≝
  78 λmcu:mcu_type.
  79  match mcu
  80   return λm.aux_im_type m → aux_im_type m → bool
  81  with
  82   [ HC05 ⇒ eq_HC05_im
  83   | HC08 ⇒ eq_HC08_im
  84   | HCS08 ⇒ eq_HCS08_im
  85   | RS08 ⇒ eq_RS08_im
  86   ].
  87
  88 ndefinition forall_op ≝
  89 λmcu:mcu_type.
  90  match mcu
  91   return λm.(aux_op_type m → bool) → bool
  92  with
  93   [ HC05 ⇒ forall_HC05_op
  94   | HC08 ⇒ forall_HC08_op
  95   | HCS08 ⇒ forall_HCS08_op
  96   | RS08 ⇒ forall_RS08_op
  97   ].
  98
  99 ndefinition forall_im ≝
 100 λmcu:mcu_type.
 101  match mcu
 102   return λm.(aux_im_type m → bool) → bool
 103  with
 104   [ HC05 ⇒ forall_HC05_im
 105   | HC08 ⇒ forall_HC08_im
 106   | HCS08 ⇒ forall_HCS08_im
 107   | RS08 ⇒ forall_RS08_im
 108   ].
 109
 110 (* ********************************************* *)
 111 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
 112 (* ********************************************* *)
 113
 114 ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_op_type mcu) (aux_im_type mcu) byte8_or_word16 byte8.
 115
 116 (* su tutta la lista quante volte compare il byte *)
 117 nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝
 118  match l with
 119   [ nil ⇒ c
 120   | cons hd tl ⇒ match thd4T … hd with
 121    [ Byte b' ⇒ match eq_b8 b b' with
 122     [ true ⇒ get_byte_count m b (succ_w16 c) tl
 123     | false ⇒ get_byte_count m b c tl
 124     ]
 125    | Word _ ⇒ get_byte_count m b c tl
 126    ]
 127   ].
 128
 129 (* su tutta la lista quante volte compare la word (0x9E+byte) *)
 130 nlet rec get_word_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝
 131  match l with
 132   [ nil ⇒ c
 133   | cons hd tl ⇒ match thd4T … hd with
 134    [ Byte _ ⇒ get_word_count m b c tl
 135    | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
 136     [ true ⇒ get_word_count m b (succ_w16 c) tl
 137     | false ⇒ get_word_count m b c tl
 138     ]
 139    ]
 140   ].
 141
 142 (* su tutta la lista quante volte compare lo pseudocodice *)
 143 nlet rec get_pseudo_count (m:mcu_type) (o:aux_op_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
 144  match l with
 145   [ nil ⇒ c
 146   | cons hd tl ⇒ match eq_op m o (fst4T … hd) with
 147    [ true ⇒ get_pseudo_count m o (succ_w16 c) tl
 148    | false ⇒ get_pseudo_count m o c tl
 149    ]
 150   ].
 151
 152 (* su tutta la lista quante volte compare la modalita' *)
 153 nlet rec get_mode_count (m:mcu_type) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
 154  match l with
 155   [ nil ⇒ c
 156   | cons hd tl ⇒ match eq_im m i (snd4T … hd) with
 157    [ true ⇒ get_mode_count m i (succ_w16 c) tl
 158    | false ⇒ get_mode_count m i c tl
 159    ]
 160   ].
 161
 162 (* b e' non implementato? *)
 163 nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
 164  match l with
 165   [ nil ⇒ false
 166   | cons hd tl ⇒ match eq_b8 b hd with
 167    [ true ⇒ true
 168    | false ⇒ test_not_impl_byte b tl
 169    ]
 170   ].
 171
 172 (* o e' non implementato? *)
 173 nlet rec test_not_impl_pseudo (m:mcu_type) (o:aux_op_type m) (l:list (aux_op_type m)) on l ≝
 174  match l with
 175   [ nil ⇒ false
 176   | cons hd tl ⇒ match eq_op m o hd with
 177    [ true ⇒ true
 178    | false ⇒ test_not_impl_pseudo m o tl
 179    ]
 180   ].
 181
 182 (* i e' non implementato? *)
 183 nlet rec test_not_impl_mode (m:mcu_type) (i:aux_im_type m) (l:list (aux_im_type m)) on l ≝
 184  match l with
 185   [ nil ⇒ false
 186   | cons hd tl ⇒ match eq_im m i hd with
 187    [ true ⇒ true
 188    | false ⇒ test_not_impl_mode m i tl
 189    ]
 190   ].
 191
 192 (* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
 193 nlet rec get_OpIm_count (m:mcu_type) (o:aux_op_type m) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
 194  match l with
 195   [ nil ⇒ c
 196   | cons hd tl ⇒
 197    match (eq_op m o (fst4T … hd)) ⊗
 198          (eq_im m i (snd4T … hd)) with
 199     [ true ⇒ get_OpIm_count m o i (succ_w16 c) tl
 200     | false ⇒ get_OpIm_count m o i c tl
 201     ]
 202   ].