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 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "emulator/read_write/fetch_base.ma".
24 include "emulator/status/status.ma".
27 (* PC < 0x8000 → segmento 1 program ram *)
28 (*else → segmento 2 program flash *)
29 ndefinition IP2022_pc_flashtest ≝
30 λpc:word16.getMSBc ? pc.
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' ].
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〉
52 | false ⇒ fetch_byte_aux m (succc ? pc) bh