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/status/status_setter.ma".
29 (* NB: fare molta attenzione alle note sulle combinazioni possibili perche'
30 il comportamento della memoria nell'RS08 e' strano e ci sono
31 precise condizioni che impediscono una semantica circolare dell'accesso
32 (divergenza=assenza di definizione) *)
33 ndefinition RS08_memory_filter_read_aux ≝
34 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
35 λT:Type.λfREG:byte8 → option T.λfMEM:word16 → option T.
36 (* possibili accessi al registro X
38 2) addr=000E (X =0F): indiretto
39 3) addr=00CF (PS=00): paging
40 [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
41 non si possono combinare due effetti contemporaneamente!
42 per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni *)
43 match (eqc ? addr 〈〈x0,x0〉:〈x0,xF〉〉) ⊕
44 (eqc ? addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eqc ? (x_map_RS08 (alu … s)) 〈x0,xF〉) ⊕
45 (eqc ? addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eqc ? (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
46 [ true ⇒ fREG (x_map_RS08 (alu … s))
48 (* possibili accessi al registro PS
50 2) addr=000E (X =1F): indiretto
51 3) addr=00DF (PS=00): paging *)
52 match (eqc ? addr 〈〈x0,x0〉:〈x1,xF〉〉) ⊕
53 (eqc ? addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eqc ? (x_map_RS08 (alu … s)) 〈x1,xF〉) ⊕
54 (eqc ? addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eqc ? (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
55 [ true ⇒ fREG (ps_map_RS08 (alu … s))
57 (* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
58 altrimenti sarebbero 2 indirezioni *)
59 match eqc ? addr 〈〈x0,x0〉:〈x0,xE〉〉 with
60 [ true ⇒ fMEM (extu_w16 (x_map_RS08 (alu … s)))
62 (* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *)
63 match inrangec ? addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
64 [ true ⇒ fMEM (orc ? (rorc ? (rorc ? 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
65 (andc ? addr 〈〈x0,x0〉:〈x3,xF〉〉))
67 | false ⇒ fMEM addr ]]]].
69 (* lettura RS08 di un byte *)
70 ndefinition RS08_memory_filter_read ≝
71 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
72 RS08_memory_filter_read_aux t s addr byte8
74 (mem_read t (mem_desc … s) (chk_desc … s) o0).
76 (* lettura RS08 di un bit *)
77 ndefinition RS08_memory_filter_read_bit ≝
78 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.
79 RS08_memory_filter_read_aux t s addr bool
80 (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
81 (λa.mem_read_bit t (mem_desc … s) (chk_desc … s) o0 a sub).
87 ndefinition RS08_memory_filter_write_aux ≝
88 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
89 λfREG:byte8 → byte8.λfMEM:word16 → option (aux_mem_type t).
90 (* possibili accessi al registro X
92 2) addr=000E (X =0F): indiretto
93 3) addr=00CF (PS=00): paging
94 [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
95 non si possono combinare due effetti contemporaneamente!
96 per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni *)
97 match (eqc ? addr 〈〈x0,x0〉:〈x0,xF〉〉) ⊕
98 (eqc ? addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eqc ? (x_map_RS08 (alu … s)) 〈x0,xF〉) ⊕
99 (eqc ? addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eqc ? (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
100 [ true ⇒ set_x_map … s (fREG (x_map_RS08 (alu … s)))
102 (* possibili accessi al registro PS
103 1) addr=001F: diretto
104 2) addr=000E (X =1F): indiretto
105 3) addr=00DF (PS=00): paging *)
106 match (eqc ? addr 〈〈x0,x0〉:〈x1,xF〉〉) ⊕
107 (eqc ? addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eqc ? (x_map_RS08 (alu … s)) 〈x1,xF〉) ⊕
108 (eqc ? addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eqc ? (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
109 [ true ⇒ set_ps_map … s (fREG (x_map_RS08 (alu … s)))
111 (* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
112 altrimenti sarebbero 2 indirezioni *)
113 match eqc ? addr 〈〈x0,x0〉:〈x0,xE〉〉 with
114 [ true ⇒ opt_map … (fMEM (extu_w16 (x_map_RS08 (alu … s))))
115 (λmem'.Some ? (set_mem_desc … s mem'))
117 (* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *)
118 match inrangec ? addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
119 [ true ⇒ opt_map … (fMEM (orc ? (rorc ? (rorc ? 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
120 (andc ? addr 〈〈x0,x0〉:〈x3,xF〉〉)))
121 (λmem'.Some ? (set_mem_desc … s mem'))
122 (* accesso normale *)
123 | false ⇒ opt_map … (fMEM addr)
124 (λmem'.Some ? (set_mem_desc … s mem')) ]]]].
126 (* scrittura RS08 di un byte *)
127 ndefinition RS08_memory_filter_write ≝
128 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λval:byte8.
129 RS08_memory_filter_write_aux t s addr
131 (λa.mem_update t (mem_desc … s) (chk_desc … s) o0 a val).
133 (* scrittura RS08 di un bit *)
134 ndefinition RS08_memory_filter_write_bit ≝
135 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
136 RS08_memory_filter_write_aux t s addr
137 (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
138 (λa.mem_update_bit t (mem_desc … s) (chk_desc … s) o0 a sub val).