helm/software/matita/contribs/ng_assembly/freescale/model.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 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/status.ma".
  24
  25 (* *********************************** *)
  26 (* IMPOSTAZIONI SPECIFICHE DEI MODELLI *)
  27 (* *********************************** *)
  28
  29 (* modelli di HC05 *)
  30 ninductive HC05_mcu_model : Type ≝
  31   MC68HC05J5A: HC05_mcu_model
  32   (*..*).
  33
  34 (* modelli di HC08 *)
  35 ninductive HC08_mcu_model : Type ≝
  36   MC68HC08AB16A: HC08_mcu_model
  37   (*..*).
  38
  39 (* modelli di HCS08 *)
  40 ninductive HCS08_mcu_model : Type ≝
  41   MC9S08AW60 : HCS08_mcu_model
  42 | MC9S08GB60 : HCS08_mcu_model
  43   (*..*).
  44
  45 (* modelli di RS08 *)
  46 ninductive RS08_mcu_model : Type ≝
  47   MC9RS08KA1 : RS08_mcu_model
  48 | MC9RS08KA2 : RS08_mcu_model.
  49
  50 (* raggruppamento dei modelli *)
  51 ninductive any_mcu_model : Type ≝
  52   FamilyHC05  : HC05_mcu_model → any_mcu_model
  53 | FamilyHC08  : HC08_mcu_model → any_mcu_model
  54 | FamilyHCS08 : HCS08_mcu_model → any_mcu_model
  55 | FamilyRS08  : RS08_mcu_model → any_mcu_model.
  56
  57 (*
  58 condizioni errore interne alla MCU
  59 (Il programma viene caricato dal produttore in ROM o impostato in EEPROM)
  60 HC05: +illegal address during opcode fetch
  61 HC08: +illegal address duting opcode fetch (ILAD mascherabile)
  62       +illegal opcode (ILOP mascherabile)
  63
  64 (Il programma viene programmato nella FLASH)
  65 HCS08: +illegal address during opcode fetch (ILAD mascherabile)
  66        +illegal opcode (ILOP mascherabile)
  67        +security = accesso a RAM e zone FLASH dichiarate sicure da zone sicure
  68                    da' 0 in lettura e ignore in scrittura, [FLASH]SEC00:SEC01 (1,0)
  69                    corrisponde a OFF, altre ON, disattivabile solo da modalita' sicura se
  70                    opzione [FLASH]KEYEN e' 1 passando chiave a 8byte da modalita' sicura.
  71                    Altrimenti disattivabile solo con FLASH mass erase. Obbiettivo
  72                    e' impedire duplicazione di software di controllo, dato che esiste
  73                    modalita' debugging. A restart viene ricaricata da FLASH impostazione
  74                    sicurezza!
  75 RS08: +illegal address durting opcode fetch (ILAD) mascherabile
  76       +illegal opcode (ILOP mascherabile)
  77       +security = solo la FLASH e' considerata sicura. Stesso meccanismo di HCS08
  78                   ma governato solo da [FLASH]SECD (0) OFF.Una volta attivato l'unica
  79                   disattivazione e' la cancellazione della FLASH.
  80 *)
  81
  82 (* memoria degli HC05 *)
  83 ndefinition memory_type_of_FamilyHC05 ≝
  84 λm:HC05_mcu_model.match m with
  85   [ MC68HC05J5A ⇒
  86    [
  87   (* astraggo molto *)
  88   (* 0x0000-0x001F,0x0FF0: sarebbe memory mapped IO *)
  89
  90      triple … 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 128B RAM+STACK *)
  91    ; triple … 〈〈x0,x3〉:〈x0,x0〉〉 〈〈x0,xC〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 2560B USER ROM *)
  92    ; triple … 〈〈x0,xE〉:〈x0,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 512B INTERNAL ROM *)
  93     ]
  94    (*..*)
  95   ].
  96
  97 (* memoria degli HC08 *)
  98 ndefinition memory_type_of_FamilyHC08 ≝
  99 λm:HC08_mcu_model.match m with
 100   [ MC68HC08AB16A ⇒
 101    [
 102   (* astraggo molto *)
 103   (* 0x0000-0x004F,0xFE00-0xFE01,0xFE03,
 104      0xFE0C-0xFE11,0xFE1A-0xFE1D,0xFE1F: sarebbe memory mapped IO *)
 105   (* 0x0500-0x057F,0xFE02,0xFE04-0xFE07,
 106      0xFE09-0xFE0B,0xFE12-0xFE19,0xFE1E,0xFFC0-0xFFCF : sarebbe reserved *)
 107
 108      triple … 〈〈x0,x0〉:〈x5,x0〉〉 〈〈x0,x2〉:〈x4,xF〉〉 MEM_READ_WRITE (* 512B RAM *)
 109    ; triple … 〈〈x0,x8〉:〈x0,x0〉〉 〈〈x0,x9〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 512B EEPROM *)
 110    ; triple … 〈〈xB,xE〉:〈x0,x0〉〉 〈〈xF,xD〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 16384B ROM *)
 111    ; triple … 〈〈xF,xE〉:〈x2,x0〉〉 〈〈xF,xF〉:〈x5,x2〉〉 MEM_READ_ONLY  (* 307B ROM *)
 112    ; triple … 〈〈xF,xF〉:〈xD,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 48B ROM *) ]
 113    (*..*)
 114   ].
 115
 116 (* memoria degli HCS08 *)
 117 ndefinition memory_type_of_FamilyHCS08 ≝
 118 λm:HCS08_mcu_model.match m with
 119   [ MC9S08AW60 ⇒
 120    [
 121   (* astraggo molto *)
 122   (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *)
 123
 124      triple … 〈〈x0,x0〉:〈x7,x0〉〉 〈〈x0,x8〉:〈x6,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
 125    ; triple … 〈〈x0,x8〉:〈x7,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 3984B FLASH *)
 126    ; triple … 〈〈x1,x8〉:〈x6,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59296B FLASH *) ]
 127   | MC9S08GB60 ⇒
 128    [
 129   (* astraggo molto *)
 130   (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *)
 131
 132      triple … 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
 133    ; triple … 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 1920B FLASH *)
 134    ; triple … 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59348B FLASH *) ]
 135   ].
 136
 137 (* memoria dei RS08 *)
 138 ndefinition memory_type_of_FamilyRS08 ≝
 139 λm:RS08_mcu_model.match m with
 140   [ MC9RS08KA1 ⇒
 141    [
 142      triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *)
 143   (* [000F] e' il registro X *)
 144   (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *)
 145    ; triple … 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *)
 146   (* [001F] e' il registro PAGESEL *)
 147    ; triple … 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *)
 148   (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *)
 149    ; triple … 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *)
 150   (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *)
 151    ; triple … 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *)
 152    ; triple … 〈〈x3,xC〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 1024B FLASH *) ]
 153   | MC9RS08KA2 ⇒
 154    [
 155      triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *)
 156   (* [000F] e' il registro X *)
 157   (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *)
 158    ; triple … 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *)
 159   (* [001F] e' il registro PAGESEL *)
 160    ; triple … 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *)
 161   (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *)
 162    ; triple … 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *)
 163   (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *)
 164    ; triple … 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *)
 165    ; triple … 〈〈x3,x8〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 2048B FLASH *) ]
 166   ].
 167
 168 (* ∀modello.descrizione della memoria installata *)
 169 ndefinition memory_type_of_mcu_version ≝
 170 λmcu:any_mcu_model.match mcu with
 171  [ FamilyHC05  m ⇒ memory_type_of_FamilyHC05 m
 172  | FamilyHC08  m ⇒ memory_type_of_FamilyHC08 m
 173  | FamilyHCS08 m ⇒ memory_type_of_FamilyHCS08 m
 174  | FamilyRS08  m ⇒ memory_type_of_FamilyRS08 m
 175  ].
 176
 177 (* dato un modello costruisce un descrittore a partire dalla lista precedente *)
 178 nlet rec build_memory_type_of_mcu_version_aux t param (result:aux_chk_type t) on param ≝
 179  match param with
 180   [ nil ⇒ result
 181   | cons hd tl ⇒
 182    build_memory_type_of_mcu_version_aux t tl
 183     (check_update_ranged t result (fst3T ??? hd) (snd3T ??? hd) (thd3T ??? hd)) ].
 184
 185 ndefinition build_memory_type_of_mcu_version ≝
 186 λmcu:any_mcu_model.λt:memory_impl.
 187  build_memory_type_of_mcu_version_aux t (memory_type_of_mcu_version mcu) (out_of_bound_memory t).
 188
 189 (* sarebbe programma da caricare/zero_memory, ora test *)
 190 ndefinition memory_of_mcu_version ≝
 191 λmcu:any_mcu_model.λt:memory_impl.match mcu with
 192  [ FamilyHC05 m ⇒ match m with
 193   [ MC68HC05J5A ⇒ zero_memory t
 194     (*..*)
 195   ]
 196  | FamilyHC08 m ⇒ match m with
 197   [ MC68HC08AB16A ⇒ zero_memory t
 198     (*..*)
 199   ]
 200  (* tralascio l'enumerazione dei casi, per ora e' tutto 0 *)
 201  | FamilyHCS08 _ ⇒ zero_memory t
 202  | FamilyRS08 _ ⇒ zero_memory t
 203  ].
 204
 205 (*
 206    parametrizzati i non deterministici rispetto a tutti i valori casuali
 207    che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
 208    l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
 209    (reset V-low), la memoria ed il check puo' essere passata, per esempio da
 210    - (memory_of_mcu_version MC68HC05J5A)
 211    - (build_memory_type_of_mcu_version MC68HC05J5A)
 212 *)
 213 ndefinition start_of_mcu_version_HC05 ≝
 214 λmcu:HC05_mcu_model.λt:memory_impl.
 215 λmem:aux_mem_type t.λchk:aux_chk_type t.
 216 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 217  let build ≝ λspm,spf,pcm:word16.
 218  let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 〈〈xF,xF〉:〈xF,xE〉〉 pcm))
 219                             (mem_read_abs t mem (and_w16 〈〈xF,xF〉:〈xF,xF〉〉 pcm)) in
 220   mk_any_status HC05 t
 221    (mk_alu_HC05
 222     (* acc_low: ? *) ndby1 (* indx_low: ? *) ndby2
 223     (* sp: reset *) (or_w16 (and_w16 〈〈x0,x0〉:〈xF,xF〉〉 spm) spf) spm spf
 224     (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm
 225     (* H: ? *) ndbo1 (* I: reset *) true (* N: ? *) ndbo2
 226     (* Z: ? *) ndbo3 (* C: ? *) ndbo4 (* IRQ: ? *) irqfl)
 227     (* mem *) mem
 228     (* chk *) chk
 229     (* clk: reset *) (None ?) in
 230  match mcu with
 231   [ MC68HC05J5A ⇒ build 〈〈x0,x0〉:〈x3,xF〉〉 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉
 232     (*..*)
 233   ].
 234
 235 ndefinition start_of_mcu_version_HC08 ≝
 236 λmcu:HC08_mcu_model.λt:memory_impl.
 237 λmem:aux_mem_type t.λchk:aux_chk_type t.
 238 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 239  let fetched_pc ≝ mk_word16 (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xE〉〉)
 240                             (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xF〉〉) in
 241   mk_any_status HC08 t
 242    (mk_alu_HC08
 243     (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *)  〈x0,x0〉
 244     (* sp: reset *) 〈〈x0,x0〉:〈xF,xF〉〉 (* pc: reset+fetch *) fetched_pc
 245     (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true
 246     (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl)
 247     (* mem *) mem
 248     (* chk *) chk
 249     (* clk: reset *) (None ?).
 250
 251 ndefinition start_of_mcu_version_HCS08 ≝
 252 λmcu:HCS08_mcu_model.λt:memory_impl.
 253 λmem:aux_mem_type t.λchk:aux_chk_type t.
 254 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 255  let fetched_pc ≝ mk_word16 (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xE〉〉)
 256                             (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xF〉〉) in
 257   mk_any_status HCS08 t
 258    (mk_alu_HC08
 259     (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *)  〈x0,x0〉
 260     (* sp: reset *) 〈〈x0,x0〉:〈xF,xF〉〉 (* pc: reset+fetch *) fetched_pc
 261     (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true
 262     (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl)
 263     (* mem *) mem
 264     (* chk *) chk
 265     (* clk: reset *) (None ?).
 266
 267 ndefinition start_of_mcu_version_RS08 ≝
 268 λmcu:RS08_mcu_model.λt:memory_impl.
 269 λmem:aux_mem_type t.λchk:aux_chk_type t.
 270 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 271  let build ≝ λpcm.
 272    mk_any_status RS08 t
 273     (mk_alu_RS08
 274      (* acc_low: reset *)  〈x0,x0〉
 275      (* pc: reset *) (and_w16 〈〈xF,xF〉:〈xF,xD〉〉 pcm) pcm
 276      (* spc: reset *) (and_w16 〈〈xF,xF〉:〈xF,xD〉〉 pcm)
 277      (* xm: reset *) 〈x0,x0〉 (* psm: *) 〈x8,x0〉
 278      (* Z: reset *) false (* C: reset *) false)
 279      (* mem *) mem
 280      (* chk *) chk
 281      (* clk: reset *) (None ?) in
 282   (* tralascio l'enumerazione dei casi, tanto i valori sono uguali *)
 283   build 〈〈x3,xF〉:〈xF,xF〉〉.
 284
 285 (*
 286    cio' che non viene resettato mantiene il valore precedente: nella documentazione
 287    viene riportato come "unaffected"/"indeterminate"/"unpredictable"
 288    il soft RESET e' diverso da un calo di tensione e la ram non variera'
 289 *)
 290 ndefinition reset_of_mcu ≝
 291 λm:mcu_type.λt:memory_impl.
 292 let pc_reset_h ≝ 〈〈xF,xF〉:〈xF,xE〉〉 in
 293 let pc_reset_l ≝ 〈〈xF,xF〉:〈xF,xF〉〉 in
 294 let pc_RS08_reset ≝ 〈〈xF,xF〉:〈xF,xD〉〉 in
 295 let sp_reset ≝ 〈〈x0,x0〉:〈xF,xF〉〉 in
 296  match m return λm:mcu_type.(any_status m t) → (any_status m t) with
 297 (* HC05: parzialmente non deterministico *)
 298   [ HC05 ⇒ λs:any_status HC05 t.match s with
 299    [ mk_any_status alu mem chk clk ⇒ match alu with
 300     [ mk_alu_HC05 acclow indxlow _ spm spf _ pcm hfl _ nfl zfl cfl irqfl ⇒
 301     let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 pc_reset_h pcm))
 302                                (mem_read_abs t mem (and_w16 pc_reset_l pcm)) in
 303     mk_any_status HC05 t
 304      (mk_alu_HC05
 305       (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow
 306       (* sp: reset *) (or_w16 (and_w16 sp_reset spm) spf) spm spf
 307       (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm
 308       (* H: inv. *) hfl (* I: reset *) true (* N: inv. *) nfl
 309       (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
 310       (* mem: inv. *) mem
 311       (* chk: inv. *) chk
 312       (* clk: reset *) (None ?) ]]
 313 (* HC08: parzialmente non deterministico *)
 314   | HC08 ⇒ λs:any_status HC08 t.match s with
 315    [ mk_any_status alu mem chk clk ⇒ match alu with
 316     [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒
 317     let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
 318                                (mem_read_abs t mem pc_reset_l) in
 319     mk_any_status HC08 t
 320      (mk_alu_HC08
 321       (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉
 322       (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
 323       (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true
 324       (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
 325       (* mem: inv. *) mem
 326       (* chk: inv. *) chk
 327       (* clk: reset *) (None ?) ]]
 328 (* HCS08: parzialmente non deterministico *)
 329   | HCS08 ⇒ λs:any_status HCS08 t.match s with
 330    [ mk_any_status alu mem chk clk ⇒ match alu with
 331     [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒
 332     let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
 333                                (mem_read_abs t mem pc_reset_l) in
 334     mk_any_status HCS08 t
 335      (mk_alu_HC08
 336       (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉
 337       (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
 338       (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true
 339       (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
 340       (* mem: inv. *) mem
 341       (* chk: inv. *) chk
 342       (* clk: reset *) (None ?) ]]
 343 (* RS08: deterministico *)
 344   | RS08 ⇒ λs:any_status RS08 t.match s with
 345    [ mk_any_status alu mem chk clk ⇒ match alu with
 346     [ mk_alu_RS08 _ _ pcm _ _ _ _ _ ⇒
 347     mk_any_status RS08 t
 348      (mk_alu_RS08
 349       (* acc_low: reset *) 〈x0,x0〉
 350       (* pc: reset *) (and_w16 pc_RS08_reset pcm) pcm
 351       (* spc: reset *) (and_w16 pc_RS08_reset pcm)
 352       (* xm: reset *) 〈x0,x0〉 (* psm: reset *) 〈x8,x0〉
 353       (* Z: reset *) false (* C: reset *) false)
 354       (* mem: inv. *) mem
 355       (* chk: inv. *) chk
 356       (* clk: reset *) (None ?) ]]
 357   ].