source: Deliverables/D4.1/Matita/Interpret.ma @ 258

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

(* include "ASM.ma". *)
include "BitVectorTrie.ma".
include "Arithmetic.ma".

ninductive SFR8051: Type[0] ≝
  SFR_SP: SFR8051
| SFR_DPL: SFR8051
| SFR_DPH: SFR8051
| SFR_PCON: SFR8051
| SFR_TCON: SFR8051
| SFR_TMOD: SFR8051
| SFR_TL0: SFR8051
| SFR_TL1: SFR8051
| SFR_TH0: SFR8051
| SFR_TH1: SFR8051
| SFR_P1: SFR8051
| SFR_SCON: SFR8051
| SFR_SBUF: SFR8051
| SFR_IE: SFR8051
| SFR_P3: SFR8051
| SFR_IP: SFR8051
| SFR_PSW: SFR8051
| SFR_ACC_A: SFR8051
| SFR_ACC_B: SFR8051.

ndefinition sfr_8051_index ≝
  λs: SFR8051.
    match s with
      [ SFR_SP ⇒ Z
      | SFR_DPL ⇒ S Z
      | SFR_DPH ⇒ two
      | SFR_PCON ⇒ three
      | SFR_TCON ⇒ four
      | SFR_TMOD ⇒ five
      | SFR_TL0 ⇒ six
      | SFR_TL1 ⇒ seven
      | SFR_TH0 ⇒ eight
      | SFR_TH1 ⇒ nine
      | SFR_P1 ⇒ ten
      | SFR_SCON ⇒ eleven
      | SFR_SBUF ⇒ twelve
      | SFR_IE ⇒ thirteen
      | SFR_P3 ⇒ fourteen
      | SFR_IP ⇒ fifteen
      | SFR_PSW ⇒ sixteen
      | SFR_ACC_A ⇒ seventeen
      | SFR_ACC_B ⇒ eighteen
      ].
      
ninductive SFR8052: Type[0] ≝
   SFR_T2CON: SFR8052
|  SFR_RCAP2L: SFR8052
|  SFR_RCAP2H: SFR8052
|  SFR_TL2: SFR8052
|  SFR_TH2: SFR8052.

ndefinition sfr_8052_index ≝
  λs: SFR8052.
    match s with
      [ SFR_T2CON ⇒ Z
      | SFR_RCAP2L ⇒ S Z
      | SFR_RCAP2H ⇒ two
      | SFR_TL2 ⇒ three
      | SFR_TH2 ⇒ four 
      ].

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Processor status.                                                          *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
nrecord Status: Type[0] ≝
{
  code_memory: BitVectorTrie Byte sixteen;
  low_internal_ram: BitVectorTrie Byte seven;
  high_internal_ram: BitVectorTrie Byte seven;
  external_ram: BitVectorTrie Byte sixteen;
 
  program_counter: Word;
  
  special_function_registers_8051: Vector Byte nineteen;
  special_function_registers_8052: Vector Byte five
}.



ndefinition initialise_status ≝
  mk_Status
    (Stub Byte sixteen)
    (Stub Byte seven)
    (Stub Byte seven)
    (Stub Byte sixteen)
    (zero sixteen)
    ([ zero eight; zero eight; zero eight; zero eight;
       zero eight; zero eight; zero eight; zero eight ]).