helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests10.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 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale_tests/micro_tests_tools.ma".
  24 include "freescale/multivm.ma".
  25 include "freescale/status_lemmas.ma".
  26
  27 (* ****************************************** *)
  28 (* MICRO TEST DI CORRETTEZZA DELLE ISTRUZIONI *)
  29 (* ****************************************** *)
  30
  31 (* ************************ *)
  32 (* TEST SU GRANULARITA' BIT *)
  33 (* ************************ *)
  34
  35 ndefinition mTest_bits_source ≝ let m ≝ HCS08 in source_to_byte8 m (
  36 (* BEFORE: va a testare [0x0070]=0x00 *)
  37 (* [0x1860] 4clk *) (compile m ? MOV (maIMM1_to_DIR1 〈xF,xF〉 〈x7,x0〉) I)
  38 (* [0x1863] *)
  39 ).
  40
  41 (* creazione del processore+caricamento+impostazione registri *)
  42 ndefinition mTest_bits_status ≝
  43 λt:memory_impl.
  44 λsub:oct.
  45 λb:byte8.
  46  setweak_n_flag HCS08 t (* N<-1 *)
  47   (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *)
  48    (start_of_mcu_version_HCS08
  49     MC9S08AW60 t
  50     (load_from_source_at t
  51      (load_from_source_at t (zero_memory t) (* carica b in RAM:mTest_HCS08_RAM *)
  52        mTest_bits_source mTest_HCS08_prog) (* carica source in ROM:mTest_HCS08_prog *)
  53       [ b ] mTest_HCS08_RAM)
  54     (check_update_bit t (* setta mTest_HCS08_RAM,o come ROM *)
  55      (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08AW60) t)
  56      mTest_HCS08_RAM sub MEM_READ_ONLY)
  57     (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
  58     false false false false false false) (* non deterministici tutti a 0 *)
  59    mTest_HCS08_prog)
  60   true.
  61
  62 (* dimostrazione senza svolgimento degli stati, immediata *)
  63 nlemma ok_mTest_bits_MEM_BITS_full :
  64  ∀sub:oct.
  65  execute HCS08 MEM_BITS (TickOK ? (mTest_bits_status MEM_BITS sub 〈x0,x0〉)) nat4 =
  66  TickOK ? (set_pc_reg HCS08 MEM_BITS (mTest_bits_status MEM_BITS sub (byte8_of_bits (setn_array8T sub ? (bits_of_byte8 〈xF,xF〉) false))) (* nuovo PC *)
  67            (mk_word16 〈x1,x8〉 〈x6,x3〉)).
  68  #sub; nelim sub;
  69  napply refl_eq.
  70 nqed.
  71
  72 (* NB: la memoria e' cambiata e bisogna applicare eq_status *)
  73 nlemma ok_mTest_bits_MEM_FUNC_full :
  74 ∀sub:oct.
  75  eq_anystatus HCS08 MEM_FUNC
  76   (match execute HCS08 MEM_FUNC (TickOK ? (mTest_bits_status MEM_FUNC sub 〈x0,x0〉)) nat4
  77    with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
  78   (set_pc_reg HCS08 MEM_FUNC (mTest_bits_status MEM_FUNC sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉)
  79   [ 〈〈x0,x0〉:〈x7,x0〉〉 ] = true.
  80  #sub; nelim sub;
  81  napply (eq_to_eqanystatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ] HCS08 MEM_FUNC
  82         (match execute HCS08 MEM_FUNC (TickOK ? (mTest_bits_status MEM_FUNC sub 〈x0,x0〉)) nat4
  83          with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
  84         (set_pc_reg HCS08 MEM_FUNC (mTest_bits_status MEM_FUNC sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉));
  85  nnormalize in ⊢ (? ? ? %);
  86  napply refl_eq.
  87 nqed.
  88
  89 nlemma ok_mTest_bits_MEM_TREE_full :
  90 ∀sub:oct.
  91  eq_anystatus HCS08 MEM_TREE
  92   (match execute HCS08 MEM_TREE (TickOK ? (mTest_bits_status MEM_TREE sub 〈x0,x0〉)) nat4
  93    with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
  94   (set_pc_reg HCS08 MEM_TREE (mTest_bits_status MEM_TREE sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉)
  95   [ 〈〈x0,x0〉:〈x7,x0〉〉 ] = true.
  96  #sub; nelim sub;
  97  napply (eq_to_eqanystatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ] HCS08 MEM_TREE
  98         (match execute HCS08 MEM_TREE (TickOK ? (mTest_bits_status MEM_TREE sub 〈x0,x0〉)) nat4
  99          with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
 100         (set_pc_reg HCS08 MEM_TREE (mTest_bits_status MEM_TREE sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉));
 101  nnormalize in ⊢ (? ? ? %);
 102  napply refl_eq.
 103 nqed.