From ea5c5aa86f3cf51bd6404aa838364f0d6c9838a1 Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Tue, 5 Jan 2021 16:41:31 +0100 Subject: [PATCH] Add sctrict AXI --- clash-protocols.cabal | 26 ++- src/Protocols/Axi4/{Raw => }/Common.hs | 16 +- src/Protocols/Axi4/Full.hs | 0 src/Protocols/Axi4/{Raw => Partial}/Full.hs | 12 +- .../Axi4/{Raw => Partial}/Full/ReadAddress.hs | 4 +- .../Axi4/{Raw => Partial}/Full/ReadData.hs | 4 +- .../{Raw => Partial}/Full/WriteAddress.hs | 4 +- .../Axi4/{Raw => Partial}/Full/WriteData.hs | 4 +- .../{Raw => Partial}/Full/WriteResponse.hs | 4 +- src/Protocols/Axi4/Strict/Full.hs | 23 +++ src/Protocols/Axi4/Strict/Full/ReadAddress.hs | 186 ++++++++++++++++++ src/Protocols/Axi4/Strict/Full/ReadData.hs | 136 +++++++++++++ .../Axi4/Strict/Full/WriteAddress.hs | 185 +++++++++++++++++ src/Protocols/Axi4/Strict/Full/WriteData.hs | 129 ++++++++++++ .../Axi4/Strict/Full/WriteResponse.hs | 126 ++++++++++++ 15 files changed, 830 insertions(+), 29 deletions(-) rename src/Protocols/Axi4/{Raw => }/Common.hs (94%) delete mode 100644 src/Protocols/Axi4/Full.hs rename src/Protocols/Axi4/{Raw => Partial}/Full.hs (63%) rename src/Protocols/Axi4/{Raw => Partial}/Full/ReadAddress.hs (98%) rename src/Protocols/Axi4/{Raw => Partial}/Full/ReadData.hs (98%) rename src/Protocols/Axi4/{Raw => Partial}/Full/WriteAddress.hs (98%) rename src/Protocols/Axi4/{Raw => Partial}/Full/WriteData.hs (97%) rename src/Protocols/Axi4/{Raw => Partial}/Full/WriteResponse.hs (97%) create mode 100644 src/Protocols/Axi4/Strict/Full.hs create mode 100644 src/Protocols/Axi4/Strict/Full/ReadAddress.hs create mode 100644 src/Protocols/Axi4/Strict/Full/ReadData.hs create mode 100644 src/Protocols/Axi4/Strict/Full/WriteAddress.hs create mode 100644 src/Protocols/Axi4/Strict/Full/WriteData.hs create mode 100644 src/Protocols/Axi4/Strict/Full/WriteResponse.hs diff --git a/clash-protocols.cabal b/clash-protocols.cabal index cbd80d4e..5b649bcd 100644 --- a/clash-protocols.cabal +++ b/clash-protocols.cabal @@ -124,12 +124,13 @@ library build-depends: -- inline-circuit-notation circuit-notation - , extra , data-default , deepseq - , hedgehog >= 1.0.2 + , extra , ghc >= 8.6 + , hedgehog >= 1.0.2 , pretty-show + , strict-tuple -- To be removed; we need 'Test.Tasty.Hedgehog.Extra' to fix upstream issues , tasty >= 1.2 && < 1.5 @@ -138,13 +139,20 @@ library exposed-modules: Protocols - Protocols.Axi4.Raw.Common - Protocols.Axi4.Raw.Full - Protocols.Axi4.Raw.Full.ReadAddress - Protocols.Axi4.Raw.Full.ReadData - Protocols.Axi4.Raw.Full.WriteAddress - Protocols.Axi4.Raw.Full.WriteData - Protocols.Axi4.Raw.Full.WriteResponse + Protocols.Axi4.Common + + Protocols.Axi4.Partial.Full + Protocols.Axi4.Partial.Full.ReadAddress + Protocols.Axi4.Partial.Full.ReadData + Protocols.Axi4.Partial.Full.WriteAddress + Protocols.Axi4.Partial.Full.WriteData + Protocols.Axi4.Partial.Full.WriteResponse + + Protocols.Axi4.Strict.Full.ReadAddress + Protocols.Axi4.Strict.Full.ReadData + Protocols.Axi4.Strict.Full.WriteAddress + Protocols.Axi4.Strict.Full.WriteData + Protocols.Axi4.Strict.Full.WriteResponse Protocols.Df Protocols.DfLike diff --git a/src/Protocols/Axi4/Raw/Common.hs b/src/Protocols/Axi4/Common.hs similarity index 94% rename from src/Protocols/Axi4/Raw/Common.hs rename to src/Protocols/Axi4/Common.hs index f80045da..451ab081 100644 --- a/src/Protocols/Axi4/Raw/Common.hs +++ b/src/Protocols/Axi4/Common.hs @@ -3,7 +3,7 @@ Types and utilities shared between AXI4, AXI4-Lite, and AXI3. -} {-# LANGUAGE UndecidableInstances #-} -module Protocols.Axi4.Raw.Common where +module Protocols.Axi4.Common where -- base import Data.Kind (Type) @@ -12,7 +12,10 @@ import GHC.TypeNats (Nat) -- clash-prelude import qualified Clash.Prelude as C -import Clash.Prelude (type (^), type (-)) +import Clash.Prelude (type (^), type (-), type (*)) + +-- strict-tuple +import Data.Tuple.Strict -- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol data IdWidth = IdWidth Nat deriving (Show) @@ -93,7 +96,7 @@ type family LockType (keepLockType :: KeepLock) where -- | Enables or disables 'Privileged', 'Secure', and 'InstructionOrData' type family PermissionsType (keepPermissions :: KeepPermissions) where - PermissionsType 'KeepPermissions = (Privileged, Secure, InstructionOrData) + PermissionsType 'KeepPermissions = T3 Privileged Secure InstructionOrData PermissionsType 'NoPermissions = () -- | Enables or disables 'Qos' @@ -121,6 +124,11 @@ type family StrobeType (byteSize :: Nat) (keepStrobe :: KeepStrobe) where StrobeType byteSize 'KeepStrobe = Strobe byteSize StrobeType byteSize 'NoStrobe = () +-- | Enable or disable 'Strobe' +type family StrictStrobeType (byteSize :: Nat) (keepStrobe :: KeepStrobe) where + StrictStrobeType byteSize 'KeepStrobe = C.Vec byteSize (C.BitVector 8) + StrictStrobeType byteSize 'NoStrobe = C.BitVector (byteSize * 8) + -- | Indicates valid bytes on data field. type Strobe (byteSize :: Nat) = C.BitVector byteSize @@ -213,7 +221,7 @@ data Allocate = NoLookupCache | LookupCache data OtherAllocate = OtherNoLookupCache | OtherLookupCache -- | See Table A4-3 AWCACHE bit allocations -type Cache = (Bufferable, Modifiable, OtherAllocate, Allocate) +type Cache = T4 Bufferable Modifiable OtherAllocate Allocate -- | Status of the write transaction. data Resp diff --git a/src/Protocols/Axi4/Full.hs b/src/Protocols/Axi4/Full.hs deleted file mode 100644 index e69de29b..00000000 diff --git a/src/Protocols/Axi4/Raw/Full.hs b/src/Protocols/Axi4/Partial/Full.hs similarity index 63% rename from src/Protocols/Axi4/Raw/Full.hs rename to src/Protocols/Axi4/Partial/Full.hs index 86af742e..4e6aaf03 100644 --- a/src/Protocols/Axi4/Raw/Full.hs +++ b/src/Protocols/Axi4/Partial/Full.hs @@ -10,7 +10,7 @@ is not. {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE UndecidableInstances #-} -module Protocols.Axi4.Raw.Full +module Protocols.Axi4.Partial.Full ( module ReadAddress , module ReadData , module WriteAddress @@ -18,8 +18,8 @@ module Protocols.Axi4.Raw.Full , module WriteResponse ) where -import Protocols.Axi4.Raw.Full.ReadAddress as ReadAddress -import Protocols.Axi4.Raw.Full.ReadData as ReadData -import Protocols.Axi4.Raw.Full.WriteAddress as WriteAddress -import Protocols.Axi4.Raw.Full.WriteData as WriteData -import Protocols.Axi4.Raw.Full.WriteResponse as WriteResponse +import Protocols.Axi4.Partial.Full.ReadAddress as ReadAddress +import Protocols.Axi4.Partial.Full.ReadData as ReadData +import Protocols.Axi4.Partial.Full.WriteAddress as WriteAddress +import Protocols.Axi4.Partial.Full.WriteData as WriteData +import Protocols.Axi4.Partial.Full.WriteResponse as WriteResponse diff --git a/src/Protocols/Axi4/Raw/Full/ReadAddress.hs b/src/Protocols/Axi4/Partial/Full/ReadAddress.hs similarity index 98% rename from src/Protocols/Axi4/Raw/Full/ReadAddress.hs rename to src/Protocols/Axi4/Partial/Full/ReadAddress.hs index a1fbbd31..4b3180df 100644 --- a/src/Protocols/Axi4/Raw/Full/ReadAddress.hs +++ b/src/Protocols/Axi4/Partial/Full/ReadAddress.hs @@ -10,7 +10,7 @@ to the AXI4 specification. {-# OPTIONS_GHC -Wno-missing-fields #-} -module Protocols.Axi4.Raw.Full.ReadAddress +module Protocols.Axi4.Partial.Full.ReadAddress ( M2S_ReadAddress(..) , S2M_ReadAddress(..) , Axi4ReadAddress @@ -27,7 +27,7 @@ import qualified Clash.Prelude as C import Clash.Prelude ((:::)) -- me -import Protocols.Axi4.Raw.Common +import Protocols.Axi4.Common import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike diff --git a/src/Protocols/Axi4/Raw/Full/ReadData.hs b/src/Protocols/Axi4/Partial/Full/ReadData.hs similarity index 98% rename from src/Protocols/Axi4/Raw/Full/ReadData.hs rename to src/Protocols/Axi4/Partial/Full/ReadData.hs index 079ad94d..dfb05c44 100644 --- a/src/Protocols/Axi4/Raw/Full/ReadData.hs +++ b/src/Protocols/Axi4/Partial/Full/ReadData.hs @@ -10,7 +10,7 @@ to the AXI4 specification. {-# OPTIONS_GHC -Wno-missing-fields #-} -module Protocols.Axi4.Raw.Full.ReadData +module Protocols.Axi4.Partial.Full.ReadData ( M2S_ReadData(..) , S2M_ReadData(..) , Axi4ReadData @@ -27,7 +27,7 @@ import qualified Clash.Prelude as C import Clash.Prelude ((:::)) -- me -import Protocols.Axi4.Raw.Common +import Protocols.Axi4.Common import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike diff --git a/src/Protocols/Axi4/Raw/Full/WriteAddress.hs b/src/Protocols/Axi4/Partial/Full/WriteAddress.hs similarity index 98% rename from src/Protocols/Axi4/Raw/Full/WriteAddress.hs rename to src/Protocols/Axi4/Partial/Full/WriteAddress.hs index e143307f..eb92aad6 100644 --- a/src/Protocols/Axi4/Raw/Full/WriteAddress.hs +++ b/src/Protocols/Axi4/Partial/Full/WriteAddress.hs @@ -10,7 +10,7 @@ to the AXI4 specification. {-# OPTIONS_GHC -Wno-missing-fields #-} -module Protocols.Axi4.Raw.Full.WriteAddress +module Protocols.Axi4.Partial.Full.WriteAddress ( M2S_WriteAddress(..) , S2M_WriteAddress(..) , Axi4WriteAddress @@ -27,7 +27,7 @@ import qualified Clash.Prelude as C import Clash.Prelude ((:::)) -- me -import Protocols.Axi4.Raw.Common +import Protocols.Axi4.Common import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike diff --git a/src/Protocols/Axi4/Raw/Full/WriteData.hs b/src/Protocols/Axi4/Partial/Full/WriteData.hs similarity index 97% rename from src/Protocols/Axi4/Raw/Full/WriteData.hs rename to src/Protocols/Axi4/Partial/Full/WriteData.hs index a7d8cdf1..418bf8f1 100644 --- a/src/Protocols/Axi4/Raw/Full/WriteData.hs +++ b/src/Protocols/Axi4/Partial/Full/WriteData.hs @@ -10,7 +10,7 @@ to the AXI4 specification. {-# OPTIONS_GHC -Wno-missing-fields #-} -module Protocols.Axi4.Raw.Full.WriteData +module Protocols.Axi4.Partial.Full.WriteData ( M2S_WriteData(..) , S2M_WriteData(..) , Axi4WriteData @@ -28,7 +28,7 @@ import qualified Clash.Prelude as C import Clash.Prelude ((:::), type (*)) -- me -import Protocols.Axi4.Raw.Common +import Protocols.Axi4.Common import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike diff --git a/src/Protocols/Axi4/Raw/Full/WriteResponse.hs b/src/Protocols/Axi4/Partial/Full/WriteResponse.hs similarity index 97% rename from src/Protocols/Axi4/Raw/Full/WriteResponse.hs rename to src/Protocols/Axi4/Partial/Full/WriteResponse.hs index 598401aa..e1bba4d1 100644 --- a/src/Protocols/Axi4/Raw/Full/WriteResponse.hs +++ b/src/Protocols/Axi4/Partial/Full/WriteResponse.hs @@ -10,7 +10,7 @@ to the AXI4 specification. {-# OPTIONS_GHC -Wno-missing-fields #-} -module Protocols.Axi4.Raw.Full.WriteResponse +module Protocols.Axi4.Partial.Full.WriteResponse ( M2S_WriteResponse(..) , S2M_WriteResponse(..) , Axi4WriteResponse @@ -27,7 +27,7 @@ import qualified Clash.Prelude as C import Clash.Prelude ((:::)) -- me -import Protocols.Axi4.Raw.Common +import Protocols.Axi4.Common import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike diff --git a/src/Protocols/Axi4/Strict/Full.hs b/src/Protocols/Axi4/Strict/Full.hs new file mode 100644 index 00000000..08c7bd21 --- /dev/null +++ b/src/Protocols/Axi4/Strict/Full.hs @@ -0,0 +1,23 @@ +{-| +Defines the full AXI4 protocol with port names corresponding to the AXI4 +specification. + +Note that every individual channel is a DfLike-protocol, but the bundled version +is not. +-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} + +module Protocols.Axi4.Strict.Full + ( module ReadAddress + , module ReadData + , module WriteAddress + , module WriteData + , module WriteResponse + ) where + +import Protocols.Axi4.Strict.Full.ReadAddress as ReadAddress +import Protocols.Axi4.Strict.Full.ReadData as ReadData +import Protocols.Axi4.Strict.Full.WriteAddress as WriteAddress +import Protocols.Axi4.Strict.Full.WriteData as WriteData +import Protocols.Axi4.Strict.Full.WriteResponse as WriteResponse diff --git a/src/Protocols/Axi4/Strict/Full/ReadAddress.hs b/src/Protocols/Axi4/Strict/Full/ReadAddress.hs new file mode 100644 index 00000000..85092e87 --- /dev/null +++ b/src/Protocols/Axi4/Strict/Full/ReadAddress.hs @@ -0,0 +1,186 @@ +{-| +Defines ReadAddress channel of full AXI4 protocol with port names corresponding +to the AXI4 specification. +-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-missing-fields #-} + +module Protocols.Axi4.Strict.Full.ReadAddress + ( M2S_ReadAddress(..) + , S2M_ReadAddress(..) + , Axi4ReadAddress + ) where + +-- base +import Data.Coerce +import Data.Kind (Type) +import Data.Proxy +import GHC.Generics (Generic) + +-- clash-prelude +import qualified Clash.Prelude as C + +-- me +import Protocols.Axi4.Common +import Protocols.Internal +import Protocols.DfLike (DfLike) +import qualified Protocols.DfLike as DfLike + +-- | AXI4 Read Address channel protocol +data Axi4ReadAddress + (dom :: C.Domain) + (kb :: KeepBurst) + (ksz :: KeepSize) + (lw :: LengthWidth) + (iw :: IdWidth) + (aw :: AddrWidth) + (kr :: KeepRegion) + (kbl :: KeepBurstLength) + (kl :: KeepLock) + (kc :: KeepCache) + (kp :: KeepPermissions) + (kq :: KeepQos) + (userType :: Type) + +instance Protocol (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where + type Fwd (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = + C.Signal dom (M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) + type Bwd (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = + C.Signal dom S2M_ReadAddress + +instance Backpressure (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where + boolsToBwd _ = C.fromList_lazy . coerce + +instance DfLike dom (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType where + type Data (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType = + M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType + + type Payload userType = userType + + type Ack (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType = + S2M_ReadAddress + + getPayload _ (M2S_ReadAddress{_aruser}) = Just _aruser + getPayload _ M2S_NoReadAddress = Nothing + {-# INLINE getPayload #-} + + setPayload _ _ dat (Just b) = dat{_aruser=b} + setPayload _ dfB _ Nothing = DfLike.noData dfB + {-# INLINE setPayload #-} + + noData _ = M2S_NoReadAddress + {-# INLINE noData #-} + + boolToAck _ = coerce + {-# INLINE boolToAck #-} + + ackToBool _ = coerce + {-# INLINE ackToBool #-} + +instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) => + Simulate (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where + + type SimulateType (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = + [M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType] + + type ExpectType (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = + [M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType] + + type SimulateChannels (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = 1 + + toSimulateType _ = id + fromSimulateType _ = id + + driveC = DfLike.drive Proxy + sampleC = DfLike.sample Proxy + stallC conf (C.head -> (stallAck, stalls)) = + DfLike.stall Proxy conf stallAck stalls + +-- | See Table A2-5 "Read address channel signals" +data M2S_ReadAddress + (kb :: KeepBurst) + (ksz :: KeepSize) + (lw :: LengthWidth) + (iw :: IdWidth) + (aw :: AddrWidth) + (kr :: KeepRegion) + (kbl :: KeepBurstLength) + (kl :: KeepLock) + (kc :: KeepCache) + (kp :: KeepPermissions) + (kq :: KeepQos) + (userType :: Type) + = M2S_NoReadAddress + | M2S_ReadAddress + { -- | Read address id* + _arid :: !(C.BitVector (Width iw)) + + -- | Read address + , _araddr :: !(C.BitVector (Width aw)) + + -- | Read region* + , _arregion :: !(RegionType kr) + + -- | Burst length* + , _arlen :: !(BurstLengthType kbl) + + -- | Burst size* + , _arsize :: !(SizeType ksz) + + -- | Burst type* + , _arburst :: !(BurstType kb) + + -- | Lock type* + , _arlock :: !(LockType kl) + + -- | Cache type* (has been renamed to modifiable in AXI spec) + , _arcache :: !(CacheType kc) + + -- | Protection type + , _arprot :: !(PermissionsType kp) + + -- | QoS value + , _arqos :: !(QosType kq) + + -- | User data + , _aruser :: !userType + } + deriving (Generic) + +-- | See Table A2-5 "Read address channel signals" +newtype S2M_ReadAddress = S2M_ReadAddress + { _arready :: Bool } + deriving (Show, Generic, C.NFDataX) + +deriving instance + ( C.KnownNat (Width iw) + , C.KnownNat (Width aw) + , Show (SizeType ksz) + , Show (BurstType kb) + , Show userType + , Show (RegionType kr) + , Show (BurstLengthType kbl) + , Show (LockType kl) + , Show (CacheType kc) + , Show (PermissionsType kp) + , Show (QosType kq) ) => + Show (M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) + +deriving instance + ( C.NFDataX userType + , C.NFDataX (BurstType kb) + , C.NFDataX (SizeType ksz) + , C.NFDataX (BurstType kb) + , C.NFDataX userType + , C.NFDataX (RegionType kr) + , C.NFDataX (BurstLengthType kbl) + , C.NFDataX (LockType kl) + , C.NFDataX (CacheType kc) + , C.NFDataX (PermissionsType kp) + , C.NFDataX (QosType kq) ) => + C.NFDataX (M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) diff --git a/src/Protocols/Axi4/Strict/Full/ReadData.hs b/src/Protocols/Axi4/Strict/Full/ReadData.hs new file mode 100644 index 00000000..a559d49e --- /dev/null +++ b/src/Protocols/Axi4/Strict/Full/ReadData.hs @@ -0,0 +1,136 @@ +{-| +Defines ReadData channel of full AXI4 protocol with port names corresponding +to the AXI4 specification. +-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-missing-fields #-} + +module Protocols.Axi4.Strict.Full.ReadData + ( M2S_ReadData(..) + , S2M_ReadData(..) + , Axi4ReadData + ) where + +-- base +import Data.Coerce (coerce) +import Data.Kind (Type) +import GHC.Generics (Generic) +import Data.Proxy + +-- clash-prelude +import qualified Clash.Prelude as C + +-- me +import Protocols.Axi4.Common +import Protocols.Internal +import Protocols.DfLike (DfLike) +import qualified Protocols.DfLike as DfLike + +-- | AXI4 Read Data channel protocol +data Axi4ReadData + (dom :: C.Domain) + (kr :: KeepResponse) + (iw :: IdWidth) + (dataType :: Type) + (userType :: Type) + +instance Protocol (Axi4ReadData dom kr iw dataType userType) where + type Fwd (Axi4ReadData dom kr iw dataType userType) = + C.Signal dom (S2M_ReadData kr iw dataType userType) + type Bwd (Axi4ReadData dom kr iw dataType userType) = + C.Signal dom M2S_ReadData + +instance Backpressure (Axi4ReadData dom kr iw dataType userType) where + boolsToBwd _ = C.fromList_lazy . coerce + +instance DfLike dom (Axi4ReadData dom kr iw dataType) userType where + type Data (Axi4ReadData dom kr iw dataType) userType = + S2M_ReadData kr iw dataType userType + + type Payload userType = userType + + type Ack (Axi4ReadData dom kr iw dataType) userType = + M2S_ReadData + + getPayload _ (S2M_ReadData{_ruser}) = Just _ruser + getPayload _ S2M_NoReadData = Nothing + {-# INLINE getPayload #-} + + setPayload _ _ dat (Just b) = dat{_ruser=b} + setPayload _ dfB _ Nothing = DfLike.noData dfB + {-# INLINE setPayload #-} + + noData _ = S2M_NoReadData + {-# INLINE noData #-} + + boolToAck _ = coerce + {-# INLINE boolToAck #-} + + ackToBool _ = coerce + {-# INLINE ackToBool #-} + +instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) => + Simulate (Axi4ReadData dom kr iw dataType userType) where + + type SimulateType (Axi4ReadData dom kr iw dataType userType) = + [S2M_ReadData kr iw dataType userType] + + type ExpectType (Axi4ReadData dom kr iw dataType userType) = + [S2M_ReadData kr iw dataType userType] + + type SimulateChannels (Axi4ReadData dom kr iw dataType userType) = 1 + + toSimulateType _ = id + fromSimulateType _ = id + + driveC = DfLike.drive Proxy + sampleC = DfLike.sample Proxy + stallC conf (C.head -> (stallAck, stalls)) = + DfLike.stall Proxy conf stallAck stalls + +-- | See Table A2-6 "Read data channel signals" +data S2M_ReadData + (kr :: KeepResponse) + (iw :: IdWidth) + (dataType :: Type) + (userType :: Type) + = S2M_NoReadData + | S2M_ReadData + { -- | Read address id* + _rid :: !(C.BitVector (Width iw)) + + , -- | Read data + _rdata :: !dataType + + -- | Read response + , _rresp :: !(ResponseType kr) + + -- | Read last + , _rlast :: !Bool + + -- | User data + , _ruser :: !userType + } + deriving (Generic) + +-- | See Table A2-6 "Read data channel signals" +newtype M2S_ReadData = M2S_ReadData { _rready :: Bool } + deriving (Show, Generic, C.NFDataX) + +deriving instance + ( C.NFDataX userType + , C.NFDataX dataType + , C.NFDataX (ResponseType kr) ) => + C.NFDataX (S2M_ReadData kr iw dataType userType) + +deriving instance + ( C.KnownNat (Width iw) + , Show userType + , Show dataType + , Show (ResponseType kr) ) => + Show (S2M_ReadData kr iw dataType userType) diff --git a/src/Protocols/Axi4/Strict/Full/WriteAddress.hs b/src/Protocols/Axi4/Strict/Full/WriteAddress.hs new file mode 100644 index 00000000..37391c1d --- /dev/null +++ b/src/Protocols/Axi4/Strict/Full/WriteAddress.hs @@ -0,0 +1,185 @@ +{-| +Defines WriteAddress channel of full AXI4 protocol with port names corresponding +to the AXI4 specification. +-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-missing-fields #-} + +module Protocols.Axi4.Strict.Full.WriteAddress + ( M2S_WriteAddress(..) + , S2M_WriteAddress(..) + , Axi4WriteAddress + ) where + +-- base +import Data.Coerce (coerce) +import Data.Kind (Type) +import Data.Proxy +import GHC.Generics (Generic) + +-- clash-prelude +import qualified Clash.Prelude as C + +-- me +import Protocols.Axi4.Common +import Protocols.Internal +import Protocols.DfLike (DfLike) +import qualified Protocols.DfLike as DfLike + +-- | AXI4 Write Address channel protocol +data Axi4WriteAddress + (dom :: C.Domain) + (kb :: KeepBurst) + (ksz :: KeepSize) + (lw :: LengthWidth) + (iw :: IdWidth) + (aw :: AddrWidth) + (kr :: KeepRegion) + (kbl :: KeepBurstLength) + (kl :: KeepLock) + (kc :: KeepCache) + (kp :: KeepPermissions) + (kq :: KeepQos) + (userType :: Type) + +instance Protocol (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where + type Fwd (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = + C.Signal dom (M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) + type Bwd (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = + C.Signal dom S2M_WriteAddress + +instance Backpressure (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where + boolsToBwd _ = C.fromList_lazy . coerce + +instance DfLike dom (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType where + type Data (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType = + M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType + + type Payload userType = userType + + type Ack (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType = + S2M_WriteAddress + + getPayload _ (M2S_WriteAddress{_awuser}) = Just _awuser + getPayload _ M2S_NoWriteAddress = Nothing + {-# INLINE getPayload #-} + + setPayload _ _ dat (Just b) = dat{_awuser=b} + setPayload _ dfB _ Nothing = DfLike.noData dfB + {-# INLINE setPayload #-} + + noData _ = M2S_NoWriteAddress + {-# INLINE noData #-} + + boolToAck _ = coerce + {-# INLINE boolToAck #-} + + ackToBool _ = coerce + {-# INLINE ackToBool #-} + +instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) => + Simulate (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where + + type SimulateType (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = + [M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType] + + type ExpectType (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = + [M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType] + + type SimulateChannels (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = 1 + + toSimulateType _ = id + fromSimulateType _ = id + + driveC = DfLike.drive Proxy + sampleC = DfLike.sample Proxy + stallC conf (C.head -> (stallAck, stalls)) = + DfLike.stall Proxy conf stallAck stalls + +-- | See Table A2-2 "Write address channel signals" +data M2S_WriteAddress + (kb :: KeepBurst) + (ksz :: KeepSize) + (lw :: LengthWidth) + (iw :: IdWidth) + (aw :: AddrWidth) + (kr :: KeepRegion) + (kbl :: KeepBurstLength) + (kl :: KeepLock) + (kc :: KeepCache) + (kp :: KeepPermissions) + (kq :: KeepQos) + (userType :: Type) + = M2S_NoWriteAddress + | M2S_WriteAddress + { -- | Write address id* + _awid :: !(C.BitVector (Width iw)) + + -- | Write address + , _awaddr :: !(C.BitVector (Width aw)) + + -- | Write region* + , _awregion:: !(RegionType kr) + + -- | Burst length* + , _awlen :: !(BurstLengthType kbl) + + -- | Burst size* + , _awsize :: !(SizeType ksz) + + -- | Burst type* + , _awburst :: !(BurstType kb) + + -- | Lock type* + , _awlock :: !(LockType kl) + + -- | Cache type* + , _awcache :: !(CacheType kc) + + -- | Protection type + , _awprot :: !(PermissionsType kp) + + -- | QoS value + , _awqos :: !(QosType kq) + + -- | User data + , _awuser :: !userType + } + deriving (Generic) + +-- | See Table A2-2 "Write address channel signals" +newtype S2M_WriteAddress = S2M_WriteAddress { _awready :: Bool } + deriving (Show, Generic, C.NFDataX) + +deriving instance + ( C.KnownNat (Width iw) + , C.KnownNat (Width aw) + , Show (SizeType ksz) + , Show (BurstType kb) + , Show userType + , Show (RegionType kr) + , Show (BurstLengthType kbl) + , Show (LockType kl) + , Show (CacheType kc) + , Show (PermissionsType kp) + , Show (QosType kq) ) => + Show (M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) + +deriving instance + ( C.NFDataX userType + , C.NFDataX (BurstType kb) + , C.NFDataX (SizeType ksz) + , C.NFDataX (BurstType kb) + , C.NFDataX userType + , C.NFDataX (RegionType kr) + , C.NFDataX (BurstLengthType kbl) + , C.NFDataX (LockType kl) + , C.NFDataX (CacheType kc) + , C.NFDataX (PermissionsType kp) + , C.NFDataX (QosType kq) ) => + C.NFDataX (M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) diff --git a/src/Protocols/Axi4/Strict/Full/WriteData.hs b/src/Protocols/Axi4/Strict/Full/WriteData.hs new file mode 100644 index 00000000..2029b850 --- /dev/null +++ b/src/Protocols/Axi4/Strict/Full/WriteData.hs @@ -0,0 +1,129 @@ +{-| +Defines WriteData channel of full AXI4 protocol with port names corresponding +to the AXI4 specification. +-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-missing-fields #-} + +module Protocols.Axi4.Strict.Full.WriteData + ( M2S_WriteData(..) + , S2M_WriteData(..) + , Axi4WriteData + ) where + +-- base +import Data.Coerce (coerce) +import Data.Kind (Type) +import GHC.Generics (Generic) +import GHC.TypeNats (Nat) +import Data.Proxy + +-- clash-prelude +import qualified Clash.Prelude as C + +-- me +import Protocols.Axi4.Common +import Protocols.Internal +import Protocols.DfLike (DfLike) +import qualified Protocols.DfLike as DfLike + +-- | AXI4 Write Data channel protocol +data Axi4WriteData + (dom :: C.Domain) + (ks :: KeepStrobe) + (nBytes :: Nat) + (userType :: Type) + +instance Protocol (Axi4WriteData dom ks nBytes userType) where + type Fwd (Axi4WriteData dom ks nBytes userType) = + C.Signal dom (M2S_WriteData ks nBytes userType) + type Bwd (Axi4WriteData dom ks nBytes userType) = + C.Signal dom S2M_WriteData + +instance Backpressure (Axi4WriteData dom ks dataType userType) where + boolsToBwd _ = C.fromList_lazy . coerce + +instance DfLike dom (Axi4WriteData dom ks dataType) userType where + type Data (Axi4WriteData dom ks dataType) userType = + M2S_WriteData ks dataType userType + + type Payload userType = userType + + type Ack (Axi4WriteData dom ks dataType) userType = + S2M_WriteData + + getPayload _ (M2S_WriteData{_wuser}) = Just _wuser + getPayload _ _ = Nothing + {-# INLINE getPayload #-} + + setPayload _ _ dat (Just b) = dat{_wuser=b} + setPayload _ dfB _ Nothing = DfLike.noData dfB + {-# INLINE setPayload #-} + + noData _ = M2S_NoWriteData + {-# INLINE noData #-} + + boolToAck _ = coerce + {-# INLINE boolToAck #-} + + ackToBool _ = coerce + {-# INLINE ackToBool #-} + +instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) => + Simulate (Axi4WriteData dom ks nBytes userType) where + + type SimulateType (Axi4WriteData dom ks nBytes userType) = + [M2S_WriteData ks nBytes userType] + + type ExpectType (Axi4WriteData dom ks nBytes userType) = + [M2S_WriteData ks nBytes userType] + + type SimulateChannels (Axi4WriteData dom ks nBytes userType) = 1 + + toSimulateType _ = id + fromSimulateType _ = id + + driveC = DfLike.drive Proxy + sampleC = DfLike.sample Proxy + stallC conf (C.head -> (stallAck, stalls)) = + DfLike.stall Proxy conf stallAck stalls + +-- | See Table A2-3 "Write data channel signals". If strobing is kept, the data +-- will be a vector of 'Maybe' bytes. If strobing is not kept, data will be a +-- 'BitVector'. +data M2S_WriteData + (ks :: KeepStrobe) + (nBytes :: Nat) + (userType :: Type) + = M2S_NoWriteData + | M2S_WriteData + { -- | Write data + _wdata :: !(StrictStrobeType nBytes ks) + + -- | Write last + , _wlast :: !Bool + + -- | User data + , _wuser :: !userType + } + deriving (Generic) + +-- | See Table A2-3 "Write data channel signals" +newtype S2M_WriteData = S2M_WriteData { _wready :: Bool } + deriving (Show, Generic, C.NFDataX) + +deriving instance + ( C.NFDataX userType + , C.NFDataX (StrictStrobeType nBytes ks) ) => + C.NFDataX (M2S_WriteData ks nBytes userType) + +deriving instance + ( Show userType + , Show (StrictStrobeType nBytes ks) + , C.KnownNat nBytes ) => + Show (M2S_WriteData ks nBytes userType) diff --git a/src/Protocols/Axi4/Strict/Full/WriteResponse.hs b/src/Protocols/Axi4/Strict/Full/WriteResponse.hs new file mode 100644 index 00000000..c86935ba --- /dev/null +++ b/src/Protocols/Axi4/Strict/Full/WriteResponse.hs @@ -0,0 +1,126 @@ +{-| +Defines WriteResponse channel of full AXI4 protocol with port names corresponding +to the AXI4 specification. +-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-missing-fields #-} + +module Protocols.Axi4.Strict.Full.WriteResponse + ( M2S_WriteResponse(..) + , S2M_WriteResponse(..) + , Axi4WriteResponse + ) where + +-- base +import Data.Coerce (coerce) +import Data.Kind (Type) +import GHC.Generics (Generic) +import Data.Proxy + +-- clash-prelude +import qualified Clash.Prelude as C + +-- me +import Protocols.Axi4.Common +import Protocols.Internal +import Protocols.DfLike (DfLike) +import qualified Protocols.DfLike as DfLike + +-- | AXI4 Read Data channel protocol +data Axi4WriteResponse + (dom :: C.Domain) + (kr :: KeepResponse) + (iw :: IdWidth) + (userType :: Type) + +instance Protocol (Axi4WriteResponse dom kr iw userType) where + type Fwd (Axi4WriteResponse dom kr iw userType) = + C.Signal dom (S2M_WriteResponse kr iw userType) + type Bwd (Axi4WriteResponse dom kr iw userType) = + C.Signal dom M2S_WriteResponse + +instance Backpressure (Axi4WriteResponse dom kr iw userType) where + boolsToBwd _ = C.fromList_lazy . coerce + +instance DfLike dom (Axi4WriteResponse dom kr iw) userType where + type Data (Axi4WriteResponse dom kr iw) userType = + S2M_WriteResponse kr iw userType + + type Payload userType = userType + + type Ack (Axi4WriteResponse dom kr iw) userType = + M2S_WriteResponse + + getPayload _ (S2M_WriteResponse{_buser}) = Just _buser + getPayload _ _ = Nothing + {-# INLINE getPayload #-} + + setPayload _ _ dat (Just b) = dat{_buser=b} + setPayload _ dfB _ Nothing = DfLike.noData dfB + {-# INLINE setPayload #-} + + noData _ = S2M_NoWriteResponse + {-# INLINE noData #-} + + boolToAck _ = coerce + {-# INLINE boolToAck #-} + + ackToBool _ = coerce + {-# INLINE ackToBool #-} + +instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) => + Simulate (Axi4WriteResponse dom kr iw userType) where + + type SimulateType (Axi4WriteResponse dom kr iw userType) = + [S2M_WriteResponse kr iw userType] + + type ExpectType (Axi4WriteResponse dom kr iw userType) = + [S2M_WriteResponse kr iw userType] + + type SimulateChannels (Axi4WriteResponse dom kr iw userType) = 1 + + toSimulateType _ = id + fromSimulateType _ = id + + driveC = DfLike.drive Proxy + sampleC = DfLike.sample Proxy + stallC conf (C.head -> (stallAck, stalls)) = + DfLike.stall Proxy conf stallAck stalls + +-- | See Table A2-4 "Write response channel signals" +data S2M_WriteResponse + (kr :: KeepResponse) + (iw :: IdWidth) + (userType :: Type) + = S2M_NoWriteResponse + | S2M_WriteResponse + { -- | Response ID + _bid :: !(C.BitVector (Width iw)) + + -- | Write response + , _bresp :: !(ResponseType kr) + + -- | User data + , _buser :: !userType + } + deriving (Generic) + +-- | See Table A2-4 "Write response channel signals" +newtype M2S_WriteResponse = M2S_WriteResponse { _bready :: Bool } + deriving (Show, Generic, C.NFDataX) + +deriving instance + ( C.NFDataX userType + , C.NFDataX (ResponseType kr) ) => + C.NFDataX (S2M_WriteResponse kr iw userType) + +deriving instance + ( Show userType + , Show (ResponseType kr) + , C.KnownNat (Width iw) ) => + Show (S2M_WriteResponse kr iw userType)