(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Interpret.ma: Operational semantics for the 8051/8052 processor. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* include "ASM.ma". *) include "Arithmetic.ma". include "BitVectorTrie.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 }. alias id "replicate" = "cic:/matita/Cerco/Vector/replicate.fix(0,1,1)". ndefinition set_8051_sfr ≝ λs: Status. λi: SFR8051. λb: Byte. let index ≝ sfr_8051_status i in let ndefinition initialise_status ≝ let status ≝ mk_Status (Stub Byte sixteen) (Stub Byte seven) (Stub Byte seven) (Stub Byte sixteen) (zero sixteen) (replicate Byte nineteen (zero eight)) (replicate Byte five (zero eight)) in status.