1 2(* Definitions for AMBA AHB bus. See AMBA Specification v2.0 from ARM for details *) 3 4open HolKernel Parse boolLib bossLib 5(* app load ["pairSyntax","mod16Theory","commonTools","ksTools","listSyntax"] *) 6 7val _ = new_theory("amba_ahb") 8 9open HolKernel Parse boolLib bossLib 10 11open pairSyntax boolTheory listSyntax 12open mod16Theory commonTools ksTools amba_common 13 14 15 16(* -------------------- abbreviations for readibility of main defs -------------------- *) 17 18val BB_INC_def = Define `BB_INC n (^bbv) = if n=4 then MOD16_INC4 (^bbv) else MOD16_INC (^bbv)`; 19 20val WS_INC_def = Define `WS_INC n (^hwsv) = if n=4 then MOD16_INC4 (^hwsv) else MOD16_INC (^hwsv)`; 21 22(* transfer types {3-9} *) 23val IDLE_def = Define `IDLE (htrans_0,htrans_1) = ~htrans_0 /\ ~htrans_1`; 24val BUSY_def = Define `BUSY (htrans_0,htrans_1) = htrans_0 /\ ~htrans_1`; 25val NOSEQ_def = Define `NOSEQ (htrans_0,htrans_1) = ~htrans_0 /\ htrans_1`; 26val SEQ_def = Define `SEQ (htrans_0,htrans_1) = htrans_0 /\ htrans_1`; 27 28(* slave responses {3-21} *) 29val OKAY_def = Define `OKAY (hresp_0,hresp_1) = ~hresp_0 /\ ~hresp_1`; 30val ERROR_def = Define `ERROR (hresp_0,hresp_1) = hresp_0 /\ ~hresp_1`; 31val RETRY_def = Define `RETRY (hresp_0,hresp_1) = ~hresp_0 /\ hresp_1`; 32val SPLIT_def = Define `SPLIT (hresp_0,hresp_1) = hresp_0 /\ hresp_1`; 33 34(* burst types {3-11} TODO: fill in the rest *) 35val SINGLE_def = Define `SINGLE (hburst_0) = ~hburst_0`; 36val INC4_def = Define `INC4 (hburst_0) = hburst_0`; 37 38val INC4M_def = Define `INC4M n (^burstm_vars) = 39if n=0 then INC4(hburstm_0_0) 40else if n=1 then INC4(hburstm_1_0) 41else if n=2 then INC4(hburstm_2_0) 42else if n=3 then INC4(hburstm_3_0) 43else if n=4 then INC4(hburstm_4_0) 44else if n=5 then INC4(hburstm_5_0) 45else if n=6 then INC4(hburstm_6_0) 46else if n=7 then INC4(hburstm_7_0) 47else if n=8 then INC4(hburstm_8_0) 48else if n=9 then INC4(hburstm_9_0) 49else if n=10 then INC4(hburstm_10_0) 50else if n=11 then INC4(hburstm_11_0) 51else if n=12 then INC4(hburstm_12_0) 52else if n=13 then INC4(hburstm_13_0) 53else if n=14 then INC4(hburstm_14_0) else INC4(hburstm_15_0) `; 54 55val BURSTM0_def = Define `BURSTM0 n (^burstm_vars) = 56if n=0 then hburstm_0_0 57else if n=1 then hburstm_1_0 58else if n=2 then hburstm_2_0 59else if n=3 then hburstm_3_0 60else if n=4 then hburstm_4_0 61else if n=5 then hburstm_5_0 62else if n=6 then hburstm_6_0 63else if n=7 then hburstm_7_0 64else if n=8 then hburstm_8_0 65else if n=9 then hburstm_9_0 66else if n=10 then hburstm_10_0 67else if n=11 then hburstm_11_0 68else if n=12 then hburstm_12_0 69else if n=13 then hburstm_13_0 70else if n=14 then hburstm_14_0 else hburstm_15_0`; 71 72val TRANSM0_def = Define `TRANSM0 n (^transm_vars) = 73if n=0 then htransm_0_0 74else if n=1 then htransm_1_0 75else if n=2 then htransm_2_0 76else if n=3 then htransm_3_0 77else if n=4 then htransm_4_0 78else if n=5 then htransm_5_0 79else if n=6 then htransm_6_0 80else if n=7 then htransm_7_0 81else if n=8 then htransm_8_0 82else if n=9 then htransm_9_0 83else if n=10 then htransm_10_0 84else if n=11 then htransm_11_0 85else if n=12 then htransm_12_0 86else if n=13 then htransm_13_0 87else if n=14 then htransm_14_0 else htransm_15_0`; 88 89val TRANSM1_def = Define `TRANSM1 n (^transm_vars) = 90if n=0 then htransm_0_1 91else if n=1 then htransm_1_1 92else if n=2 then htransm_2_1 93else if n=3 then htransm_3_1 94else if n=4 then htransm_4_1 95else if n=5 then htransm_5_1 96else if n=6 then htransm_6_1 97else if n=7 then htransm_7_1 98else if n=8 then htransm_8_1 99else if n=9 then htransm_9_1 100else if n=10 then htransm_10_1 101else if n=11 then htransm_11_1 102else if n=12 then htransm_12_1 103else if n=13 then htransm_13_1 104else if n=14 then htransm_14_1 else htransm_15_1`; 105 106val IDLEM_def = Define `IDLEM n (^transm_vars) = 107if n=0 then IDLE(htransm_0_0,htransm_0_1) 108else if n=1 then IDLE(htransm_1_0,htransm_1_1) 109else if n=2 then IDLE(htransm_2_0,htransm_2_1) 110else if n=3 then IDLE(htransm_3_0,htransm_3_1) 111else if n=4 then IDLE(htransm_4_0,htransm_4_1) 112else if n=5 then IDLE(htransm_5_0,htransm_5_1) 113else if n=6 then IDLE(htransm_6_0,htransm_6_1) 114else if n=7 then IDLE(htransm_7_0,htransm_7_1) 115else if n=8 then IDLE(htransm_8_0,htransm_8_1) 116else if n=9 then IDLE(htransm_9_0,htransm_9_1) 117else if n=10 then IDLE(htransm_10_0,htransm_10_1) 118else if n=11 then IDLE(htransm_11_0,htransm_11_1) 119else if n=12 then IDLE(htransm_12_0,htransm_12_1) 120else if n=13 then IDLE(htransm_13_0,htransm_13_1) 121else if n=14 then IDLE(htransm_14_0,htransm_14_1) else IDLE(htransm_15_0,htransm_15_1)`; 122 123val BUSYM_def = Define `BUSYM n (^transm_vars) = 124if n=0 then BUSY(htransm_0_0,htransm_0_1) 125else if n=1 then BUSY(htransm_1_0,htransm_1_1) 126else if n=2 then BUSY(htransm_2_0,htransm_2_1) 127else if n=3 then BUSY(htransm_3_0,htransm_3_1) 128else if n=4 then BUSY(htransm_4_0,htransm_4_1) 129else if n=5 then BUSY(htransm_5_0,htransm_5_1) 130else if n=6 then BUSY(htransm_6_0,htransm_6_1) 131else if n=7 then BUSY(htransm_7_0,htransm_7_1) 132else if n=8 then BUSY(htransm_8_0,htransm_8_1) 133else if n=9 then BUSY(htransm_9_0,htransm_9_1) 134else if n=10 then BUSY(htransm_10_0,htransm_10_1) 135else if n=11 then BUSY(htransm_11_0,htransm_11_1) 136else if n=12 then BUSY(htransm_12_0,htransm_12_1) 137else if n=13 then BUSY(htransm_13_0,htransm_13_1) 138else if n=14 then BUSY(htransm_14_0,htransm_14_1) else BUSY(htransm_15_0,htransm_15_1)`; 139 140val NOSEQM_def = Define `NOSEQM n (^transm_vars) = 141if n=0 then NOSEQ(htransm_0_0,htransm_0_1) 142else if n=1 then NOSEQ(htransm_1_0,htransm_1_1) 143else if n=2 then NOSEQ(htransm_2_0,htransm_2_1) 144else if n=3 then NOSEQ(htransm_3_0,htransm_3_1) 145else if n=4 then NOSEQ(htransm_4_0,htransm_4_1) 146else if n=5 then NOSEQ(htransm_5_0,htransm_5_1) 147else if n=6 then NOSEQ(htransm_6_0,htransm_6_1) 148else if n=7 then NOSEQ(htransm_7_0,htransm_7_1) 149else if n=8 then NOSEQ(htransm_8_0,htransm_8_1) 150else if n=9 then NOSEQ(htransm_9_0,htransm_9_1) 151else if n=10 then NOSEQ(htransm_10_0,htransm_10_1) 152else if n=11 then NOSEQ(htransm_11_0,htransm_11_1) 153else if n=12 then NOSEQ(htransm_12_0,htransm_12_1) 154else if n=13 then NOSEQ(htransm_13_0,htransm_13_1) 155else if n=14 then NOSEQ(htransm_14_0,htransm_14_1) else NOSEQ(htransm_15_0,htransm_15_1)`; 156 157val SEQM_def = Define `SEQM n (^transm_vars) = 158if n=0 then SEQ(htransm_0_0,htransm_0_1) 159else if n=1 then SEQ(htransm_1_0,htransm_1_1) 160else if n=2 then SEQ(htransm_2_0,htransm_2_1) 161else if n=3 then SEQ(htransm_3_0,htransm_3_1) 162else if n=4 then SEQ(htransm_4_0,htransm_4_1) 163else if n=5 then SEQ(htransm_5_0,htransm_5_1) 164else if n=6 then SEQ(htransm_6_0,htransm_6_1) 165else if n=7 then SEQ(htransm_7_0,htransm_7_1) 166else if n=8 then SEQ(htransm_8_0,htransm_8_1) 167else if n=9 then SEQ(htransm_9_0,htransm_9_1) 168else if n=10 then SEQ(htransm_10_0,htransm_10_1) 169else if n=11 then SEQ(htransm_11_0,htransm_11_1) 170else if n=12 then SEQ(htransm_12_0,htransm_12_1) 171else if n=13 then SEQ(htransm_13_0,htransm_13_1) 172else if n=14 then SEQ(htransm_14_0,htransm_14_1) else SEQ(htransm_15_0,htransm_15_1)`; 173 174val ALL_SPLIT_def = Define `ALL_SPLIT (^split_vars) = hsplit_15 /\ hsplit_14 /\ hsplit_13 /\ hsplit_12 /\ hsplit_11 /\ hsplit_10 /\ hsplit_9 /\ hsplit_8 /\ hsplit_7 /\ hsplit_6 /\ hsplit_5 /\ hsplit_4 /\ hsplit_3 /\ hsplit_2 /\ hsplit_1`; 175 176(* FIXME: autogen this on number of masters *) 177val MASK_def = Define `MASK n (^mask_vars) = 178if n=0 then hmask_0 179else if n=1 then hmask_1 180else if n=2 then hmask_2 181else if n=3 then hmask_3 182else if n=4 then hmask_4 183else if n=5 then hmask_5 184else if n=6 then hmask_6 185else if n=7 then hmask_7 186else if n=8 then hmask_8 187else if n=9 then hmask_9 188else if n=10 then hmask_10 189else if n=11 then hmask_11 190else if n=12 then hmask_12 191else if n=13 then hmask_13 192else if n=14 then hmask_14 else hmask_15`; 193 194val BUSREQ_def = Define `BUSREQ n (^busreq_vars) = 195if n=0 then hbusreq_0 196else if n=1 then hbusreq_1 197else if n=2 then hbusreq_2 198else if n=3 then hbusreq_3 199else if n=4 then hbusreq_4 200else if n=5 then hbusreq_5 201else if n=6 then hbusreq_6 202else if n=7 then hbusreq_7 203else if n=8 then hbusreq_8 204else if n=9 then hbusreq_9 205else if n=10 then hbusreq_10 206else if n=11 then hbusreq_11 207else if n=12 then hbusreq_12 208else if n=13 then hbusreq_13 209else if n=14 then hbusreq_14 else hbusreq_15`; 210 211val HSPLIT_def = Define `HSPLIT n (^split_vars) = 212if n=0 then hsplit_0 213else if n=1 then hsplit_1 214else if n=2 then hsplit_2 215else if n=3 then hsplit_3 216else if n=4 then hsplit_4 217else if n=5 then hsplit_5 218else if n=6 then hsplit_6 219else if n=7 then hsplit_7 220else if n=8 then hsplit_8 221else if n=9 then hsplit_9 222else if n=10 then hsplit_10 223else if n=11 then hsplit_11 224else if n=12 then hsplit_12 225else if n=13 then hsplit_13 226else if n=14 then hsplit_14 else hsplit_15`; 227 228val NO_BUSREQ_def = Define `NO_BUSREQ (^busreq_vars) = ^nbrr`; 229 230val NO_HSPLIT_def = Define `NO_HSPLIT (^split_vars) = ^nhsr`; 231 232val NO_MASK_def = Define `NO_MASK (^mask_vars) = ^nmr`; 233 234val INIT_GRANT_def = Define `INIT_GRANT (^grant_vars) = MOD16_N2B ^(fromMLnum (nm-1)) (^grant_vars)` 235 236val GRANT_def = Define `GRANT n (^grant_vars) = MOD16_N2B n (^grant_vars)`; 237 238val INIT_MASTER_def = Define `INIT_MASTER (^master_vars) = MOD16_N2B ^(fromMLnum (nm-1)) (^master_vars)`; 239 240val MASTER_def = Define `MASTER n (^master_vars) = MOD16_N2B n (^master_vars)`; 241 242val HSEL_def = Define `HSEL n (^hselv) = MOD16_N2B n (^hselv)`; 243 244val SLVSPLT_def = Define `SLVSPLT n (^slvsplt_vars) = (EL n ^ssv)`; 245 246(* nth slave has split on mth master (if m is 0, then no split since you can't split on dummy master) *) 247(* this assumes a slave may split on no more than one master at a time *) 248val HSLVSPLT_def = Define `HSLVSPLT n m (^slvsplt_vars) = MOD16_N2B m (EL n ^ssv)` 249 250val NO_HSLVSPLT_def = Define `NO_HSLVSPLT (^slvsplt_vars) = ^nss`; 251 252(* -------------------- init state predicates --------------------------------------------*) 253 254(* HTRANS = IDLE and no one is requesting the bus*) 255 (*(!n. n<16 ==> (^(mk_pabs(transm_vars, ``IDLEM n (^transm_vars)``))) (^transm_vars)) /\ *) 256 257val Im = Define `INIT_M (^Im_state) = 258 IDLE(htrans_0,htrans_1) /\ 259 NO_BUSREQ (^busreq_vars) 260 `; 261val INIT_M_def = Im; 262 263(* HREADYOUT [FAQ] /\ HRESP = OKAY [FAQ] *) 264(* (hsel_0=~haddr_0) /\ (hsel_1 = haddr_0) *) 265val Is = Define `INIT_S (^Is_state)= 266 hreadyout /\ 267 OKAY(hresp_0,hresp_1) /\ 268 NO_HSPLIT (^split_vars) /\ 269 HSEL 0 (^hselv)`; 270val INIT_S_def = Is; 271 272(* 0 is dummy master 273 15 is default master (hence INIT_GRANT's defn) *) 274(* default master has the bus :FAQ *) 275val Ia = Define `INIT_A (^Ia_state) = 276 INIT_GRANT (^grant_vars) /\ 277 INIT_MASTER (^master_vars)`; 278val INIT_A_def = Ia; 279 280(* -------------------- transition relation predicates --------------------------------------------*) 281 282(* arbiter: simple priority based *) 283val Ra = Define `TRANS_A n (^Ra_state,^Ra_state') = 284 (if n=0 then hgrant_0' else if ~MASK n (^mask_vars) /\ BUSREQ n (^busreq_vars) /\ IDLE (^htransv) then GRANT n (^grant_vars') 285 else TRANS_A (n-1) (^Ra_state,^Ra_state')) /\ 286(* whoever is granted gets bus ownership when hreadyout goes high *) 287 ((^master_vars') = if ~hreadyout then (^master_vars) else (^grant_vars)) 288`; 289val TRANS_A_def = Ra; 290 291(* default master is nm-1, gets the bus if no one asks for it*) 292val Rm = Define `TRANS_AHB_M n (^Rm_state,^Rm_state') = 293if n=0 then (* dummy master *) 294 (MASTER n (^grant_vars) ==> IDLE(htransm_0_0',htransm_0_1')) /\ (* always signal IDLE on grant *) 295 (~BUSREQ n (^busreq_vars')) (* dummy never requests the bus *) 296else (* generic master *) 297(* keep requesting bus if you get ownership (so arbiter only takes it away for higher priorty req) until transfer is done *) 298 (~(OKAY(hresp_0,hresp_1) /\ hreadyout) /\ MASTER n (^grant_vars) ==> BUSREQ n (^busreq_vars')) /\ 299(* latch busreq until grant *) 300 (BUSREQ n (^busreq_vars) /\ ~GRANT n (^grant_vars) ==> BUSREQ n (^busreq_vars')) /\ 301(* starting transfer (if not already in the middle of one) *) 302 (hreadyout /\ IDLEM n (^transm_vars) /\ OKAY(hresp_0,hresp_1) /\ MASTER n (^grant_vars) 303 ==> NOSEQM n (^transm_vars')) /\ 304(* do not start transfer if not master, or not ok+rdy *) 305 ((~(hreadyout /\ OKAY(hresp_0,hresp_1)) \/ ~MASTER n (^grant_vars)) 306 ==> ~NOSEQM n (^transm_vars')) /\ 307(* switch to SEQ mode *) 308 (NOSEQM n (^transm_vars) /\ OKAY(hresp_0,hresp_1) /\ INC4M n (^burstm_vars) /\ MASTER n (^grant_vars) 309 ==> (BUSYM n (^transm_vars') \/ SEQM n (^transm_vars')) /\ INC4M n (^burstm_vars')) /\ 310(* mid-burst bookkeeping - may signal BUSY or SEQ after a SEQ (as long as burst beats remain) *) 311 (SEQM n (^transm_vars) /\ OKAY(hresp_0,hresp_1) /\ ~MOD16_N2B ^(fromMLnum (nb-1)) (bb3,bb2,bb1,bb0) /\ MASTER n (^grant_vars) 312 ==> (BUSYM n (^transm_vars') \/ SEQM n (^transm_vars')) /\ INC4M n (^burstm_vars')) /\ 313(* end-burst bookkeeping - must signal IDLE when burst beats finish - this is to prevent a single master from taking over the 314 bus forever, since arbiter only grants if the bus is idle *) 315 (SEQM n (^transm_vars) /\ OKAY(hresp_0,hresp_1) /\ MOD16_N2B ^(fromMLnum (nb-1)) (bb3,bb2,bb1,bb0) /\ MASTER n (^grant_vars) 316 ==> IDLEM n (^transm_vars')) /\ 317(* mid-burst bookkeeping - may not signal BUSY after a BUSY (as long as burst beats remain) ) *) 318(* specification does not say this but we need it to prevent livelock *) 319 (BUSYM n (^transm_vars)) /\ ~MOD16_N2B ^(fromMLnum (nb-1)) (bb3,bb2,bb1,bb0) /\ OKAY(hresp_0,hresp_1) /\ MASTER n (^grant_vars) 320 ==> (SEQM n (^transm_vars') /\ INC4M n (^burstm_vars')) /\ 321(* response to first cycle of retry - no need to reset bb; they take an extra cycle to reset but retry is two cycle so no prob *) 322 (~hreadyout /\ RETRY(hresp_0,hresp_1) /\ GRANT n (^grant_vars) 323 ==> IDLEM n (^transm_vars')) /\ 324(* response to second cycle of retry - {3-22} says master *must* retry *) 325 (hreadyout /\ RETRY(hresp_0,hresp_1) /\ GRANT n (^grant_vars) 326 ==> NOSEQM n (^transm_vars')) /\ 327(* response to first cycle of error ;{3-23} gives the option of continuing or cancelling transfer - we choose cancel*) 328 (~hreadyout /\ ERROR(hresp_0,hresp_1) /\GRANT n (^grant_vars) 329 ==> IDLEM n (^transm_vars')) /\ 330(* response to second cycle of error ;{3-23} gives the option of continuing or cancelling transfer - we choose cancel*) 331 (hreadyout /\ ERROR(hresp_0,hresp_1) /\ GRANT n (^grant_vars) 332 ==> IDLEM n (^transm_vars')) /\ 333(* record the number of a split master for future masking/unmasking *) 334 (if SPLIT(hresp_0,hresp_1) /\ ~hreadyout /\ MASTER n (^master_vars) then MASK n (^mask_vars') 335 else if HSPLIT n (^split_vars) then ~MASK n (^mask_vars') 336 else MASK n (^mask_vars') = MASK n (^mask_vars)) 337`; 338val TRANS_AHB_M_def = Rm; 339 340(* slave (SPLIT-capable) *) 341val Rs = Define `TRANS_AHB_S n (^Rs_state,^Rs_state') = 342(* latch hsel if hreadyout is low, otherwise hsel is free: this should be moved to the decoder*) 343 (~hreadyout ==> (^hselv'=^hselv)) /\ 344(* force hreadyout to high because slave can't do more than nw wait states *) 345 (HSEL n (^hselv) /\ MOD16_N2B ^(fromMLnum (nw-1)) (hws3,hws2,hws1,hws0) ==> hreadyout') /\ 346(* signal end of transfer (single or part of a burst) (don't need to check for rdy because value of rdy irrelevent to address phase) *) 347 (HSEL n (^hselv) /\ (NOSEQ(htrans_0,htrans_1) \/ SEQ(htrans_0,htrans_1)) /\ OKAY(hresp_0,hresp_1) 348 ==> OKAY(hresp_0',hresp_1') /\ hreadyout') /\ 349(* {3-9} slave response to IDLE is READY + OKAY *) 350 (HSEL n (^hselv) /\ IDLE(htrans_0,htrans_1) ==> hreadyout' /\ OKAY(hresp_0',hresp_1')) /\ 351(* {3-9} slave response to BUSY is OKAY *) 352 (HSEL n (^hselv) /\ BUSY(htrans_0,htrans_1) ==> OKAY(hresp_0',hresp_1')) /\ 353(* if m0 is granted then respond with OK always (to prevent RETRY or SPLIT on m0 *) 354 (HSEL n (^hselv) /\ GRANT 0 (^grant_vars) ==> OKAY(hresp_0',hresp_1')) /\ 355(* disable all but ok response*) 356 (HSEL n (^hselv) ==> (~SPLIT(hresp_0',hresp_1') /\ ~RETRY(hresp_0',hresp_1') /\ ~ERROR(hresp_0',hresp_1'))) /\ 357(* disable assertion of HSPLIT*) 358 (!m. m<^(fromMLnum nm) ==> (\m. ~HSPLIT m (^split_vars')) m) /\ 359(* drive second cycle of RETRY *) 360 (HSEL n (^hselv) /\ ~hreadyout /\ ~(IDLE(htrans_0,htrans_1) \/ BUSY(htrans_0,htrans_1)) /\ RETRY(hresp_0,hresp_1) 361 ==> hreadyout' /\ RETRY(hresp_0',hresp_1')) /\ 362(* drive second cycle of ERROR *) 363 (HSEL n (^hselv) /\ ~hreadyout /\ ~(IDLE(htrans_0,htrans_1) \/ BUSY(htrans_0,htrans_1)) /\ ERROR(hresp_0,hresp_1) 364 ==> hreadyout' /\ ERROR(hresp_0',hresp_1')) /\ 365(* drive second cycle of SPLIT *) 366 (HSEL n (^hselv) /\ ~hreadyout /\ ~(IDLE(htrans_0,htrans_1) \/ BUSY(htrans_0,htrans_1)) /\ SPLIT(hresp_0,hresp_1) 367 ==> hreadyout' /\ SPLIT(hresp_0',hresp_1')) /\ 368(* if SPLITing record current master's number *) 369 (if (HSEL n (^hselv) /\ ~hreadyout /\ SPLIT(hresp_0,hresp_1)) 370 then !m. m<16 ==> MASTER m (^master_vars) ==> HSLVSPLT n m (^slvsplt_vars') 371 else (SLVSPLT n (^slvsplt_vars') = SLVSPLT n (^slvsplt_vars))) /\ 372(* note we don't do anything about slave asserting HSPLIT because abstracting that away *) 373(* however, we do need to ensure that if we have split on Mx, we don't assert HSPLITy where x!=y *) 374(* with >1 split-capable slave we would have to use HSPLITx to avoid conflict, but with only one we can access HSPLIT directly *) 375 (!m. m<^(fromMLnum nm) ==> (\m. ~HSLVSPLT n m (^slvsplt_vars) ==> ~HSPLIT m (^split_vars')) m) /\ 376(* since slave can only split on one master, do not split if have already done so*) 377 (~HSLVSPLT n 0 (^slvsplt_vars) ==> ~SPLIT(hresp_0',hresp_1')) /\ 378(* if asserting hsplit, drive down hslvsplt (again since can only split on at most one master) *) 379 (!m. m<^(fromMLnum nm) ==> (\m. HSLVSPLT n m (^slvsplt_vars) /\ HSPLIT m (^split_vars) 380 ==> HSLVSPLT n 0 (^slvsplt_vars')) m) 381`; 382val TRANS_AHB_S_def = Rs; 383 384(*(* make sure non-existent slaves are never selected *) 385 (~HSEL 8 (^hselv') /\ ~HSEL 9 (^hselv') /\ ~HSEL 10 (^hselv') /\ ~HSEL 11 (^hselv') /\ 386 ~HSEL 12 (^hselv') /\ ~HSEL 13 (^hselv') /\ ~HSEL 14 (^hselv') /\ ~HSEL 15 (^hselv')) /\*) 387 388(* mux, which sends the current bus owner's signals through *) 389(* technically we should be using hmaster_0 (rather than hgrant) here but can't because 390 it is triggered in the same cycle (see Ra and {3-31})*) 391(* FIXME: previously we had no such thing as hburst_m_0 which has now appeared via BURSTM0 0. might create problems *) 392val Rx = Define `TRANS_X (^Rx_state,^Rx_state') = 393(htrans_0 = !n. n <^(fromMLnum nm) ==> (\n. MASTER n (^grant_vars) ==> TRANSM0 n (^transm_vars)) n) /\ 394(htrans_1 = !n. n <^(fromMLnum nm) ==> (\n. MASTER n (^grant_vars) ==> TRANSM1 n (^transm_vars)) n) /\ 395(hburst_0 = !n. n <^(fromMLnum nm) ==> (\n. MASTER n (^grant_vars) ==> BURSTM0 n (^burstm_vars)) n) /\ 396(htrans_0' = !n. n <^(fromMLnum nm) ==> (\n. MASTER n (^grant_vars') ==> TRANSM0 n (^transm_vars')) n) /\ 397(htrans_1' = !n. n <^(fromMLnum nm) ==> (\n. MASTER n (^grant_vars') ==> TRANSM1 n (^transm_vars')) n) /\ 398(hburst_0' = !n. n <^(fromMLnum nm) ==> (\n. MASTER n (^grant_vars') ==> BURSTM0 n (^burstm_vars')) n)`; 399val TRANS_X_def = Rx; 400 401(* FIXME: right now we are abtracting this out. wen we have arrays, this should be fixed *) 402(* decoder, decodes higher order address bits to figure out which slave is being targeted *) 403(*val Rd = Define `TRANS_D (^Rd_state,^Rd_state') = 404(* we only decode if hreadyout goes high, else hold old value *) 405 (hsel_0' = if hreadyout then ~haddr_0 else hsel_0) /\ 406 (hsel_1' = if hreadyout then haddr_0 else hsel_1) 407`;*) 408 409(* global counters go here *) 410val RCn = Define `TRANS_CNT (^RCn_state,^RCn_state') = 411(* wait state counter *) 412(* climb to hws2 on ~hreadyout, resetting on hreadyout (slaves do this if hws2 is reached) *) 413(~hreadyout ==> ((hws3',hws2',hws1',hws0') = WS_INC ^(fromMLnum nw) (hws3,hws2,hws1,hws0))) /\ 414(* burst beat counter *) 415(* start counting at noseq, increment for every seq, but hold if busy, reset if idle or ~hreadyout*) 416(* not sure if I should hold or reset if idle; or does that depend on where the counter is?*) 417(* FIXME: get rid of having to have a lambda here*) 418 ((bb3',bb2',bb1',bb0') = (\(bb3,bb2,bb1,bb0). 419 if hreadyout then 420 if NOSEQ(htrans_0,htrans_1) then MOD16_ONE(bb3,bb2,bb1,bb0) 421 else if SEQ(htrans_0,htrans_1) then BB_INC ^(fromMLnum nb) (bb3,bb2,bb1,bb0) 422 else if BUSY(htrans_0,htrans_1) then MOD16_HOLD(bb3,bb2,bb1,bb0) 423 else MOD16_ZERO(bb3,bb2,bb1,bb0) 424 else MOD16_ZERO(bb3,bb2,bb1,bb0)) (bb3,bb2,bb1,bb0)) 425`; 426val TRANS_CNT_def = RCn; 427 428(* (hws0' = ~hreadyout) /\ 429 (hws1' = ~hreadyout /\ hws0) /\ 430 (hws2' = ~hreadyout /\ hws1) /\ 431(* (hws3' = ~hreadyout /\ hws2) *) (*no need for this because the last waitstate is when slave drives hreadyout high on *next* tick *)*) 432 433val I1h = Define `INIT_AHB (^I1h_state) = 434^(lhs(concl(Drule.SPEC_ALL Im))) /\ 435^(lhs(concl(Drule.SPEC_ALL Is))) /\ 436^(lhs(concl(Drule.SPEC_ALL Ia))) `; 437val INIT_AHB_def = I1h; 438 439val Rr = list_mk_exists 440 ((strip_pair bbv)@(strip_pair bbv')@(strip_pair hwsv)@(strip_pair hwsv'), 441 list_mk_conj [``INIT_AHB (^I1h_state) ==> (MOD16_IS_ZERO (^bbv') /\ MOD16_IS_ZERO (^hwsv'))``, 442 lhs(concl(Drule.SPEC_ALL RCn)), 443 (list_mk_exists 444 ((strip_pair mask_vars)@(strip_pair mask_vars'), 445 list_mk_conj [``INIT_AHB (^I1h_state) ==> NO_MASK (^mask_vars)``, 446 lhs(concl(Drule.SPEC_ALL (SPEC (fromMLnum (nm-1)) Ra))), 447 list_mk_exists((strip_pair transm_vars)@(strip_pair transm_vars') 448 @(strip_pair burstm_vars)@(strip_pair burstm_vars'), 449 (list_mk_conj[``INIT_AHB (^I1h_state) ==> !m. m<16 ==> IDLEM m (^transm_vars)``, 450 list_mk_conj(List.tabulate(nm, 451 fn n => lhs(concl(Drule.SPEC_ALL (SPEC (fromMLnum n) Rm))))), 452 lhs(concl(Drule.SPEC_ALL Rx))]))])), 453 list_mk_exists 454 ((strip_pair slvsplt_vars)@(strip_pair slvsplt_vars'), 455 list_mk_conj([``INIT_AHB (^I1h_state) ==> NO_HSLVSPLT (^slvsplt_vars)``, 456 list_mk_conj(List.tabulate(ns,fn n => lhs(concl(Drule.SPEC_ALL (SPEC (fromMLnum n) Rs)))))]))]) 457 458(*^(lhs(concl(Drule.SPEC_ALL Rd)))*) 459val R1h = Define `TRANS_AHB (^R1h_state,^R1h_state') = ^Rr`; 460val TRANS_AHB_def = R1h; 461 462val abbrev_defs = [IDLE_def,BUSY_def,NOSEQ_def,SEQ_def,OKAY_def,ERROR_def,RETRY_def,SPLIT_def,SINGLE_def,INC4_def, 463 INC4M_def,BURSTM0_def,TRANSM0_def,TRANSM1_def,IDLEM_def,BUSYM_def,NOSEQM_def,SEQM_def,ALL_SPLIT_def, 464 MASK_def,BUSREQ_def,HSPLIT_def,NO_BUSREQ_def,NO_HSPLIT_def,NO_MASK_def,INIT_GRANT_def,GRANT_def, 465 INIT_MASTER_def, MASTER_def,HSLVSPLT_def,SLVSPLT_def,NO_HSLVSPLT_def,HSEL_def,BB_INC_def,WS_INC_def] 466 467val I1rh = save_thm("amba_ahb_I1rh",SIMP_RULE (pure_ss++BETA_ss++pairSimps.PAIR_ss++ARITH_ss) 468 ([INIT_M_def,INIT_S_def,INIT_A_def,COND_CLAUSES]@abbrev_defs@m16n2b@m16exp) INIT_AHB_def) 469 470val Rc = rhs(concl(SPEC_ALL TRANS_AHB_def)) 471 472val R1rh = save_thm("amba_ahb_R1rh", EVERY_CONJ_CONV (STRIP_QUANT_CONV 473 (EVERY_CONJ_CONV (STRIP_QUANT_CONV (EVERY_CONJ_CONV 474 (unroll_ahb_CONV [TRANS_AHB_M_def,TRANS_X_def,(*TRANS_D_def,*)TRANS_CNT_def,TRANS_AHB_S_def,I1rh] 475 TRANS_A_def abbrev_defs))))) Rc) 476 477val _ = export_theory() 478