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