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".
26 (* opcode a byte : HC05 / RS08 *)
27 (* caricamento solo da segmento 0 *)
28 ndefinition fetch_byte ≝
29 λm,t.λs:any_status m t.λpc:word16.
30 match mem_read t (mem_desc … s) (chk_desc … s) o0 pc with
31 [ None ⇒ FetchERR ? ILL_FETCH_AD
32 | Some bh ⇒ fetch_byte_aux m (succc ? pc) bh ].
34 (* opcode a byte o 0x9E + byte : HC08 / HCS08 *)
35 (* caricamento solo da segmento 0 *)
36 ndefinition Freescale_fetch_byte_or_word ≝
37 λm,t.λs:any_status m t.λpc:word16.
38 match mem_read t (mem_desc … s) (chk_desc … s) o0 pc with
39 [ None ⇒ FetchERR ? ILL_FETCH_AD
40 | Some bh ⇒ match eqc ? bh 〈x9,xE〉 with
41 [ true ⇒ match mem_read t (mem_desc … s) (chk_desc … s) o0 (succc ? pc) with
42 [ None ⇒ FetchERR ? ILL_FETCH_AD
43 | Some bl ⇒ fetch_word_aux m (succc ? (succc ? pc)) 〈bh:bl〉
45 | false ⇒ fetch_byte_aux m (succc ? pc) bh