Line | |
---|
1 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
2 | (* Interpret.ma: Operational semantics for the 8051/8052 processor. *) |
---|
3 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
4 | |
---|
5 | (* include "ASM.ma". *) |
---|
6 | include "BitVectorTrie.ma". |
---|
7 | include "Arithmetic.ma". |
---|
8 | |
---|
9 | ninductive SFR8051: Type[0] ≝ |
---|
10 | SFR_SP: SFR8051 |
---|
11 | | SFR_DPL: SFR8051 |
---|
12 | | SFR_DPH: SFR8051 |
---|
13 | | SFR_PCON: SFR8051 |
---|
14 | | SFR_TCON: SFR8051 |
---|
15 | | SFR_TMOD: SFR8051 |
---|
16 | | SFR_TL0: SFR8051 |
---|
17 | | SFR_TL1: SFR8051 |
---|
18 | | SFR_TH0: SFR8051 |
---|
19 | | SFR_TH1: SFR8051 |
---|
20 | | SFR_P1: SFR8051 |
---|
21 | | SFR_SCON: SFR8051 |
---|
22 | | SFR_SBUF: SFR8051 |
---|
23 | | SFR_IE: SFR8051 |
---|
24 | | SFR_P3: SFR8051 |
---|
25 | | SFR_IP: SFR8051 |
---|
26 | | SFR_PSW: SFR8051 |
---|
27 | | SFR_ACC_A: SFR8051 |
---|
28 | | SFR_ACC_B: SFR8051. |
---|
29 | |
---|
30 | ndefinition sfr_8051_index ≝ |
---|
31 | λs: SFR8051. |
---|
32 | match s with |
---|
33 | [ SFR_SP ⇒ Z |
---|
34 | | SFR_DPL ⇒ S Z |
---|
35 | | SFR_DPH ⇒ two |
---|
36 | | SFR_PCON ⇒ three |
---|
37 | | SFR_TCON ⇒ four |
---|
38 | | SFR_TMOD ⇒ five |
---|
39 | | SFR_TL0 ⇒ six |
---|
40 | | SFR_TL1 ⇒ seven |
---|
41 | | SFR_TH0 ⇒ eight |
---|
42 | | SFR_TH1 ⇒ nine |
---|
43 | | SFR_P1 ⇒ ten |
---|
44 | | SFR_SCON ⇒ eleven |
---|
45 | | SFR_SBUF ⇒ twelve |
---|
46 | | SFR_IE ⇒ thirteen |
---|
47 | | SFR_P3 ⇒ fourteen |
---|
48 | | SFR_IP ⇒ fifteen |
---|
49 | | SFR_PSW ⇒ sixteen |
---|
50 | | SFR_ACC_A ⇒ seventeen |
---|
51 | | SFR_ACC_B ⇒ eighteen |
---|
52 | ]. |
---|
53 | |
---|
54 | ninductive SFR8052: Type[0] ≝ |
---|
55 | SFR_T2CON: SFR8052 |
---|
56 | | SFR_RCAP2L: SFR8052 |
---|
57 | | SFR_RCAP2H: SFR8052 |
---|
58 | | SFR_TL2: SFR8052 |
---|
59 | | SFR_TH2: SFR8052. |
---|
60 | |
---|
61 | ndefinition sfr_8052_index ≝ |
---|
62 | λs: SFR8052. |
---|
63 | match s with |
---|
64 | [ SFR_T2CON ⇒ Z |
---|
65 | | SFR_RCAP2L ⇒ S Z |
---|
66 | | SFR_RCAP2H ⇒ two |
---|
67 | | SFR_TL2 ⇒ three |
---|
68 | | SFR_TH2 ⇒ four |
---|
69 | ]. |
---|
70 | |
---|
71 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
72 | (* Processor status. *) |
---|
73 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
74 | nrecord Status: Type[0] ≝ |
---|
75 | { |
---|
76 | code_memory: BitVectorTrie Byte sixteen; |
---|
77 | low_internal_ram: BitVectorTrie Byte seven; |
---|
78 | high_internal_ram: BitVectorTrie Byte seven; |
---|
79 | external_ram: BitVectorTrie Byte sixteen; |
---|
80 | |
---|
81 | program_counter: Word; |
---|
82 | |
---|
83 | special_function_registers_8051: Vector Byte nineteen; |
---|
84 | special_function_registers_8052: Vector Byte five |
---|
85 | }. |
---|
86 | |
---|
87 | |
---|
88 | |
---|
89 | ndefinition initialise_status ≝ |
---|
90 | mk_Status |
---|
91 | (Stub Byte sixteen) |
---|
92 | (Stub Byte seven) |
---|
93 | (Stub Byte seven) |
---|
94 | (Stub Byte sixteen) |
---|
95 | (zero sixteen) |
---|
96 | ([ zero eight; zero eight; zero eight; zero eight; |
---|
97 | zero eight; zero eight; zero eight; zero eight ]). |
---|
Note: See
TracBrowser
for help on using the repository browser.