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 *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "freescale_tests/micro_tests_tools.ma".
24 include "freescale/multivm.ma".
25 include "freescale/status_lemmas.ma".
27 (* ****************************************** *)
28 (* MICRO TEST DI CORRETTEZZA DELLE ISTRUZIONI *)
29 (* ****************************************** *)
31 (* ************************ *)
32 (* TEST SU GRANULARITA' BIT *)
33 (* ************************ *)
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)
41 (* creazione del processore+caricamento+impostazione registri *)
42 ndefinition mTest_bits_status ≝
46 setweak_n_flag HCS08 t (* N<-1 *)
47 (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *)
48 (start_of_mcu_version_HCS08
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 *)
62 (* dimostrazione senza svolgimento degli stati, immediata *)
63 nlemma ok_mTest_bits_MEM_BITS_full :
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〉)).
72 (* NB: la memoria e' cambiata e bisogna applicare eq_status *)
73 nlemma ok_mTest_bits_MEM_FUNC_full :
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.
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 ⊢ (? ? ? %);
89 nlemma ok_mTest_bits_MEM_TREE_full :
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.
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 ⊢ (? ? ? %);