]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly2/emulator/read_write/IP2022_fetch.ma
mod change (-x)
[helm.git] / helm / software / matita / contribs / ng_assembly2 / emulator / read_write / IP2022_fetch.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/read_write/fetch_base.ma".
24 include "emulator/status/status.ma".
25
26 (* PC word aligned *)
27 (* PC < 0x8000 → segmento 1 program ram *)
28 (*else         → segmento 2 program flash *)
29 ndefinition IP2022_pc_flashtest ≝
30 λpc:word16.getMSBc ? pc.
31
32 ndefinition IP2022_pc_translation ≝
33 λpc:word16.match shlc ? pc with
34  [ pair msb pc' ⇒ pair …
35   match msb with [ true ⇒ o2 | false ⇒ o1 ] pc' ].
36
37 (* opcode a byte o 0x00 + byte : IP2022 *)
38 (* opcode + operando a dimensione fissa 16bit *)
39 ndefinition IP2022_fetch_byte_or_word ≝
40 λm,t.λs:any_status m t.λpc:word16.
41  match mem_read t (mem_desc … s) (chk_desc … s)
42                 (fst … (IP2022_pc_translation pc))
43                 (snd … (IP2022_pc_translation pc)) with
44   [ None ⇒ FetchERR ? ILL_FETCH_AD
45   | Some bh ⇒ match eqc ? bh 〈x0,x0〉 with
46    [ true ⇒ match mem_read t (mem_desc … s) (chk_desc … s)
47                              (fst … (IP2022_pc_translation pc))
48                              (succc ? (snd … (IP2022_pc_translation pc))) with
49     [ None ⇒ FetchERR ? ILL_FETCH_AD
50     | Some bl ⇒ fetch_word_aux m (succc ? pc) 〈bh:bl〉
51     ]
52    | false ⇒ fetch_byte_aux m (succc ? pc) bh
53    ]
54   ].