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

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

Added exponential functions for nats. Working on operational semantics of processor.

File size: 2.5 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5(* include "ASM.ma". *)
6include "BitVectorTrie.ma".
7include "Arithmetic.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
87ndefinition initialise_status ≝
88  mk_Status
89    (Stub Byte sixteen)
90    (Stub Byte seven)
91    (Stub Byte seven)
92    (Stub Byte sixteen)
93    (zero sixteen)
94    ([ zero eight; zero eight; zero eight; zero eight;
95       zero eight; zero eight; zero eight; zero eight ]).
Note: See TracBrowser for help on using the repository browser.