matita/matita/contribs/ng_assembly/emulator/read_write/RS08_read_write.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/status/status_setter.ma".
  24
  25 (* **** *)
  26 (* READ *)
  27 (* **** *)
  28
  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:word32.
  35 λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option T.
  36 (* solo indirizzi nei 64Kb *)
  37  match gt_w16 (cnH ? addr) 〈〈x0,x0〉:〈x0,x0〉〉 with
  38   [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) addr
  39   | false ⇒
  40 (* possibili accessi al registro X
  41    1) addr=000F: diretto
  42    2) addr=000E (X =0F): indiretto
  43    3) addr=00CF (PS=00): paging
  44    [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
  45    non si possono combinare due effetti contemporaneamente!
  46    per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni *)
  47  match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
  48        (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x0,xF〉) ⊕
  49        (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
  50   [ true ⇒ fREG (x_map_RS08 (alu … s))
  51   | false ⇒
  52 (* possibili accessi al registro PS
  53    1) addr=001F: diretto
  54    2) addr=000E (X =1F): indiretto
  55    3) addr=00DF (PS=00): paging *)
  56  match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
  57        (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x1,xF〉) ⊕
  58        (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
  59   [ true ⇒ fREG (ps_map_RS08 (alu … s))
  60   | false ⇒
  61 (* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
  62    altrimenti sarebbero 2 indirezioni *)
  63  match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 with
  64   [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) (ext_word32 〈〈x0,x0〉:(x_map_RS08 (alu … s))〉)
  65   | false ⇒
  66 (* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *)
  67  match inrange_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
  68   [ true ⇒ fMEM (mem_desc … s) (chk_desc … s)
  69                 (ext_word32 (or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
  70                                     (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉)))
  71 (* accesso normale *)
  72   | false ⇒ fMEM (mem_desc … s) (chk_desc … s) addr ]]]]].
  73
  74 (* lettura RS08 di un byte *)
  75 ndefinition RS08_memory_filter_read ≝
  76 λt:memory_impl.λs:any_status RS08 t.λaddr:word32.
  77  RS08_memory_filter_read_aux t s addr byte8
  78   (λb.Some byte8 b)
  79   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read t m c a).
  80
  81 (* lettura RS08 di un bit *)
  82 ndefinition RS08_memory_filter_read_bit ≝
  83 λt:memory_impl.λs:any_status RS08 t.λaddr:word32.λsub:oct.
  84  RS08_memory_filter_read_aux t s addr bool
  85   (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
  86   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read_bit t m c a sub).
  87
  88 (* ***** *)
  89 (* WRITE *)
  90 (* ***** *)
  91
  92 ndefinition RS08_memory_filter_write_aux ≝
  93 λt:memory_impl.λs:any_status RS08 t.λaddr:word32.
  94 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option (aux_mem_type t).
  95 (* solo indirizzi nei 64Kb *)
  96  match gt_w16 (cnH ? addr) 〈〈x0,x0〉:〈x0,x0〉〉 with
  97   [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)
  98             (λmem'.Some ? (set_mem_desc … s mem'))
  99   | false ⇒
 100 (* possibili accessi al registro X
 101    1) addr=000F: diretto
 102    2) addr=000E (X =0F): indiretto
 103    3) addr=00CF (PS=00): paging
 104    [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
 105    non si possono combinare due effetti contemporaneamente!
 106    per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni *)
 107  match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
 108        (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x0,xF〉) ⊕
 109        (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
 110   [ true ⇒ set_x_map … s (fREG (x_map_RS08 (alu … s)))
 111   | false ⇒
 112 (* possibili accessi al registro PS
 113    1) addr=001F: diretto
 114    2) addr=000E (X =1F): indiretto
 115    3) addr=00DF (PS=00): paging *)
 116  match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
 117        (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x1,xF〉) ⊕
 118        (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
 119   [ true ⇒ set_ps_map … s (fREG (x_map_RS08 (alu … s)))
 120   | false ⇒
 121 (* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
 122    altrimenti sarebbero 2 indirezioni *)
 123  match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 with
 124   [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) (ext_word32 〈〈x0,x0〉:(x_map_RS08 (alu … s))〉))
 125             (λmem'.Some ? (set_mem_desc … s mem'))
 126   | false ⇒
 127 (* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *)
 128  match inrange_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
 129   [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s)
 130                            (ext_word32 (or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
 131                                                (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉))))
 132             (λmem'.Some ? (set_mem_desc … s mem'))
 133 (* accesso normale *)
 134   | false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)
 135              (λmem'.Some ? (set_mem_desc … s mem')) ]]]]].
 136
 137 (* scrittura RS08 di un byte *)
 138 ndefinition RS08_memory_filter_write ≝
 139 λt:memory_impl.λs:any_status RS08 t.λaddr:word32.λval:byte8.
 140  RS08_memory_filter_write_aux t s addr
 141   (λb.val)
 142   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update t m c a val).
 143
 144 (* scrittura RS08 di un bit *)
 145 ndefinition RS08_memory_filter_write_bit ≝
 146 λt:memory_impl.λs:any_status RS08 t.λaddr:word32.λsub:oct.λval:bool.
 147  RS08_memory_filter_write_aux t s addr
 148   (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
 149   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update_bit t m c a sub val).