Add AXI4 definitions

clash-protocols.cabal

@@ -137,6 +137,8 @@ library
 
   exposed-modules:
     Protocols
+    Protocols.Axi
+    Protocols.Axi4
     Protocols.Df
     Protocols.DfLike
     Protocols.Hedgehog

src/Protocols/Axi.hs

@@ -0,0 +1,173 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Protocols.Axi where
+
+-- base
+import Data.Kind (Type)
+import GHC.Generics (Generic)
+import GHC.TypeNats (Nat)
+
+-- clash-prelude
+import qualified Clash.Prelude as C
+import Clash.Prelude (type (^))
+
+data IdWidth = IdWidth Nat deriving (Show)
+data AddrWidth = AddrWidth Nat deriving (Show)
+data LengthWidth = LengthWidth Nat deriving (Show)
+data UserType = UserType Type KeepStrobe
+
+data KeepBurst       = KeepBurst       | NoBurst       deriving (Show)
+data KeepBurstLength = KeepBurstLength | NoBurstLength deriving (Show)
+data KeepLast        = KeepLast        | NoLast        deriving (Show)
+data KeepLock        = KeepLock        | NoLock        deriving (Show)
+data KeepModifiable  = KeepModifiable  | NoModifiable  deriving (Show)
+data KeepPermissions = KeepPermissions | NoPermissions deriving (Show)
+data KeepQos         = KeepQos         | NoQos         deriving (Show)
+data KeepRegion      = KeepRegion      | NoRegion      deriving (Show)
+data KeepResponse    = KeepResponse    | NoResponse    deriving (Show)
+data KeepSize        = KeepSize        | NoSize        deriving (Show)
+data KeepStrobe      = KeepStrobe      | NoStrobe      deriving (Show)
+
+type family Width (a :: k) :: Nat where
+  Width ('IdWidth n) = n
+  Width ('AddrWidth n) = n
+  Width ('LengthWidth n) = n
+
+type family BurstType (keepBurst :: KeepBurst) where
+  BurstType 'KeepBurst = BurstMode
+  BurstType 'NoBurst = ()
+
+type family BurstLengthType (keepBurstLength :: KeepBurstLength) where
+  BurstLengthType 'KeepBurstLength = C.Index (2^8)
+  BurstLengthType 'NoBurstLength = ()
+
+type family LastType (keepLast :: KeepLast) where
+  LastType 'KeepLast = Bool
+  LastType 'NoLast = ()
+
+type family LockType (keepLockType :: KeepLock) where
+  LockType 'KeepLock = AtomicAccess
+  LockType 'NoLock = ()
+
+type family ModifiableType (keepModifiable :: KeepModifiable) where
+  ModifiableType 'KeepModifiable = Modifiable
+  ModifiableType 'NoModifiable = ()
+
+type family PermissionsType (keepPermissions :: KeepPermissions) where
+  PermissionsType 'KeepPermissions = (Privileged, Secure, InstructionOrData)
+  PermissionsType 'NoPermissions = ()
+
+type family QosType (keepQos :: KeepQos) where
+  QosType 'KeepQos = C.Index (2^4)
+  QosType 'NoQos = ()
+
+type family RegionType (keepRegion :: KeepRegion) where
+  RegionType 'KeepRegion = C.BitVector 4
+  RegionType 'NoRegion = ()
+
+type family ResponseType (keepResponse :: KeepResponse) where
+  ResponseType 'KeepResponse = Resp
+  ResponseType 'NoResponse = ()
+
+type family SizeType (keepSize :: KeepSize) where
+  SizeType 'KeepSize = BurstSize
+  SizeType 'NoSize = ()
+
+type family StrobeWidth (userType :: Type) (keepStrobe :: KeepStrobe) where
+  StrobeWidth userType 'KeepStrobe = C.BitSize userType `C.DivRU` 8
+  StrobeWidth userType 'NoStrobe = 0
+
+type family StrobeType (bitSize :: Nat) (keepStrobe :: KeepStrobe) where
+  StrobeType bitSize 'KeepStrobe = C.BitVector (bitSize `C.DivRU` 8)
+  StrobeType bitSize 'NoStrobe = ()
+
+
+data BurstMode
+  -- | In a fixed burst, the address is the same for every transfer in the
+  -- burst. This burst type is used for repeated accesses to the same location
+  -- such as when loading or emptying a FIFO
+  = BmFixed
+  -- | Incrementing. In an incrementing burst, the address for each transfer in
+  -- the burst is an increment of the address for the previous transfer. The
+  -- increment value depends on the size of the transfer. For example, the
+  -- address for each transfer in a burst with a size of four bytes is the
+  -- previous address plus four. This burst type is used for accesses to normal
+  -- sequential memory.
+  | BmIncr
+  -- | A wrapping burst is similar to an incrementing burst, except that the
+  -- address wraps around to a lower address if an upper address limit is
+  -- reached. The following restrictions apply to wrapping bursts:
+  --
+  --   * the start address must be aligned to the size of each transfer
+  --   * the length of the burst must be 2, 4, 8, or 16 transfers.
+  --
+  -- The behavior of a wrapping burst is:
+  --
+  --   * The lowest address used by the burst is aligned to the total size of
+  --     the data to be transferred, that is, to ((size of each transfer in the
+  --     burst) × (number of transfers in the burst)). This address is defined
+  --     as the _wrap boundary_.
+  --
+  --   * After each transfer, the address increments in the same way as for an
+  --     INCR burst. However, if this incremented address is ((wrap boundary) +
+  --     (total size of data to be transferred)) then the address wraps round to
+  --     the wrap boundary.
+  --
+  --   * The first transfer in the burst can use an address that is higher than
+  --     the wrap boundary, subject to the restrictions that apply to wrapping
+  --     bursts. This means that the address wraps for any WRAP burst for which
+  --     the first address is higher than the wrap boundary.
+  --
+  -- This burst type is used for cache line accesses.
+  --
+  | BmWrap
+  | BmReserved
+  deriving (Show, C.ShowX, Generic, C.NFDataX)
+
+-- | The maximum number of bytes to transfer in each data transfer, or beat,
+-- in a burst.
+data BurstSize
+  = Bs1
+  | Bs2
+  | Bs4
+  | Bs8
+  | Bs16
+  | Bs32
+  | Bs64
+  | Bs128
+  deriving (Show, C.ShowX, Generic, C.NFDataX)
+
+data Resp
+  -- | Normal access success. Indicates that a normal access has been
+  -- successful. Can also indicate an exclusive access has failed.
+  = ROkay
+  -- | Exclusive access okay. Indicates that either the read or write portion
+  -- of an exclusive access has been successful.
+  | RExclusiveOkay
+  -- | Slave error. Used when the access has reached the slave successfully, but
+  -- the slave wishes to return an error condition to the originating master.
+  | RSlaveError
+  -- | Decode error. Generated, typically by an interconnect component, to
+  -- indicate that there is no slave at the transaction address.
+  | RDecodeError
+  deriving (Show, C.ShowX, Generic, C.NFDataX)
+
+data AtomicAccess
+  = NonExclusiveAccess
+  | ExclusiveAccess
+
+data Modifiable
+  = NonModifiable
+  | Modifiable
+
+data Secure
+  = Secure
+  | NonSecure
+
+data Privileged
+  = NotPrivileged
+  | Privileged
+
+data InstructionOrData
+  = Data
+  | Instruction