(* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
altrimenti sarebbero 2 indirezioni *)
match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 with
- [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:(x_map_RS08 (alu … s))〉〉
+ [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) (ext_word32 〈〈x0,x0〉:(x_map_RS08 (alu … s))〉)
| false ⇒
(* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *)
match inrange_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
[ true ⇒ fMEM (mem_desc … s) (chk_desc … s)
- (〈〈〈x0,x0〉:〈x0,x0〉〉.(or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
- (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉))〉)
+ (ext_word32 (or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
+ (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉)))
(* accesso normale *)
| false ⇒ fMEM (mem_desc … s) (chk_desc … s) addr ]]]]].
(* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
altrimenti sarebbero 2 indirezioni *)
match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 with
- [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:(x_map_RS08 (alu … s))〉〉)
+ [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) (ext_word32 〈〈x0,x0〉:(x_map_RS08 (alu … s))〉))
(λmem'.Some ? (set_mem_desc … s mem'))
| false ⇒
(* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *)
match inrange_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
[ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s)
- (〈〈〈x0,x0〉:〈x0,x0〉〉.(or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
- (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉))〉))
+ (ext_word32 (or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
+ (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉))))
(λmem'.Some ? (set_mem_desc … s mem'))
(* accesso normale *)
| false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)