1
2(* Definitions for AMBA APB bus. See AMBA Specification v2.0 from ARM for details  *)
3
4open HolKernel Parse boolLib bossLib
5
6val _ = new_theory("amba_apb")
7
8open HolKernel Parse boolLib bossLib pairSyntax
9open mod16Theory commonTools amba_common
10
11val I1p = Define `INIT_APB (paddr:bool,pwrite:bool,psel:bool,psel_3:bool,psel_2:bool,psel_1:bool,psel_0:bool,penable:bool,pdata:bool,mdata:bool,maddr:bool,sdata_0:bool,saddr_0:bool,sdata_1:bool,saddr_1:bool) = ~psel /\ ~penable`;
12val INIT_APB_def = I1p;
13
14(* FIXME: transitions for pdata of the form pdata_0' = ... , so we can use pdata in the defs of m' and s' *)
15(* FIXME: scale, separate read/write buses *)
16(* note: psel_x is a family signals, where x identifies the slave, so the x is not bits e.g. psel_2 is a valid signal *)
17
18val PSEL_def = Define `PSEL x (psel_3:bool,psel_2:bool,psel_1:bool,psel_0:bool) = MOD16_N2B x (psel_3,psel_2,psel_1,psel_0)`;
19
20(*these are temporary, pending implementation of DI, at which point SDATA will lose the second argument and these can be removed
21  or at the very least they will be removed by DI. however, the saddr_x, sdata_x vars will definitely go  *)
22val SDATA_def = Define `SDATA x b = if (x=0) then FST b else SND b`
23val SADDR_def = Define `SADDR x b = if (x=0) then FST b else SND b`
24
25val Rm = Define `TRANS_APB_M (^Rpm_state,^Rpm_state') =
26  (penable' = psel /\ ~penable) /\
27  (psel ==> (pwrite' = pwrite)) /\
28  ((psel /\ ~penable) ==> ((psel'=psel) /\ (psel_3'=psel_3) /\ (psel_2'=psel_2) /\ (psel_1'=psel_1) /\ (psel_0'=psel_0)))  /\
29  (penable ==> (mdata' = if pwrite then mdata else pdata)) /\
30  (penable ==> (maddr' = if pwrite then maddr else paddr))
31`;
32val TRANS_APB_M_def = Rm;
33
34(* the saddr and sdata vars will go away once we have DI *)
35val Rs = Define `TRANS_APB_S x (^Rps_state,^Rps_state') =
36    (psel /\ PSEL x (psel_3,psel_2,psel_1,psel_0) /\ penable ==>
37        (SDATA x (sdata_0',sdata_1') = if pwrite then pdata else SDATA x (sdata_0,sdata_1))) /\
38    (psel /\ PSEL x (psel_3,psel_2,psel_1,psel_0) /\ penable ==>
39        (SADDR x (saddr_0',saddr_1') = if pwrite then paddr else SADDR x (saddr_0,saddr_1)))
40`;
41val TRANS_APB_S_def = Rs;
42
43val Rb = Define `TRANS_BUS x (^Rp_state,^Rp_state') =
44  (psel /\ PSEL x (psel_3,psel_2,psel_1,psel_0) /\ ~penable ==>
45                                                (paddr' = if pwrite then maddr else SADDR x (saddr_0,saddr_1))) /\
46  (psel /\ PSEL x (psel_3,psel_2,psel_1,psel_0) /\ ~penable ==>
47                                                (pdata' = if pwrite then mdata else SDATA x (sdata_0,sdata_1)))
48`;
49val TRANS_BUS_def = Rb;
50
51val R1p = Define `TRANS_APB (^Rp_state,^Rp_state') =
52^(lhs(concl(Drule.SPEC_ALL Rm)))  /\
53^(list_mk_conj(List.tabulate(num_apb_slaves,fn n => lhs(concl(Drule.SPEC_ALL (SPEC (fromMLnum n) Rs))))))  /\
54^(list_mk_conj(List.tabulate(num_apb_slaves,fn n => lhs(concl(Drule.SPEC_ALL (SPEC (fromMLnum n) Rb))))))
55`;
56val TRANS_APB_def = R1p;
57
58val _ = export_theory()
59