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