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

Last change on this file since 259 was 259, checked in by mulligan, 9 years ago

Need stronger set_ and get_index functions on vectors (current ones return a Maybe type).

File size: 2.8 KB
RevLine 
[257]1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5(* include "ASM.ma". *)
[259]6include "Arithmetic.ma".
[257]7include "BitVectorTrie.ma".
8
9ninductive 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
30ndefinition 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     
54ninductive SFR8052: Type[0] ≝
55   SFR_T2CON: SFR8052
56|  SFR_RCAP2L: SFR8052
57|  SFR_RCAP2H: SFR8052
58|  SFR_TL2: SFR8052
59|  SFR_TH2: SFR8052.
60
61ndefinition 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(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
74nrecord 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
[259]87alias id "replicate" = "cic:/matita/Cerco/Vector/replicate.fix(0,1,1)".
[258]88
[259]89ndefinition set_8051_sfr ≝
90  λs: Status.
91  λi: SFR8051.
92  λb: Byte.
93    let index ≝ sfr_8051_status i in
94    let
[258]95
[257]96ndefinition initialise_status ≝
[259]97  let status ≝ mk_Status (Stub Byte sixteen)
98                         (Stub Byte seven)
99                         (Stub Byte seven)
100                         (Stub Byte sixteen)
101                         (zero sixteen)
102                         (replicate Byte nineteen (zero eight))
103                         (replicate Byte five (zero eight)) in
104  status.
Note: See TracBrowser for help on using the repository browser.