From 32b6d0909e50eea549567ca60a1f48fe126337cf Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Tue, 5 Jan 2021 15:16:34 +0100 Subject: [PATCH 01/12] Drop injectivity requirement of Bwd --- src/Protocols/Df.hs | 21 +++++------------ src/Protocols/DfLike.hs | 3 ++- src/Protocols/Internal.hs | 47 ++++++++++++++++++--------------------- 3 files changed, 30 insertions(+), 41 deletions(-) diff --git a/src/Protocols/Df.hs b/src/Protocols/Df.hs index 26f18707..a8ab8412 100644 --- a/src/Protocols/Df.hs +++ b/src/Protocols/Df.hs @@ -16,7 +16,7 @@ carries data, no metadata. For documentation see: module Protocols.Df ( -- * Types - Df, Data(..), Ack(..) + Df, Data(..) -- * Operations on Df like protocols , const, void, pure @@ -65,7 +65,6 @@ import Prelude hiding import Data.Bifunctor (Bifunctor) import Data.Coerce (coerce) -import Data.Default (Default) import Data.Kind (Type) import qualified Data.Maybe as Maybe import Data.Proxy @@ -77,7 +76,7 @@ import Clash.Signal.Internal (Signal) import qualified Clash.Prelude as C -- me -import Protocols.Internal hiding (Ack(..)) +import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike @@ -98,11 +97,11 @@ instance Protocol (Df dom a) where -- | Forward part of simple dataflow: @Signal dom (Data meta a)@ type Fwd (Df dom a) = Signal dom (Data a) - -- | Backward part of simple dataflow: @Signal dom (Ack meta a)@ - type Bwd (Df dom a) = Signal dom (Ack a) + -- | Backward part of simple dataflow: @Signal dom Bool@ + type Bwd (Df dom a) = Signal dom Ack instance Backpressure (Df dom a) where - boolsToBwd = C.fromList_lazy . coerce + boolsToBwd _ = C.fromList_lazy . coerce -- | Data sent over forward channel of 'Df'. Note that this data type is strict -- on its data field. @@ -135,14 +134,6 @@ dataToMaybe :: Data a -> Maybe a dataToMaybe NoData = Nothing dataToMaybe (Data a) = Just a --- | Like 'Protocols.Df.Ack', but carrying phantom type variables to satisfy --- 'Bwd's injectivity requirement. -newtype Ack a = Ack Bool - deriving (Show) - -instance Default (Ack a) where - def = Ack True - instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom a) where type SimulateType (Df dom a) = [Data a] type ExpectType (Df dom a) = [a] @@ -158,7 +149,7 @@ instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom instance DfLike dom (Df dom) a where type Data (Df dom) a = Data a type Payload a = a - type Ack (Df dom) a = Ack a + type Ack (Df dom) a = Ack getPayload _ (Data a) = Just a getPayload _ NoData = Nothing diff --git a/src/Protocols/DfLike.hs b/src/Protocols/DfLike.hs index f6e7cc59..844ce715 100644 --- a/src/Protocols/DfLike.hs +++ b/src/Protocols/DfLike.hs @@ -96,7 +96,7 @@ class ( Protocol (df a) type Payload a = (r :: Type) | r -> a -- | Acknowledgement data carried on backward channel - type Ack df a = (r :: Type) | r -> a + type Ack df a noData :: Proxy (df a) -> @@ -108,6 +108,7 @@ class ( Protocol (df a) Maybe (Payload a) setPayload :: + HasCallStack => DfLike dom df b => Proxy (df a) -> Proxy (df b) -> diff --git a/src/Protocols/Internal.hs b/src/Protocols/Internal.hs index 066482eb..03023854 100644 --- a/src/Protocols/Internal.hs +++ b/src/Protocols/Internal.hs @@ -98,19 +98,16 @@ import GHC.Generics (Generic) -- data. Similar to /Bool/ we define: -- -- @ --- data Ack a = DfNack | Ack +-- newtype Ack = Ack Bool -- @ -- --- (For technical reasons[1] we need the type variable /a/ in this definition, --- even though we don't use it on the right hand side.) --- -- With these three definitions we're ready to make an instance for /Fwd/ and -- /Bwd/: -- -- @ -- instance Protocol (Df dom a) where -- type Fwd (Df dom a) = Signal dom (Data a) --- type Bwd (Df dom a) = Signal dom (Ack a) +-- type Bwd (Df dom a) = Signal dom Ack -- @ -- -- Having defined all this, we can take a look at /Circuit/ once more: now @@ -128,7 +125,7 @@ import GHC.Generics (Generic) -- +------------------------>+ +-------------------------> -- | | -- | | --- Signal dom (Ack a) | | Signal dom (Ack b) +-- Signal dom Ack | | Signal dom Ack -- <-------------------------+ +<------------------------+ -- | | -- +-----------+ @@ -141,15 +138,6 @@ import GHC.Generics (Generic) -- -- 2. It eliminates the need for manually routing acknowledgement lines -- --- Footnotes: --- --- 1. Fwd and Bwd are injective type families. I.e., something on --- the right hand side of a type instance must uniquely identify the left --- hand side and vice versa. This helps type inference and error messages --- substantially, in exchange for a slight syntactical artifact. As a --- result, any type variables on the left hand side must occur on the right --- hand side too. --- newtype Circuit a b = Circuit ( (Fwd a, Bwd b) -> (Bwd a, Fwd b) ) @@ -157,11 +145,17 @@ newtype Circuit a b = newtype Ack = Ack Bool deriving (Generic, C.NFDataX) +-- | Acknowledge. Used in circuit-notation plugin to drive ignore components. +instance Default Ack where + def = Ack True + -- | Circuit protocol with /CSignal dom a/ in its forward direction, and -- /CSignal dom ()/ in its backward direction. Convenient for exposing -- protocol internals. data CSignal dom a = CSignal (Signal dom a) +instance Default a => Default (CSignal dom a) where + def = CSignal def -- | A protocol describes the in- and outputs of one side of a 'Circuit'. class Protocol a where @@ -171,7 +165,7 @@ class Protocol a where -- | Receiver to sender type family. See 'Circuit' for an explanation on the -- existence of 'Bwd'. - type Bwd (a :: Type) = (r :: Type) | r -> a + type Bwd (a :: Type) instance Protocol () where type Fwd () = () @@ -196,7 +190,7 @@ instance C.KnownNat n => Protocol (C.Vec n a) where -- XXX: Type families with Signals on LHS are currently broken on Clash: instance Protocol (CSignal dom a) where type Fwd (CSignal dom a) = CSignal dom a - type Bwd (CSignal dom a) = CSignal dom (Const () a) + type Bwd (CSignal dom a) = CSignal dom () -- | Left-to-right circuit composition. -- @@ -231,22 +225,25 @@ infixr 1 |> class Protocol a => Backpressure a where -- | Interpret list of booleans as a list of acknowledgements at every cycle. -- Implementations don't have to account for finite lists. - boolsToBwd :: [Bool] -> Bwd a + boolsToBwd :: Proxy a -> [Bool] -> Bwd a instance Backpressure () where - boolsToBwd _ = () + boolsToBwd _ _ = () instance (Backpressure a, Backpressure b) => Backpressure (a, b) where - boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs) + boolsToBwd _ bs = (boolsToBwd (Proxy @a) bs, boolsToBwd (Proxy @b) bs) instance (Backpressure a, Backpressure b, Backpressure c) => Backpressure (a, b, c) where - boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs, boolsToBwd bs) + boolsToBwd _ bs = + ( boolsToBwd (Proxy @a) bs + , boolsToBwd (Proxy @b) bs + , boolsToBwd (Proxy @c) bs ) instance (C.KnownNat n, Backpressure a) => Backpressure (C.Vec n a) where - boolsToBwd bs = C.repeat (boolsToBwd bs) + boolsToBwd _ bs = C.repeat (boolsToBwd (Proxy @a) bs) instance Backpressure (CSignal dom a) where - boolsToBwd _ = CSignal (pure (Const ())) + boolsToBwd _ _ = CSignal (pure ()) -- | Right-to-left circuit composition. -- @@ -480,7 +477,7 @@ instance (Simulate a, Simulate b) => Simulate (a, b) where sampleC conf (Circuit f) = let bools = replicate (resetCycles conf) False <> repeat True - (_, (fwd1, fwd2)) = f ((), (boolsToBwd bools, boolsToBwd bools)) + (_, (fwd1, fwd2)) = f ((), (boolsToBwd (Proxy @a) bools, boolsToBwd (Proxy @b) bools)) in ( sampleC conf (Circuit $ \_ -> ((), fwd1)) , sampleC conf (Circuit $ \_ -> ((), fwd2)) ) @@ -517,7 +514,7 @@ instance (C.KnownNat n, Simulate a) => Simulate (C.Vec n a) where sampleC conf (Circuit f) = let bools = replicate (resetCycles conf) False <> repeat True - (_, fwds) = f ((), (C.repeat (boolsToBwd bools))) + (_, fwds) = f ((), (C.repeat (boolsToBwd (Proxy @a) bools))) in C.map (\fwd -> sampleC conf (Circuit $ \_ -> ((), fwd))) fwds From 42b390d131115a1b67f41b944fb0d4cf11b4d8f6 Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Mon, 4 Jan 2021 17:07:22 +0100 Subject: [PATCH 02/12] Cleanup --- src/Protocols/Df.hs | 14 -------------- src/Protocols/DfLike.hs | 2 +- 2 files changed, 1 insertion(+), 15 deletions(-) diff --git a/src/Protocols/Df.hs b/src/Protocols/Df.hs index a8ab8412..4148a295 100644 --- a/src/Protocols/Df.hs +++ b/src/Protocols/Df.hs @@ -168,20 +168,6 @@ instance DfLike dom (Df dom) a where ackToBool _ = coerce {-# INLINE ackToBool #-} --- | Interpret simple dataflow carrying a tuple as 'Df' with /meta/ and /payload/ --- asDf :: Circuit (Df dom (meta, payload)) (Df dom meta payload) --- asDf = Df.mapInternal (B.swapMap go coerce) --- where --- go (Data (meta, a)) = Df.Data meta a --- go NoData = Df.NoData - --- -- | Interpret 'Df' as simple dataflow carrying a tuple of /meta/ and /payload/ --- asDf :: Circuit (Df dom meta payload) (Df dom (meta, payload)) --- asDf = Df.mapInternal (B.swapMap go coerce) --- where --- go (Df.Data meta a) = Data (meta, a) --- go Df.NoData = NoData - -- | Force a /nack/ on the backward channel and /no data/ on the forward -- channel if reset is asserted. forceResetSanity :: forall dom a. C.HiddenClockResetEnable dom => Circuit (Df dom a) (Df dom a) diff --git a/src/Protocols/DfLike.hs b/src/Protocols/DfLike.hs index 844ce715..50373b6b 100644 --- a/src/Protocols/DfLike.hs +++ b/src/Protocols/DfLike.hs @@ -67,6 +67,7 @@ import Data.Kind (Type) import qualified Data.Maybe as Maybe import Data.Proxy (Proxy(..)) import qualified Data.List.NonEmpty +import Data.List ((\\)) import GHC.Stack (HasCallStack) -- me @@ -77,7 +78,6 @@ import Clash.Prelude (Domain, type (+), type (-), type (<=)) import Clash.Signal.Internal (Signal(..)) import qualified Clash.Prelude as C import qualified Clash.Explicit.Prelude as CE -import Data.List ((\\)) -- | Generalization of Df-like protocols (Df, DfMeta, AXI, Avalon, ..). This From 9919236e975769c6da0efb22ca99831c712b775d Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Mon, 4 Jan 2021 10:16:12 +0100 Subject: [PATCH 03/12] Add AXI4 definitions --- clash-protocols.cabal | 9 + src/Protocols.hs | 2 +- src/Protocols/Axi4/Full.hs | 0 src/Protocols/Axi4/Raw/Common.hs | 264 +++++++++++++++++++ src/Protocols/Axi4/Raw/Full.hs | 25 ++ src/Protocols/Axi4/Raw/Full/ReadAddress.hs | 189 +++++++++++++ src/Protocols/Axi4/Raw/Full/ReadData.hs | 140 ++++++++++ src/Protocols/Axi4/Raw/Full/WriteAddress.hs | 189 +++++++++++++ src/Protocols/Axi4/Raw/Full/WriteData.hs | 134 ++++++++++ src/Protocols/Axi4/Raw/Full/WriteResponse.hs | 130 +++++++++ src/Protocols/Internal.hs | 6 + 11 files changed, 1087 insertions(+), 1 deletion(-) create mode 100644 src/Protocols/Axi4/Full.hs create mode 100644 src/Protocols/Axi4/Raw/Common.hs create mode 100644 src/Protocols/Axi4/Raw/Full.hs create mode 100644 src/Protocols/Axi4/Raw/Full/ReadAddress.hs create mode 100644 src/Protocols/Axi4/Raw/Full/ReadData.hs create mode 100644 src/Protocols/Axi4/Raw/Full/WriteAddress.hs create mode 100644 src/Protocols/Axi4/Raw/Full/WriteData.hs create mode 100644 src/Protocols/Axi4/Raw/Full/WriteResponse.hs diff --git a/clash-protocols.cabal b/clash-protocols.cabal index 352e6534..cbd80d4e 100644 --- a/clash-protocols.cabal +++ b/clash-protocols.cabal @@ -137,6 +137,15 @@ 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.Df Protocols.DfLike Protocols.Hedgehog diff --git a/src/Protocols.hs b/src/Protocols.hs index 627c3c62..427e6a47 100644 --- a/src/Protocols.hs +++ b/src/Protocols.hs @@ -47,7 +47,7 @@ module Protocols , def -- * Circuit notation plugin - , circuit + , circuit, (-<) ) where import Data.Default (def) diff --git a/src/Protocols/Axi4/Full.hs b/src/Protocols/Axi4/Full.hs new file mode 100644 index 00000000..e69de29b diff --git a/src/Protocols/Axi4/Raw/Common.hs b/src/Protocols/Axi4/Raw/Common.hs new file mode 100644 index 00000000..f80045da --- /dev/null +++ b/src/Protocols/Axi4/Raw/Common.hs @@ -0,0 +1,264 @@ +{-| +Types and utilities shared between AXI4, AXI4-Lite, and AXI3. +-} +{-# LANGUAGE UndecidableInstances #-} + +module Protocols.Axi4.Raw.Common 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 (^), type (-)) + +-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol +data IdWidth = IdWidth Nat deriving (Show) + +-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol +data AddrWidth = AddrWidth Nat deriving (Show) + +-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol +data LengthWidth = LengthWidth Nat deriving (Show) + +-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol +data UserType = UserType Type KeepStrobe + +-- | Keep or remove Burst, see 'BurstMode' +data KeepBurst = KeepBurst | NoBurst deriving (Show) + +-- | Keep or remove Burst Length, see 'BurstSize' +data KeepBurstLength = KeepBurstLength | NoBurstLength deriving (Show) + +-- | Keep or remove cache field, see 'Cache' +data KeepCache = KeepCache | NoCache deriving (Show) + +-- | Keep or remove last field +data KeepLast = KeepLast | NoLast deriving (Show) + +-- | Keep or remove lock, see 'AtomicAccess' +data KeepLock = KeepLock | NoLock deriving (Show) + +-- | Keep or remove permissions, see 'Privileged', 'Secure', and +-- 'InstructionOrData'. +data KeepPermissions = KeepPermissions | NoPermissions deriving (Show) + +-- | Keep or remove quality of service field. See 'Qos'. +data KeepQos = KeepQos | NoQos deriving (Show) + +-- | Keep or remove region field +data KeepRegion = KeepRegion | NoRegion deriving (Show) + +-- | Keep or remove response field. See 'Resp'. +data KeepResponse = KeepResponse | NoResponse deriving (Show) + +-- | Keep or remove burst size field. See 'BurstSize'. +data KeepSize = KeepSize | NoSize deriving (Show) + +-- | Keep or remove strobe field. See 'Strobe' +data KeepStrobe = KeepStrobe | NoStrobe deriving (Show) + +-- | Extracts Nat from 'IdWidth', 'AddrWidth', and 'LengthWidth' +type family Width (a :: k) :: Nat where + Width ('IdWidth n) = n + Width ('AddrWidth n) = n + Width ('LengthWidth n) = n + +-- | Enables or disables 'BurstMode' +type family BurstType (keepBurst :: KeepBurst) where + BurstType 'KeepBurst = BurstMode + BurstType 'NoBurst = () + +-- | Enables or disables burst length +type family BurstLengthType (keepBurstLength :: KeepBurstLength) where + BurstLengthType 'KeepBurstLength = C.Index (2^8) + BurstLengthType 'NoBurstLength = () + +-- | Enables or disables 'Cache' +type family CacheType (keepCache :: KeepCache) where + CacheType 'KeepCache = Cache + CacheType 'NoCache = () + +-- | Enables or disables a boolean indicating whether a transaction is done +type family LastType (keepLast :: KeepLast) where + LastType 'KeepLast = Bool + LastType 'NoLast = () + +-- | Enables or disables 'AtomicAccess' +type family LockType (keepLockType :: KeepLock) where + LockType 'KeepLock = AtomicAccess + LockType 'NoLock = () + +-- | Enables or disables 'Privileged', 'Secure', and 'InstructionOrData' +type family PermissionsType (keepPermissions :: KeepPermissions) where + PermissionsType 'KeepPermissions = (Privileged, Secure, InstructionOrData) + PermissionsType 'NoPermissions = () + +-- | Enables or disables 'Qos' +type family QosType (keepQos :: KeepQos) where + QosType 'KeepQos = Qos + QosType 'NoQos = () + +-- | Enables or disables region type +type family RegionType (keepRegion :: KeepRegion) where + RegionType 'KeepRegion = C.BitVector 4 + RegionType 'NoRegion = () + +-- | Enables or disables 'Resp' +type family ResponseType (keepResponse :: KeepResponse) where + ResponseType 'KeepResponse = Resp + ResponseType 'NoResponse = () + +-- | Enables or disables 'BurstSize' +type family SizeType (keepSize :: KeepSize) where + SizeType 'KeepSize = BurstSize + SizeType 'NoSize = () + +-- | Enable or disable 'Strobe' +type family StrobeType (byteSize :: Nat) (keepStrobe :: KeepStrobe) where + StrobeType byteSize 'KeepStrobe = Strobe byteSize + StrobeType byteSize 'NoStrobe = () + +-- | Indicates valid bytes on data field. +type Strobe (byteSize :: Nat) = C.BitVector byteSize + +-- | The protocol does not specify the exact use of the QoS identifier. This +-- specification recommends that AxQOS is used as a priority indicator for the +-- associated write or read transaction. A higher value indicates a higher +-- priority transaction. +-- +-- A default value of 0 indicates that the interface is not participating in any +-- QoS scheme. +type Qos = C.Index ((2^4) - 1) + +-- | The burst type and the size information, determine how the address for +-- each transfer within the burst is calculated. +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 + 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) + +-- | Convert burst size to a numeric value +burstSizeToNum :: Num a => BurstSize -> a +burstSizeToNum = \case + Bs1 -> 1 + Bs2 -> 2 + Bs4 -> 4 + Bs8 -> 8 + Bs16 -> 16 + Bs32 -> 32 + Bs64 -> 64 + Bs128 -> 128 + +-- | Whether a transaction is bufferable +data Bufferable = NonBufferable | Bufferable + +-- | When set to "LookupCache", it is recommended that this transaction is +-- allocated in the cache for performance reasons. +data Allocate = NoLookupCache | LookupCache + +-- | When set to "OtherLookupCache", it is recommended that this transaction is +-- allocated in the cache for performance reasons. +data OtherAllocate = OtherNoLookupCache | OtherLookupCache + +-- | See Table A4-3 AWCACHE bit allocations +type Cache = (Bufferable, Modifiable, OtherAllocate, Allocate) + +-- | Status of the write transaction. +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) + +-- | Whether a resource is accessed with exclusive access or not +data AtomicAccess + = NonExclusiveAccess + | ExclusiveAccess + +-- | Whether transaction can be modified +data Modifiable + = Modifiable + | NonModifiable + +-- | An AXI master might support Secure and Non-secure operating states, and +-- extend this concept of security to memory access. +data Secure + = Secure + | NonSecure + +-- | An AXI master might support more than one level of operating privilege, +-- and extend this concept of privilege to memory access. +data Privileged + = NotPrivileged + | Privileged + +-- | Whether the transaction is an instruction access or a data access. The AXI +-- protocol defines this indication as a hint. It is not accurate in all cases, +-- for example, where a transaction contains a mix of instruction and data +-- items. This specification recommends that a master sets it to "Data", to +-- indicate a data access unless the access is specifically known to be an +-- instruction access. +data InstructionOrData + = Data + | Instruction diff --git a/src/Protocols/Axi4/Raw/Full.hs b/src/Protocols/Axi4/Raw/Full.hs new file mode 100644 index 00000000..86af742e --- /dev/null +++ b/src/Protocols/Axi4/Raw/Full.hs @@ -0,0 +1,25 @@ +{-| +Defines the full AXI4 protocol with port names corresponding to the AXI4 +specification. Because some fields are defined partially, it's not advised to +use this in Clash designs. Instead, look at (losslessly) converting it to +"Protocols.Axi4.Full" or (losslessy or lossy) converting it to "Protocols.Df". + +Note that every individual channel is a DfLike-protocol, but the bundled version +is not. +-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} + +module Protocols.Axi4.Raw.Full + ( module ReadAddress + , module ReadData + , module WriteAddress + , module WriteData + , 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 diff --git a/src/Protocols/Axi4/Raw/Full/ReadAddress.hs b/src/Protocols/Axi4/Raw/Full/ReadAddress.hs new file mode 100644 index 00000000..a1fbbd31 --- /dev/null +++ b/src/Protocols/Axi4/Raw/Full/ReadAddress.hs @@ -0,0 +1,189 @@ +{-| +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.Raw.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 +import Clash.Prelude ((:::)) + +-- me +import Protocols.Axi4.Raw.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{_arvalid=True, _aruser}) = Just _aruser + getPayload _ _ = Nothing + {-# INLINE getPayload #-} + + setPayload _ _ dat (Just b) = dat{_arvalid=True, _aruser=b} + setPayload _ dfB _ Nothing = DfLike.noData dfB + {-# INLINE setPayload #-} + + noData _ = M2S_ReadAddress{_arvalid=False} + {-# 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_ReadAddress + { -- | Read address id* + _arid :: "ARID" ::: C.BitVector (Width iw) + + -- | Read address + , _araddr :: "ARADDR" ::: C.BitVector (Width aw) + + -- | Read region* + , _arregion:: "ARREGION" ::: RegionType kr + + -- | Burst length* + , _arlen :: "ARLEN" ::: BurstLengthType kbl + + -- | Burst size* + , _arsize :: "ARSIZE" ::: SizeType ksz + + -- | Burst type* + , _arburst :: "ARBURST" ::: BurstType kb + + -- | Lock type* + , _arlock :: "ARLOCK" ::: LockType kl + + -- | Cache type* (has been renamed to modifiable in AXI spec) + , _arcache :: "ARCACHE" ::: CacheType kc + + -- | Protection type + , _arprot :: "ARPROT" ::: PermissionsType kp + + -- | QoS value + , _arqos :: "ARQOS" ::: QosType kq + + -- | Read address valid + , _arvalid :: "ARVALID" ::: Bool + + -- | User data + , _aruser :: "ARUSER" ::: userType + } + deriving (Generic) + +-- | See Table A2-5 "Read address channel signals" +newtype S2M_ReadAddress = S2M_ReadAddress + { _arready :: "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/Raw/Full/ReadData.hs b/src/Protocols/Axi4/Raw/Full/ReadData.hs new file mode 100644 index 00000000..079ad94d --- /dev/null +++ b/src/Protocols/Axi4/Raw/Full/ReadData.hs @@ -0,0 +1,140 @@ +{-| +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.Raw.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 +import Clash.Prelude ((:::)) + +-- me +import Protocols.Axi4.Raw.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{_rvalid=True, _ruser}) = Just _ruser + getPayload _ _ = Nothing + {-# INLINE getPayload #-} + + setPayload _ _ dat (Just b) = dat{_rvalid=True, _ruser=b} + setPayload _ dfB _ Nothing = DfLike.noData dfB + {-# INLINE setPayload #-} + + noData _ = S2M_ReadData{_rvalid=False} + {-# 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_ReadData + { -- | Read address id* + _rid :: "RID" ::: C.BitVector (Width iw) + + , -- | Read data + _rdata :: "RDATA" ::: dataType + + -- | Read response + , _rresp :: "RRESP" ::: ResponseType kr + + -- | Read last + , _rlast :: "RLAST" ::: Bool + + -- | Read valid + , _rvalid :: "RVALID" ::: Bool + + -- | User data + , _ruser :: "RUSER" ::: userType + } + deriving (Generic) + +-- | See Table A2-6 "Read data channel signals" +newtype M2S_ReadData = M2S_ReadData + { _rready :: "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/Raw/Full/WriteAddress.hs b/src/Protocols/Axi4/Raw/Full/WriteAddress.hs new file mode 100644 index 00000000..e143307f --- /dev/null +++ b/src/Protocols/Axi4/Raw/Full/WriteAddress.hs @@ -0,0 +1,189 @@ +{-| +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.Raw.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 +import Clash.Prelude ((:::)) + +-- me +import Protocols.Axi4.Raw.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{_awvalid=True, _awuser}) = Just _awuser + getPayload _ _ = Nothing + {-# INLINE getPayload #-} + + setPayload _ _ dat (Just b) = dat{_awvalid=True, _awuser=b} + setPayload _ dfB _ Nothing = DfLike.noData dfB + {-# INLINE setPayload #-} + + noData _ = M2S_WriteAddress{_awvalid=False} + {-# 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_WriteAddress + { -- | Write address id* + _awid :: "AWID" ::: C.BitVector (Width iw) + + -- | Write address + , _awaddr :: "AWADDR" ::: C.BitVector (Width aw) + + -- | Write region* + , _awregion:: "AWREGION" ::: RegionType kr + + -- | Burst length* + , _awlen :: "AWLEN" ::: BurstLengthType kbl + + -- | Burst size* + , _awsize :: "AWSIZE" ::: SizeType ksz + + -- | Burst type* + , _awburst :: "AWBURST" ::: BurstType kb + + -- | Lock type* + , _awlock :: "AWLOCK" ::: LockType kl + + -- | Cache type* + , _awcache :: "AWCACHE" ::: CacheType kc + + -- | Protection type + , _awprot :: "AWPROT" ::: PermissionsType kp + + -- | QoS value + , _awqos :: "AWQOS" ::: QosType kq + + -- | Write address valid + , _awvalid :: "AWVALID" ::: Bool + + -- | User data + , _awuser :: "AWUSER" ::: userType + } + deriving (Generic) + +-- | See Table A2-2 "Write address channel signals" +newtype S2M_WriteAddress = S2M_WriteAddress + { _awready :: "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/Raw/Full/WriteData.hs b/src/Protocols/Axi4/Raw/Full/WriteData.hs new file mode 100644 index 00000000..a7d8cdf1 --- /dev/null +++ b/src/Protocols/Axi4/Raw/Full/WriteData.hs @@ -0,0 +1,134 @@ +{-| +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.Raw.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 +import Clash.Prelude ((:::), type (*)) + +-- me +import Protocols.Axi4.Raw.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{_wvalid=True, _wuser}) = Just _wuser + getPayload _ _ = Nothing + {-# INLINE getPayload #-} + + setPayload _ _ dat (Just b) = dat{_wvalid=True, _wuser=b} + setPayload _ dfB _ Nothing = DfLike.noData dfB + {-# INLINE setPayload #-} + + noData _ = M2S_WriteData{_wvalid=False} + {-# 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" +data M2S_WriteData + (ks :: KeepStrobe) + (nBytes :: Nat) + (userType :: Type) = + M2S_WriteData + { -- | Write data + _wdata :: "WDATA" ::: C.BitVector (nBytes*8) + + -- | Write strobes + , _wstrb :: "WSTRB" ::: StrobeType nBytes ks + + -- | Write last + , _wlast :: "WLAST" ::: Bool + + -- | Write valid + , _wvalid :: "WVALID" ::: Bool + + -- | User data + , _wuser :: "WUSER" ::: userType + } + deriving (Generic) + +-- | See Table A2-3 "Write data channel signals" +newtype S2M_WriteData = S2M_WriteData + { _wready :: "WREADY" ::: Bool } + deriving (Show, Generic, C.NFDataX) + +deriving instance + ( C.NFDataX userType + , C.NFDataX (StrobeType nBytes ks) ) => + C.NFDataX (M2S_WriteData ks nBytes userType) + +deriving instance + ( Show userType + , Show (StrobeType nBytes ks) + , C.KnownNat nBytes ) => + Show (M2S_WriteData ks nBytes userType) diff --git a/src/Protocols/Axi4/Raw/Full/WriteResponse.hs b/src/Protocols/Axi4/Raw/Full/WriteResponse.hs new file mode 100644 index 00000000..598401aa --- /dev/null +++ b/src/Protocols/Axi4/Raw/Full/WriteResponse.hs @@ -0,0 +1,130 @@ +{-| +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.Raw.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 +import Clash.Prelude ((:::)) + +-- me +import Protocols.Axi4.Raw.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{_bvalid=True, _buser}) = Just _buser + getPayload _ _ = Nothing + {-# INLINE getPayload #-} + + setPayload _ _ dat (Just b) = dat{_bvalid=True, _buser=b} + setPayload _ dfB _ Nothing = DfLike.noData dfB + {-# INLINE setPayload #-} + + noData _ = S2M_WriteResponse{_bvalid=False} + {-# 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_WriteResponse + { -- | Response ID + _bid :: "BID" ::: C.BitVector (Width iw) + + -- | Write response + , _bresp :: "BRESP" ::: ResponseType kr + + -- | Write response valid + , _bvalid :: "BVALID" ::: Bool + + -- | User data + , _buser :: "BUSER" ::: userType + } + deriving (Generic) + +-- | See Table A2-4 "Write response channel signals" +newtype M2S_WriteResponse = M2S_WriteResponse + { _bready :: "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) diff --git a/src/Protocols/Internal.hs b/src/Protocols/Internal.hs index 03023854..07c4d2e1 100644 --- a/src/Protocols/Internal.hs +++ b/src/Protocols/Internal.hs @@ -622,3 +622,9 @@ simulateCSE c = simulateCS (c clk rst ena) circuit :: Any circuit = error "'protocol' called: did you forget to enable \"Protocols.Plugin\"?" + +-- | Picked up by "Protocols.Plugin" to tie circuits together. See +-- "Protocols.Plugin" for more information. +(-<) :: Any +(-<) = + error "(-<) called: did you forget to enable \"Protocols.Plugin\"?" From de46d3a6fef2dd294db28225d7e530c00668e102 Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Tue, 5 Jan 2021 16:41:31 +0100 Subject: [PATCH 04/12] Add sctrict AXI --- clash-protocols.cabal | 27 ++- 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, 831 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..c0365e87 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,21 @@ 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 + 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) From da0c3c6cc622bda89dcc9d78cf905fcd68c8dfbb Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Tue, 5 Jan 2021 21:19:02 +0100 Subject: [PATCH 05/12] Add AXI conversion functions --- src/Protocols/Axi4/Common.hs | 10 ++- src/Protocols/Axi4/Partial/Full.hs | 15 ++-- .../Axi4/Partial/Full/ReadAddress.hs | 52 ++++++++++++ src/Protocols/Axi4/Partial/Full/ReadData.hs | 52 ++++++++++++ .../Axi4/Partial/Full/WriteAddress.hs | 52 ++++++++++++ src/Protocols/Axi4/Partial/Full/WriteData.hs | 82 ++++++++++++++++++- .../Axi4/Partial/Full/WriteResponse.hs | 52 ++++++++++++ src/Protocols/Axi4/Strict/Full/WriteData.hs | 2 +- 8 files changed, 308 insertions(+), 9 deletions(-) diff --git a/src/Protocols/Axi4/Common.hs b/src/Protocols/Axi4/Common.hs index 451ab081..5cba3efc 100644 --- a/src/Protocols/Axi4/Common.hs +++ b/src/Protocols/Axi4/Common.hs @@ -1,6 +1,7 @@ {-| Types and utilities shared between AXI4, AXI4-Lite, and AXI3. -} +{-# LANGUAGE GADTs #-} {-# LANGUAGE UndecidableInstances #-} module Protocols.Axi4.Common where @@ -15,7 +16,7 @@ import qualified Clash.Prelude as C import Clash.Prelude (type (^), type (-), type (*)) -- strict-tuple -import Data.Tuple.Strict +import Data.Tuple.Strict (T3, T4) -- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol data IdWidth = IdWidth Nat deriving (Show) @@ -63,6 +64,11 @@ data KeepSize = KeepSize | NoSize deriving (Show) -- | Keep or remove strobe field. See 'Strobe' data KeepStrobe = KeepStrobe | NoStrobe deriving (Show) +-- | Type used to introduce strobe information on the term level +data SKeepStrobe (strobeType :: KeepStrobe) where + SKeepStrobe :: SKeepStrobe 'KeepStrobe + SNoStrobe :: SKeepStrobe 'NoStrobe + -- | Extracts Nat from 'IdWidth', 'AddrWidth', and 'LengthWidth' type family Width (a :: k) :: Nat where Width ('IdWidth n) = n @@ -126,7 +132,7 @@ type family StrobeType (byteSize :: Nat) (keepStrobe :: KeepStrobe) where -- | Enable or disable 'Strobe' type family StrictStrobeType (byteSize :: Nat) (keepStrobe :: KeepStrobe) where - StrictStrobeType byteSize 'KeepStrobe = C.Vec byteSize (C.BitVector 8) + StrictStrobeType byteSize 'KeepStrobe = C.Vec byteSize (Maybe (C.BitVector 8)) StrictStrobeType byteSize 'NoStrobe = C.BitVector (byteSize * 8) -- | Indicates valid bytes on data field. diff --git a/src/Protocols/Axi4/Partial/Full.hs b/src/Protocols/Axi4/Partial/Full.hs index 4e6aaf03..16b82130 100644 --- a/src/Protocols/Axi4/Partial/Full.hs +++ b/src/Protocols/Axi4/Partial/Full.hs @@ -18,8 +18,13 @@ module Protocols.Axi4.Partial.Full , module WriteResponse ) where -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 +import Protocols.Axi4.Partial.Full.ReadAddress + as ReadAddress hiding (toStrict, toStrictDf, fromStrict, fromStrictDf) +import Protocols.Axi4.Partial.Full.ReadData + as ReadData hiding (toStrict, toStrictDf, fromStrict, fromStrictDf) +import Protocols.Axi4.Partial.Full.WriteAddress + as WriteAddress hiding (toStrict, toStrictDf, fromStrict, fromStrictDf) +import Protocols.Axi4.Partial.Full.WriteData + as WriteData hiding (toStrict, toStrictDf, fromStrict, fromStrictDf) +import Protocols.Axi4.Partial.Full.WriteResponse + as WriteResponse hiding (toStrict, toStrictDf, fromStrict, fromStrictDf) diff --git a/src/Protocols/Axi4/Partial/Full/ReadAddress.hs b/src/Protocols/Axi4/Partial/Full/ReadAddress.hs index 4b3180df..7c014fff 100644 --- a/src/Protocols/Axi4/Partial/Full/ReadAddress.hs +++ b/src/Protocols/Axi4/Partial/Full/ReadAddress.hs @@ -6,6 +6,7 @@ to the AXI4 specification. {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-missing-fields #-} @@ -14,6 +15,8 @@ module Protocols.Axi4.Partial.Full.ReadAddress ( M2S_ReadAddress(..) , S2M_ReadAddress(..) , Axi4ReadAddress + , toStrict, toStrictDf + , fromStrict, fromStrictDf ) where -- base @@ -31,6 +34,9 @@ import Protocols.Axi4.Common import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike +import qualified Protocols.Axi4.Strict.Full.ReadAddress as Strict +import qualified Protocols.Df as Df +import Protocols.Df (Df) -- | AXI4 Read Address channel protocol data Axi4ReadAddress @@ -187,3 +193,49 @@ deriving instance , C.NFDataX (PermissionsType kp) , C.NFDataX (QosType kq) ) => C.NFDataX (M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) + +-- | Convert an 'Axi4ReadAddress' into its strict version +-- 'Strict.Axi4ReadAddress'. The latter is usually preferred in Clash designs +-- as its definitions don't contain partial fields. Note that the functions +-- defined over these circuits operate on @userType@. If you need functions to +-- map over all fields, consider using 'toStrictDf'. +toStrict :: + Circuit + (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) + (Strict.Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) +toStrict = Circuit (C.unbundle . fmap go . C.bundle) + where + go (M2S_ReadAddress{..}, ack) + | _arvalid = (coerce ack, Strict.M2S_ReadAddress{..}) + | otherwise = (coerce ack, Strict.M2S_NoReadAddress) + +-- | Convert a 'Strict.Axi4ReadAddress' into 'Axi4ReadAddress' +fromStrict :: + Circuit + (Strict.Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) + (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) +fromStrict = Circuit (C.unbundle . fmap go . C.bundle) + where + go (Strict.M2S_ReadAddress{..}, ack) = (coerce ack, M2S_ReadAddress{_arvalid=True,..}) + go (Strict.M2S_NoReadAddress, ack) = (coerce ack, M2S_ReadAddress{_arvalid=False}) + +-- | Convert an 'Axi4ReadAddress' into its strict 'Df' equivalent. +toStrictDf :: + Circuit + (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) + (Df dom (Strict.M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)) +toStrictDf = Circuit (C.unbundle . fmap go . C.bundle) + where + go (M2S_ReadAddress{..}, ack) + | _arvalid = (coerce ack, Df.Data (Strict.M2S_ReadAddress{..})) + | otherwise = (coerce ack, Df.NoData) + +-- | Convert a into 'Axi4ReadAddress' from its Df equivalent +fromStrictDf :: + Circuit + (Df dom (Strict.M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)) + (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) +fromStrictDf = Circuit (C.unbundle . fmap go . C.bundle) + where + go (Df.Data (Strict.M2S_ReadAddress{..}), ack) = (coerce ack, M2S_ReadAddress{_arvalid=True,..}) + go (_, ack) = (coerce ack, M2S_ReadAddress{_arvalid=False}) diff --git a/src/Protocols/Axi4/Partial/Full/ReadData.hs b/src/Protocols/Axi4/Partial/Full/ReadData.hs index dfb05c44..ef6244cb 100644 --- a/src/Protocols/Axi4/Partial/Full/ReadData.hs +++ b/src/Protocols/Axi4/Partial/Full/ReadData.hs @@ -6,6 +6,7 @@ to the AXI4 specification. {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-missing-fields #-} @@ -14,6 +15,8 @@ module Protocols.Axi4.Partial.Full.ReadData ( M2S_ReadData(..) , S2M_ReadData(..) , Axi4ReadData + , toStrict, toStrictDf + , fromStrict, fromStrictDf ) where -- base @@ -31,6 +34,9 @@ import Protocols.Axi4.Common import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike +import qualified Protocols.Axi4.Strict.Full.ReadData as Strict +import qualified Protocols.Df as Df +import Protocols.Df (Df) -- | AXI4 Read Data channel protocol data Axi4ReadData @@ -138,3 +144,49 @@ deriving instance , Show dataType , Show (ResponseType kr) ) => Show (S2M_ReadData kr iw dataType userType) + +-- | Convert an 'Axi4ReadData' into its strict version +-- 'Strict.Axi4ReadData'. The latter is usually preferred in Clash designs +-- as its definitions don't contain partial fields. Note that the functions +-- defined over these circuits operate on @userType@. If you need functions to +-- map over all fields, consider using 'toStrictDf'. +toStrict :: + Circuit + (Axi4ReadData dom kr iw dataType userType) + (Strict.Axi4ReadData dom kr iw dataType userType) +toStrict = Circuit (C.unbundle . fmap go . C.bundle) + where + go (S2M_ReadData{..}, ack) + | _rvalid = (coerce ack, Strict.S2M_ReadData{..}) + | otherwise = (coerce ack, Strict.S2M_NoReadData) + +-- | Convert a 'Strict.Axi4ReadData' into 'Axi4ReadData' +fromStrict :: + Circuit + (Strict.Axi4ReadData dom kr iw dataType userType) + (Axi4ReadData dom kr iw dataType userType) +fromStrict = Circuit (C.unbundle . fmap go . C.bundle) + where + go (Strict.S2M_ReadData{..}, ack) = (coerce ack, S2M_ReadData{_rvalid=True,..}) + go (Strict.S2M_NoReadData, ack) = (coerce ack, S2M_ReadData{_rvalid=False}) + +-- | Convert an 'Axi4ReadData' into its strict 'Df' equivalent. +toStrictDf :: + Circuit + (Axi4ReadData dom kr iw dataType userType) + (Df dom (Strict.S2M_ReadData kr iw dataType userType)) +toStrictDf = Circuit (C.unbundle . fmap go . C.bundle) + where + go (S2M_ReadData{..}, ack) + | _rvalid = (coerce ack, Df.Data (Strict.S2M_ReadData{..})) + | otherwise = (coerce ack, Df.NoData) + +-- | Convert a into 'Axi4ReadData' from its Df equivalent +fromStrictDf :: + Circuit + (Df dom (Strict.S2M_ReadData kr iw dataType userType)) + (Axi4ReadData dom kr iw dataType userType) +fromStrictDf = Circuit (C.unbundle . fmap go . C.bundle) + where + go (Df.Data (Strict.S2M_ReadData{..}), ack) = (coerce ack, S2M_ReadData{_rvalid=True,..}) + go (_, ack) = (coerce ack, S2M_ReadData{_rvalid=False}) diff --git a/src/Protocols/Axi4/Partial/Full/WriteAddress.hs b/src/Protocols/Axi4/Partial/Full/WriteAddress.hs index eb92aad6..572bbbb5 100644 --- a/src/Protocols/Axi4/Partial/Full/WriteAddress.hs +++ b/src/Protocols/Axi4/Partial/Full/WriteAddress.hs @@ -6,6 +6,7 @@ to the AXI4 specification. {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-missing-fields #-} @@ -14,6 +15,8 @@ module Protocols.Axi4.Partial.Full.WriteAddress ( M2S_WriteAddress(..) , S2M_WriteAddress(..) , Axi4WriteAddress + , toStrict, toStrictDf + , fromStrict, fromStrictDf ) where -- base @@ -31,6 +34,9 @@ import Protocols.Axi4.Common import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike +import qualified Protocols.Axi4.Strict.Full.WriteAddress as Strict +import qualified Protocols.Df as Df +import Protocols.Df (Df) -- | AXI4 Write Address channel protocol data Axi4WriteAddress @@ -187,3 +193,49 @@ deriving instance , C.NFDataX (PermissionsType kp) , C.NFDataX (QosType kq) ) => C.NFDataX (M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) + +-- | Convert an 'Axi4WriteAddress' into its strict version +-- 'Strict.Axi4WriteAddress'. The latter is usually preferred in Clash designs +-- as its definitions don't contain partial fields. Note that the functions +-- defined over these circuits operate on @userType@. If you need functions to +-- map over all fields, consider using 'toStrictDf'. +toStrict :: + Circuit + (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) + (Strict.Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) +toStrict = Circuit (C.unbundle . fmap go . C.bundle) + where + go (M2S_WriteAddress{..}, ack) + | _awvalid = (coerce ack, Strict.M2S_WriteAddress{..}) + | otherwise = (coerce ack, Strict.M2S_NoWriteAddress) + +-- | Convert a 'Strict.Axi4WriteAddress' into 'Axi4WriteAddress' +fromStrict :: + Circuit + (Strict.Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) + (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) +fromStrict = Circuit (C.unbundle . fmap go . C.bundle) + where + go (Strict.M2S_WriteAddress{..}, ack) = (coerce ack, M2S_WriteAddress{_awvalid=True,..}) + go (Strict.M2S_NoWriteAddress, ack) = (coerce ack, M2S_WriteAddress{_awvalid=False}) + +-- | Convert an 'Axi4WriteAddress' into its strict 'Df' equivalent. +toStrictDf :: + Circuit + (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) + (Df dom (Strict.M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)) +toStrictDf = Circuit (C.unbundle . fmap go . C.bundle) + where + go (M2S_WriteAddress{..}, ack) + | _awvalid = (coerce ack, Df.Data (Strict.M2S_WriteAddress{..})) + | otherwise = (coerce ack, Df.NoData) + +-- | Convert a into 'Axi4WriteAddress' from its Df equivalent +fromStrictDf :: + Circuit + (Df dom (Strict.M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)) + (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) +fromStrictDf = Circuit (C.unbundle . fmap go . C.bundle) + where + go (Df.Data (Strict.M2S_WriteAddress{..}), ack) = (coerce ack, M2S_WriteAddress{_awvalid=True,..}) + go (_, ack) = (coerce ack, M2S_WriteAddress{_awvalid=False}) diff --git a/src/Protocols/Axi4/Partial/Full/WriteData.hs b/src/Protocols/Axi4/Partial/Full/WriteData.hs index 418bf8f1..fbea71b7 100644 --- a/src/Protocols/Axi4/Partial/Full/WriteData.hs +++ b/src/Protocols/Axi4/Partial/Full/WriteData.hs @@ -6,6 +6,7 @@ to the AXI4 specification. {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-missing-fields #-} @@ -14,14 +15,17 @@ module Protocols.Axi4.Partial.Full.WriteData ( M2S_WriteData(..) , S2M_WriteData(..) , Axi4WriteData + , toStrict, toStrictDf + , fromStrict, fromStrictDf ) where -- base import Data.Coerce (coerce) import Data.Kind (Type) +import Data.Maybe (fromMaybe, isJust) +import Data.Proxy import GHC.Generics (Generic) import GHC.TypeNats (Nat) -import Data.Proxy -- clash-prelude import qualified Clash.Prelude as C @@ -32,6 +36,9 @@ import Protocols.Axi4.Common import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike +import qualified Protocols.Axi4.Strict.Full.WriteData as Strict +import qualified Protocols.Df as Df +import Protocols.Df (Df) -- | AXI4 Write Data channel protocol data Axi4WriteData @@ -132,3 +139,76 @@ deriving instance , Show (StrobeType nBytes ks) , C.KnownNat nBytes ) => Show (M2S_WriteData ks nBytes userType) + +-- | Convert an 'Axi4WriteData' into its strict version +-- 'Strict.Axi4WriteData'. The latter is usually preferred in Clash designs +-- as its definitions don't contain partial fields. Note that the functions +-- defined over these circuits operate on @userType@. If you need functions to +-- map over all fields, consider using 'toStrictDf'. +toStrict :: + C.KnownNat nBytes => + SKeepStrobe ks -> + Circuit + (Axi4WriteData dom ks nBytes userType) + (Strict.Axi4WriteData dom ks nBytes userType) +toStrict SNoStrobe = Circuit (C.unbundle . fmap go . C.bundle) + where + go (M2S_WriteData{..}, ack) + | _wvalid = (coerce ack, Strict.M2S_WriteData{..}) + | otherwise = (coerce ack, Strict.M2S_NoWriteData) +toStrict SKeepStrobe = Circuit (C.unbundle . fmap go . C.bundle) + where + go (M2S_WriteData{..}, ack) + | _wvalid = (coerce ack, Strict.M2S_WriteData{_wdata=strobedData _wdata _wstrb,..}) + | otherwise = (coerce ack, Strict.M2S_NoWriteData) + + strobedData dat strb = C.zipWith orNothing (C.unpack strb) (C.unpack dat) + orNothing p a = if p then Just a else Nothing + +-- | Convert a 'Strict.Axi4WriteData' into 'Axi4WriteData' +fromStrict :: + C.KnownNat nBytes => + SKeepStrobe ks -> + Circuit + (Strict.Axi4WriteData dom ks nBytes userType) + (Axi4WriteData dom ks nBytes userType) +fromStrict SNoStrobe = Circuit (C.unbundle . fmap go . C.bundle) + where + go (Strict.M2S_WriteData{..}, ack) = (coerce ack, M2S_WriteData{_wvalid=True,..}) + go (_, ack) = (coerce ack, M2S_WriteData{_wvalid=False}) +fromStrict SKeepStrobe = Circuit (C.unbundle . fmap go . C.bundle) + where + go (Strict.M2S_WriteData{..}, ack) = + (coerce ack, M2S_WriteData + { _wdata=C.pack (C.map (fromMaybe 0) _wdata) + , _wstrb=C.pack (C.map isJust _wdata) + , _wvalid=True + , .. }) + go (_, ack) = + (coerce ack, M2S_WriteData{_wvalid=False}) + +-- | Convert an 'Axi4WriteData' into its strict 'Df' equivalent. +toStrictDf :: + C.KnownNat nBytes => + SKeepStrobe ks -> + Circuit + (Axi4WriteData dom ks nBytes userType) + (Df dom (Strict.M2S_WriteData ks nBytes userType)) +toStrictDf keepStrobe = + toStrict keepStrobe |> Circuit (C.unbundle . fmap go . C.bundle) + where + go (dat@Strict.M2S_WriteData {}, ack) = (coerce ack, Df.Data dat) + go (_, ack) = (coerce ack, Df.NoData) + +-- | Convert an 'Axi4WriteData' into its strict 'Df' equivalent. +fromStrictDf :: + C.KnownNat nBytes => + SKeepStrobe ks -> + Circuit + (Df dom (Strict.M2S_WriteData ks nBytes userType)) + (Axi4WriteData dom ks nBytes userType) +fromStrictDf keepStrobe = + Circuit (C.unbundle . fmap go . C.bundle) |> fromStrict keepStrobe + where + go (Df.Data dat, ack) = (coerce ack, dat) + go (_, ack) = (coerce ack, Strict.M2S_NoWriteData) diff --git a/src/Protocols/Axi4/Partial/Full/WriteResponse.hs b/src/Protocols/Axi4/Partial/Full/WriteResponse.hs index e1bba4d1..a4ebefbe 100644 --- a/src/Protocols/Axi4/Partial/Full/WriteResponse.hs +++ b/src/Protocols/Axi4/Partial/Full/WriteResponse.hs @@ -6,6 +6,7 @@ to the AXI4 specification. {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-missing-fields #-} @@ -14,6 +15,8 @@ module Protocols.Axi4.Partial.Full.WriteResponse ( M2S_WriteResponse(..) , S2M_WriteResponse(..) , Axi4WriteResponse + , toStrict, toStrictDf + , fromStrict, fromStrictDf ) where -- base @@ -31,6 +34,9 @@ import Protocols.Axi4.Common import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike +import qualified Protocols.Axi4.Strict.Full.WriteResponse as Strict +import qualified Protocols.Df as Df +import Protocols.Df (Df) -- | AXI4 Read Data channel protocol data Axi4WriteResponse @@ -128,3 +134,49 @@ deriving instance , Show (ResponseType kr) , C.KnownNat (Width iw) ) => Show (S2M_WriteResponse kr iw userType) + +-- | Convert an 'Axi4WriteResponse' into its strict version +-- 'Strict.Axi4WriteResponse'. The latter is usually preferred in Clash designs +-- as its definitions don't contain partial fields. Note that the functions +-- defined over these circuits operate on @userType@. If you need functions to +-- map over all fields, consider using 'toStrictDf'. +toStrict :: + Circuit + (Axi4WriteResponse dom kr iw userType) + (Strict.Axi4WriteResponse dom kr iw userType) +toStrict = Circuit (C.unbundle . fmap go . C.bundle) + where + go (S2M_WriteResponse{..}, ack) + | _bvalid = (coerce ack, Strict.S2M_WriteResponse{..}) + | otherwise = (coerce ack, Strict.S2M_NoWriteResponse) + +-- | Convert a 'Strict.Axi4WriteResponse' into 'Axi4WriteResponse' +fromStrict :: + Circuit + (Strict.Axi4WriteResponse dom kr iw userType) + (Axi4WriteResponse dom kr iw userType) +fromStrict = Circuit (C.unbundle . fmap go . C.bundle) + where + go (Strict.S2M_WriteResponse{..}, ack) = (coerce ack, S2M_WriteResponse{_bvalid=True,..}) + go (Strict.S2M_NoWriteResponse, ack) = (coerce ack, S2M_WriteResponse{_bvalid=False}) + +-- | Convert an 'Axi4WriteResponse' into its strict 'Df' equivalent. +toStrictDf :: + Circuit + (Axi4WriteResponse dom kr iw userType) + (Df dom (Strict.S2M_WriteResponse kr iw userType)) +toStrictDf = Circuit (C.unbundle . fmap go . C.bundle) + where + go (S2M_WriteResponse{..}, ack) + | _bvalid = (coerce ack, Df.Data (Strict.S2M_WriteResponse{..})) + | otherwise = (coerce ack, Df.NoData) + +-- | Convert a into 'Axi4WriteResponse' from its Df equivalent +fromStrictDf :: + Circuit + (Df dom (Strict.S2M_WriteResponse kr iw userType)) + (Axi4WriteResponse dom kr iw userType) +fromStrictDf = Circuit (C.unbundle . fmap go . C.bundle) + where + go (Df.Data (Strict.S2M_WriteResponse{..}), ack) = (coerce ack, S2M_WriteResponse{_bvalid=True,..}) + go (_, ack) = (coerce ack, S2M_WriteResponse{_bvalid=False}) diff --git a/src/Protocols/Axi4/Strict/Full/WriteData.hs b/src/Protocols/Axi4/Strict/Full/WriteData.hs index 2029b850..dcdbcc79 100644 --- a/src/Protocols/Axi4/Strict/Full/WriteData.hs +++ b/src/Protocols/Axi4/Strict/Full/WriteData.hs @@ -95,7 +95,7 @@ instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType -- | 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'. +-- 'C.BitVector'. data M2S_WriteData (ks :: KeepStrobe) (nBytes :: Nat) From badcbfbbebbbeba478256105eae095e27536c268 Mon Sep 17 00:00:00 2001 From: Pieter Staal Date: Thu, 9 Dec 2021 11:22:36 +0100 Subject: [PATCH 06/12] Remove Partial AXI4 --- clash-protocols.cabal | 18 +- src/Protocols/Axi4/Partial/Full.hs | 30 --- .../Axi4/Partial/Full/ReadAddress.hs | 241 ------------------ src/Protocols/Axi4/Partial/Full/ReadData.hs | 192 -------------- .../Axi4/Partial/Full/WriteAddress.hs | 241 ------------------ src/Protocols/Axi4/Partial/Full/WriteData.hs | 214 ---------------- .../Axi4/Partial/Full/WriteResponse.hs | 182 ------------- .../Axi4/{Strict/Full => }/ReadAddress.hs | 4 +- .../Axi4/{Strict/Full => }/ReadData.hs | 57 +++-- src/Protocols/Axi4/Strict/Full.hs | 23 -- .../Axi4/{Strict/Full => }/WriteAddress.hs | 3 +- .../Axi4/{Strict/Full => }/WriteData.hs | 6 +- .../Axi4/{Strict/Full => }/WriteResponse.hs | 3 +- 13 files changed, 50 insertions(+), 1164 deletions(-) delete mode 100644 src/Protocols/Axi4/Partial/Full.hs delete mode 100644 src/Protocols/Axi4/Partial/Full/ReadAddress.hs delete mode 100644 src/Protocols/Axi4/Partial/Full/ReadData.hs delete mode 100644 src/Protocols/Axi4/Partial/Full/WriteAddress.hs delete mode 100644 src/Protocols/Axi4/Partial/Full/WriteData.hs delete mode 100644 src/Protocols/Axi4/Partial/Full/WriteResponse.hs rename src/Protocols/Axi4/{Strict/Full => }/ReadAddress.hs (99%) rename src/Protocols/Axi4/{Strict/Full => }/ReadData.hs (61%) delete mode 100644 src/Protocols/Axi4/Strict/Full.hs rename src/Protocols/Axi4/{Strict/Full => }/WriteAddress.hs (99%) rename src/Protocols/Axi4/{Strict/Full => }/WriteData.hs (96%) rename src/Protocols/Axi4/{Strict/Full => }/WriteResponse.hs (98%) diff --git a/clash-protocols.cabal b/clash-protocols.cabal index c0365e87..9b1ac996 100644 --- a/clash-protocols.cabal +++ b/clash-protocols.cabal @@ -141,19 +141,11 @@ library 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 - 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.Axi4.ReadAddress + Protocols.Axi4.ReadData + Protocols.Axi4.WriteAddress + Protocols.Axi4.WriteData + Protocols.Axi4.WriteResponse Protocols.Df Protocols.DfLike diff --git a/src/Protocols/Axi4/Partial/Full.hs b/src/Protocols/Axi4/Partial/Full.hs deleted file mode 100644 index 16b82130..00000000 --- a/src/Protocols/Axi4/Partial/Full.hs +++ /dev/null @@ -1,30 +0,0 @@ -{-| -Defines the full AXI4 protocol with port names corresponding to the AXI4 -specification. Because some fields are defined partially, it's not advised to -use this in Clash designs. Instead, look at (losslessly) converting it to -"Protocols.Axi4.Full" or (losslessy or lossy) converting it to "Protocols.Df". - -Note that every individual channel is a DfLike-protocol, but the bundled version -is not. --} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE UndecidableInstances #-} - -module Protocols.Axi4.Partial.Full - ( module ReadAddress - , module ReadData - , module WriteAddress - , module WriteData - , module WriteResponse - ) where - -import Protocols.Axi4.Partial.Full.ReadAddress - as ReadAddress hiding (toStrict, toStrictDf, fromStrict, fromStrictDf) -import Protocols.Axi4.Partial.Full.ReadData - as ReadData hiding (toStrict, toStrictDf, fromStrict, fromStrictDf) -import Protocols.Axi4.Partial.Full.WriteAddress - as WriteAddress hiding (toStrict, toStrictDf, fromStrict, fromStrictDf) -import Protocols.Axi4.Partial.Full.WriteData - as WriteData hiding (toStrict, toStrictDf, fromStrict, fromStrictDf) -import Protocols.Axi4.Partial.Full.WriteResponse - as WriteResponse hiding (toStrict, toStrictDf, fromStrict, fromStrictDf) diff --git a/src/Protocols/Axi4/Partial/Full/ReadAddress.hs b/src/Protocols/Axi4/Partial/Full/ReadAddress.hs deleted file mode 100644 index 7c014fff..00000000 --- a/src/Protocols/Axi4/Partial/Full/ReadAddress.hs +++ /dev/null @@ -1,241 +0,0 @@ -{-| -Defines ReadAddress channel of full AXI4 protocol with port names corresponding -to the AXI4 specification. --} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -Wno-missing-fields #-} - -module Protocols.Axi4.Partial.Full.ReadAddress - ( M2S_ReadAddress(..) - , S2M_ReadAddress(..) - , Axi4ReadAddress - , toStrict, toStrictDf - , fromStrict, fromStrictDf - ) where - --- base -import Data.Coerce -import Data.Kind (Type) -import Data.Proxy -import GHC.Generics (Generic) - --- clash-prelude -import qualified Clash.Prelude as C -import Clash.Prelude ((:::)) - --- me -import Protocols.Axi4.Common -import Protocols.Internal -import Protocols.DfLike (DfLike) -import qualified Protocols.DfLike as DfLike -import qualified Protocols.Axi4.Strict.Full.ReadAddress as Strict -import qualified Protocols.Df as Df -import Protocols.Df (Df) - --- | 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{_arvalid=True, _aruser}) = Just _aruser - getPayload _ _ = Nothing - {-# INLINE getPayload #-} - - setPayload _ _ dat (Just b) = dat{_arvalid=True, _aruser=b} - setPayload _ dfB _ Nothing = DfLike.noData dfB - {-# INLINE setPayload #-} - - noData _ = M2S_ReadAddress{_arvalid=False} - {-# 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_ReadAddress - { -- | Read address id* - _arid :: "ARID" ::: C.BitVector (Width iw) - - -- | Read address - , _araddr :: "ARADDR" ::: C.BitVector (Width aw) - - -- | Read region* - , _arregion:: "ARREGION" ::: RegionType kr - - -- | Burst length* - , _arlen :: "ARLEN" ::: BurstLengthType kbl - - -- | Burst size* - , _arsize :: "ARSIZE" ::: SizeType ksz - - -- | Burst type* - , _arburst :: "ARBURST" ::: BurstType kb - - -- | Lock type* - , _arlock :: "ARLOCK" ::: LockType kl - - -- | Cache type* (has been renamed to modifiable in AXI spec) - , _arcache :: "ARCACHE" ::: CacheType kc - - -- | Protection type - , _arprot :: "ARPROT" ::: PermissionsType kp - - -- | QoS value - , _arqos :: "ARQOS" ::: QosType kq - - -- | Read address valid - , _arvalid :: "ARVALID" ::: Bool - - -- | User data - , _aruser :: "ARUSER" ::: userType - } - deriving (Generic) - --- | See Table A2-5 "Read address channel signals" -newtype S2M_ReadAddress = S2M_ReadAddress - { _arready :: "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) - --- | Convert an 'Axi4ReadAddress' into its strict version --- 'Strict.Axi4ReadAddress'. The latter is usually preferred in Clash designs --- as its definitions don't contain partial fields. Note that the functions --- defined over these circuits operate on @userType@. If you need functions to --- map over all fields, consider using 'toStrictDf'. -toStrict :: - Circuit - (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) - (Strict.Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) -toStrict = Circuit (C.unbundle . fmap go . C.bundle) - where - go (M2S_ReadAddress{..}, ack) - | _arvalid = (coerce ack, Strict.M2S_ReadAddress{..}) - | otherwise = (coerce ack, Strict.M2S_NoReadAddress) - --- | Convert a 'Strict.Axi4ReadAddress' into 'Axi4ReadAddress' -fromStrict :: - Circuit - (Strict.Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) - (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) -fromStrict = Circuit (C.unbundle . fmap go . C.bundle) - where - go (Strict.M2S_ReadAddress{..}, ack) = (coerce ack, M2S_ReadAddress{_arvalid=True,..}) - go (Strict.M2S_NoReadAddress, ack) = (coerce ack, M2S_ReadAddress{_arvalid=False}) - --- | Convert an 'Axi4ReadAddress' into its strict 'Df' equivalent. -toStrictDf :: - Circuit - (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) - (Df dom (Strict.M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)) -toStrictDf = Circuit (C.unbundle . fmap go . C.bundle) - where - go (M2S_ReadAddress{..}, ack) - | _arvalid = (coerce ack, Df.Data (Strict.M2S_ReadAddress{..})) - | otherwise = (coerce ack, Df.NoData) - --- | Convert a into 'Axi4ReadAddress' from its Df equivalent -fromStrictDf :: - Circuit - (Df dom (Strict.M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)) - (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) -fromStrictDf = Circuit (C.unbundle . fmap go . C.bundle) - where - go (Df.Data (Strict.M2S_ReadAddress{..}), ack) = (coerce ack, M2S_ReadAddress{_arvalid=True,..}) - go (_, ack) = (coerce ack, M2S_ReadAddress{_arvalid=False}) diff --git a/src/Protocols/Axi4/Partial/Full/ReadData.hs b/src/Protocols/Axi4/Partial/Full/ReadData.hs deleted file mode 100644 index ef6244cb..00000000 --- a/src/Protocols/Axi4/Partial/Full/ReadData.hs +++ /dev/null @@ -1,192 +0,0 @@ -{-| -Defines ReadData channel of full AXI4 protocol with port names corresponding -to the AXI4 specification. --} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -Wno-missing-fields #-} - -module Protocols.Axi4.Partial.Full.ReadData - ( M2S_ReadData(..) - , S2M_ReadData(..) - , Axi4ReadData - , toStrict, toStrictDf - , fromStrict, fromStrictDf - ) 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 -import Clash.Prelude ((:::)) - --- me -import Protocols.Axi4.Common -import Protocols.Internal -import Protocols.DfLike (DfLike) -import qualified Protocols.DfLike as DfLike -import qualified Protocols.Axi4.Strict.Full.ReadData as Strict -import qualified Protocols.Df as Df -import Protocols.Df (Df) - --- | 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{_rvalid=True, _ruser}) = Just _ruser - getPayload _ _ = Nothing - {-# INLINE getPayload #-} - - setPayload _ _ dat (Just b) = dat{_rvalid=True, _ruser=b} - setPayload _ dfB _ Nothing = DfLike.noData dfB - {-# INLINE setPayload #-} - - noData _ = S2M_ReadData{_rvalid=False} - {-# 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_ReadData - { -- | Read address id* - _rid :: "RID" ::: C.BitVector (Width iw) - - , -- | Read data - _rdata :: "RDATA" ::: dataType - - -- | Read response - , _rresp :: "RRESP" ::: ResponseType kr - - -- | Read last - , _rlast :: "RLAST" ::: Bool - - -- | Read valid - , _rvalid :: "RVALID" ::: Bool - - -- | User data - , _ruser :: "RUSER" ::: userType - } - deriving (Generic) - --- | See Table A2-6 "Read data channel signals" -newtype M2S_ReadData = M2S_ReadData - { _rready :: "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) - --- | Convert an 'Axi4ReadData' into its strict version --- 'Strict.Axi4ReadData'. The latter is usually preferred in Clash designs --- as its definitions don't contain partial fields. Note that the functions --- defined over these circuits operate on @userType@. If you need functions to --- map over all fields, consider using 'toStrictDf'. -toStrict :: - Circuit - (Axi4ReadData dom kr iw dataType userType) - (Strict.Axi4ReadData dom kr iw dataType userType) -toStrict = Circuit (C.unbundle . fmap go . C.bundle) - where - go (S2M_ReadData{..}, ack) - | _rvalid = (coerce ack, Strict.S2M_ReadData{..}) - | otherwise = (coerce ack, Strict.S2M_NoReadData) - --- | Convert a 'Strict.Axi4ReadData' into 'Axi4ReadData' -fromStrict :: - Circuit - (Strict.Axi4ReadData dom kr iw dataType userType) - (Axi4ReadData dom kr iw dataType userType) -fromStrict = Circuit (C.unbundle . fmap go . C.bundle) - where - go (Strict.S2M_ReadData{..}, ack) = (coerce ack, S2M_ReadData{_rvalid=True,..}) - go (Strict.S2M_NoReadData, ack) = (coerce ack, S2M_ReadData{_rvalid=False}) - --- | Convert an 'Axi4ReadData' into its strict 'Df' equivalent. -toStrictDf :: - Circuit - (Axi4ReadData dom kr iw dataType userType) - (Df dom (Strict.S2M_ReadData kr iw dataType userType)) -toStrictDf = Circuit (C.unbundle . fmap go . C.bundle) - where - go (S2M_ReadData{..}, ack) - | _rvalid = (coerce ack, Df.Data (Strict.S2M_ReadData{..})) - | otherwise = (coerce ack, Df.NoData) - --- | Convert a into 'Axi4ReadData' from its Df equivalent -fromStrictDf :: - Circuit - (Df dom (Strict.S2M_ReadData kr iw dataType userType)) - (Axi4ReadData dom kr iw dataType userType) -fromStrictDf = Circuit (C.unbundle . fmap go . C.bundle) - where - go (Df.Data (Strict.S2M_ReadData{..}), ack) = (coerce ack, S2M_ReadData{_rvalid=True,..}) - go (_, ack) = (coerce ack, S2M_ReadData{_rvalid=False}) diff --git a/src/Protocols/Axi4/Partial/Full/WriteAddress.hs b/src/Protocols/Axi4/Partial/Full/WriteAddress.hs deleted file mode 100644 index 572bbbb5..00000000 --- a/src/Protocols/Axi4/Partial/Full/WriteAddress.hs +++ /dev/null @@ -1,241 +0,0 @@ -{-| -Defines WriteAddress channel of full AXI4 protocol with port names corresponding -to the AXI4 specification. --} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -Wno-missing-fields #-} - -module Protocols.Axi4.Partial.Full.WriteAddress - ( M2S_WriteAddress(..) - , S2M_WriteAddress(..) - , Axi4WriteAddress - , toStrict, toStrictDf - , fromStrict, fromStrictDf - ) 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 -import Clash.Prelude ((:::)) - --- me -import Protocols.Axi4.Common -import Protocols.Internal -import Protocols.DfLike (DfLike) -import qualified Protocols.DfLike as DfLike -import qualified Protocols.Axi4.Strict.Full.WriteAddress as Strict -import qualified Protocols.Df as Df -import Protocols.Df (Df) - --- | 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{_awvalid=True, _awuser}) = Just _awuser - getPayload _ _ = Nothing - {-# INLINE getPayload #-} - - setPayload _ _ dat (Just b) = dat{_awvalid=True, _awuser=b} - setPayload _ dfB _ Nothing = DfLike.noData dfB - {-# INLINE setPayload #-} - - noData _ = M2S_WriteAddress{_awvalid=False} - {-# 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_WriteAddress - { -- | Write address id* - _awid :: "AWID" ::: C.BitVector (Width iw) - - -- | Write address - , _awaddr :: "AWADDR" ::: C.BitVector (Width aw) - - -- | Write region* - , _awregion:: "AWREGION" ::: RegionType kr - - -- | Burst length* - , _awlen :: "AWLEN" ::: BurstLengthType kbl - - -- | Burst size* - , _awsize :: "AWSIZE" ::: SizeType ksz - - -- | Burst type* - , _awburst :: "AWBURST" ::: BurstType kb - - -- | Lock type* - , _awlock :: "AWLOCK" ::: LockType kl - - -- | Cache type* - , _awcache :: "AWCACHE" ::: CacheType kc - - -- | Protection type - , _awprot :: "AWPROT" ::: PermissionsType kp - - -- | QoS value - , _awqos :: "AWQOS" ::: QosType kq - - -- | Write address valid - , _awvalid :: "AWVALID" ::: Bool - - -- | User data - , _awuser :: "AWUSER" ::: userType - } - deriving (Generic) - --- | See Table A2-2 "Write address channel signals" -newtype S2M_WriteAddress = S2M_WriteAddress - { _awready :: "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) - --- | Convert an 'Axi4WriteAddress' into its strict version --- 'Strict.Axi4WriteAddress'. The latter is usually preferred in Clash designs --- as its definitions don't contain partial fields. Note that the functions --- defined over these circuits operate on @userType@. If you need functions to --- map over all fields, consider using 'toStrictDf'. -toStrict :: - Circuit - (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) - (Strict.Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) -toStrict = Circuit (C.unbundle . fmap go . C.bundle) - where - go (M2S_WriteAddress{..}, ack) - | _awvalid = (coerce ack, Strict.M2S_WriteAddress{..}) - | otherwise = (coerce ack, Strict.M2S_NoWriteAddress) - --- | Convert a 'Strict.Axi4WriteAddress' into 'Axi4WriteAddress' -fromStrict :: - Circuit - (Strict.Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) - (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) -fromStrict = Circuit (C.unbundle . fmap go . C.bundle) - where - go (Strict.M2S_WriteAddress{..}, ack) = (coerce ack, M2S_WriteAddress{_awvalid=True,..}) - go (Strict.M2S_NoWriteAddress, ack) = (coerce ack, M2S_WriteAddress{_awvalid=False}) - --- | Convert an 'Axi4WriteAddress' into its strict 'Df' equivalent. -toStrictDf :: - Circuit - (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) - (Df dom (Strict.M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)) -toStrictDf = Circuit (C.unbundle . fmap go . C.bundle) - where - go (M2S_WriteAddress{..}, ack) - | _awvalid = (coerce ack, Df.Data (Strict.M2S_WriteAddress{..})) - | otherwise = (coerce ack, Df.NoData) - --- | Convert a into 'Axi4WriteAddress' from its Df equivalent -fromStrictDf :: - Circuit - (Df dom (Strict.M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)) - (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) -fromStrictDf = Circuit (C.unbundle . fmap go . C.bundle) - where - go (Df.Data (Strict.M2S_WriteAddress{..}), ack) = (coerce ack, M2S_WriteAddress{_awvalid=True,..}) - go (_, ack) = (coerce ack, M2S_WriteAddress{_awvalid=False}) diff --git a/src/Protocols/Axi4/Partial/Full/WriteData.hs b/src/Protocols/Axi4/Partial/Full/WriteData.hs deleted file mode 100644 index fbea71b7..00000000 --- a/src/Protocols/Axi4/Partial/Full/WriteData.hs +++ /dev/null @@ -1,214 +0,0 @@ -{-| -Defines WriteData channel of full AXI4 protocol with port names corresponding -to the AXI4 specification. --} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -Wno-missing-fields #-} - -module Protocols.Axi4.Partial.Full.WriteData - ( M2S_WriteData(..) - , S2M_WriteData(..) - , Axi4WriteData - , toStrict, toStrictDf - , fromStrict, fromStrictDf - ) where - --- base -import Data.Coerce (coerce) -import Data.Kind (Type) -import Data.Maybe (fromMaybe, isJust) -import Data.Proxy -import GHC.Generics (Generic) -import GHC.TypeNats (Nat) - --- clash-prelude -import qualified Clash.Prelude as C -import Clash.Prelude ((:::), type (*)) - --- me -import Protocols.Axi4.Common -import Protocols.Internal -import Protocols.DfLike (DfLike) -import qualified Protocols.DfLike as DfLike -import qualified Protocols.Axi4.Strict.Full.WriteData as Strict -import qualified Protocols.Df as Df -import Protocols.Df (Df) - --- | 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{_wvalid=True, _wuser}) = Just _wuser - getPayload _ _ = Nothing - {-# INLINE getPayload #-} - - setPayload _ _ dat (Just b) = dat{_wvalid=True, _wuser=b} - setPayload _ dfB _ Nothing = DfLike.noData dfB - {-# INLINE setPayload #-} - - noData _ = M2S_WriteData{_wvalid=False} - {-# 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" -data M2S_WriteData - (ks :: KeepStrobe) - (nBytes :: Nat) - (userType :: Type) = - M2S_WriteData - { -- | Write data - _wdata :: "WDATA" ::: C.BitVector (nBytes*8) - - -- | Write strobes - , _wstrb :: "WSTRB" ::: StrobeType nBytes ks - - -- | Write last - , _wlast :: "WLAST" ::: Bool - - -- | Write valid - , _wvalid :: "WVALID" ::: Bool - - -- | User data - , _wuser :: "WUSER" ::: userType - } - deriving (Generic) - --- | See Table A2-3 "Write data channel signals" -newtype S2M_WriteData = S2M_WriteData - { _wready :: "WREADY" ::: Bool } - deriving (Show, Generic, C.NFDataX) - -deriving instance - ( C.NFDataX userType - , C.NFDataX (StrobeType nBytes ks) ) => - C.NFDataX (M2S_WriteData ks nBytes userType) - -deriving instance - ( Show userType - , Show (StrobeType nBytes ks) - , C.KnownNat nBytes ) => - Show (M2S_WriteData ks nBytes userType) - --- | Convert an 'Axi4WriteData' into its strict version --- 'Strict.Axi4WriteData'. The latter is usually preferred in Clash designs --- as its definitions don't contain partial fields. Note that the functions --- defined over these circuits operate on @userType@. If you need functions to --- map over all fields, consider using 'toStrictDf'. -toStrict :: - C.KnownNat nBytes => - SKeepStrobe ks -> - Circuit - (Axi4WriteData dom ks nBytes userType) - (Strict.Axi4WriteData dom ks nBytes userType) -toStrict SNoStrobe = Circuit (C.unbundle . fmap go . C.bundle) - where - go (M2S_WriteData{..}, ack) - | _wvalid = (coerce ack, Strict.M2S_WriteData{..}) - | otherwise = (coerce ack, Strict.M2S_NoWriteData) -toStrict SKeepStrobe = Circuit (C.unbundle . fmap go . C.bundle) - where - go (M2S_WriteData{..}, ack) - | _wvalid = (coerce ack, Strict.M2S_WriteData{_wdata=strobedData _wdata _wstrb,..}) - | otherwise = (coerce ack, Strict.M2S_NoWriteData) - - strobedData dat strb = C.zipWith orNothing (C.unpack strb) (C.unpack dat) - orNothing p a = if p then Just a else Nothing - --- | Convert a 'Strict.Axi4WriteData' into 'Axi4WriteData' -fromStrict :: - C.KnownNat nBytes => - SKeepStrobe ks -> - Circuit - (Strict.Axi4WriteData dom ks nBytes userType) - (Axi4WriteData dom ks nBytes userType) -fromStrict SNoStrobe = Circuit (C.unbundle . fmap go . C.bundle) - where - go (Strict.M2S_WriteData{..}, ack) = (coerce ack, M2S_WriteData{_wvalid=True,..}) - go (_, ack) = (coerce ack, M2S_WriteData{_wvalid=False}) -fromStrict SKeepStrobe = Circuit (C.unbundle . fmap go . C.bundle) - where - go (Strict.M2S_WriteData{..}, ack) = - (coerce ack, M2S_WriteData - { _wdata=C.pack (C.map (fromMaybe 0) _wdata) - , _wstrb=C.pack (C.map isJust _wdata) - , _wvalid=True - , .. }) - go (_, ack) = - (coerce ack, M2S_WriteData{_wvalid=False}) - --- | Convert an 'Axi4WriteData' into its strict 'Df' equivalent. -toStrictDf :: - C.KnownNat nBytes => - SKeepStrobe ks -> - Circuit - (Axi4WriteData dom ks nBytes userType) - (Df dom (Strict.M2S_WriteData ks nBytes userType)) -toStrictDf keepStrobe = - toStrict keepStrobe |> Circuit (C.unbundle . fmap go . C.bundle) - where - go (dat@Strict.M2S_WriteData {}, ack) = (coerce ack, Df.Data dat) - go (_, ack) = (coerce ack, Df.NoData) - --- | Convert an 'Axi4WriteData' into its strict 'Df' equivalent. -fromStrictDf :: - C.KnownNat nBytes => - SKeepStrobe ks -> - Circuit - (Df dom (Strict.M2S_WriteData ks nBytes userType)) - (Axi4WriteData dom ks nBytes userType) -fromStrictDf keepStrobe = - Circuit (C.unbundle . fmap go . C.bundle) |> fromStrict keepStrobe - where - go (Df.Data dat, ack) = (coerce ack, dat) - go (_, ack) = (coerce ack, Strict.M2S_NoWriteData) diff --git a/src/Protocols/Axi4/Partial/Full/WriteResponse.hs b/src/Protocols/Axi4/Partial/Full/WriteResponse.hs deleted file mode 100644 index a4ebefbe..00000000 --- a/src/Protocols/Axi4/Partial/Full/WriteResponse.hs +++ /dev/null @@ -1,182 +0,0 @@ -{-| -Defines WriteResponse channel of full AXI4 protocol with port names corresponding -to the AXI4 specification. --} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -Wno-missing-fields #-} - -module Protocols.Axi4.Partial.Full.WriteResponse - ( M2S_WriteResponse(..) - , S2M_WriteResponse(..) - , Axi4WriteResponse - , toStrict, toStrictDf - , fromStrict, fromStrictDf - ) 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 -import Clash.Prelude ((:::)) - --- me -import Protocols.Axi4.Common -import Protocols.Internal -import Protocols.DfLike (DfLike) -import qualified Protocols.DfLike as DfLike -import qualified Protocols.Axi4.Strict.Full.WriteResponse as Strict -import qualified Protocols.Df as Df -import Protocols.Df (Df) - --- | 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{_bvalid=True, _buser}) = Just _buser - getPayload _ _ = Nothing - {-# INLINE getPayload #-} - - setPayload _ _ dat (Just b) = dat{_bvalid=True, _buser=b} - setPayload _ dfB _ Nothing = DfLike.noData dfB - {-# INLINE setPayload #-} - - noData _ = S2M_WriteResponse{_bvalid=False} - {-# 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_WriteResponse - { -- | Response ID - _bid :: "BID" ::: C.BitVector (Width iw) - - -- | Write response - , _bresp :: "BRESP" ::: ResponseType kr - - -- | Write response valid - , _bvalid :: "BVALID" ::: Bool - - -- | User data - , _buser :: "BUSER" ::: userType - } - deriving (Generic) - --- | See Table A2-4 "Write response channel signals" -newtype M2S_WriteResponse = M2S_WriteResponse - { _bready :: "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) - --- | Convert an 'Axi4WriteResponse' into its strict version --- 'Strict.Axi4WriteResponse'. The latter is usually preferred in Clash designs --- as its definitions don't contain partial fields. Note that the functions --- defined over these circuits operate on @userType@. If you need functions to --- map over all fields, consider using 'toStrictDf'. -toStrict :: - Circuit - (Axi4WriteResponse dom kr iw userType) - (Strict.Axi4WriteResponse dom kr iw userType) -toStrict = Circuit (C.unbundle . fmap go . C.bundle) - where - go (S2M_WriteResponse{..}, ack) - | _bvalid = (coerce ack, Strict.S2M_WriteResponse{..}) - | otherwise = (coerce ack, Strict.S2M_NoWriteResponse) - --- | Convert a 'Strict.Axi4WriteResponse' into 'Axi4WriteResponse' -fromStrict :: - Circuit - (Strict.Axi4WriteResponse dom kr iw userType) - (Axi4WriteResponse dom kr iw userType) -fromStrict = Circuit (C.unbundle . fmap go . C.bundle) - where - go (Strict.S2M_WriteResponse{..}, ack) = (coerce ack, S2M_WriteResponse{_bvalid=True,..}) - go (Strict.S2M_NoWriteResponse, ack) = (coerce ack, S2M_WriteResponse{_bvalid=False}) - --- | Convert an 'Axi4WriteResponse' into its strict 'Df' equivalent. -toStrictDf :: - Circuit - (Axi4WriteResponse dom kr iw userType) - (Df dom (Strict.S2M_WriteResponse kr iw userType)) -toStrictDf = Circuit (C.unbundle . fmap go . C.bundle) - where - go (S2M_WriteResponse{..}, ack) - | _bvalid = (coerce ack, Df.Data (Strict.S2M_WriteResponse{..})) - | otherwise = (coerce ack, Df.NoData) - --- | Convert a into 'Axi4WriteResponse' from its Df equivalent -fromStrictDf :: - Circuit - (Df dom (Strict.S2M_WriteResponse kr iw userType)) - (Axi4WriteResponse dom kr iw userType) -fromStrictDf = Circuit (C.unbundle . fmap go . C.bundle) - where - go (Df.Data (Strict.S2M_WriteResponse{..}), ack) = (coerce ack, S2M_WriteResponse{_bvalid=True,..}) - go (_, ack) = (coerce ack, S2M_WriteResponse{_bvalid=False}) diff --git a/src/Protocols/Axi4/Strict/Full/ReadAddress.hs b/src/Protocols/Axi4/ReadAddress.hs similarity index 99% rename from src/Protocols/Axi4/Strict/Full/ReadAddress.hs rename to src/Protocols/Axi4/ReadAddress.hs index 85092e87..6b63af49 100644 --- a/src/Protocols/Axi4/Strict/Full/ReadAddress.hs +++ b/src/Protocols/Axi4/ReadAddress.hs @@ -10,7 +10,7 @@ to the AXI4 specification. {-# OPTIONS_GHC -Wno-missing-fields #-} -module Protocols.Axi4.Strict.Full.ReadAddress +module Protocols.Axi4.ReadAddress ( M2S_ReadAddress(..) , S2M_ReadAddress(..) , Axi4ReadAddress @@ -102,6 +102,7 @@ instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType DfLike.stall Proxy conf stallAck stalls -- | See Table A2-5 "Read address channel signals" + data M2S_ReadAddress (kb :: KeepBurst) (ksz :: KeepSize) @@ -184,3 +185,4 @@ deriving instance , 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/ReadData.hs similarity index 61% rename from src/Protocols/Axi4/Strict/Full/ReadData.hs rename to src/Protocols/Axi4/ReadData.hs index a559d49e..4baee7ec 100644 --- a/src/Protocols/Axi4/Strict/Full/ReadData.hs +++ b/src/Protocols/Axi4/ReadData.hs @@ -10,10 +10,11 @@ to the AXI4 specification. {-# OPTIONS_GHC -Wno-missing-fields #-} -module Protocols.Axi4.Strict.Full.ReadData +module Protocols.Axi4.ReadData ( M2S_ReadData(..) , S2M_ReadData(..) , Axi4ReadData + , map ) where -- base @@ -21,6 +22,8 @@ import Data.Coerce (coerce) import Data.Kind (Type) import GHC.Generics (Generic) import Data.Proxy +import Prelude hiding + ((!!), map, zip, zipWith, filter, fst, snd, either, const, pure) -- clash-prelude import qualified Clash.Prelude as C @@ -36,32 +39,32 @@ data Axi4ReadData (dom :: C.Domain) (kr :: KeepResponse) (iw :: IdWidth) - (dataType :: Type) (userType :: Type) + (dataType :: 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) = +instance Protocol (Axi4ReadData dom kr iw userType dataType) where + type Fwd (Axi4ReadData dom kr iw userType dataType) = + C.Signal dom (S2M_ReadData kr iw userType dataType) + type Bwd (Axi4ReadData dom kr iw userType dataType) = C.Signal dom M2S_ReadData -instance Backpressure (Axi4ReadData dom kr iw dataType userType) where +instance Backpressure (Axi4ReadData dom kr iw userType dataType) 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 +instance DfLike dom (Axi4ReadData dom kr iw userType) dataType where + type Data (Axi4ReadData dom kr iw userType) dataType = + S2M_ReadData kr iw userType dataType - type Payload userType = userType + type Payload dataType = dataType - type Ack (Axi4ReadData dom kr iw dataType) userType = + type Ack (Axi4ReadData dom kr iw userType) dataType = M2S_ReadData - getPayload _ (S2M_ReadData{_ruser}) = Just _ruser + getPayload _ (S2M_ReadData{_rdata}) = Just _rdata getPayload _ S2M_NoReadData = Nothing {-# INLINE getPayload #-} - setPayload _ _ dat (Just b) = dat{_ruser=b} + setPayload _ _ dat (Just b) = dat{_rdata=b} setPayload _ dfB _ Nothing = DfLike.noData dfB {-# INLINE setPayload #-} @@ -74,16 +77,16 @@ instance DfLike dom (Axi4ReadData dom kr iw dataType) userType where ackToBool _ = coerce {-# INLINE ackToBool #-} -instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) => - Simulate (Axi4ReadData dom kr iw dataType userType) where +instance (C.KnownDomain dom, C.NFDataX dataType, C.ShowX dataType, Show dataType) => + Simulate (Axi4ReadData dom kr iw userType dataType) where - type SimulateType (Axi4ReadData dom kr iw dataType userType) = - [S2M_ReadData kr iw dataType userType] + type SimulateType (Axi4ReadData dom kr iw userType dataType) = + [S2M_ReadData kr iw userType dataType] - type ExpectType (Axi4ReadData dom kr iw dataType userType) = - [S2M_ReadData kr iw dataType userType] + type ExpectType (Axi4ReadData dom kr iw userType dataType) = + [S2M_ReadData kr iw userType dataType] - type SimulateChannels (Axi4ReadData dom kr iw dataType userType) = 1 + type SimulateChannels (Axi4ReadData dom kr iw userType dataType) = 1 toSimulateType _ = id fromSimulateType _ = id @@ -97,8 +100,8 @@ instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType data S2M_ReadData (kr :: KeepResponse) (iw :: IdWidth) - (dataType :: Type) (userType :: Type) + (dataType :: Type) = S2M_NoReadData | S2M_ReadData { -- | Read address id* @@ -126,11 +129,17 @@ deriving instance ( C.NFDataX userType , C.NFDataX dataType , C.NFDataX (ResponseType kr) ) => - C.NFDataX (S2M_ReadData kr iw dataType userType) + C.NFDataX (S2M_ReadData kr iw userType dataType) deriving instance ( C.KnownNat (Width iw) , Show userType , Show dataType , Show (ResponseType kr) ) => - Show (S2M_ReadData kr iw dataType userType) + Show (S2M_ReadData kr iw userType dataType) + + +map :: (a -> b) -> Circuit + (Axi4ReadData dom kr iw dataType a) + (Axi4ReadData dom kr iw dataType b) +map = DfLike.map Proxy Proxy diff --git a/src/Protocols/Axi4/Strict/Full.hs b/src/Protocols/Axi4/Strict/Full.hs deleted file mode 100644 index 08c7bd21..00000000 --- a/src/Protocols/Axi4/Strict/Full.hs +++ /dev/null @@ -1,23 +0,0 @@ -{-| -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/WriteAddress.hs b/src/Protocols/Axi4/WriteAddress.hs similarity index 99% rename from src/Protocols/Axi4/Strict/Full/WriteAddress.hs rename to src/Protocols/Axi4/WriteAddress.hs index 37391c1d..16ac35a9 100644 --- a/src/Protocols/Axi4/Strict/Full/WriteAddress.hs +++ b/src/Protocols/Axi4/WriteAddress.hs @@ -10,7 +10,7 @@ to the AXI4 specification. {-# OPTIONS_GHC -Wno-missing-fields #-} -module Protocols.Axi4.Strict.Full.WriteAddress +module Protocols.Axi4.WriteAddress ( M2S_WriteAddress(..) , S2M_WriteAddress(..) , Axi4WriteAddress @@ -183,3 +183,4 @@ deriving instance , 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/WriteData.hs similarity index 96% rename from src/Protocols/Axi4/Strict/Full/WriteData.hs rename to src/Protocols/Axi4/WriteData.hs index dcdbcc79..70bdc8e2 100644 --- a/src/Protocols/Axi4/Strict/Full/WriteData.hs +++ b/src/Protocols/Axi4/WriteData.hs @@ -10,10 +10,11 @@ to the AXI4 specification. {-# OPTIONS_GHC -Wno-missing-fields #-} -module Protocols.Axi4.Strict.Full.WriteData +module Protocols.Axi4.WriteData ( M2S_WriteData(..) , S2M_WriteData(..) , Axi4WriteData + , map ) where -- base @@ -22,6 +23,8 @@ import Data.Kind (Type) import GHC.Generics (Generic) import GHC.TypeNats (Nat) import Data.Proxy +import Prelude hiding + ((!!), map, zip, zipWith, filter, fst, snd, either, const, pure) -- clash-prelude import qualified Clash.Prelude as C @@ -127,3 +130,4 @@ deriving instance , 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/WriteResponse.hs similarity index 98% rename from src/Protocols/Axi4/Strict/Full/WriteResponse.hs rename to src/Protocols/Axi4/WriteResponse.hs index c86935ba..950218bc 100644 --- a/src/Protocols/Axi4/Strict/Full/WriteResponse.hs +++ b/src/Protocols/Axi4/WriteResponse.hs @@ -10,7 +10,7 @@ to the AXI4 specification. {-# OPTIONS_GHC -Wno-missing-fields #-} -module Protocols.Axi4.Strict.Full.WriteResponse +module Protocols.Axi4.WriteResponse ( M2S_WriteResponse(..) , S2M_WriteResponse(..) , Axi4WriteResponse @@ -124,3 +124,4 @@ deriving instance , Show (ResponseType kr) , C.KnownNat (Width iw) ) => Show (S2M_WriteResponse kr iw userType) + From 02fe32b7111254c9b808fdbc69770ad21fd91fa5 Mon Sep 17 00:00:00 2001 From: Pieter Staal Date: Thu, 9 Dec 2021 11:22:54 +0100 Subject: [PATCH 07/12] Add mapDfLike --- src/Protocols/Axi4/ReadAddress.hs | 13 +++++++++++++ src/Protocols/Axi4/ReadData.hs | 12 ++++++++++++ src/Protocols/Axi4/WriteAddress.hs | 12 ++++++++++++ src/Protocols/Axi4/WriteData.hs | 8 +++++++- src/Protocols/Axi4/WriteResponse.hs | 11 +++++++++++ src/Protocols/DfLike.hs | 27 +++++++++++++++++++++++---- 6 files changed, 78 insertions(+), 5 deletions(-) diff --git a/src/Protocols/Axi4/ReadAddress.hs b/src/Protocols/Axi4/ReadAddress.hs index 6b63af49..4532de08 100644 --- a/src/Protocols/Axi4/ReadAddress.hs +++ b/src/Protocols/Axi4/ReadAddress.hs @@ -14,6 +14,7 @@ module Protocols.Axi4.ReadAddress ( M2S_ReadAddress(..) , S2M_ReadAddress(..) , Axi4ReadAddress + , mapDfLike ) where -- base @@ -186,3 +187,15 @@ deriving instance , C.NFDataX (QosType kq) ) => C.NFDataX (M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) + +mapFull :: + forall dom + kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 t1 + kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 t2 . + (M2S_ReadAddress kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 t1 -> + M2S_ReadAddress kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 t2) -> + (S2M_ReadAddress -> S2M_ReadAddress) -> + Circuit + (Axi4ReadAddress dom kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 t1) + (Axi4ReadAddress dom kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 t2) +mapFull = DfLike.mapDfLike Proxy Proxy diff --git a/src/Protocols/Axi4/ReadData.hs b/src/Protocols/Axi4/ReadData.hs index 4baee7ec..21050a4d 100644 --- a/src/Protocols/Axi4/ReadData.hs +++ b/src/Protocols/Axi4/ReadData.hs @@ -15,6 +15,7 @@ module Protocols.Axi4.ReadData , S2M_ReadData(..) , Axi4ReadData , map + , mapDfLike ) where -- base @@ -143,3 +144,14 @@ map :: (a -> b) -> Circuit (Axi4ReadData dom kr iw dataType a) (Axi4ReadData dom kr iw dataType b) map = DfLike.map Proxy Proxy + +mapFull :: + forall dom + kr1 iw1 userType1 dataType1 + kr2 iw2 userType2 dataType2 . + (S2M_ReadData kr1 iw1 userType1 dataType1 -> S2M_ReadData kr2 iw2 userType2 dataType2) -> + (M2S_ReadData -> M2S_ReadData) -> + Circuit + (Axi4ReadData dom kr1 iw1 userType1 dataType1) + (Axi4ReadData dom kr2 iw2 userType2 dataType2) +mapFull = DfLike.mapDfLike Proxy Proxy diff --git a/src/Protocols/Axi4/WriteAddress.hs b/src/Protocols/Axi4/WriteAddress.hs index 16ac35a9..02990f05 100644 --- a/src/Protocols/Axi4/WriteAddress.hs +++ b/src/Protocols/Axi4/WriteAddress.hs @@ -14,6 +14,7 @@ module Protocols.Axi4.WriteAddress ( M2S_WriteAddress(..) , S2M_WriteAddress(..) , Axi4WriteAddress + , mapDfLike ) where -- base @@ -184,3 +185,14 @@ deriving instance , C.NFDataX (QosType kq) ) => C.NFDataX (M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) +mapFull :: + forall dom + kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 userType1 + kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 userType2 . + (M2S_WriteAddress kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 userType1 -> + M2S_WriteAddress kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 userType2) -> + (S2M_WriteAddress -> S2M_WriteAddress) -> + Circuit + (Axi4WriteAddress dom kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 userType1) + (Axi4WriteAddress dom kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 userType2) +mapFull = DfLike.mapDfLike Proxy Proxy diff --git a/src/Protocols/Axi4/WriteData.hs b/src/Protocols/Axi4/WriteData.hs index 70bdc8e2..efd2b275 100644 --- a/src/Protocols/Axi4/WriteData.hs +++ b/src/Protocols/Axi4/WriteData.hs @@ -14,7 +14,7 @@ module Protocols.Axi4.WriteData ( M2S_WriteData(..) , S2M_WriteData(..) , Axi4WriteData - , map + , mapDfLike ) where -- base @@ -131,3 +131,9 @@ deriving instance , C.KnownNat nBytes ) => Show (M2S_WriteData ks nBytes userType) +mapFull :: + forall dom ks1 ks2 nBytes1 nBytes2 t1 t2. + (M2S_WriteData ks1 nBytes1 t1 -> M2S_WriteData ks2 nBytes2 t2) -> + (S2M_WriteData -> S2M_WriteData) -> + Circuit ((Axi4WriteData dom ks1 nBytes1) t1) ((Axi4WriteData dom ks2 nBytes2) t2) +mapFull = DfLike.mapDfLike Proxy Proxy diff --git a/src/Protocols/Axi4/WriteResponse.hs b/src/Protocols/Axi4/WriteResponse.hs index 950218bc..e2bffff0 100644 --- a/src/Protocols/Axi4/WriteResponse.hs +++ b/src/Protocols/Axi4/WriteResponse.hs @@ -14,6 +14,7 @@ module Protocols.Axi4.WriteResponse ( M2S_WriteResponse(..) , S2M_WriteResponse(..) , Axi4WriteResponse + , mapDfLike ) where -- base @@ -125,3 +126,13 @@ deriving instance , C.KnownNat (Width iw) ) => Show (S2M_WriteResponse kr iw userType) +mapFull :: + forall dom + kr1 iw1 userType1 + kr2 iw2 userType2 . + (S2M_WriteResponse kr1 iw1 userType1 -> S2M_WriteResponse kr2 iw2 userType2) -> + (M2S_WriteResponse -> M2S_WriteResponse) -> + Circuit + (Axi4WriteResponse dom kr1 iw1 userType1) + (Axi4WriteResponse dom kr2 iw2 userType2) +mapFull = DfLike.mapDfLike Proxy Proxy diff --git a/src/Protocols/DfLike.hs b/src/Protocols/DfLike.hs index 50373b6b..1abc4d55 100644 --- a/src/Protocols/DfLike.hs +++ b/src/Protocols/DfLike.hs @@ -21,6 +21,7 @@ module Protocols.DfLike -- * Operations on Df like protocols , const, pure, void + , mapDfLike , map, bimap , fst, snd , mapMaybe, catMaybes @@ -123,7 +124,7 @@ hasPayload :: DfLike dom df a => Proxy (df a) -> Data df a -> Bool hasPayload dfA = Maybe.isJust . getPayload dfA {-# INLINE hasPayload #-} -mapData :: +mapPayload :: forall df dom a b. ( DfLike dom df a , DfLike dom df b ) => @@ -132,9 +133,27 @@ mapData :: (Payload a -> Payload b) -> Data df a -> Data df b -mapData dfA dfB f fwdA = +mapPayload dfA dfB f fwdA = setPayload dfA dfB fwdA (fmap f (getPayload dfA fwdA)) -{-# INLINE mapData #-} +{-# INLINE mapPayload #-} + + +-- | Allows conversion of one DfLike protocol into another, given two functions that +-- transform the data and ack type of one protocol to the other. +mapDfLike :: + forall df1 df2 dom a1 a2. + ( DfLike dom df1 a1 + , DfLike dom df2 a2 ) => + Proxy (df1 a1) -> + Proxy (df2 a2) -> + (Data df1 a1 -> Data df2 a2) -> + (Ack df2 a2 -> Ack df1 a1) -> + Circuit (df1 a1) (df2 a2) +mapDfLike Proxy Proxy fData fAck = Circuit (CE.unbundle . fmap go . CE.bundle) + where + go :: (Data df1 a1, Ack df2 a2) -> (Ack df1 a1, Data df2 a2) + go (d, ack) = (fAck ack, fData d) + -- | Like 'P.map' map :: @@ -149,7 +168,7 @@ map dfA dfB f = Circuit (uncurry go) where go fwd bwd = ( boolToAck dfA . ackToBool dfB <$> bwd - , mapData dfA dfB f <$> fwd ) + , mapPayload dfA dfB f <$> fwd ) {-# INLINE map #-} -- | Like 'P.fst' From 8f0c8807f7f9bbacfd308e7a8df81bd2aa8d132e Mon Sep 17 00:00:00 2001 From: Pieter Staal Date: Thu, 9 Dec 2021 14:40:51 +0100 Subject: [PATCH 08/12] Add DfLike convenience functions to AXI4 Read Data channel --- src/Protocols/Axi4/ReadAddress.hs | 2 +- src/Protocols/Axi4/ReadData.hs | 276 +++++++++++++++++++++++++++- src/Protocols/Axi4/WriteAddress.hs | 2 +- src/Protocols/Axi4/WriteData.hs | 2 +- src/Protocols/Axi4/WriteResponse.hs | 2 +- 5 files changed, 276 insertions(+), 8 deletions(-) diff --git a/src/Protocols/Axi4/ReadAddress.hs b/src/Protocols/Axi4/ReadAddress.hs index 4532de08..9fc50ba1 100644 --- a/src/Protocols/Axi4/ReadAddress.hs +++ b/src/Protocols/Axi4/ReadAddress.hs @@ -14,7 +14,7 @@ module Protocols.Axi4.ReadAddress ( M2S_ReadAddress(..) , S2M_ReadAddress(..) , Axi4ReadAddress - , mapDfLike + , mapFull ) where -- base diff --git a/src/Protocols/Axi4/ReadData.hs b/src/Protocols/Axi4/ReadData.hs index 21050a4d..03901d1b 100644 --- a/src/Protocols/Axi4/ReadData.hs +++ b/src/Protocols/Axi4/ReadData.hs @@ -14,12 +14,38 @@ module Protocols.Axi4.ReadData ( M2S_ReadData(..) , S2M_ReadData(..) , Axi4ReadData - , map - , mapDfLike + , mapFull + + -- * Operations on Df like protocols + , const, void, pure + , map, bimap + , fst, snd + , mapMaybe, catMaybes + , filter + , either + , first, {-firstT,-} mapLeft + , second, {-secondT,-} mapRight + , zipWith, zip + , partition + , route + , select + , selectN + , selectUntil + , fanin + , mfanin + , fanout + , bundleVec + , unbundleVec + , roundrobin + , roundrobinCollect + , registerFwd + , registerBwd + ) where -- base import Data.Coerce (coerce) +import Data.Bifunctor (Bifunctor) import Data.Kind (Type) import GHC.Generics (Generic) import Data.Proxy @@ -140,11 +166,252 @@ deriving instance Show (S2M_ReadData kr iw userType dataType) +-- | Like 'P.map', but over the data in the AXI4 read channel. map :: (a -> b) -> Circuit - (Axi4ReadData dom kr iw dataType a) - (Axi4ReadData dom kr iw dataType b) + (Axi4ReadData dom kr iw userType a) + (Axi4ReadData dom kr iw userType b) map = DfLike.map Proxy Proxy +-- | Like 'bimap', but over the data in the AXI4 read channel. +bimap :: Bifunctor p => (a -> b) -> (c -> d) -> Circuit + (Axi4ReadData dom kr iw userType (p a c)) + (Axi4ReadData dom kr iw userType (p b d)) +bimap = DfLike.bimap + +-- | Like 'P.fst', but over the data in the AXI4 read channel. +fst :: Circuit + (Axi4ReadData dom kr iw userType (a, b)) + (Axi4ReadData dom kr iw userType a) +fst = DfLike.fst + +-- | Like 'P.snd', but over the data in the AXI4 read channel. +snd :: Circuit + (Axi4ReadData dom kr iw userType (a, b)) + (Axi4ReadData dom kr iw userType b) +snd = DfLike.snd + +-- | Like 'Data.Bifunctor.first', but over the data in the AXI4 read channel. +first :: Bifunctor p => (a -> b) -> Circuit + (Axi4ReadData dom kr iw userType (p a c)) + (Axi4ReadData dom kr iw userType (p b c)) +first = DfLike.first + +-- | Like 'Data.Bifunctor.second', but over the data in the AXI4 read channel. +second :: Bifunctor p => (b -> c) -> Circuit + (Axi4ReadData dom kr iw userType (p a b)) + (Axi4ReadData dom kr iw userType (p a c)) +second = DfLike.second + +-- | Acknowledge but ignore data from LHS protocol. Send a static value /b/. +const :: C.HiddenReset dom => S2M_ReadData kr iw userType b -> Circuit + (Axi4ReadData dom kr iw userType a) + (Axi4ReadData dom kr iw userType b) +const = DfLike.const Proxy Proxy + +-- | Drive a constant value composed of /a/. +pure :: S2M_ReadData kr iw userType a -> Circuit + () + (Axi4ReadData dom kr iw userType a) +pure = DfLike.pure Proxy + +-- | Drive a constant value composed of /a/. +void :: C.HiddenReset dom => Circuit (Axi4ReadData dom kr iw userType a) () +void = DfLike.void Proxy + +-- | Like 'Data.Maybe.catMaybes', but over a AXI4 read data stream. +catMaybes :: Circuit + (Axi4ReadData dom kr iw userType (Maybe a)) + (Axi4ReadData dom kr iw userType a) +catMaybes = DfLike.catMaybes Proxy Proxy + +-- | Like 'Data.Maybe.mapMaybe', but over payload (/a/) of a AXI4 read data stream. +mapMaybe :: (a -> Maybe b) -> Circuit + (Axi4ReadData dom kr iw userType a) + (Axi4ReadData dom kr iw userType b) +mapMaybe = DfLike.mapMaybe + +-- | Like 'P.filter', but over a AXI4 read data stream. +filter :: forall dom a kr iw userType. (a -> Bool) -> Circuit + (Axi4ReadData dom kr iw userType a) + (Axi4ReadData dom kr iw userType a) +filter = DfLike.filter Proxy + +-- | Like 'Data.Either.Combinators.mapLeft', but over the data in the AXI4 read channel. +mapLeft :: (a -> b) -> Circuit + (Axi4ReadData dom kr iw userType (Either a c)) + (Axi4ReadData dom kr iw userType (Either b c)) +mapLeft = DfLike.mapLeft + +-- | Like 'Data.Either.Combinators.mapRight', but over the data in the AXI4 read channel. +mapRight :: (b -> c) -> Circuit + (Axi4ReadData dom kr iw userType (Either a b)) + (Axi4ReadData dom kr iw userType (Either a c)) +mapRight = DfLike.mapRight + +-- | Like 'Data.Either.either', but over a AXI4 read data stream. +either :: (a -> c) -> (b -> c) -> Circuit + (Axi4ReadData dom kr iw userType (Either a b)) + (Axi4ReadData dom kr iw userType c) +either = DfLike.either + + +-- | Like 'P.zipWith', but over two AXI4 read data streams. +zipWith :: + forall dom a b c kr iw userType . + (a -> b -> c) -> + Circuit + (Axi4ReadData dom kr iw userType a, Axi4ReadData dom kr iw userType b) + (Axi4ReadData dom kr iw userType c) +zipWith = DfLike.zipWith Proxy Proxy Proxy + +-- | Like 'P.zip', but over two AXI4 read data streams. +zip :: forall a b dom kr iw userType . Circuit + (Axi4ReadData dom kr iw userType a, Axi4ReadData dom kr iw userType b) + (Axi4ReadData dom kr iw userType (a, b)) +zip = DfLike.zip Proxy Proxy Proxy + +-- | Like 'P.partition', but over AXI4 read data streams +partition :: forall dom a kr iw userType. (a -> Bool) -> Circuit + (Axi4ReadData dom kr iw userType a) + (Axi4ReadData dom kr iw userType a, Axi4ReadData dom kr iw userType a) +partition = DfLike.partition Proxy + + +-- | Route a AXI4 read data stream to another corresponding to the index +route :: + forall n dom a kr iw userType . + C.KnownNat n => Circuit + (Axi4ReadData dom kr iw userType (C.Index n, a)) + (C.Vec n (Axi4ReadData dom kr iw userType a)) +route = DfLike.route Proxy Proxy + + +-- | Select data from the channel indicated by the AXI4 read data stream carrying +-- @Index n@. +select :: + forall n dom a kr iw userType . + C.KnownNat n => + Circuit + (C.Vec n (Axi4ReadData dom kr iw userType a), Axi4ReadData dom kr iw userType (C.Index n)) + (Axi4ReadData dom kr iw userType a) +select = DfLike.select + + + +-- | Select /selectN/ samples from channel /n/. +selectN :: + forall n selectN dom a kr iw userType. + ( C.HiddenClockResetEnable dom + , C.KnownNat selectN + , C.KnownNat n + ) => + Circuit + (C.Vec n (Axi4ReadData dom kr iw userType a), Axi4ReadData dom kr iw userType (C.Index n, C.Index selectN)) + (Axi4ReadData dom kr iw userType a) +selectN = DfLike.selectN Proxy Proxy + +-- | Selects samples from channel /n/ until the predicate holds. The cycle in +-- which the predicate turns true is included. +selectUntil :: + forall n dom a kr iw userType . + C.KnownNat n => + (a -> Bool) -> + Circuit + (C.Vec n (Axi4ReadData dom kr iw userType a), Axi4ReadData dom kr iw userType (C.Index n)) + (Axi4ReadData dom kr iw userType a) +selectUntil = DfLike.selectUntil Proxy Proxy + +-- | Copy data of a single AXI4 read data stream to multiple. LHS will only receive +-- an acknowledgement when all RHS receivers have acknowledged data. +fanout :: + forall n dom a kr iw userType . + (C.KnownNat n, C.HiddenClockResetEnable dom, 1 C.<= n) => + Circuit + (Axi4ReadData dom kr iw userType a) + (C.Vec n (Axi4ReadData dom kr iw userType a)) +fanout = DfLike.fanout Proxy + +-- | Merge data of multiple AXI4 read data streams using a user supplied function +fanin :: + forall n dom a kr iw userType . + (C.KnownNat n, 1 C.<= n) => + (a -> a -> a) -> + Circuit + (C.Vec n (Axi4ReadData dom kr iw userType a)) + (Axi4ReadData dom kr iw userType a) +fanin = DfLike.fanin + +-- | Merge data of multiple AXI4 read data streams using Monoid's '<>'. +mfanin :: + forall n dom a kr iw userType . + (C.KnownNat n, Monoid a, 1 C.<= n) => + Circuit + (C.Vec n (Axi4ReadData dom kr iw userType a)) + (Axi4ReadData dom kr iw userType a) +mfanin = DfLike.mfanin + +-- | Bundle a vector of AXI4 read data streams into one. +bundleVec :: + forall n dom a kr iw userType . + (C.KnownNat n, 1 C.<= n) => + Circuit + (C.Vec n (Axi4ReadData dom kr iw userType a)) + (Axi4ReadData dom kr iw userType (C.Vec n a)) +bundleVec = DfLike.bundleVec Proxy Proxy + +-- | Split up a AXI4 read data stream of a vector into multiple independent AXI4 read data streams. +unbundleVec :: + forall n dom a kr iw userType . + (C.KnownNat n, C.NFDataX a, C.HiddenClockResetEnable dom, 1 C.<= n) => + Circuit + (Axi4ReadData dom kr iw userType (C.Vec n a)) + (C.Vec n (Axi4ReadData dom kr iw userType a)) +unbundleVec = DfLike.unbundleVec Proxy Proxy + +-- | Distribute data across multiple components on the RHS. Useful if you want +-- to parallelize a workload across multiple (slow) workers. For optimal +-- throughput, you should make sure workers can accept data every /n/ cycles. +roundrobin :: + forall n dom a kr iw userType . + (C.KnownNat n, C.HiddenClockResetEnable dom, 1 C.<= n) => + Circuit + (Axi4ReadData dom kr iw userType a) + (C.Vec n (Axi4ReadData dom kr iw userType a)) +roundrobin = DfLike.roundrobin Proxy + +-- | Opposite of 'roundrobin'. Useful to collect data from workers that only +-- produce a result with an interval of /n/ cycles. +roundrobinCollect :: + forall n dom a kr iw userType . + (C.KnownNat n, C.HiddenClockResetEnable dom, 1 C.<= n) => + DfLike.CollectMode -> + Circuit + (C.Vec n (Axi4ReadData dom kr iw userType a)) + (Axi4ReadData dom kr iw userType a) +roundrobinCollect = DfLike.roundrobinCollect Proxy + +-- | Place register on /forward/ part of a circuit. +registerFwd :: + forall dom a kr iw userType . + (C.NFDataX a, C.HiddenClockResetEnable dom, C.NFDataX (ResponseType kr), C.NFDataX userType) => + Circuit + (Axi4ReadData dom kr iw userType a) + (Axi4ReadData dom kr iw userType a) +registerFwd = DfLike.registerFwd Proxy + +-- | Place register on /backward/ part of a circuit. This is implemented using a +-- in-logic two-element shift register. +registerBwd :: + (C.NFDataX a, C.HiddenClockResetEnable dom, C.NFDataX (ResponseType kr), C.NFDataX userType) => + Circuit + (Axi4ReadData dom kr iw userType a) + (Axi4ReadData dom kr iw userType a) +registerBwd = DfLike.registerBwd Proxy + + +-- | Circuit that transforms the LHS version of the 'Axi4ReadData' protocol to a +-- version using different parameters according to two functions +-- that can transform the data and ack signal accordingly to and from the other protocol. mapFull :: forall dom kr1 iw1 userType1 dataType1 @@ -155,3 +422,4 @@ mapFull :: (Axi4ReadData dom kr1 iw1 userType1 dataType1) (Axi4ReadData dom kr2 iw2 userType2 dataType2) mapFull = DfLike.mapDfLike Proxy Proxy + diff --git a/src/Protocols/Axi4/WriteAddress.hs b/src/Protocols/Axi4/WriteAddress.hs index 02990f05..1cf79322 100644 --- a/src/Protocols/Axi4/WriteAddress.hs +++ b/src/Protocols/Axi4/WriteAddress.hs @@ -14,7 +14,7 @@ module Protocols.Axi4.WriteAddress ( M2S_WriteAddress(..) , S2M_WriteAddress(..) , Axi4WriteAddress - , mapDfLike + , mapFull ) where -- base diff --git a/src/Protocols/Axi4/WriteData.hs b/src/Protocols/Axi4/WriteData.hs index efd2b275..b58a70ba 100644 --- a/src/Protocols/Axi4/WriteData.hs +++ b/src/Protocols/Axi4/WriteData.hs @@ -14,7 +14,7 @@ module Protocols.Axi4.WriteData ( M2S_WriteData(..) , S2M_WriteData(..) , Axi4WriteData - , mapDfLike + , mapFull ) where -- base diff --git a/src/Protocols/Axi4/WriteResponse.hs b/src/Protocols/Axi4/WriteResponse.hs index e2bffff0..64ff65a7 100644 --- a/src/Protocols/Axi4/WriteResponse.hs +++ b/src/Protocols/Axi4/WriteResponse.hs @@ -14,7 +14,7 @@ module Protocols.Axi4.WriteResponse ( M2S_WriteResponse(..) , S2M_WriteResponse(..) , Axi4WriteResponse - , mapDfLike + , mapFull ) where -- base From 24b92540fdb82b86de94494a3815ad6afbaaeac8 Mon Sep 17 00:00:00 2001 From: Pieter Staal Date: Mon, 13 Dec 2021 10:04:38 +0100 Subject: [PATCH 09/12] Add Eq instance to most AXI4 types --- src/Protocols/Axi4/Common.hs | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/Protocols/Axi4/Common.hs b/src/Protocols/Axi4/Common.hs index 5cba3efc..4afe799c 100644 --- a/src/Protocols/Axi4/Common.hs +++ b/src/Protocols/Axi4/Common.hs @@ -19,50 +19,50 @@ import Clash.Prelude (type (^), type (-), type (*)) import Data.Tuple.Strict (T3, T4) -- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol -data IdWidth = IdWidth Nat deriving (Show) +data IdWidth = IdWidth Nat deriving (Show, Eq) -- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol -data AddrWidth = AddrWidth Nat deriving (Show) +data AddrWidth = AddrWidth Nat deriving (Show, Eq) -- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol -data LengthWidth = LengthWidth Nat deriving (Show) +data LengthWidth = LengthWidth Nat deriving (Show, Eq) -- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol data UserType = UserType Type KeepStrobe -- | Keep or remove Burst, see 'BurstMode' -data KeepBurst = KeepBurst | NoBurst deriving (Show) +data KeepBurst = KeepBurst | NoBurst deriving (Show, Eq) -- | Keep or remove Burst Length, see 'BurstSize' -data KeepBurstLength = KeepBurstLength | NoBurstLength deriving (Show) +data KeepBurstLength = KeepBurstLength | NoBurstLength deriving (Show, Eq) -- | Keep or remove cache field, see 'Cache' -data KeepCache = KeepCache | NoCache deriving (Show) +data KeepCache = KeepCache | NoCache deriving (Show, Eq) -- | Keep or remove last field -data KeepLast = KeepLast | NoLast deriving (Show) +data KeepLast = KeepLast | NoLast deriving (Show, Eq) -- | Keep or remove lock, see 'AtomicAccess' -data KeepLock = KeepLock | NoLock deriving (Show) +data KeepLock = KeepLock | NoLock deriving (Show, Eq) -- | Keep or remove permissions, see 'Privileged', 'Secure', and -- 'InstructionOrData'. -data KeepPermissions = KeepPermissions | NoPermissions deriving (Show) +data KeepPermissions = KeepPermissions | NoPermissions deriving (Show, Eq) -- | Keep or remove quality of service field. See 'Qos'. -data KeepQos = KeepQos | NoQos deriving (Show) +data KeepQos = KeepQos | NoQos deriving (Show, Eq) -- | Keep or remove region field -data KeepRegion = KeepRegion | NoRegion deriving (Show) +data KeepRegion = KeepRegion | NoRegion deriving (Show, Eq) -- | Keep or remove response field. See 'Resp'. -data KeepResponse = KeepResponse | NoResponse deriving (Show) +data KeepResponse = KeepResponse | NoResponse deriving (Show, Eq) -- | Keep or remove burst size field. See 'BurstSize'. -data KeepSize = KeepSize | NoSize deriving (Show) +data KeepSize = KeepSize | NoSize deriving (Show, Eq) -- | Keep or remove strobe field. See 'Strobe' -data KeepStrobe = KeepStrobe | NoStrobe deriving (Show) +data KeepStrobe = KeepStrobe | NoStrobe deriving (Show, Eq) -- | Type used to introduce strobe information on the term level data SKeepStrobe (strobeType :: KeepStrobe) where @@ -188,7 +188,7 @@ data BurstMode -- This burst type is used for cache line accesses. -- | BmWrap - deriving (Show, C.ShowX, Generic, C.NFDataX) + deriving (Show, C.ShowX, Generic, C.NFDataX, Eq) -- | The maximum number of bytes to transfer in each data transfer, or beat, -- in a burst. From d3a48f1920d2f30245a8042f9de4d764dea9997f Mon Sep 17 00:00:00 2001 From: Pieter Staal Date: Mon, 17 Jan 2022 09:00:29 +0100 Subject: [PATCH 10/12] Add missing documentation --- src/Protocols/Axi4/ReadAddress.hs | 4 +++- src/Protocols/Axi4/WriteAddress.hs | 3 +++ src/Protocols/Axi4/WriteData.hs | 3 +++ src/Protocols/Axi4/WriteResponse.hs | 3 +++ 4 files changed, 12 insertions(+), 1 deletion(-) diff --git a/src/Protocols/Axi4/ReadAddress.hs b/src/Protocols/Axi4/ReadAddress.hs index 9fc50ba1..d6e2c10d 100644 --- a/src/Protocols/Axi4/ReadAddress.hs +++ b/src/Protocols/Axi4/ReadAddress.hs @@ -187,7 +187,9 @@ deriving instance , C.NFDataX (QosType kq) ) => C.NFDataX (M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) - +-- | Circuit that transforms the LHS 'Axi4ReadAddress' protocol to a +-- version using different type parameters according to two functions +-- that can transform the data and ack signal to and from the other protocol. mapFull :: forall dom kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 t1 diff --git a/src/Protocols/Axi4/WriteAddress.hs b/src/Protocols/Axi4/WriteAddress.hs index 1cf79322..143cb2e8 100644 --- a/src/Protocols/Axi4/WriteAddress.hs +++ b/src/Protocols/Axi4/WriteAddress.hs @@ -185,6 +185,9 @@ deriving instance , C.NFDataX (QosType kq) ) => C.NFDataX (M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType) +-- | Circuit that transforms the LHS 'Axi4WriteAddress' protocol to a +-- version using different type parameters according to two functions +-- that can transform the data and ack signal to and from the other protocol. mapFull :: forall dom kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 userType1 diff --git a/src/Protocols/Axi4/WriteData.hs b/src/Protocols/Axi4/WriteData.hs index b58a70ba..e8679eba 100644 --- a/src/Protocols/Axi4/WriteData.hs +++ b/src/Protocols/Axi4/WriteData.hs @@ -131,6 +131,9 @@ deriving instance , C.KnownNat nBytes ) => Show (M2S_WriteData ks nBytes userType) +-- | Circuit that transforms the LHS 'Axi4WriteData' protocol to a +-- version using different type parameters according to two functions +-- that can transform the data and ack signal to and from the other protocol. mapFull :: forall dom ks1 ks2 nBytes1 nBytes2 t1 t2. (M2S_WriteData ks1 nBytes1 t1 -> M2S_WriteData ks2 nBytes2 t2) -> diff --git a/src/Protocols/Axi4/WriteResponse.hs b/src/Protocols/Axi4/WriteResponse.hs index 64ff65a7..a437d248 100644 --- a/src/Protocols/Axi4/WriteResponse.hs +++ b/src/Protocols/Axi4/WriteResponse.hs @@ -126,6 +126,9 @@ deriving instance , C.KnownNat (Width iw) ) => Show (S2M_WriteResponse kr iw userType) +-- | Circuit that transforms the LHS 'Axi4WriteResponse' protocol to a +-- version using different type parameters according to two functions +-- that can transform the data and ack signal to and from the other protocol. mapFull :: forall dom kr1 iw1 userType1 From 65ce0770f0dc0f9dc23c6cd524d82c22f00159ea Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Fri, 14 Jan 2022 13:39:56 +0100 Subject: [PATCH 11/12] Setup GitHub Actions --- .ci/docker/Dockerfile | 41 --------- .ci/docker/build-and-publish-docker-image.sh | 24 ----- .ci/setup.sh | 26 ------ .ci/test_whitespace.sh | 11 +++ .github/workflows/ci.yml | 96 ++++++++++++++++++++ .gitlab-ci.yml | 48 ---------- stack.yaml | 5 +- 7 files changed, 110 insertions(+), 141 deletions(-) delete mode 100644 .ci/docker/Dockerfile delete mode 100755 .ci/docker/build-and-publish-docker-image.sh delete mode 100755 .ci/setup.sh create mode 100755 .ci/test_whitespace.sh create mode 100644 .github/workflows/ci.yml delete mode 100644 .gitlab-ci.yml diff --git a/.ci/docker/Dockerfile b/.ci/docker/Dockerfile deleted file mode 100644 index 118cb441..00000000 --- a/.ci/docker/Dockerfile +++ /dev/null @@ -1,41 +0,0 @@ -FROM ubuntu:focal -ARG GHC_VERSION - -ENV DEBIAN_FRONTEND=noninteractive LANG=C.UTF-8 LC_ALL=C.UTF-8 PATH=/opt/bin:/root/.ghcup/bin:$PATH - -ENV LATEST_STACK=linux-x86_64.tar.gz -ENV STACK_DEPS="g++ gcc libc6-dev libffi-dev libgmp-dev make xz-utils zlib1g-dev git gnupg netbase" -ARG GHC_DEPS="curl libc6-dev libgmp-dev pkg-config libnuma-dev build-essential" - -ENV CABAL_VERSION=3.2.0.0 - -ARG GHCUP_URL="https://downloads.haskell.org/~ghcup/x86_64-linux-ghcup" -ARG GHCUP_BIN=/root/.ghcup/bin/ghcup - -# Install GHC + Cabal -RUN apt-get update \ - && apt-get install -y $GHC_DEPS curl \ - && mkdir -p $(dirname $GHCUP_BIN) \ - && curl $GHCUP_URL --output $GHCUP_BIN \ - && chmod +x $GHCUP_BIN \ - && ghcup upgrade \ - && ghcup install ghc ${GHC_VERSION} \ - && ghcup set ghc ${GHC_VERSION} \ - && ghcup install cabal ${CABAL_VERSION} \ - && ghcup set cabal ${CABAL_VERSION} - -# Install Stack -RUN apt-get update \ - && apt-get -y install wget \ - && apt-get -y install $STACK_DEPS \ - && wget https://get.haskellstack.org/stable/$LATEST_STACK \ - && tar xzf $LATEST_STACK && rm $LATEST_STACK \ - && mv stack*/stack /usr/bin - -# Clash dependency -RUN apt-get update \ - && apt-get -y install libtinfo-dev - -# Compression utils -RUN apt-get update \ - && apt-get -y install tar zip zstd diff --git a/.ci/docker/build-and-publish-docker-image.sh b/.ci/docker/build-and-publish-docker-image.sh deleted file mode 100755 index aef2d56c..00000000 --- a/.ci/docker/build-and-publish-docker-image.sh +++ /dev/null @@ -1,24 +0,0 @@ -#!/usr/bin/env bash - -set -xeo pipefail - -REPO="docker.pkg.github.com/clash-lang/clash-protocols" -DIR=$(dirname "$0") -now=$(date +%F) - -for GHC_VERSION in "8.6.5" "8.10.2" -do - NAME="protocols-focal-ghc-cabal-stack-${GHC_VERSION}" - - docker build -t "${REPO}/${NAME}:$now" "$DIR" --build-arg GHC_VERSION=${GHC_VERSION} - docker tag "${REPO}/${NAME}:$now" "${REPO}/${NAME}:latest" - - read -p "Push to GitHub? (y/N) " push - - if [[ $push =~ ^[Yy]$ ]]; then - docker push "${REPO}/${NAME}:$now" - docker push "${REPO}/${NAME}:latest" - else - echo "Skipping push to container registry" - fi -done diff --git a/.ci/setup.sh b/.ci/setup.sh deleted file mode 100755 index 43fb83a4..00000000 --- a/.ci/setup.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/bash -set -xou pipefail - -grep \ - -E ' $' -n -r . \ - --include=*.{hs,hs-boot,sh,cabal,md,yml} \ - --exclude-dir=dist-newstyle --exclude-dir=deps -if [[ $? == 0 ]]; then - echo "EOL whitespace detected. See ^" - exit 1; -fi - -set -e - -ghcup set ghc ${GHC_VERSION} -ghcup set cabal ${CABAL_VERSION} - -cabal --version -ghc --version - -# run new-update first to generate the cabal config file that we can then modify -# retry 5 times, as hackage servers are not perfectly reliable -NEXT_WAIT_TIME=0 -until cabal update || [ $NEXT_WAIT_TIME -eq 5 ]; do - sleep $(( NEXT_WAIT_TIME++ )) -done diff --git a/.ci/test_whitespace.sh b/.ci/test_whitespace.sh new file mode 100755 index 00000000..fb4ea880 --- /dev/null +++ b/.ci/test_whitespace.sh @@ -0,0 +1,11 @@ +#!/bin/bash +set -xou pipefail + +grep \ + -E ' $' -n -r . \ + --include=*.{hs,hs-boot,sh,cabal,md,yml} \ + --exclude-dir=dist-newstyle --exclude-dir=deps +if [[ $? == 0 ]]; then + echo "EOL whitespace detected. See ^" + exit 1; +fi diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 00000000..7f8e5542 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,96 @@ +name: CI + +# Trigger the workflow on all pull requests and pushes/merges to master branch +on: + pull_request: + push: + branches: [master] + +jobs: + stack: + name: Stack tests + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v2 + + - name: Setup Stack / GHC + uses: haskell/actions/setup@v1 + with: + ghc-version: '8.10.7' # Exact version of ghc to use + enable-stack: true + stack-version: 'latest' + + - name: Cache dependencies + uses: actions/cache@v2 + with: + path: ~/.stack + key: ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}-${{ github.sha }} + restore-keys: | + ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}-${{ github.sha }} + ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}- + ${{ runner.os }}-ghc-${{ matrix.ghc }}- + + # Ask Stack to use system GHC instead of installing its own copy + - name: Use system GHC + run: | + stack config set system-ghc --global true + + - name: Test with Stack + run: | + .ci/test_stack.sh + + cabal: + name: Cabal tests - ${{ matrix.os }} / ghc ${{ matrix.ghc }} + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest] + cabal: + - "3.2" + ghc: + - "8.10.7" + + steps: + - name: Checkout + uses: actions/checkout@v2 + + - name: Setup Haskell + uses: haskell/actions/setup@v1 + id: setup-haskell-cabal + with: + ghc-version: ${{ matrix.ghc }} + cabal-version: ${{ matrix.cabal }} + + - name: Cache dependencies + uses: actions/cache@v2 + with: + path: ~/.cabal + key: ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}-${{ github.sha }} + restore-keys: | + ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}-${{ github.sha }} + ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}- + ${{ runner.os }}-ghc-${{ matrix.ghc }}- + + - name: Build + run: | + cabal build all -fci + + - name: Test + run: | + .ci/test_cabal.sh + + - name: Documentation + run: | + .ci/build_docs.sh + + linting: + name: Source code linting + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v2 + + - name: Whitespace + run: | + .ci/test_whitespace.sh diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml deleted file mode 100644 index 803c289a..00000000 --- a/.gitlab-ci.yml +++ /dev/null @@ -1,48 +0,0 @@ -.common: - timeout: 1 hour - retry: - max: 2 - when: - - runner_system_failure - - stuck_or_timeout_failure - cache: - key: $CI_JOB_NAME - paths: - - cache.tar.zstd - tags: - - local - before_script: - - export THREADS=$(nproc) - - export CABAL_JOBS=$(nproc) - - tar -xf cache.tar.zstd -C / || true - - .ci/setup.sh - - export - after_script: - - tar -cf - $(ls -d /root/.cabal /root/.stack /nix || true) | zstd -T0 -3 > cache.tar.zstd - -.common-810: - extends: .common - image: docker.pkg.github.com/clash-lang/clash-protocols/protocols-focal-ghc-cabal-stack-8.10.2:2020-12-07 - variables: - GHC_VERSION: "8.10.2" - CABAL_VERSION: "3.2.0.0" - -# Haddock is broken on 865. -haddock: - extends: .common-810 - artifacts: - paths: - - docs/* - expire_in: 1 month - script: - - .ci/build_docs.sh - -cabal-8.10.2: - extends: .common-810 - script: - - .ci/test_cabal.sh - -stack: - extends: .common-810 - script: - - .ci/test_stack.sh diff --git a/stack.yaml b/stack.yaml index 2c9506e2..e4d6850c 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,4 +1,4 @@ -resolver: nightly-2020-12-14 +resolver: lts-18.21 # ghc-8.10.7 packages: - . @@ -9,7 +9,8 @@ extra-deps: subdirs: - hedgehog - git: https://github.com/cchalmers/circuit-notation.git - commit: 0fe897cb95bd1be87abed044f4072f104dec2f7d + commit: 2574640364eef12222517af059b9e4a7e6b503a7 +- clash-prelude-1.2.5 flags: clash-prelude: From 7ad8007f8bcb9daec23adecd618c362d3149e814 Mon Sep 17 00:00:00 2001 From: Pieter Staal Date: Tue, 18 Jan 2022 15:06:44 +0100 Subject: [PATCH 12/12] Update circuit-notation dependency --- cabal.project | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cabal.project b/cabal.project index f2b2371b..93e00d27 100644 --- a/cabal.project +++ b/cabal.project @@ -11,7 +11,7 @@ package clash-prelude source-repository-package type: git location: https://github.com/cchalmers/circuit-notation.git - tag: 0fe897cb95bd1be87abed044f4072f104dec2f7d + tag: 2574640364eef12222517af059b9e4a7e6b503a7 source-repository-package type: git