(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* 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 }. ncheck special_function_registers_8051. naxiom sfr8051_index_nineteen: ∀i: SFR8051. sfr_8051_index i < nineteen. naxiom sfr8052_index_five: ∀i: SFR8052. sfr_8052_index i < five. ndefinition get_8051_sfr ≝ λs: Status. λi: SFR8051. let sfr ≝ special_function_registers_8051 s in let index ≝ sfr_8051_index i in get_index … sfr index ?. napply (sfr8051_index_nineteen i). nqed. ndefinition get_8052_sfr ≝ λs: Status. λi: SFR8052. let sfr ≝ special_function_registers_8052 s in let index ≝ sfr_8052_index i in get_index … sfr index ?. napply (sfr8052_index_five i). nqed. ndefinition set_8051_sfr ≝ λs: Status. λi: SFR8051. λb: Byte. let index ≝ sfr_8051_index i in let old_code_memory ≝ code_memory s in let old_low_internal_ram ≝ low_internal_ram s in let old_high_internal_ram ≝ high_internal_ram s in let old_external_ram ≝ external_ram s in let old_program_counter ≝ program_counter s in let old_special_function_registers_8051 ≝ special_function_registers_8051 s in let old_special_function_registers_8052 ≝ special_function_registers_8052 s in let new_special_function_registers_8051 ≝ cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in mk_Status old_code_memory old_low_internal_ram old_high_internal_ram old_external_ram old_program_counter new_special_function_registers_8051 old_special_function_registers_8052. napply (sfr8051_index_nineteen i). nqed. ndefinition set_8052_sfr ≝ λs: Status. λi: SFR8052. λb: Byte. let index ≝ sfr_8052_index i in let old_code_memory ≝ code_memory s in let old_low_internal_ram ≝ low_internal_ram s in let old_high_internal_ram ≝ high_internal_ram s in let old_external_ram ≝ external_ram s in let old_program_counter ≝ program_counter s in let old_special_function_registers_8051 ≝ special_function_registers_8051 s in let old_special_function_registers_8052 ≝ special_function_registers_8052 s in let new_special_function_registers_8052 ≝ cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in mk_Status old_code_memory old_low_internal_ram old_high_internal_ram old_external_ram old_program_counter old_special_function_registers_8051 new_special_function_registers_8052. napply (sfr8052_index_five i). nqed. ndefinition set_program_counter ≝ λs: Status. λi: SFR8052. λw: Word. let index ≝ sfr_8052_index i in let old_code_memory ≝ code_memory s in let old_low_internal_ram ≝ low_internal_ram s in let old_high_internal_ram ≝ high_internal_ram s in let old_external_ram ≝ external_ram s in let old_special_function_registers_8051 ≝ special_function_registers_8051 s in let old_special_function_registers_8052 ≝ special_function_registers_8052 s in mk_Status old_code_memory old_low_internal_ram old_high_internal_ram old_external_ram w old_special_function_registers_8051 old_special_function_registers_8052. ndefinition set_code_memory ≝ λs: Status. λi: SFR8052. λr: BitVectorTrie Byte sixteen. let index ≝ sfr_8052_index i in let old_low_internal_ram ≝ low_internal_ram s in let old_high_internal_ram ≝ high_internal_ram s in let old_external_ram ≝ external_ram s in let old_program_counter ≝ program_counter s in let old_special_function_registers_8051 ≝ special_function_registers_8051 s in let old_special_function_registers_8052 ≝ special_function_registers_8052 s in mk_Status r old_low_internal_ram old_high_internal_ram old_external_ram old_program_counter old_special_function_registers_8051 old_special_function_registers_8052. ndefinition set_low_internal_ram ≝ λs: Status. λi: SFR8052. λr: BitVectorTrie Byte seven. let index ≝ sfr_8052_index i in let old_code_memory ≝ code_memory s in let old_high_internal_ram ≝ high_internal_ram s in let old_external_ram ≝ external_ram s in let old_program_counter ≝ program_counter s in let old_special_function_registers_8051 ≝ special_function_registers_8051 s in let old_special_function_registers_8052 ≝ special_function_registers_8052 s in mk_Status old_code_memory r old_high_internal_ram old_external_ram old_program_counter old_special_function_registers_8051 old_special_function_registers_8052. ndefinition get_cy_flag ≝ λs: Status. let sfr ≝ special_function_registers_8051 s in let psw ≝ get_index … (get_8051_index SFR_PSW) s ? in get_index … Z psw ?. ndefinition set_high_internal_ram ≝ λs: Status. λi: SFR8052. λr: BitVectorTrie Byte seven. let index ≝ sfr_8052_index i in let old_code_memory ≝ code_memory s in let old_low_internal_ram ≝ low_internal_ram s in let old_high_internal_ram ≝ high_internal_ram s in let old_external_ram ≝ external_ram s in let old_program_counter ≝ program_counter s in let old_special_function_registers_8051 ≝ special_function_registers_8051 s in let old_special_function_registers_8052 ≝ special_function_registers_8052 s in mk_Status old_code_memory old_low_internal_ram r old_external_ram old_program_counter old_special_function_registers_8051 old_special_function_registers_8052. 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.