1
2open HolKernel boolLib bossLib Parse;
3open wordsTheory wordsLib listTheory;
4
5open armTheory arm_coretypesTheory;
6
7val _ = new_theory "lpc_uart";
8
9
10(* We define the state of a UART interface *)
11
12val _ = Hol_datatype `
13  uart0_state = <|
14
15    (* physical state components *)
16
17    U0RBR : word8;   (* receive buffer *)
18    U0THR : word8;   (* transmit holding buffer *)
19    U0LCR : word32;  (* line control register *)
20    U0LSR : word32;  (* line status register *)
21
22    (* logical state components *)
23
24    input_list  : word8 list;  (* list of bytes that will be received from serial cable *)
25    input_time  : num;         (* time from which U0THR is ready for next read *)
26
27    output_list : word8 list;  (* list of bytes that have been sent via serial cable *)
28    output_time : num          (* time from which U0RBR is ready for next write *)
29
30    (* Why are these time components here? Answer: we want the
31       interface to eventually respond: both in and out can either be
32       in a state ready for operation {in,out}put_time <= current_time
33       or be in a state which waits for current_time to increase to
34       the point where {in,out}put_time <= current_time is true. This
35       has a baked in assumption of liveness of the other party: we
36       assume that the UART never has to wait forever for the other
37       party (device at the other end of the serial cable). *)
38
39  |>`;
40
41
42(* We define an invariant for the UART0 state *)
43
44val uart0_ok_def = Define `
45  uart0_ok current_time (uart0:uart0_state) =
46    (* U0LCR must be in a usable state *)
47    (uart0.U0LCR ' 7 = F) /\
48    (* U0LSR bit 0 and bit 5 indicate whether U0RBR and U0THR, resp., are ready for use *)
49    (uart0.U0LSR ' 0 = (uart0.input_time <= current_time) /\ ~(uart0.input_list = [])) /\
50    (uart0.U0LSR ' 5 = (uart0.output_time <= current_time)) /\
51    (* Content of U0RBR and U0THR is determined by state of U0LSR *)
52    (?w. uart0.U0RBR = if uart0.U0LSR ' 0 then HD (uart0.input_list) else w) /\
53    (?w. uart0.U0THR = if uart0.U0LSR ' 5 then w else HD (uart0.output_list))`;
54
55
56(* We define what addresses are owned by UART0, and whether they can be read and written *)
57
58val UART0_addresses_def = Define `
59  UART0_addresses =
60    { x | 0xE000C000w <=+ x /\ x <+ 0xE000C034w } : word32 set`;
61
62
63(* We define what value the core sees if it reads one of UART0's addresses *)
64
65val mm_byte_reader_def = Define `
66  mm_byte_reader (a:word32) (b:word8) = (a =+ b)`;
67
68val mm_word_reader_def = Define `
69  mm_word_reader (a:word32) (w:word32) =
70    (a+0w =+ ( 7 ><  0) w) o
71    (a+1w =+ (15 ><  8) w) o
72    (a+2w =+ (23 >< 16) w) o
73    (a+3w =+ (31 >< 24) w)`;
74
75val UART0_read_def = Define `
76  UART0_read (uart0:uart0_state) =
77   (mm_byte_reader 0xE000C000w (uart0.U0RBR) o
78    mm_word_reader 0xE000C00Cw (uart0.U0LCR) o
79    mm_word_reader 0xE000C014w (uart0.U0LSR)) (\a. ARB)`;
80
81
82(* We define the possible next states (some s2) after a clock tick (starting from s1) *)
83
84val BYTE_WRITTEN_TO_MEM_def = Define `
85  (BYTE_WRITTEN_TO_MEM a [] = ARB) /\
86  (BYTE_WRITTEN_TO_MEM a ((MEM_READ w)::xs) = BYTE_WRITTEN_TO_MEM a xs) /\
87  (BYTE_WRITTEN_TO_MEM a ((MEM_WRITE w v)::xs) = if a = w then v else BYTE_WRITTEN_TO_MEM a xs)`;
88
89val _ = wordsLib.guess_lengths();
90val WORD_WRITTEN_TO_MEM_def = Define `
91  WORD_WRITTEN_TO_MEM a accesses =
92    BYTE_WRITTEN_TO_MEM (a+3w) accesses @@
93    BYTE_WRITTEN_TO_MEM (a+2w) accesses @@
94    BYTE_WRITTEN_TO_MEM (a+1w) accesses @@
95    BYTE_WRITTEN_TO_MEM (a+0w) accesses`;
96
97val ADDR_SET_def = Define `
98  (ADDR_SET [] = {}) /\
99  (ADDR_SET ((MEM_READ a)::xs) = a INSERT ADDR_SET xs) /\
100  (ADDR_SET ((MEM_WRITE a b)::xs) = a INSERT ADDR_SET xs)`;
101
102val ALL_OR_NOTHING_def = Define `
103  ALL_OR_NOTHING x a = (x INTER a = a) \/ (x INTER a = {})`;
104
105val IS_MEM_READ_def = Define `
106  (IS_MEM_READ (MEM_READ a) = T) /\ (IS_MEM_READ _ = F)`;
107
108val IS_MEM_WRITE_def = Define `
109  (IS_MEM_WRITE (MEM_WRITE a w) = T) /\ (IS_MEM_WRITE _ = F)`;
110
111(* read-write enabled *)
112val REG32_RW_NEXT_def = Define `
113  REG32_RW_NEXT addr pre_value accesses post_value =
114    let a = {addr; addr+1w; addr+2w; addr+3w} in
115    let reads = ADDR_SET (FILTER IS_MEM_READ accesses) in
116    let writes = ADDR_SET (FILTER IS_MEM_WRITE accesses) in
117      ALL_OR_NOTHING reads a /\
118      ALL_OR_NOTHING writes a /\
119      (post_value = if addr IN writes
120                    then WORD_WRITTEN_TO_MEM addr accesses
121                    else pre_value)`;
122
123
124(* read only version *)
125val REG32_RO_NEXT_def = Define `
126  REG32_RO_NEXT addr accesses =
127    let a = {addr; addr+1w; addr+2w; addr+3w} in
128    let reads = ADDR_SET (FILTER IS_MEM_READ accesses) in
129    let writes = ADDR_SET (FILTER IS_MEM_WRITE accesses) in
130      ALL_OR_NOTHING reads a /\
131      (a INTER writes = {})`;
132
133
134val UART0_NEXT_def = Define `
135  UART0_NEXT current_time (accesses:memory_access list) (s1:uart0_state) (s2:uart0_state) =
136
137    (* both before and after state must be consistent, i.e. logical components of
138       each state must agree with physical components of resp. state. *)
139    uart0_ok current_time s1 /\ uart0_ok (current_time+1) s2 /\
140
141    (* if read happened then ... else ... *)
142    (if MEM (MEM_READ 0xE000C000w) accesses then
143       (s1.U0LSR ' 0 = T) /\ (* fail if UART0 was not ready for a read *)
144       (s2.input_list = TL s1.input_list) (* pop one element off input list *)
145       (* implicity let input_delay in s2 be any natural number *)
146     else
147       (* if no read happened then do nothing *)
148       (s2.input_time = s1.input_time) /\
149       (s2.input_list = s1.input_list)) /\
150
151    (* if write happened then ... else ... *)
152    (if ?w. MEM (MEM_WRITE 0xE000C000w w) accesses then
153       (s1.U0LSR ' 5 = T) /\ (* fail if UART0 was not ready for a write *)
154       (s2.output_list = w2w (BYTE_WRITTEN_TO_MEM 0xE000C000w accesses) :: s1.output_list) (* cons new output *)
155       (* implicity let output_delay in s2 be any natural number *)
156     else
157       (* if no write happened then do nothing *)
158       (s2.output_time = s1.output_time) /\
159       (s2.output_list = s1.output_list)) /\
160
161    (* the 32-bit memory-mapped registers *)
162    REG32_RW_NEXT 0xE000C00Cw (s1.U0LCR) accesses (s2.U0LCR) /\
163    REG32_RO_NEXT 0xE000C014w accesses`;
164
165
166
167
168(* A lemma needed later on *)
169
170val REG32_NEXT_NIL = prove(
171  ``!x w1 w2. (REG32_RW_NEXT x w1 [] w2 = (w1 = w2)) /\
172              (REG32_RO_NEXT x [] = T)``,
173  SIMP_TAC std_ss [REG32_RW_NEXT_def,REG32_RO_NEXT_def,LET_DEF,FILTER,ADDR_SET_def,
174     pred_setTheory.NOT_IN_EMPTY,ALL_OR_NOTHING_def,pred_setTheory.INTER_EMPTY]
175  THEN METIS_TAC []);
176
177val BIT_UPDATE_def = Define `
178  BIT_UPDATE i b (w:'a word) = (FCP j. if i = j then b else w ' j):'a word`;
179
180val APPLY_BIT_UPDATE_THM = store_thm("APPLY_BIT_UPDATE_THM",
181  ``!i j b w.
182      j < dimindex (:'a) ==>
183      (BIT_UPDATE i b (w:'a word) ' j = if i = j then b else w ' j)``,
184  SIMP_TAC std_ss [fcpTheory.CART_EQ,BIT_UPDATE_def,fcpTheory.FCP_BETA]);
185
186val UART0_NEXT_EXISTS = store_thm("UART0_NEXT_EXISTS",
187  ``!t s1. uart0_ok t s1 ==> ?s2. UART0_NEXT t [] s1 s2``,
188  SIMP_TAC std_ss [UART0_NEXT_def,uart0_ok_def,MEM,REG32_NEXT_NIL]
189  THEN REPEAT STRIP_TAC
190  THEN EXISTS_TAC
191  ``<| U0RBR := if s1.input_time <= t + 1 /\ s1.input_list <> [] then HD s1.input_list else ARB;
192       U0THR := if s1.output_time <= t + 1 then ARB else HD s1.output_list;
193       U0LCR := s1.U0LCR;
194       U0LSR := BIT_UPDATE 0 (s1.input_time <= t + 1 /\ s1.input_list <> [])
195               (BIT_UPDATE 5 (s1.output_time <= t + 1) s1.U0LSR);
196       input_list  := s1.input_list;
197       input_time  := s1.input_time;
198       output_list := s1.output_list;
199       output_time := s1.output_time |>``
200  THEN SRW_TAC [] [APPLY_BIT_UPDATE_THM]);
201
202val UART0_READ_def = Define `
203  UART0_READ (uart0:uart0_state) =
204    (uart0.input_list,uart0.input_time,uart0.output_list,uart0.output_time)`;
205
206
207(* -- old part of script commented out, but might be used in the future
208
209
210
211(* UART0 does nothing observable when left untouched,
212   similarly reading LSR has no observable effect. *)
213
214val UART0_NEXT_NIL = store_thm("UART0_NEXT_NIL",
215  ``!t s1 s2.
216      UART0_NEXT t [] s1 s2 =
217      uart0_ok t s1 /\ uart0_ok (t+1) s2 /\ (UART0_READ s1 = UART0_READ s2)``,
218  SIMP_TAC std_ss [UART0_READ_def,UART0_NEXT_def,MEM] THEN METIS_TAC []);
219
220val UART0_NEXT_READ_LSR = store_thm("UART0_NEXT_READ_LSR",
221  ``!t s1 s2.
222      UART0_NEXT t [MEM_READ 0xE000C014w] s1 s2 =
223      uart0_ok t s1 /\ uart0_ok (t+1) s2 /\ (UART0_READ s1 = UART0_READ s2)``,
224  SIMP_TAC (std_ss++SIZES_ss) [UART0_READ_def,UART0_NEXT_def,MEM,
225    memory_access_11,memory_access_distinct,n2w_11] THEN METIS_TAC []);
226
227val UART0_NEXT_EXISTS = store_thm("UART0_NEXT_EXISTS",
228  ``!t s1. uart0_ok t s1 ==>
229           ?s2. UART0_NEXT t [] s1 s2 /\
230                UART0_NEXT t [MEM_READ 0xE000C014w] s1 s2``,
231  SIMP_TAC std_ss [UART0_NEXT_NIL,UART0_NEXT_READ_LSR,uart0_ok_def]
232  THEN REPEAT STRIP_TAC
233  THEN EXISTS_TAC
234  ``<| U0RBR := if s1.input_time <= t + 1 /\ s1.input_list <> [] then HD s1.input_list else ARB;
235       U0THR := if s1.output_time <= t + 1 then ARB else HD s1.output_list;
236       U0LCR := s1.U0LCR;
237       U0LSR := BIT_UPDATE 0 (s1.input_time <= t + 1 /\ s1.input_list <> [])
238               (BIT_UPDATE 5 (s1.output_time <= t + 1) s1.U0LSR);
239       input_list  := s1.input_list;
240       input_time  := s1.input_time;
241       output_list := s1.output_list;
242       output_time := s1.output_time |>``
243  THEN SRW_TAC [] [UART0_READ_def,APPLY_BIT_UPDATE_THM]);
244
245
246(* UART successfully reads and writes *)
247
248val UART0_READ = store_thm("UART0_READ",
249  ``!t s1 w. uart0_ok t s1 /\ s1.U0LSR ' 0 ==>
250             ?s2. UART0_NEXT t [MEM_READ 0xE000C000w] s1 s2``,
251  SIMP_TAC std_ss [uart0_ok_def,UART0_NEXT_def,MEM,memory_access_11,
252    memory_access_distinct,BYTE_WRITTEN_TO_MEM_def]
253  THEN REPEAT STRIP_TAC
254  THEN EXISTS_TAC
255  ``<| U0RBR := ARB;
256       U0THR := if s1.output_time <= t + 1 then ARB else HD s1.output_list;
257       U0LCR := s1.U0LCR;
258       U0LSR := BIT_UPDATE 0 F
259               (BIT_UPDATE 5 (s1.output_time <= t + 1) s1.U0LSR);
260       input_list  := TL s1.input_list;
261       input_time  := t + 5;
262       output_list := s1.output_list;
263       output_time := s1.output_time |>``
264  THEN SRW_TAC [] [UART0_READ_def,APPLY_BIT_UPDATE_THM]
265  THEN FULL_SIMP_TAC std_ss []);
266
267val UART0_WRITE = store_thm("UART0_WRITE",
268  ``!t s1 w. uart0_ok t s1 /\ s1.U0LSR ' 5 ==>
269             ?s2. UART0_NEXT t [MEM_WRITE 0xE000C000w w] s1 s2``,
270  SIMP_TAC std_ss [uart0_ok_def,UART0_NEXT_def,MEM,memory_access_11,
271    memory_access_distinct,BYTE_WRITTEN_TO_MEM_def]
272  THEN REPEAT STRIP_TAC
273  THEN EXISTS_TAC
274  ``<| U0RBR := if s1.input_time <= t + 1 /\ s1.input_list <> [] then HD s1.input_list else ARB;
275       U0THR := w2w (w:word8);
276       U0LCR := s1.U0LCR;
277       U0LSR := BIT_UPDATE 0 (s1.input_time <= t + 1 /\ s1.input_list <> [])
278               (BIT_UPDATE 5 F s1.U0LSR);
279       input_list  := s1.input_list;
280       input_time  := s1.input_time;
281       output_list := (w2w (w:word8)) :: s1.output_list;
282       output_time := t + 5 |>``
283  THEN SRW_TAC [] [UART0_READ_def,APPLY_BIT_UPDATE_THM]
284  THEN FULL_SIMP_TAC std_ss []);
285
286*)
287
288val _ = export_theory();
289