diff --git a/clash-protocols.cabal b/clash-protocols.cabal index fc216ddb..8fb7374a 100644 --- a/clash-protocols.cabal +++ b/clash-protocols.cabal @@ -77,6 +77,7 @@ common common-options -fplugin GHC.TypeLits.Extra.Solver -fplugin GHC.TypeLits.Normalise -fplugin GHC.TypeLits.KnownNat.Solver + -fconstraint-solver-iterations=6 -- Clash needs access to the source code in compiled modules -fexpose-all-unfoldings @@ -163,6 +164,12 @@ library Protocols.Axi4.WriteAddress Protocols.Axi4.WriteData Protocols.Axi4.WriteResponse + Protocols.PacketStream.Base + Protocols.PacketStream.AsyncFifo + Protocols.PacketStream.Converters + Protocols.PacketStream.PacketFifo + Protocols.PacketStream.Packetizers + Protocols.PacketStream.Routing Protocols.Cpp Protocols.Df Protocols.DfConv @@ -189,6 +196,8 @@ library other-modules: Data.Bifunctor.Extra + Data.Maybe.Extra + Clash.Sized.Vector.Extra Paths_clash_protocols Protocols.Internal.Classes @@ -208,6 +217,13 @@ test-suite unittests Tests.Protocols.Axi4 Tests.Protocols.Plugin Tests.Protocols.Wishbone + Tests.Protocols.PacketStream + Tests.Protocols.PacketStream.AsyncFifo + Tests.Protocols.PacketStream.Base + Tests.Protocols.PacketStream.Converters + Tests.Protocols.PacketStream.Packetizers + Tests.Protocols.PacketStream.PacketFifo + Tests.Protocols.PacketStream.Routing Util build-depends: diff --git a/src/Clash/Sized/Vector/Extra.hs b/src/Clash/Sized/Vector/Extra.hs new file mode 100644 index 00000000..fc801654 --- /dev/null +++ b/src/Clash/Sized/Vector/Extra.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE NoImplicitPrelude #-} + +module Clash.Sized.Vector.Extra ( + dropLe, + takeLe, + appendVec, +) where + +import Clash.Prelude + +-- | Like 'drop' but uses a 'Data.Type.Ord.<=' constraint +dropLe :: + forall + (n :: Nat) + (m :: Nat) + (a :: Type). + (n <= m) => + -- | How many elements to take + SNat n -> + -- | input vector + Vec m a -> + Vec (m - n) a +dropLe SNat vs = leToPlus @n @m $ dropI vs + +-- | Like 'take' but uses a 'Data.Type.Ord.<=' constraint +takeLe :: + forall + (n :: Nat) + (m :: Nat) + (a :: Type). + (n <= m) => + -- | How many elements to take + SNat n -> + -- | input vector + Vec m a -> + Vec n a +takeLe SNat vs = leToPlus @n @m $ takeI vs + +-- | Take the first 'valid' elements of 'xs', append 'ys', then pad with 0s +appendVec :: + forall n m a. + (KnownNat n) => + (Num a) => + Index n -> + Vec n a -> + Vec m a -> + Vec (n + m) a +appendVec valid xs ys = results !! valid + where + go :: forall l. SNat l -> Vec (n + m) a + go l@SNat = + let f = addSNat l d1 + in case compareSNat f (SNat @n) of + SNatLE -> takeLe (addSNat l d1) xs ++ ys ++ extra + where + extra :: Vec (n - (l + 1)) a + extra = repeat 0 + _ -> error "appendVec: Absurd" + results = smap (\s _ -> go s) xs diff --git a/src/Data/Maybe/Extra.hs b/src/Data/Maybe/Extra.hs new file mode 100644 index 00000000..84847c51 --- /dev/null +++ b/src/Data/Maybe/Extra.hs @@ -0,0 +1,8 @@ +module Data.Maybe.Extra ( + toMaybe, +) where + +-- | Wrap a value in a Just if True +toMaybe :: Bool -> a -> Maybe a +toMaybe True x = Just x +toMaybe False _ = Nothing diff --git a/src/Protocols/PacketStream/AsyncFifo.hs b/src/Protocols/PacketStream/AsyncFifo.hs new file mode 100644 index 00000000..a5bb39b9 --- /dev/null +++ b/src/Protocols/PacketStream/AsyncFifo.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE NoImplicitPrelude #-} + +{- | +Provides `asyncFifoC` for crossing clock domains in the packet stream protocol. +-} +module Protocols.PacketStream.AsyncFifo (asyncFifoC) where + +import Data.Maybe.Extra (toMaybe) + +import Clash.Explicit.Prelude (asyncFIFOSynchronizer) +import Clash.Prelude + +import Protocols.Internal (Circuit, fromSignals) +import Protocols.PacketStream.Base + +{- | Asynchronous FIFO circuit that can be used to safely cross clock domains. +Uses `Clash.Explicit.Prelude.asyncFIFOSynchronizer` internally. +-} +asyncFifoC :: + forall + (depth :: Nat) + (dataWidth :: Nat) + (wDom :: Domain) + (rDom :: Domain) + (metaType :: Type). + ( KnownDomain wDom + , KnownDomain rDom + , KnownNat depth + , 2 <= depth + , KnownNat dataWidth + , 1 <= dataWidth + , NFDataX metaType + ) => + -- | 2^depth is the number of elements this component can store + SNat depth -> + -- | Clock signal in the write domain + Clock wDom -> + -- | Reset signal in the write domain + Reset wDom -> + -- | Enable signal in the write domain + Enable wDom -> + -- | Clock signal in the read domain + Clock rDom -> + -- | Reset signal in the read domain + Reset rDom -> + -- | Enable signal in the read domain + Enable rDom -> + Circuit (PacketStream wDom dataWidth metaType) (PacketStream rDom dataWidth metaType) +asyncFifoC depth wClk wRst wEn rClk rRst rEn = fromSignals ckt + where + ckt (fwdIn, bwdIn) = (bwdOut, fwdOut) + where + (element, isEmpty, isFull) = asyncFIFOSynchronizer depth wClk rClk wRst rRst wEn rEn readReq fwdIn + notEmpty = not <$> isEmpty + -- If the FIFO is empty, we output Nothing. Else, we output the oldest element. + fwdOut = toMaybe <$> notEmpty <*> element + -- Assert backpressure when the FIFO is full. + bwdOut = PacketStreamS2M . not <$> isFull + -- Next component is ready to read if the fifo is not empty and it does not assert backpressure. + readReq = notEmpty .&&. _ready <$> bwdIn diff --git a/src/Protocols/PacketStream/Base.hs b/src/Protocols/PacketStream/Base.hs new file mode 100644 index 00000000..276b79ee --- /dev/null +++ b/src/Protocols/PacketStream/Base.hs @@ -0,0 +1,213 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NoImplicitPrelude #-} + +{- | +Definitions and instances of the packet stream protocol +-} +module Protocols.PacketStream.Base ( + PacketStreamM2S (..), + PacketStreamS2M (..), + PacketStream, + unsafeToPacketStream, + fromPacketStream, + forceResetSanity, + filterMetaS, + filterMeta, + mapMetaS, + mapMeta, +) where + +import Clash.Prelude hiding (sample) +import qualified Prelude as P + +import qualified Protocols.Df as Df +import qualified Protocols.DfConv as DfConv +import Protocols.Hedgehog.Internal +import Protocols.Internal + +import Control.DeepSeq (NFData) +import Data.Coerce (coerce) +import qualified Data.Maybe as Maybe +import Data.Proxy + +{- | Data sent from manager to subordinate, a simplified AXI4-Stream like interface +with metadata that can only change on packet delineation. +_tdest, _tuser and _tid are bundled into one big _meta field which holds metadata. +There are no null or position bytes so _tstrb is replaced by a last indicator +that indicates the index of the last valid byte in the _data vector. +_tvalid is modeled via wrapping this in a `Maybe`. +-} +data PacketStreamM2S (dataWidth :: Nat) (metaType :: Type) = PacketStreamM2S + { _data :: Vec dataWidth (BitVector 8) + -- ^ The bytes to be transmitted + , _last :: Maybe (Index dataWidth) + -- ^ If Nothing, we are not yet at the last byte, otherwise index of last valid byte of _data + , _meta :: metaType + -- ^ the metadata of a packet. Must be constant during a packet. + , _abort :: Bool + -- ^ If True, the current transfer is aborted and the subordinate should ignore the current transfer + } + deriving (Eq, Generic, ShowX, Show, NFData, Bundle, Functor) + +{- | Data sent from the subordinate to the manager +The only information transmitted is whether the subordinate is ready to receive data +-} +newtype PacketStreamS2M = PacketStreamS2M + { _ready :: Bool + -- ^ Iff True, the subordinate is ready to receive data + } + deriving (Eq, Generic, ShowX, Show, NFData, Bundle, NFDataX) + +-- | The packet stream protocol for communication between components +data PacketStream (dom :: Domain) (dataWidth :: Nat) (metaType :: Type) + +deriving instance + (KnownNat dataWidth, NFDataX metaType) => + NFDataX (PacketStreamM2S dataWidth metaType) + +instance Protocol (PacketStream dom dataWidth metaType) where + type + Fwd (PacketStream dom dataWidth metaType) = + Signal dom (Maybe (PacketStreamM2S dataWidth metaType)) + type Bwd (PacketStream dom dataWidth metaType) = Signal dom PacketStreamS2M + +instance Backpressure (PacketStream dom dataWidth metaType) where + boolsToBwd _ = fromList_lazy . fmap PacketStreamS2M + +instance DfConv.DfConv (PacketStream dom dataWidth metaType) where + type Dom (PacketStream dom dataWidth metaType) = dom + type FwdPayload (PacketStream dom dataWidth metaType) = PacketStreamM2S dataWidth metaType + + toDfCircuit _ = fromSignals go + where + go (fwdIn, bwdIn) = + ( (fmap coerce bwdIn, pure undefined) + , fmap Df.dataToMaybe $ P.fst fwdIn + ) + + fromDfCircuit _ = fromSignals go + where + go (fwdIn, bwdIn) = + ( fmap coerce $ P.fst bwdIn + , (fmap Df.maybeToData fwdIn, pure undefined) + ) + +instance + (KnownDomain dom) => + Simulate (PacketStream dom dataWidth metaType) + where + type + SimulateFwdType (PacketStream dom dataWidth metaType) = + [Maybe (PacketStreamM2S dataWidth metaType)] + type SimulateBwdType (PacketStream dom dataWidth metaType) = [PacketStreamS2M] + type SimulateChannels (PacketStream dom dataWidth metaType) = 1 + + simToSigFwd _ = fromList_lazy + simToSigBwd _ = fromList_lazy + sigToSimFwd _ s = sample_lazy s + sigToSimBwd _ s = sample_lazy s + + stallC conf (head -> (stallAck, stalls)) = + withClockResetEnable clockGen resetGen enableGen + $ DfConv.stall Proxy Proxy conf stallAck stalls + +instance + (KnownDomain dom) => + Drivable (PacketStream dom dataWidth metaType) + where + type + ExpectType (PacketStream dom dataWidth metaType) = + [PacketStreamM2S dataWidth metaType] + + toSimulateType Proxy = fmap Just + fromSimulateType Proxy = Maybe.catMaybes + + driveC conf vals = + withClockResetEnable clockGen resetGen enableGen + $ DfConv.drive Proxy conf vals + sampleC conf ckt = + withClockResetEnable clockGen resetGen enableGen + $ DfConv.sample Proxy conf ckt + +instance + ( KnownNat dataWidth + , NFDataX metaType + , NFData metaType + , ShowX metaType + , Show metaType + , Eq metaType + , KnownDomain dom + ) => + Test (PacketStream dom dataWidth metaType) + where + expectToLengths Proxy = pure . P.length + expectN Proxy options nExpected sampled = + expectN (Proxy @(Df.Df dom _)) options nExpected + $ Df.maybeToData + <$> sampled + +-- | Circuit to convert a CSignal into a PacketStream. This is unsafe, because it drops backpressure. +unsafeToPacketStream :: + Circuit (CSignal dom (Maybe (PacketStreamM2S n a))) (PacketStream dom n a) +unsafeToPacketStream = Circuit (\(fwdInS, _) -> (pure (), fwdInS)) + +-- | Converts a PacketStream into a CSignal. +fromPacketStream :: + forall dom n meta. + (HiddenClockResetEnable dom) => + Circuit (PacketStream dom n meta) (CSignal dom (Maybe (PacketStreamM2S n meta))) +fromPacketStream = forceResetSanity |> Circuit (\(inFwd, _) -> (pure (PacketStreamS2M True), inFwd)) + +-- | Ensures a circuit does not send out ready on reset +forceResetSanity :: + forall dom n meta. + (HiddenClockResetEnable dom) => + Circuit (PacketStream dom n meta) (PacketStream dom n meta) +forceResetSanity = + Circuit (\(fwd, bwd) -> unbundle . fmap f . bundle $ (rstLow, fwd, bwd)) + where + f (True, _, _) = (PacketStreamS2M False, Nothing) + f (False, fwd, bwd) = (bwd, fwd) + rstLow = unsafeToActiveHigh hasReset + +{- | Filter a packet stream based on its metadata, + with the predicate wrapped in a @Signal@. +-} +filterMetaS :: + -- | Predicate which specifies whether to keep a fragment based on its metadata, + -- wrapped in a @Signal@ + Signal dom (meta -> Bool) -> + Circuit (PacketStream dom dataWidth meta) (PacketStream dom dataWidth meta) +filterMetaS pS = Circuit $ \(fwdIn, bwdIn) -> unbundle (go <$> bundle (fwdIn, bwdIn, pS)) + where + go (Nothing, bwdIn, _) = (bwdIn, Nothing) + go (Just inPkt, bwdIn, predicate) + | predicate (_meta inPkt) = (bwdIn, Just inPkt) + -- It's illegal to look at bwdIn when sending out a Nothing. + -- So if we drive a Nothing, force an acknowledgement. + | otherwise = (PacketStreamS2M True, Nothing) + +-- | Filter a packet stream based on its metadata. +filterMeta :: + -- | Predicate which specifies whether to keep a fragment based on its metadata + (meta -> Bool) -> + Circuit (PacketStream dom dataWidth meta) (PacketStream dom dataWidth meta) +filterMeta p = filterMetaS (pure p) + +{- | Map a function on the metadata of a packet stream, + with the function wrapped in a @Signal@. +-} +mapMetaS :: + -- | Function to apply on the metadata, wrapped in a @Signal@ + Signal dom (a -> b) -> + Circuit (PacketStream dom dataWidth a) (PacketStream dom dataWidth b) +mapMetaS fS = Circuit $ \(fwdIn, bwdIn) -> (bwdIn, go <$> bundle (fwdIn, fS)) + where + go (inp, f) = (\inPkt -> inPkt{_meta = f (_meta inPkt)}) <$> inp + +-- | Map a function on the metadata of a packet stream. +mapMeta :: + -- | Function to apply on the metadata + (a -> b) -> + Circuit (PacketStream dom dataWidth a) (PacketStream dom dataWidth b) +mapMeta f = mapMetaS (pure f) diff --git a/src/Protocols/PacketStream/Converters.hs b/src/Protocols/PacketStream/Converters.hs new file mode 100644 index 00000000..c323e82c --- /dev/null +++ b/src/Protocols/PacketStream/Converters.hs @@ -0,0 +1,235 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE NoImplicitPrelude #-} + +{- | +Provides an upconverter and downconverter for changing the data width of packet streams. +-} +module Protocols.PacketStream.Converters ( + upConverterC, + downConverterC, +) where + +import Clash.Prelude + +import Protocols (Circuit (..), fromSignals, (|>)) +import Protocols.PacketStream.Base + +import Data.Maybe (isJust, isNothing) +import Data.Maybe.Extra + +-- | Upconverter state, consisting of at most p `BitVector 8`s and a vector indicating which bytes are valid +data UpConverterState (dataWidth :: Nat) = UpConverterState + { _ucBuf :: Vec dataWidth (BitVector 8) + -- ^ The buffer we are filling + , _ucIdx :: Index dataWidth + -- ^ Where in the buffer we need to write the next element + , _ucFlush :: Bool + -- ^ If this is true the current state can presented as packetstream word + , _ucFreshBuf :: Bool + -- ^ If this is true we need to start a fresh buffer + , _ucAborted :: Bool + -- ^ Current packet is aborted + , _ucLastIdx :: Maybe (Index dataWidth) + -- ^ If true the current buffer contains the last byte of the current packet + } + deriving (Generic, NFDataX) + +toPacketStream :: UpConverterState dataWidth -> Maybe (PacketStreamM2S dataWidth ()) +toPacketStream UpConverterState{..} = toMaybe _ucFlush (PacketStreamM2S _ucBuf _ucLastIdx () _ucAborted) + +nextState :: + (KnownNat dataWidth) => + UpConverterState dataWidth -> + Maybe (PacketStreamM2S 1 ()) -> + PacketStreamS2M -> + UpConverterState dataWidth +nextState st@(UpConverterState{..}) Nothing (PacketStreamS2M inReady) = + nextSt + where + outReady = not _ucFlush || inReady + -- If we can accept data we can always set _ucFlush to false, + -- since we only change state if we can transmit and receive data + nextStRaw = + st + { _ucFlush = False + , _ucAborted = isNothing _ucLastIdx && _ucAborted + , _ucLastIdx = Nothing + } + nextSt = if outReady then nextStRaw else st +nextState st@(UpConverterState{..}) (Just PacketStreamM2S{..}) (PacketStreamS2M inReady) = + nextSt + where + inLast = isJust _last + -- We smear an abort over the entire rest of the packet + -- so the next abort is set: + -- - If fragment we are potentially flushing was not the last and we were already aborting; + -- - or if the incoming fragment is aborted + nextAbort = (isNothing _ucLastIdx && _ucAborted) || _abort + -- If we are not flushing we can accept data to be stored in _ucBuf, + -- but when we are flushing we can only accept if the current + -- output fragment is accepted by the sink + outReady = not _ucFlush || inReady + bufFull = _ucIdx == maxBound + currBuf = if _ucFreshBuf then (repeat 0) else _ucBuf + nextBuf = replace _ucIdx (head _data) currBuf + + nextFlush = inLast || bufFull + nextIdx = if nextFlush then 0 else _ucIdx + 1 + + nextStRaw = + UpConverterState + { _ucBuf = nextBuf + , _ucIdx = nextIdx + , _ucFlush = nextFlush + , _ucFreshBuf = nextFlush + , _ucAborted = nextAbort + , _ucLastIdx = toMaybe inLast _ucIdx + } + nextSt = if outReady then nextStRaw else st + +upConverter :: + forall (dataWidth :: Nat) (dom :: Domain). + (HiddenClockResetEnable dom) => + (1 <= dataWidth) => + (KnownNat dataWidth) => + -- | Input packet stream from the source + -- Input backpressure from the sink + ( Signal dom (Maybe (PacketStreamM2S 1 ())) + , Signal dom PacketStreamS2M + ) -> + -- | Output backpressure to the source + -- Output packet stream to the sink + ( Signal dom PacketStreamS2M + , Signal dom (Maybe (PacketStreamM2S dataWidth ())) + ) +upConverter = mealyB go s0 + where + s0 = UpConverterState (repeat undefined) 0 False True False Nothing + go :: + UpConverterState dataWidth -> + (Maybe (PacketStreamM2S 1 ()), PacketStreamS2M) -> + ( UpConverterState dataWidth + , (PacketStreamS2M, Maybe (PacketStreamM2S dataWidth ())) + ) + go st@(UpConverterState{..}) (fwdIn, bwdIn) = + (nextState st fwdIn bwdIn, (PacketStreamS2M outReady, toPacketStream st)) + where + outReady = not _ucFlush || (_ready bwdIn) + +{- | Converts packet streams of single bytes to packet streams of a higher data widths. +Has one cycle of latency, but optimal throughput. +-} +upConverterC :: + forall (dataWidth :: Nat) (dom :: Domain). + (HiddenClockResetEnable dom) => + (1 <= dataWidth) => + (KnownNat dataWidth) => + Circuit (PacketStream dom 1 ()) (PacketStream dom dataWidth ()) +upConverterC = forceResetSanity |> fromSignals upConverter + +data DownConverterState (dataWidth :: Nat) = DownConverterState + { _dcBuf :: Vec dataWidth (BitVector 8) + -- ^ Buffer + , _dcSize :: Index (dataWidth + 1) + -- ^ Number of valid bytes in _dcBuf + , _dcLastVec :: Bool + -- ^ True if last byte of _dcBuf was marked as last byte by incoming stream + , _dcAborted :: Bool + -- ^ If True, outgoing bytes should be marked as aborted until _dcBuf is replaced + } + deriving (Generic, NFDataX) + +-- | Computes new state from incoming data +fromPacketStreamM2S :: + forall (dataWidth :: Nat). + (KnownNat dataWidth) => + PacketStreamM2S dataWidth () -> + DownConverterState dataWidth +fromPacketStreamM2S (PacketStreamM2S vs lastIdx _ aborted) = + DownConverterState + { _dcBuf = vs + , _dcSize = maybe (natToNum @dataWidth) (succ . resize) lastIdx -- lastIdx points to the last valid byte, so the buffer size is one more + , _dcLastVec = isJust lastIdx + , _dcAborted = aborted + } + +-- | Computes output of down converter +toMaybePacketStreamM2S :: + forall (dataWidth :: Nat). + (1 <= dataWidth) => + (KnownNat dataWidth) => + DownConverterState dataWidth -> + Maybe (PacketStreamM2S 1 ()) +toMaybePacketStreamM2S DownConverterState{..} = toMaybe (_dcSize > 0) out + where + out = + PacketStreamM2S + { _data = leToPlusKN @1 @dataWidth head _dcBuf :> Nil + , _last = toMaybe (_dcSize == 1 && _dcLastVec) 0 + , _meta = () + , _abort = _dcAborted + } + +downConverter :: + forall (dataWidth :: Nat) (dom :: Domain). + (HiddenClockResetEnable dom) => + (1 <= dataWidth) => + (KnownNat dataWidth) => + -- | Input packet stream from the source and backpressure from the sink + ( Signal dom (Maybe (PacketStreamM2S dataWidth ())) + , Signal dom PacketStreamS2M + ) -> + -- | Output backpressure to the source + -- Output packet stream to the sink + ( Signal dom PacketStreamS2M + , Signal dom (Maybe (PacketStreamM2S 1 ())) + ) +downConverter = mealyB go s0 + where + s0 = + DownConverterState + { _dcBuf = errorX "downConverter: undefined initial value" + , _dcSize = 0 + , _dcLastVec = False + , _dcAborted = False + } + go :: + DownConverterState dataWidth -> + (Maybe (PacketStreamM2S dataWidth ()), PacketStreamS2M) -> + (DownConverterState dataWidth, (PacketStreamS2M, Maybe (PacketStreamM2S 1 ()))) + go st@(DownConverterState{..}) (fwdIn, PacketStreamS2M inReady) = (st', (bwdOut, fwdOut)) + where + (_dcSize', _dcBuf') = + if _dcSize > 0 && inReady + then (_dcSize - 1, _dcBuf <<+ 0) + else (_dcSize, _dcBuf) + + -- If the next buffer contains no valid bytes, + -- and the final byte was acknowledged, we can + -- acknowledge the newly received data. + -- The || is lazy, and we need this: if the output + -- of the downconverter is Nothing, we are not allowed to + -- evaluate inReady. + outReady = _dcSize == 0 || (_dcSize == 1 && inReady) + st' = case fwdIn of + Just inp | outReady -> fromPacketStreamM2S inp + _ -> + st + { _dcBuf = _dcBuf' + , _dcSize = _dcSize' + } + + bwdOut = PacketStreamS2M outReady + fwdOut = toMaybePacketStreamM2S st + +{- | Converts packet streams of arbitrary data widths to packet streams of single bytes. +Has one clock cycle of latency, but optimal throughput, i.e. a packet of n bytes is +sent out in n clock cycles, even if `_last` is set. +-} +downConverterC :: + forall (dataWidth :: Nat) (dom :: Domain). + (HiddenClockResetEnable dom) => + (1 <= dataWidth) => + (KnownNat dataWidth) => + Circuit (PacketStream dom dataWidth ()) (PacketStream dom 1 ()) +downConverterC = forceResetSanity |> fromSignals downConverter diff --git a/src/Protocols/PacketStream/PacketFifo.hs b/src/Protocols/PacketStream/PacketFifo.hs new file mode 100644 index 00000000..e097733c --- /dev/null +++ b/src/Protocols/PacketStream/PacketFifo.hs @@ -0,0 +1,186 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NoImplicitPrelude #-} + +{- | +Optimized Store and forward FIFO circuit for packet streams. +-} +module Protocols.PacketStream.PacketFifo ( + packetFifoC, + overflowDropPacketFifoC, +) where + +import Clash.Prelude + +import Protocols (CSignal, Circuit (..), fromSignals, (|>)) +import Protocols.PacketStream.Base + +import Data.Maybe +import Data.Maybe.Extra + +type PacketStreamContent (dataWidth :: Nat) (metaType :: Type) = + (Vec dataWidth (BitVector 8), Maybe (Index dataWidth)) + +toPacketStreamContent :: + PacketStreamM2S dataWidth metaType -> PacketStreamContent dataWidth metaType +toPacketStreamContent PacketStreamM2S{_data = d, _last = l, _meta = _, _abort = _} = (d, l) + +toPacketStreamM2S :: + PacketStreamContent dataWidth metaType -> metaType -> PacketStreamM2S dataWidth metaType +toPacketStreamM2S (d, l) m = PacketStreamM2S d l m False + +packetFifoImpl :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (metaType :: Type) + (contentSizeBits :: Nat) + (metaSizeBits :: Nat). + (HiddenClockResetEnable dom) => + (KnownNat dataWidth) => + (1 <= contentSizeBits) => + (1 <= metaSizeBits) => + (NFDataX metaType) => + -- | Depth of the content of the packet buffer, this is equal to 2^contentSizeBits + SNat contentSizeBits -> + -- | Depth of the content of the meta buffer, this is equal to 2^metaSizeBits + SNat metaSizeBits -> + -- | Input packetStream + ( Signal dom (Maybe (PacketStreamM2S dataWidth metaType)) + , Signal dom PacketStreamS2M + ) -> + -- | Output CSignal s + ( Signal dom PacketStreamS2M + , Signal dom (Maybe (PacketStreamM2S dataWidth metaType)) + ) +packetFifoImpl SNat SNat (fwdIn, bwdIn) = (PacketStreamS2M . not <$> fullBuffer, fwdOut) + where + fwdOut = toMaybe <$> (not <$> emptyBuffer) <*> (toPacketStreamM2S <$> ramContent <*> ramMeta) + + -- The backing ram + ramContent = + blockRam1 + NoClearOnReset + (SNat @(2 ^ contentSizeBits)) + (errorX "initial block ram content") + cReadAddr' + writeCommand + ramMeta = + blockRam1 + NoClearOnReset + (SNat @(2 ^ metaSizeBits)) + (errorX "initial block ram meta content") + mReadAddr' + mWriteCommand + + -- The write commands to the RAM + writeCommand = + toMaybe + <$> writeEnable + <*> bundle (cWordAddr, toPacketStreamContent . fromJustX <$> fwdIn) + mWriteCommand = toMaybe <$> nextPacketIn <*> bundle (mWriteAddr, _meta . fromJustX <$> fwdIn) + + -- Addresses for the content data + cWordAddr, cPacketAddr, cReadAddr :: Signal dom (Unsigned contentSizeBits) + cWordAddr = register 0 $ mux dropping' cPacketAddr $ mux writeEnable (cWordAddr + 1) cWordAddr + cPacketAddr = register 0 $ mux nextPacketIn (cWordAddr + 1) cPacketAddr + cReadAddr' = mux readEnable (cReadAddr + 1) cReadAddr + cReadAddr = register 0 cReadAddr' + + -- Addresses for the meta data + mWriteAddr, mReadAddr :: Signal dom (Unsigned metaSizeBits) + mWriteAddr = register 0 mWriteAddr' + mWriteAddr' = mux nextPacketIn (mWriteAddr + 1) mWriteAddr + + mReadAddr' = mux mReadEnable (mReadAddr + 1) mReadAddr + mReadAddr = register 0 mReadAddr' + -- only read the next value if we've outpustted the last word of a packet + mReadEnable = lastWordOut .&&. readEnable + + -- Registers : status + dropping', dropping, emptyBuffer :: Signal dom Bool + -- start dropping packet on abort + dropping' = abortIn .||. dropping + dropping = register False $ dropping' .&&. (not <$> lastWordIn) + -- the buffer is empty if the metaBuffer is empty as the metabuffer only updates when a packet is complete + emptyBuffer = register 0 mWriteAddr .==. mReadAddr + + -- Only write if there is space and we're not dropping + writeEnable = writeRequest .&&. (not <$> fullBuffer) .&&. (not <$> dropping') + -- Read when the word has been received + readEnable = (not <$> emptyBuffer) .&&. (_ready <$> bwdIn) + + -- The status signals + fullBuffer = ((cWordAddr + 1) .==. cReadAddr) .||. ((mWriteAddr + 1) .==. mReadAddr) + writeRequest = isJust <$> fwdIn + lastWordIn = maybe False (isJust . _last) <$> fwdIn + lastWordOut = maybe False (isJust . _last) <$> fwdOut + abortIn = maybe False _abort <$> fwdIn + nextPacketIn = lastWordIn .&&. writeEnable + +-- | A circuit that sends an abort forward if there is backpressure from the forward circuit +abortOnBackPressure :: + forall (dom :: Domain) (dataWidth :: Nat) (metaType :: Type). + (HiddenClockResetEnable dom) => + (KnownNat dataWidth) => + (NFDataX metaType) => + ( Signal dom (Maybe (PacketStreamM2S dataWidth metaType)) + , Signal dom PacketStreamS2M + ) -> + -- | Does not give backpressure, sends an abort forward instead + ( Signal dom () + , Signal dom (Maybe (PacketStreamM2S dataWidth metaType)) + ) +abortOnBackPressure (fwdInS, bwdInS) = (pure (), go <$> bundle (fwdInS, bwdInS)) + where + go (fwdIn, bwdIn) = fmap (\pkt -> pkt{_abort = _abort pkt || not (_ready bwdIn)}) fwdIn + +{- | Packet buffer, a circuit which stores words in a buffer until the packet is complete +once a packet is complete it will send the entire packet out at once without stalls. +If a word in a packet has `_abort` set to true, the packetBuffer will drop the entire packet. +If a packet is equal to or larger than 2^sizeBits-1, the packetBuffer will have a deadlock, this should be avoided! +-} +packetFifoC :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (metaType :: Type) + (contentSizeBits :: Nat) + (metaSizeBits :: Nat). + (HiddenClockResetEnable dom) => + (KnownNat dataWidth) => + (1 <= contentSizeBits) => + (1 <= metaSizeBits) => + (NFDataX metaType) => + -- | Depth of the content of the packet buffer, this is equal to 2^contentSizeBits + SNat contentSizeBits -> + -- | Depth for the meta of the packet buffer, this is equal to 2^metaSizeBits. + -- This can usually be smaller than contentSizeBits as for every packet we only need a single meta entry, while we usually have many words. + SNat metaSizeBits -> + Circuit (PacketStream dom dataWidth metaType) (PacketStream dom dataWidth metaType) +packetFifoC cSizeBits mSizeBits = forceResetSanity |> fromSignals (packetFifoImpl cSizeBits mSizeBits) + +-- | A packet buffer that drops packets when it is full, instead of giving backpressure, see packetBufferC for more detailed explanation +overflowDropPacketFifoC :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (metaType :: Type) + (contentSizeBits :: Nat) + (metaSizeBits :: Nat). + (HiddenClockResetEnable dom) => + (KnownNat dataWidth) => + (1 <= contentSizeBits) => + (1 <= metaSizeBits) => + (NFDataX metaType) => + SNat contentSizeBits -> + SNat metaSizeBits -> + Circuit + (CSignal dom (Maybe (PacketStreamM2S dataWidth metaType))) + (PacketStream dom dataWidth metaType) +overflowDropPacketFifoC cSizeBits mSizeBits = backPressureC |> packetFifoC cSizeBits mSizeBits + where + backPressureC :: + Circuit + (CSignal dom (Maybe (PacketStreamM2S dataWidth metaType))) + (PacketStream dom dataWidth metaType) + backPressureC = fromSignals abortOnBackPressure diff --git a/src/Protocols/PacketStream/Packetizers.hs b/src/Protocols/PacketStream/Packetizers.hs new file mode 100644 index 00000000..ed5ffced --- /dev/null +++ b/src/Protocols/PacketStream/Packetizers.hs @@ -0,0 +1,652 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE NoImplicitPrelude #-} + +{- | +Utility circuits for appending and stripping headers to and from the beginning of packets. +-} +module Protocols.PacketStream.Packetizers ( + packetizerC, + depacketizerC, + packetizeFromDfC, + depacketizeToDfC, +) where + +import Clash.Prelude +import Clash.Sized.Vector.Extra + +import Protocols +import Protocols.Df (Data (..)) +import qualified Protocols.Df as Df +import Protocols.PacketStream.Base + +import Data.Maybe +import Data.Maybe.Extra +import Data.Type.Equality ((:~:) (Refl)) + +type HeaderBufSize (headerBytes :: Nat) (dataWidth :: Nat) = + headerBytes + dataWidth + +-- The amount of bytes that we still need to forward due to +-- @headerBytes@ not aligning with @dataWidth@. +type ForwardBufSize (headerBytes :: Nat) (dataWidth :: Nat) = + headerBytes `Mod` dataWidth + +data PacketizerState (metaOut :: Type) (headerBytes :: Nat) (dataWidth :: Nat) + = Insert + { _counter :: Index (headerBytes `DivRU` dataWidth) + , _hdrBuf :: Vec (HeaderBufSize headerBytes dataWidth) (BitVector 8) + , _aborted :: Bool + } + | Forward + { _fwdBuf :: Vec (ForwardBufSize headerBytes dataWidth) (BitVector 8) + , _aborted :: Bool + } + | LastForward + {_lastFragment :: PacketStreamM2S dataWidth metaOut} + deriving (Generic, Show, ShowX) + +deriving instance + (NFDataX metaOut, PacketizerCt headerBytes dataWidth) => + NFDataX (PacketizerState metaOut headerBytes dataWidth) + +type PacketizerCt (headerBytes :: Nat) (dataWidth :: Nat) = + ( KnownNat dataWidth + , 1 <= dataWidth + , KnownNat headerBytes + ) + +defaultByte :: BitVector 8 +defaultByte = 0x00 + +-- The initial state of our packetizer. For readability purposes, because we use this exact expression a lot. +initialState :: + forall + (metaOut :: Type) + (headerBytes :: Nat) + (dataWidth :: Nat). + (PacketizerCt headerBytes dataWidth) => + PacketizerState metaOut headerBytes dataWidth +initialState = Insert 0 (repeat defaultByte) False + +adjustLast :: + forall + (headerBytes :: Nat) + (dataWidth :: Nat). + ( headerBytes `Mod` dataWidth <= dataWidth + , KnownNat dataWidth + , 1 <= dataWidth + ) => + SNat headerBytes -> + Index dataWidth -> + Either (Index dataWidth) (Index dataWidth) +adjustLast SNat idx = if outputNow then Left nowIdx else Right nextIdx + where + outputNow = case compareSNat (SNat @(ForwardBufSize headerBytes dataWidth)) d0 of + SNatGT -> idx < natToNum @(dataWidth - ForwardBufSize headerBytes dataWidth) + _ -> True + nowIdx = idx + natToNum @(ForwardBufSize headerBytes dataWidth) + nextIdx = idx - natToNum @(dataWidth - ForwardBufSize headerBytes dataWidth) + +packetizerT :: + forall + (headerBytes :: Nat) + (dataWidth :: Nat) + (header :: Type) + (metaIn :: Type) + (metaOut :: Type). + (BitSize header ~ headerBytes * 8) => + (BitPack header) => + (PacketizerCt headerBytes dataWidth) => + (ForwardBufSize headerBytes dataWidth <= dataWidth) => + (metaIn -> metaOut) -> + (metaIn -> header) -> + PacketizerState metaOut headerBytes dataWidth -> + (Maybe (PacketStreamM2S dataWidth metaIn), PacketStreamS2M) -> + ( PacketizerState metaOut headerBytes dataWidth + , (PacketStreamS2M, Maybe (PacketStreamM2S dataWidth metaOut)) + ) +packetizerT toMetaOut toHeader st@Insert{..} (Just pkt@PacketStreamM2S{..}, bwdIn) = + (nextStOut, (bwdOut, fwdOut)) + where + alignedCmp = compareSNat (SNat @(ForwardBufSize headerBytes dataWidth)) d0 + nextAborted = _aborted || _abort + header = bitCoerce (toHeader _meta) + metaOut = toMetaOut _meta + hdrBuf = if _counter == 0 then header ++ _data else _hdrBuf + (newHdrBuf, dataOut) = shiftOutFrom0 (SNat @dataWidth) hdrBuf + forwardBytes = snd $ shiftOutFromN (SNat @(ForwardBufSize headerBytes dataWidth)) _data + + newLast = case alignedCmp of + SNatGT -> fmap (adjustLast (SNat @headerBytes)) _last + _ -> Nothing + + fwdOut = + Just + pkt + { _data = dataOut + , _last = if _counter == maxBound then either Just (const Nothing) =<< newLast else Nothing + , _meta = metaOut + , _abort = nextAborted + } + + nextSt = case (_counter == maxBound, newLast) of + (False, _) -> Insert (succ _counter) newHdrBuf nextAborted + (True, Nothing) -> Forward forwardBytes nextAborted + (True, Just (Left _)) -> initialState + (True, Just (Right idx)) -> + LastForward + (PacketStreamM2S (take (SNat @dataWidth) newHdrBuf) (Just idx) metaOut nextAborted) + + nextStOut = if isNothing fwdOut || _ready bwdIn then nextSt else st + + -- Assert backpressure while inserting the header. If shifting needs to be done + -- and we are at the last cycle of insertion, we do not need to assert backpressure + -- because we put the rest of the data in _fwdBuf (of course, unless our subordinate asserts backpressure). + bwdOut = PacketStreamS2M $ case alignedCmp of + SNatGT -> _ready bwdIn && _counter == maxBound + _ -> False +packetizerT toMetaOut _ st@Forward{..} (Just pkt@PacketStreamM2S{..}, bwdIn) = (nextStOut, (bwdIn, Just outPkt)) + where + nextAborted = _aborted || _abort + metaOut = toMetaOut _meta + (dataOut, nextFwdBuf) = splitAt (SNat @dataWidth) (_fwdBuf ++ _data) + dataLast = nextFwdBuf ++ repeat @(dataWidth - ForwardBufSize headerBytes dataWidth) defaultByte + newLast = fmap (adjustLast (SNat @headerBytes)) _last + + outPkt = + pkt + { _data = dataOut + , _last = either Just (const Nothing) =<< newLast + , _meta = metaOut + , _abort = nextAborted + } + + nextSt = case newLast of + Nothing -> Forward nextFwdBuf nextAborted + Just (Left _) -> initialState + Just (Right idx) -> LastForward (PacketStreamM2S dataLast (Just idx) metaOut nextAborted) + + nextStOut = if _ready bwdIn then nextSt else st +packetizerT _ _ st@LastForward{..} (_, bwdIn) = (nextStOut, (PacketStreamS2M False, Just _lastFragment)) + where + nextStOut = if _ready bwdIn then initialState else st +packetizerT _ _ s (Nothing, bwdIn) = (s, (bwdIn, Nothing)) + +{- | Puts a portion of the metadata in front of the packet stream, and shifts the stream accordingly. + This portion is defined by the metadata to header transformer function. If this function is `id`, + the entire metadata is put in front of the packet stream. +-} +packetizerC :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (metaIn :: Type) + (metaOut :: Type) + (header :: Type) + (headerBytes :: Nat). + ( HiddenClockResetEnable dom + , NFDataX metaOut + , BitPack header + , BitSize header ~ headerBytes * 8 + , KnownNat headerBytes + , 1 <= dataWidth + , KnownNat dataWidth + ) => + -- | Metadata transformer function + (metaIn -> metaOut) -> + -- | metaData to header that will be packetized transformer function + (metaIn -> header) -> + Circuit (PacketStream dom dataWidth metaIn) (PacketStream dom dataWidth metaOut) +packetizerC toMetaOut toHeader = fromSignals outCircuit + where + outCircuit = case compareSNat (SNat @(ForwardBufSize headerBytes dataWidth)) (SNat @dataWidth) of + SNatLE -> mealyB (packetizerT @headerBytes toMetaOut toHeader) initialState + _ -> + clashCompileError + "packetizerC: Absurd, Report this to the Clash compiler team: https://github.com/clash-lang/clash-compiler/issues" + +-- Since the header might be unaligned compared to the datawidth +-- we need to store a partial fragment when forwarding. +-- The fragment we need to store depends on our "unalignedness". +-- +-- Ex. We parse a header of 17 bytes and our @dataWidth@ is 4 bytes. +-- That means at the end of the header we can have upto 3 bytes left +-- in the fragment which we may need to forward. +type DeForwardBufSize (headerBytes :: Nat) (dataWidth :: Nat) = + (dataWidth - (headerBytes `Mod` dataWidth)) `Mod` dataWidth + +type DepacketizerCt (headerBytes :: Nat) (dataWidth :: Nat) = + ( headerBytes `Mod` dataWidth <= dataWidth + , KnownNat dataWidth + , 1 <= dataWidth + , KnownNat headerBytes + ) + +data DepacketizerState (headerBytes :: Nat) (dataWidth :: Nat) + = DeParse + { _deAborted :: Bool + , _deParseBuf :: Vec (dataWidth * headerBytes `DivRU` dataWidth) (BitVector 8) + , _deFwdBuf :: Vec (DeForwardBufSize headerBytes dataWidth) (BitVector 8) + , _deCounter :: Index (headerBytes `DivRU` dataWidth) + } + | DeForward + { _deAborted :: Bool + , _deParseBuf :: Vec (dataWidth * headerBytes `DivRU` dataWidth) (BitVector 8) + , _deFwdBuf :: Vec (DeForwardBufSize headerBytes dataWidth) (BitVector 8) + , _deCounter :: Index (headerBytes `DivRU` dataWidth) + } + | DeLastForward + { _deAborted :: Bool + , _deParseBuf :: Vec (dataWidth * headerBytes `DivRU` dataWidth) (BitVector 8) + , _deFwdBuf :: Vec (DeForwardBufSize headerBytes dataWidth) (BitVector 8) + , _deCounter :: Index (headerBytes `DivRU` dataWidth) + , _deLastIdx :: Index dataWidth + } + deriving (Show, ShowX, Generic) + +deriving instance + (DepacketizerCt headerBytes dataWidth) => + NFDataX (DepacketizerState headerBytes dataWidth) + +depacketizerT :: + forall + (headerBytes :: Nat) + (dataWidth :: Nat) + (header :: Type) + (metaIn :: Type) + (metaOut :: Type). + (BitSize header ~ headerBytes * 8) => + (BitPack header) => + (NFDataX metaIn) => + (DepacketizerCt headerBytes dataWidth) => + (DeForwardBufSize headerBytes dataWidth <= dataWidth) => + (headerBytes <= dataWidth * headerBytes `DivRU` dataWidth) => + (header -> metaIn -> metaOut) -> + DepacketizerState headerBytes dataWidth -> + (Maybe (PacketStreamM2S dataWidth metaIn), PacketStreamS2M) -> + ( DepacketizerState headerBytes dataWidth + , (PacketStreamS2M, Maybe (PacketStreamM2S dataWidth metaOut)) + ) +depacketizerT _ DeParse{..} (Just PacketStreamM2S{..}, _) = (nextSt, (PacketStreamS2M outReady, Nothing)) + where + nextAborted = _deAborted || _abort + nextParseBuf = fst $ shiftInAtN _deParseBuf _data + fwdBuf :: Vec (DeForwardBufSize headerBytes dataWidth) (BitVector 8) + fwdBuf = dropLe (SNat @(dataWidth - DeForwardBufSize headerBytes dataWidth)) _data + + prematureEnd idx = + case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of + SNatGT -> idx < (natToNum @(headerBytes `Mod` dataWidth)) + _ -> True + + nextCounter = pred _deCounter + + nextSt = + case (_deCounter == 0, _last) of + (False, Nothing) -> + DeParse nextAborted nextParseBuf fwdBuf nextCounter + (done, Just idx) + | not done || prematureEnd idx -> + DeParse False nextParseBuf fwdBuf maxBound + (True, Just idx) -> + DeLastForward + nextAborted + nextParseBuf + fwdBuf + nextCounter + (idx - natToNum @(headerBytes `Mod` dataWidth)) + (True, Nothing) -> + DeForward nextAborted nextParseBuf fwdBuf nextCounter + _ -> + clashCompileError + "depacketizerT Parse: Absurd, Report this to the Clash compiler team: https://github.com/clash-lang/clash-compiler/issues" + + outReady + | DeLastForward{} <- nextSt = False + | otherwise = True +depacketizerT _ st@DeParse{} (Nothing, bwdIn) = (st, (bwdIn, Nothing)) +depacketizerT toMetaOut st@DeForward{..} (Just pkt@PacketStreamM2S{..}, bwdIn) = (nextStOut, (PacketStreamS2M outReady, Just outPkt)) + where + nextAborted = _deAborted || _abort + dataOut :: Vec dataWidth (BitVector 8) + nextFwdBuf :: Vec (DeForwardBufSize headerBytes dataWidth) (BitVector 8) + (dataOut, nextFwdBuf) = splitAt (SNat @dataWidth) $ _deFwdBuf ++ _data + + deAdjustLast :: Index dataWidth -> Either (Index dataWidth) (Index dataWidth) + deAdjustLast idx = if outputNow then Left nowIdx else Right nextIdx + where + outputNow = case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of + SNatGT -> idx < natToNum @(headerBytes `Mod` dataWidth) + _ -> True + nowIdx = idx + natToNum @(DeForwardBufSize headerBytes dataWidth) + nextIdx = idx - natToNum @(headerBytes `Mod` dataWidth) + + newLast = fmap deAdjustLast _last + outPkt = + pkt + { _abort = nextAborted + , _data = dataOut + , _meta = toMetaOut (bitCoerce $ takeLe (SNat @headerBytes) _deParseBuf) _meta + , _last = either Just (const Nothing) =<< newLast + } + + nextSt = case newLast of + Nothing -> DeForward nextAborted _deParseBuf nextFwdBuf _deCounter + Just (Left _) -> DeParse False _deParseBuf nextFwdBuf maxBound + Just (Right idx) -> DeLastForward nextAborted _deParseBuf nextFwdBuf _deCounter idx + nextStOut = if _ready bwdIn then nextSt else st + + outReady + | DeLastForward{} <- nextSt = False + | otherwise = _ready bwdIn +depacketizerT _ st@DeForward{} (Nothing, bwdIn) = (st, (bwdIn, Nothing)) +depacketizerT toMetaOut st@DeLastForward{..} (fwdIn, bwdIn) = (nextStOut, (bwdIn, Just outPkt)) + where + -- We can only get in this state if the previous clock cycle we received a fwdIn + -- which was also the last fragment + inPkt = fromJustX fwdIn + outPkt = + PacketStreamM2S + { _abort = _deAborted || _abort inPkt + , _data = + _deFwdBuf ++ repeat @(dataWidth - DeForwardBufSize headerBytes dataWidth) defaultByte + , _meta = toMetaOut (bitCoerce $ takeLe (SNat @headerBytes) _deParseBuf) (_meta inPkt) + , _last = Just $ fromJustX (_last inPkt) - natToNum @(headerBytes `Mod` dataWidth) + } + nextStOut = if _ready bwdIn then DeParse False _deParseBuf _deFwdBuf maxBound else st + +-- | Reads bytes at the start of each packet into metadata. +depacketizerC :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (metaIn :: Type) + (metaOut :: Type) + (header :: Type) + (headerBytes :: Nat). + ( HiddenClockResetEnable dom + , NFDataX metaOut + , NFDataX metaIn + , BitPack header + , BitSize header ~ headerBytes * 8 + , KnownNat headerBytes + , 1 <= dataWidth + , KnownNat dataWidth + ) => + -- | Used to compute final metadata of outgoing packets from header and incoming metadata + (header -> metaIn -> metaOut) -> + Circuit (PacketStream dom dataWidth metaIn) (PacketStream dom dataWidth metaOut) +depacketizerC toMetaOut = forceResetSanity |> fromSignals outCircuit + where + modProof = compareSNat (SNat @(headerBytes `Mod` dataWidth)) (SNat @dataWidth) + divProof = compareSNat (SNat @headerBytes) (SNat @(dataWidth * headerBytes `DivRU` dataWidth)) + + outCircuit = + case (modProof, divProof) of + (SNatLE, SNatLE) -> case compareSNat (SNat @(DeForwardBufSize headerBytes dataWidth)) (SNat @dataWidth) of + SNatLE -> + mealyB + (depacketizerT @headerBytes toMetaOut) + (DeParse False (repeat undefined) (repeat undefined) maxBound) + _ -> + clashCompileError + "depacketizerC1: Absurd, Report this to the Clash compiler team: https://github.com/clash-lang/clash-compiler/issues" + _ -> + clashCompileError + "depacketizerC0: Absurd, Report this to the Clash compiler team: https://github.com/clash-lang/clash-compiler/issues" + +{- | If dataWidth >= headerBytes, we don't need a buffer because we can immediately send + the fragment. Else, we need a buffer that stores the headerBytes minus the size + of the fragment we send out immediately. +-} +type DfHeaderBufSize headerBytes dataWidth = dataWidth `Max` headerBytes - dataWidth + +data DfPacketizerState (metaOut :: Type) (headerBytes :: Nat) (dataWidth :: Nat) + = DfIdle + | DfInsert + { _dfCounter :: Index (headerBytes `DivRU` dataWidth - 1) + , _dfHdrBuf :: Vec (DfHeaderBufSize headerBytes dataWidth) (BitVector 8) + } + deriving (Generic, NFDataX, Show, ShowX) + +packetizeFromDfT :: + forall + (dataWidth :: Nat) + (a :: Type) + (metaOut :: Type) + (header :: Type) + (headerBytes :: Nat). + (NFDataX metaOut) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (KnownNat headerBytes) => + (KnownNat dataWidth) => + (1 <= dataWidth) => + (1 <= headerBytes `DivRU` dataWidth) => + (dataWidth `Min` headerBytes <= dataWidth) => + (dataWidth `Max` headerBytes - dataWidth + dataWidth `Min` headerBytes ~ headerBytes) => + -- | function that transforms the Df input to the output metadata. + (a -> metaOut) -> + -- | function that transforms the Df input to the header that will be packetized. + (a -> header) -> + DfPacketizerState metaOut headerBytes dataWidth -> + (Data a, PacketStreamS2M) -> + ( DfPacketizerState metaOut headerBytes dataWidth + , (Ack, Maybe (PacketStreamM2S dataWidth metaOut)) + ) +packetizeFromDfT toMetaOut toHeader DfIdle (Data dataIn, bwdIn) = (nextStOut, (bwdOut, Just outPkt)) + where + rotatedHdr = + rotateRightS (bitCoerce (toHeader dataIn)) (SNat @(DfHeaderBufSize headerBytes dataWidth)) + (hdrBuf, dataOut) = splitAt (SNat @(DfHeaderBufSize headerBytes dataWidth)) rotatedHdr + dataOutPadded = dataOut ++ repeat @(dataWidth - dataWidth `Min` headerBytes) defaultByte + outPkt = PacketStreamM2S dataOutPadded newLast (toMetaOut dataIn) False + + (nextSt, bwdOut, newLast) = case compareSNat (SNat @headerBytes) (SNat @dataWidth) of + SNatLE -> (DfIdle, Ack (_ready bwdIn), Just l) + where + l = case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of + SNatGT -> natToNum @(headerBytes `Mod` dataWidth - 1) + _ -> natToNum @(dataWidth - 1) + SNatGT -> (DfInsert 0 hdrBuf, Ack False, Nothing) + + nextStOut = if _ready bwdIn then nextSt else DfIdle + +-- fwdIn is always Data in this state, because we assert backpressure in Idle before we go here +-- Thus, we don't need to store the metadata in the state. +packetizeFromDfT toMetaOut _ st@DfInsert{..} (Data dataIn, bwdIn) = (nextStOut, (bwdOut, Just outPkt)) + where + (dataOut, newHdrBuf) = splitAt (SNat @dataWidth) (_dfHdrBuf ++ repeat @dataWidth defaultByte) + outPkt = PacketStreamM2S dataOut newLast (toMetaOut dataIn) False + + newLast = toMaybe (_dfCounter == maxBound) $ case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of + SNatGT -> natToNum @(headerBytes `Mod` dataWidth - 1) + _ -> natToNum @(dataWidth - 1) + + bwdOut = Ack (_ready bwdIn && _dfCounter == maxBound) + nextSt = if _dfCounter == maxBound then DfIdle else DfInsert (succ _dfCounter) newHdrBuf + nextStOut = if _ready bwdIn then nextSt else st +packetizeFromDfT _ _ s (NoData, bwdIn) = (s, (Ack (_ready bwdIn), Nothing)) + +{- | Starts a packet stream upon receiving some data. + The bytes to be packetized and the output metadata + are specified by the input functions. +-} +packetizeFromDfC :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (a :: Type) + (metaOut :: Type) + (header :: Type) + (headerBytes :: Nat). + (HiddenClockResetEnable dom) => + (NFDataX metaOut) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (KnownNat headerBytes) => + (KnownNat dataWidth) => + (1 <= dataWidth) => + -- | Function that transforms the Df input to the output metadata. + (a -> metaOut) -> + -- | Function that transforms the Df input to the header that will be packetized. + (a -> header) -> + Circuit (Df dom a) (PacketStream dom dataWidth metaOut) +packetizeFromDfC toMetaOut toHeader = fromSignals ckt + where + maxMinProof = + sameNat + (SNat @headerBytes) + (SNat @(dataWidth `Max` headerBytes - dataWidth + dataWidth `Min` headerBytes)) + minProof = compareSNat (SNat @(dataWidth `Min` headerBytes)) (SNat @dataWidth) + divRuProof = compareSNat d1 (SNat @(headerBytes `DivRU` dataWidth)) + + ckt = case (maxMinProof, minProof, divRuProof) of + (Just Refl, SNatLE, SNatLE) -> mealyB (packetizeFromDfT toMetaOut toHeader) DfIdle + _ -> + clashCompileError + "packetizeFromDfC: Absurd, Report this to the Clash compiler team: https://github.com/clash-lang/clash-compiler/issues" + +type ParseBufSize (headerBytes :: Nat) (dataWidth :: Nat) = + dataWidth * headerBytes `DivRU` dataWidth + +type DepacketizeToDfCt (headerBytes :: Nat) (dataWidth :: Nat) = + ( 1 <= headerBytes `DivRU` dataWidth + , headerBytes `Mod` dataWidth <= dataWidth + , headerBytes <= ParseBufSize headerBytes dataWidth + , KnownNat dataWidth + , 1 <= dataWidth + , KnownNat headerBytes + ) + +data DfDepacketizerState (a :: Type) (headerBytes :: Nat) (dataWidth :: Nat) + = Parse + { _dfDeAborted :: Bool + -- ^ whether any of the fragments parsed from the current packet were aborted. + , _dfDeParseBuf :: Vec (ParseBufSize headerBytes dataWidth) (BitVector 8) + -- ^ the accumulator for header bytes. + , _dfDeCounter :: Index (headerBytes `DivRU` dataWidth) + -- ^ how many of the _parseBuf bytes are currently valid (accumulation count). We flush at counter == maxBound + } + | ConsumePadding + { _dfDeAborted :: Bool + -- ^ whether any of the fragments parsed from the current packet were aborted. + , _dfDeParseBuf :: Vec (ParseBufSize headerBytes dataWidth) (BitVector 8) + } + deriving (Generic, Show, ShowX) + +deriving instance + (NFDataX a, DepacketizeToDfCt headerBytes dataWidth) => + NFDataX (DfDepacketizerState a headerBytes dataWidth) + +dfDeInitialState :: + forall (a :: Type) (headerBytes :: Nat) (dataWidth :: Nat). + (KnownNat dataWidth) => + (KnownNat headerBytes) => + (1 <= dataWidth) => + DfDepacketizerState a headerBytes dataWidth +dfDeInitialState = Parse False (repeat undefined) maxBound + +depacketizeToDfT :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (a :: Type) + (meta :: Type) + (header :: Type) + (headerBytes :: Nat). + (HiddenClockResetEnable dom) => + (NFDataX meta) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (DepacketizeToDfCt headerBytes dataWidth) => + (header -> meta -> a) -> + DfDepacketizerState a headerBytes dataWidth -> + (Maybe (PacketStreamM2S dataWidth meta), Ack) -> + (DfDepacketizerState a headerBytes dataWidth, (PacketStreamS2M, Df.Data a)) +depacketizeToDfT toOut st@Parse{..} (Just (PacketStreamM2S{..}), Ack readyIn) = (nextStOut, (PacketStreamS2M readyOut, fwdOut)) + where + nextAborted = _dfDeAborted || _abort + nextParseBuf = fst (shiftInAtN _dfDeParseBuf _data) + outDf = toOut (bitCoerce (takeLe (SNat @headerBytes) nextParseBuf)) _meta + + prematureEnd idx = + case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of + SNatGT -> idx < (natToNum @(headerBytes `Mod` dataWidth - 1)) + _ -> idx < (natToNum @(dataWidth - 1)) + + (nextSt, fwdOut) = + case (_dfDeCounter == 0, _last) of + (False, Nothing) -> + (Parse nextAborted nextParseBuf (pred _dfDeCounter), Df.NoData) + (c, Just idx) + | not c || prematureEnd idx -> + (dfDeInitialState, Df.NoData) + (True, Just _) -> + (dfDeInitialState, if nextAborted then Df.NoData else Df.Data outDf) + (True, Nothing) -> + (ConsumePadding nextAborted nextParseBuf, Df.NoData) + _ -> + clashCompileError + "depacketizeToDfT Parse: Absurd, Report this to the Clash compiler team: https://github.com/clash-lang/clash-compiler/issues" + + readyOut = isNothing (Df.dataToMaybe fwdOut) || readyIn + nextStOut = if readyOut then nextSt else st +depacketizeToDfT toOut st@ConsumePadding{..} (Just (PacketStreamM2S{..}), Ack readyIn) = (nextStOut, (PacketStreamS2M readyOut, fwdOut)) + where + nextAborted = _dfDeAborted || _abort + outDf = toOut (bitCoerce (takeLe (SNat @headerBytes) _dfDeParseBuf)) _meta + + (nextSt, fwdOut) = + if isJust _last + then (dfDeInitialState, if nextAborted then Df.NoData else Df.Data outDf) + else (st{_dfDeAborted = nextAborted}, Df.NoData) + + readyOut = isNothing (Df.dataToMaybe fwdOut) || readyIn + nextStOut = if readyOut then nextSt else st +depacketizeToDfT _ st (Nothing, Ack ready) = (st, (PacketStreamS2M ready, Df.NoData)) + +{- | Reads bytes at the start of each packet into a dataflow. +Consumes the remainder of the packet and drops this. If a +packet ends sooner than the assumed length of the header, +`depacketizeToDfC` does not send out anything. +If any of the fragments in the packet has _abort set, it drops +the entire packet. +-} +depacketizeToDfC :: + forall + (dom :: Domain) + (dataWidth :: Nat) + (a :: Type) + (meta :: Type) + (header :: Type) + (headerBytes :: Nat). + (HiddenClockResetEnable dom) => + (NFDataX meta) => + (NFDataX a) => + (BitPack header) => + (KnownNat headerBytes) => + (KnownNat dataWidth) => + (1 <= dataWidth) => + (BitSize header ~ headerBytes * 8) => + -- | function that transforms the given meta + parsed header to the output Df + (header -> meta -> a) -> + Circuit (PacketStream dom dataWidth meta) (Df dom a) +depacketizeToDfC toOut = forceResetSanity |> fromSignals outCircuit + where + divProof = compareSNat (SNat @headerBytes) (SNat @(dataWidth * headerBytes `DivRU` dataWidth)) + modProof = compareSNat (SNat @(headerBytes `Mod` dataWidth)) (SNat @dataWidth) + + outCircuit = + case (divProof, modProof) of + (SNatLE, SNatLE) -> case compareSNat d1 (SNat @(headerBytes `DivRU` dataWidth)) of + SNatLE -> mealyB (depacketizeToDfT toOut) dfDeInitialState + _ -> + clashCompileError + "depacketizeToDfC0: Absurd, Report this to the Clash compiler team: https://github.com/clash-lang/clash-compiler/issues" + _ -> + clashCompileError + "depacketizeToDfC1: Absurd, Report this to the Clash compiler team: https://github.com/clash-lang/clash-compiler/issues" diff --git a/src/Protocols/PacketStream/Routing.hs b/src/Protocols/PacketStream/Routing.hs new file mode 100644 index 00000000..a39d04b8 --- /dev/null +++ b/src/Protocols/PacketStream/Routing.hs @@ -0,0 +1,92 @@ +{-# LANGUAGE NoImplicitPrelude #-} + +{- | +Provides a packet arbiter and dispatcher, for merging and splitting packet streams. +-} +module Protocols.PacketStream.Routing ( + packetArbiterC, + ArbiterMode (..), + packetDispatcherC, + routeBy, +) where + +import Clash.Prelude + +import Protocols +import Protocols.PacketStream.Base + +import Data.Bifunctor (Bifunctor (second)) +import qualified Data.Bifunctor as B +import Data.Maybe + +-- | Collect mode for `packetArbiterC` +data ArbiterMode + = -- | Collect in a round-robin fashion. Fair and cheaper than `Parallel`. + RoundRobin + | -- | Check components in parallel. This mode has a higher throughput, but is + -- biased towards the last source and also slightly more expensive. + Parallel + +-- | Collects packets from all sources, respecting packet boundaries. +packetArbiterC :: + forall dom p n a. + ( HiddenClockResetEnable dom + , KnownNat p + , 1 <= p + ) => + -- | See `ArbiterMode` + ArbiterMode -> + Circuit (Vec p (PacketStream dom n a)) (PacketStream dom n a) +packetArbiterC mode = Circuit (B.first unbundle . mealyB go (maxBound, True) . B.first bundle) + where + go :: + (Index p, Bool) -> + (Vec p (Maybe (PacketStreamM2S n a)), PacketStreamS2M) -> + ((Index p, Bool), (Vec p PacketStreamS2M, Maybe (PacketStreamM2S n a))) + go (i, first) (fwds, bwd@(PacketStreamS2M ack)) = ((i', continue), (bwds, fwd)) + where + bwds = replace i bwd (repeat (PacketStreamS2M False)) + fwd = fwds !! i + continue = case fwd of + Nothing -> first -- only switch sources if this is not somewhere inside a packet + Just (PacketStreamM2S _ (Just _) _ _) -> ack -- switch source once last packet is acknowledged + _ -> False + i' = case (mode, continue) of + (_, False) -> i + (RoundRobin, _) -> satSucc SatWrap i -- next index + (Parallel, _) -> fromMaybe maxBound $ fold @(p - 1) (<|>) (zipWith (<$) indicesI fwds) -- index of last sink with data + +{- | Routes packets depending on their metadata, using given routing functions. + +Data is sent to at most one element of the output vector, for which the +dispatch function evaluates to true on the metadata of the input. If none of +the functions evaluate to true, the input is dropped. If more than one of the +predicates are true, the first one is picked. + +Sends out packets in the same clock cycle as they are received. +-} +packetDispatcherC :: + forall (dom :: Domain) (p :: Nat) (n :: Nat) (a :: Type). + ( HiddenClockResetEnable dom + , KnownNat p + ) => + -- | Dispatch function. If function at index i returns true for the metaData it + -- dispatches the current packet to that sink. + Vec p (a -> Bool) -> + Circuit (PacketStream dom n a) (Vec p (PacketStream dom n a)) +packetDispatcherC fs = Circuit (second unbundle . unbundle . fmap go . bundle . second bundle) + where + go (Just x, bwds) = case findIndex id $ zipWith ($) fs (pure $ _meta x) of + Just i -> (bwds !! i, replace i (Just x) (repeat Nothing)) + _ -> (PacketStreamS2M True, repeat Nothing) + go _ = (PacketStreamS2M False, repeat Nothing) + +{- | Routing function for `packetDispatcherC` that matches against values with +an `Eq` instance. Useful to route according to a record field. +-} +routeBy :: + (Eq b) => + (a -> b) -> + Vec p b -> + Vec p (a -> Bool) +routeBy f = fmap $ \x -> (== x) . f diff --git a/tests/Tests/Protocols.hs b/tests/Tests/Protocols.hs index a09bc008..0fc7e78e 100644 --- a/tests/Tests/Protocols.hs +++ b/tests/Tests/Protocols.hs @@ -5,6 +5,7 @@ import qualified Tests.Protocols.Avalon import qualified Tests.Protocols.Axi4 import qualified Tests.Protocols.Df import qualified Tests.Protocols.DfConv +import qualified Tests.Protocols.PacketStream import qualified Tests.Protocols.Wishbone tests :: TestTree @@ -16,6 +17,7 @@ tests = , Tests.Protocols.Avalon.tests , Tests.Protocols.Axi4.tests , Tests.Protocols.Wishbone.tests + , Tests.Protocols.PacketStream.tests ] main :: IO () diff --git a/tests/Tests/Protocols/PacketStream.hs b/tests/Tests/Protocols/PacketStream.hs new file mode 100644 index 00000000..c349afc7 --- /dev/null +++ b/tests/Tests/Protocols/PacketStream.hs @@ -0,0 +1,20 @@ +module Tests.Protocols.PacketStream (tests) where + +import Test.Tasty + +import qualified Tests.Protocols.PacketStream.AsyncFifo +import qualified Tests.Protocols.PacketStream.Converters +import qualified Tests.Protocols.PacketStream.PacketFifo +import qualified Tests.Protocols.PacketStream.Packetizers +import qualified Tests.Protocols.PacketStream.Routing + +tests :: TestTree +tests = + testGroup + "PacketStream" + [ Tests.Protocols.PacketStream.AsyncFifo.tests + , Tests.Protocols.PacketStream.Converters.tests + , Tests.Protocols.PacketStream.PacketFifo.tests + , Tests.Protocols.PacketStream.Packetizers.tests + , Tests.Protocols.PacketStream.Routing.tests + ] diff --git a/tests/Tests/Protocols/PacketStream/AsyncFifo.hs b/tests/Tests/Protocols/PacketStream/AsyncFifo.hs new file mode 100644 index 00000000..6be94c64 --- /dev/null +++ b/tests/Tests/Protocols/PacketStream/AsyncFifo.hs @@ -0,0 +1,127 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Tests.Protocols.PacketStream.AsyncFifo where + +-- base +import Prelude + +-- clash-prelude +import Clash.Prelude as C + +-- hedgehog +import Hedgehog +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +-- tasty +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +-- clash-protocols +import Protocols +import Protocols.Hedgehog +import Protocols.PacketStream.AsyncFifo +import Protocols.PacketStream.Base + +genVec :: (KnownNat n, 1 C.<= n) => Gen a -> Gen (Vec n a) +genVec gen = sequence (C.repeat gen) + +createDomain + vSystem + { vName = "TestDom50" + , vPeriod = 20_000 + , vActiveEdge = Rising + , vResetKind = Asynchronous + , vInitBehavior = Unknown + , vResetPolarity = ActiveHigh + } + +createDomain + vSystem + { vName = "TestDom125" + , vPeriod = 8_000 + , vActiveEdge = Rising + , vResetKind = Asynchronous + , vInitBehavior = Unknown + , vResetPolarity = ActiveHigh + } + +clk50 :: Clock TestDom50 +clk50 = clockGen + +clk125 :: Clock TestDom125 +clk125 = clockGen + +rst50 :: Reset TestDom50 +rst50 = resetGen @TestDom50 + +rst125 :: Reset TestDom125 +rst125 = resetGen @TestDom125 + +en50 :: Enable TestDom50 +en50 = enableGen + +en125 :: Enable TestDom125 +en125 = enableGen + +generateAsyncFifoIdProp :: + forall (wDom :: Domain) (rDom :: Domain). + (KnownDomain wDom, KnownDomain rDom) => + Clock wDom -> + Reset wDom -> + Enable wDom -> + Clock rDom -> + Reset rDom -> + Enable rDom -> + Property +generateAsyncFifoIdProp wClk wRst wEn rClk rRst rEn = + propWithModel + defExpectOptions + (Gen.list (Range.linear 0 100) genPackets) + id + ckt + (===) + where + ckt :: + (KnownDomain wDom, KnownDomain rDom) => + Circuit + (PacketStream wDom 1 Int) + (PacketStream rDom 1 Int) + ckt = asyncFifoC (C.SNat @8) wClk wRst wEn rClk rRst rEn + -- This is used to generate + genPackets = + PacketStreamM2S + <$> genVec Gen.enumBounded + <*> Gen.maybe Gen.enumBounded + <*> Gen.enumBounded + <*> Gen.enumBounded + +{- | The async FIFO circuit should forward all of its input data without loss and without producing extra data. + This property tests whether this is true, when the clock of the writer and reader is equally fast (50 MHz). +-} +prop_asyncfifo_writer_speed_equal_to_reader_id :: Property +prop_asyncfifo_writer_speed_equal_to_reader_id = generateAsyncFifoIdProp clk50 rst50 en50 clk50 rst50 en50 + +{- | The async FIFO circuit should forward all of its input data without loss and without producing extra data. + This property tests whether this is true, when the clock of the writer (50 MHz) is slower than the clock of the reader (125 MHz). +-} +prop_asyncfifo_writer_speed_slower_than_reader_id :: Property +prop_asyncfifo_writer_speed_slower_than_reader_id = generateAsyncFifoIdProp clk50 rst50 en50 clk125 rst125 en125 + +{- | The async FIFO circuit should forward all of its input data without loss and without producing extra data. + This property tests whether this is true, when the clock of the writer (125 MHz) is faster than the clock of the reader (50 MHz). +-} +prop_asyncfifo_writer_speed_faster_than_reader_id :: Property +prop_asyncfifo_writer_speed_faster_than_reader_id = generateAsyncFifoIdProp clk125 rst125 en125 clk50 rst50 en50 + +tests :: TestTree +tests = + localOption (mkTimeout 12_000_000 {- 12 seconds -}) $ + localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator) diff --git a/tests/Tests/Protocols/PacketStream/Base.hs b/tests/Tests/Protocols/PacketStream/Base.hs new file mode 100644 index 00000000..c53c7a9a --- /dev/null +++ b/tests/Tests/Protocols/PacketStream/Base.hs @@ -0,0 +1,188 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE RecordWildCards #-} + +module Tests.Protocols.PacketStream.Base ( + chunkBy, + chunkByPacket, + smearAbort, + chopBy, + chunkToPacket, + chopPacket, + fullPackets, + dropAbortedPackets, + downConvert, + upConvert, + cleanPackets, + makeValid, + genValidPacket, + genValidPackets, +) where + +-- base +import qualified Data.List as L +import qualified Data.Maybe as M +import Prelude + +-- clash +import qualified Clash.Prelude as C +import qualified Clash.Sized.Vector as Vec + +-- hedgehog +import Hedgehog +import qualified Hedgehog.Gen as Gen + +-- clash-protocols +import Protocols.PacketStream.Base + +-- | Partition a list based on given function +chunkBy :: (a -> Bool) -> [a] -> [[a]] +chunkBy _ [] = [] +chunkBy predicate list = L.filter (not . null) $ chunkByHelper predicate list [] + +-- Helper function to accumulate chunks +chunkByHelper :: (a -> Bool) -> [a] -> [a] -> [[a]] +chunkByHelper _ [] acc = [L.reverse acc] +chunkByHelper predicate (x : xs) acc + | predicate x = L.reverse (x : acc) : chunkByHelper predicate xs [] + | otherwise = chunkByHelper predicate xs (x : acc) + +-- | Partition a list of PacketStreams into complete packets +chunkByPacket :: [PacketStreamM2S n meta] -> [[PacketStreamM2S n meta]] +chunkByPacket = chunkBy (M.isJust . _last) + +-- | Smear abort over the rest of a list of packets +smearAbort :: [PacketStreamM2S n meta] -> [PacketStreamM2S n meta] +smearAbort [] = [] +smearAbort (x : xs) = L.reverse $ L.foldl' go [x] xs + where + go [] _ = [] + go l@(a : _) (PacketStreamM2S dat last' meta abort) = + PacketStreamM2S dat last' meta (_abort a || abort) : l + +-- | Partition a list into groups of given size +chopBy :: Int -> [a] -> [[a]] +chopBy _ [] = [] +chopBy n xs = as : chopBy n bs where (as, bs) = splitAt n xs + +-- | Merge a list of PacketStream 1 into a PacketStream n +chunkToPacket :: (C.KnownNat n) => [PacketStreamM2S 1 meta] -> PacketStreamM2S n meta +chunkToPacket l = + PacketStreamM2S + { _last = + if M.isJust $ _last $ L.last l then M.Just (fromIntegral $ L.length l - 1) else Nothing + , _abort = or $ fmap _abort l + , _meta = _meta $ L.head l + , _data = L.foldr (C.+>>) (C.repeat 0) $ fmap (C.head . _data) l + } + +-- | Split a PacketStream n into a list of PacketStream 1 +chopPacket :: + forall n meta. + (1 C.<= n) => + (C.KnownNat n) => + PacketStreamM2S n meta -> + [PacketStreamM2S 1 meta] +chopPacket PacketStreamM2S{..} = packets + where + lasts = case _last of + Nothing -> repeat Nothing + Just in' -> replicate (fromIntegral in') Nothing ++ [Just (0 :: C.Index 1)] + + datas = case _last of + Nothing -> C.toList _data + Just in' -> take (fromIntegral in' + 1) $ C.toList _data + + packets = (\(idx, dat) -> PacketStreamM2S (pure dat) idx _meta _abort) <$> zip lasts datas + +-- | Set the _last of the last element of a list of PacketStreams to 0 +fullPackets :: (C.KnownNat n) => [PacketStreamM2S n meta] -> [PacketStreamM2S n meta] +fullPackets [] = [] +fullPackets fragments = + let lastFragment = (last fragments){_last = Just 0} + in init fragments ++ [lastFragment] + +-- | Drops packets if one of the words in the packet has the abort flag set +dropAbortedPackets :: [PacketStreamM2S n meta] -> [PacketStreamM2S n meta] +dropAbortedPackets packets = concat $ filter (not . any _abort) (chunkByPacket packets) + +-- | Split a list of PacketStream n into a list of PacketStream 1 +downConvert :: + forall n meta. + (1 C.<= n) => + (C.KnownNat n) => + [PacketStreamM2S n meta] -> + [PacketStreamM2S 1 meta] +downConvert = concatMap chopPacket + +-- | Merge a list of PacketStream 1 into a list of PacketStream n +upConvert :: + forall n meta. + (1 C.<= n) => + (C.KnownNat n) => + [PacketStreamM2S 1 meta] -> + [PacketStreamM2S n meta] +upConvert packets = chunkToPacket <$> chopBy (C.natToNum @n) packets + +-- | Set all invalid bytes to null-bytes +cleanPackets :: + forall n meta. + (1 C.<= n) => + (C.KnownNat n) => + [PacketStreamM2S n meta] -> + [PacketStreamM2S n meta] +cleanPackets = map cleanPacket + where + cleanPacket pkt@PacketStreamM2S{..} = case _last of + Nothing -> pkt + Just i -> pkt{_data = M.fromJust $ Vec.fromList datas} + where + datas = + take (1 + fromIntegral i) (C.toList _data) + ++ replicate ((C.natToNum @n) - 1 - fromIntegral i) 0 + +-- | Make an existing list of packets valid, meaning all words in a packet share the same meta value, and the list always contain full packets +makeValid :: + forall (dataWidth :: C.Nat) (metaType :: C.Type). + (C.KnownNat dataWidth) => + (1 C.<= dataWidth) => + [PacketStreamM2S dataWidth metaType] -> + [PacketStreamM2S dataWidth metaType] +makeValid packets = fullPackets $ concatMap sameMeta $ chunkByPacket packets + where + sameMeta :: [PacketStreamM2S dataWidth metaType] -> [PacketStreamM2S dataWidth metaType] + sameMeta [] = [] + sameMeta list@(x : _) = fullPackets $ fmap (\pkt -> pkt{_meta = _meta x}) list + +{- | Generates a single valid packet using the given generator, + the meta value of the first word will be that of all words, and only the last value in the packet will have Last = Just .. +-} +genValidPacket :: + forall (dataWidth :: C.Nat) (metaType :: C.Type). + (C.KnownNat dataWidth) => + (1 C.<= dataWidth) => + Range Int -> + Gen (PacketStreamM2S dataWidth metaType) -> + Gen [PacketStreamM2S dataWidth metaType] +genValidPacket range gen = do + genWords <- Gen.list range gen + return $ makeValidPacket genWords + where + makeValidPacket :: + [PacketStreamM2S dataWidth metaType] -> [PacketStreamM2S dataWidth metaType] + makeValidPacket [] = [] + makeValidPacket list@(x : _) = fullPackets $ fmap (\pkt -> pkt{_meta = _meta x, _last = Nothing}) list + +-- | Generates a list filled with valid packets, packets which have the same meta value for all words +genValidPackets :: + forall (dataWidth :: C.Nat) (metaType :: C.Type). + (C.KnownNat dataWidth) => + (1 C.<= dataWidth) => + -- | Range specifying the amount of packets to generate + Range Int -> + -- | Range specifying the size of packets to generate + Range Int -> + -- | Generator for a single packet + Gen (PacketStreamM2S dataWidth metaType) -> + Gen [PacketStreamM2S dataWidth metaType] +genValidPackets range packetRange gen = concat <$> Gen.list range (genValidPacket packetRange gen) diff --git a/tests/Tests/Protocols/PacketStream/Converters.hs b/tests/Tests/Protocols/PacketStream/Converters.hs new file mode 100644 index 00000000..152aba76 --- /dev/null +++ b/tests/Tests/Protocols/PacketStream/Converters.hs @@ -0,0 +1,118 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE RecordWildCards #-} + +module Tests.Protocols.PacketStream.Converters where + +-- base +import qualified Data.Maybe as M +import Prelude + +-- clash-prelude +import Clash.Prelude (type (<=)) +import qualified Clash.Prelude as C + +-- hedgehog +import Hedgehog +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +-- tasty +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +-- clash-protocols +import Protocols +import Protocols.Hedgehog +import Protocols.PacketStream.Base +import Protocols.PacketStream.Converters + +-- tests +import Tests.Protocols.PacketStream.Base + +genVec :: (C.KnownNat n, 1 <= n) => Gen a -> Gen (C.Vec n a) +genVec gen = sequence (C.repeat gen) + +ucModel :: forall n. (C.KnownNat n) => [PacketStreamM2S 1 ()] -> [PacketStreamM2S n ()] +ucModel fragments = out + where + wholePackets = smearAbort <$> chunkBy (M.isJust . _last) fragments + chunks = wholePackets >>= chopBy (C.natToNum @n) + out = fmap chunkToPacket chunks + +-- | Test the upconverter stream instance +upconverterTest :: forall n. (1 <= n) => C.SNat n -> Property +upconverterTest C.SNat = + propWithModelSingleDomain + @C.System + defExpectOptions + (fmap fullPackets (Gen.list (Range.linear 0 100) genPackets)) -- Input packets + (C.exposeClockResetEnable ucModel) -- Desired behaviour of UpConverter + (C.exposeClockResetEnable @C.System (ckt @n)) -- Implementation of UpConverter + (===) -- Property to test + where + ckt :: + forall (dataWidth :: C.Nat) (dom :: C.Domain). + (C.HiddenClockResetEnable dom) => + (1 <= dataWidth) => + (C.KnownNat dataWidth) => + Circuit (PacketStream dom 1 ()) (PacketStream dom dataWidth ()) + ckt = upConverterC + + -- This generates the packets + genPackets = + PacketStreamM2S + <$> genVec Gen.enumBounded + <*> Gen.maybe Gen.enumBounded + <*> Gen.enumBounded + <*> Gen.enumBounded + +prop_upconverter_d1, prop_upconverter_d2, prop_upconverter_d4 :: Property +prop_upconverter_d1 = upconverterTest (C.SNat @1) +prop_upconverter_d2 = upconverterTest (C.SNat @2) +prop_upconverter_d4 = upconverterTest (C.SNat @4) + +dcModel :: + forall n. (1 <= n) => (C.KnownNat n) => [PacketStreamM2S n ()] -> [PacketStreamM2S 1 ()] +dcModel = downConvert + +-- | Test the downconverter stream instance +downconverterTest :: forall n. (1 <= n) => C.SNat n -> Property +downconverterTest C.SNat = + propWithModelSingleDomain + @C.System + defExpectOptions + (Gen.list (Range.linear 0 100) genPackets) -- Input packets + (C.exposeClockResetEnable dcModel) -- Desired behaviour of DownConverter + (C.exposeClockResetEnable @C.System (ckt @n)) -- Implementation of DownConverter + (===) -- Property to test + where + ckt :: + forall (dataWidth :: C.Nat) (dom :: C.Domain). + (C.HiddenClockResetEnable dom) => + (1 <= dataWidth) => + (C.KnownNat dataWidth) => + Circuit (PacketStream dom dataWidth ()) (PacketStream dom 1 ()) + ckt = downConverterC + + -- This generates the packets + genPackets = + PacketStreamM2S + <$> genVec Gen.enumBounded + <*> Gen.maybe Gen.enumBounded + <*> Gen.enumBounded + <*> Gen.enumBounded + +prop_downconverter_d1, prop_downconverter_d2, prop_downconverter_d4 :: Property +prop_downconverter_d1 = downconverterTest (C.SNat @1) +prop_downconverter_d2 = downconverterTest (C.SNat @2) +prop_downconverter_d4 = downconverterTest (C.SNat @4) + +tests :: TestTree +tests = + localOption (mkTimeout 12_000_000 {- 12 seconds -}) $ + localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator) diff --git a/tests/Tests/Protocols/PacketStream/PacketFifo.hs b/tests/Tests/Protocols/PacketStream/PacketFifo.hs new file mode 100644 index 00000000..0742adb3 --- /dev/null +++ b/tests/Tests/Protocols/PacketStream/PacketFifo.hs @@ -0,0 +1,182 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE RecordWildCards #-} + +module Tests.Protocols.PacketStream.PacketFifo where + +-- base +import Data.Int (Int16) +import Prelude + +-- clash-prelude +import Clash.Prelude hiding (drop, take, undefined, (++)) +import qualified Clash.Prelude as C + +-- hedgehog +import Hedgehog as H +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +-- tasty +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +-- clash-protocols +import Protocols +import Protocols.Hedgehog +import Protocols.PacketStream.Base +import Protocols.PacketStream.PacketFifo (overflowDropPacketFifoC, packetFifoC) + +-- tests +import Tests.Protocols.PacketStream.Base as U + +genVec :: (C.KnownNat n, 1 C.<= n) => Gen a -> Gen (C.Vec n a) +genVec gen = sequence (C.repeat gen) + +-- | generate a "clean" packet: a packet without an abort +genCleanWord :: Gen (PacketStreamM2S 4 Int16) +genCleanWord = + PacketStreamM2S + <$> genVec Gen.enumBounded + <*> pure Nothing + <*> Gen.enumBounded + <*> pure False + +genWord :: Gen (PacketStreamM2S 4 Int16) +genWord = + PacketStreamM2S + <$> genVec Gen.enumBounded + <*> Gen.maybe Gen.enumBounded + <*> Gen.enumBounded + <*> Gen.enumBounded + +genPackets :: Range Int -> Gen [PacketStreamM2S 4 Int16] +genPackets range = makeValid <$> Gen.list range genWord + +isSubsequenceOf :: (Eq a) => [a] -> [a] -> Bool +isSubsequenceOf [] _ = True +isSubsequenceOf _ [] = False +isSubsequenceOf (x : xs) (y : ys) + | x == y = isSubsequenceOf xs ys + | otherwise = isSubsequenceOf xs (y : ys) + +-- | test for id and proper dropping of aborted packets +prop_packetFifo_id :: Property +prop_packetFifo_id = + idWithModelSingleDomain + @C.System + defExpectOptions + (genPackets (Range.linear 0 100)) + (C.exposeClockResetEnable dropAbortedPackets) + (C.exposeClockResetEnable ckt) + where + ckt :: + (HiddenClockResetEnable System) => + Circuit (PacketStream System 4 Int16) (PacketStream System 4 Int16) + ckt = packetFifoC d12 d12 + +-- test for id with a small buffer to ensure backpressure is tested +prop_packetFifo_small_buffer_id :: Property +prop_packetFifo_small_buffer_id = + idWithModelSingleDomain + @C.System + defExpectOptions + (genValidPackets (Range.linear 0 10) (Range.linear 0 31) genCleanWord) + (C.exposeClockResetEnable dropAbortedPackets) + (C.exposeClockResetEnable ckt) + where + ckt :: + (HiddenClockResetEnable System) => + Circuit (PacketStream System 4 Int16) (PacketStream System 4 Int16) + ckt = packetFifoC d5 d5 + +-- | test to check if there are no gaps inside of packets +prop_packetFifo_no_gaps :: Property +prop_packetFifo_no_gaps = property $ do + let packetFifoSize = d12 + maxInputSize = 50 + ckt = + exposeClockResetEnable + (packetFifoC packetFifoSize packetFifoSize) + systemClockGen + resetGen + enableGen + gen = genPackets (Range.linear 0 100) + + packets :: [PacketStreamM2S 4 Int16] <- H.forAll gen + + let packetSize = 2 Prelude.^ snatToInteger packetFifoSize + cfg = SimulationConfig 1 (2 * packetSize) False + cktResult = simulateC ckt cfg (Just <$> packets) + + assert $ noGaps $ take (5 * maxInputSize) cktResult + where + noGaps :: [Maybe (PacketStreamM2S 4 Int16)] -> Bool + noGaps (Just (PacketStreamM2S{_last = Nothing}) : Nothing : _) = False + noGaps (_ : xs) = noGaps xs + noGaps _ = True + +-- | test for id and proper dropping of aborted packets +prop_overFlowDrop_packetFifo_id :: Property +prop_overFlowDrop_packetFifo_id = + idWithModelSingleDomain + @C.System + defExpectOptions + (genPackets (Range.linear 0 100)) + (C.exposeClockResetEnable dropAbortedPackets) + (C.exposeClockResetEnable ckt) + where + ckt :: + (HiddenClockResetEnable System) => + Circuit (PacketStream System 4 Int16) (PacketStream System 4 Int16) + ckt = fromPacketStream |> overflowDropPacketFifoC d12 d12 + +-- | test for proper dropping when full +prop_overFlowDrop_packetFifo_drop :: Property +prop_overFlowDrop_packetFifo_drop = + idWithModelSingleDomain + @C.System + (ExpectOptions 50 (Just 1_000) 30 False) + -- make sure the timeout is long as the packetFifo can be quiet for a while while dropping + (liftA3 (\a b c -> a ++ b ++ c) genSmall genBig genSmall) + (C.exposeClockResetEnable model) + (C.exposeClockResetEnable ckt) + where + bufferSize = d5 + + ckt :: + (HiddenClockResetEnable System) => + Circuit (PacketStream System 4 Int16) (PacketStream System 4 Int16) + ckt = fromPacketStream |> overflowDropPacketFifoC bufferSize bufferSize + + model :: [PacketStreamM2S 4 Int16] -> [PacketStreamM2S 4 Int16] + model packets = Prelude.concat $ take 1 packetChunk ++ drop 2 packetChunk + where + packetChunk = chunkByPacket packets + + genSmall = genValidPacket (Range.linear 1 5) genCleanWord + genBig = genValidPacket (Range.linear 33 50) genCleanWord + +-- | test for id using a small metabuffer to ensure backpressure using the metabuffer is tested +prop_packetFifo_small_metaBuffer :: Property +prop_packetFifo_small_metaBuffer = + idWithModelSingleDomain + @C.System + defExpectOptions + (genPackets (Range.linear 0 100)) + (C.exposeClockResetEnable dropAbortedPackets) + (C.exposeClockResetEnable ckt) + where + ckt :: + (HiddenClockResetEnable System) => + Circuit (PacketStream System 4 Int16) (PacketStream System 4 Int16) + ckt = packetFifoC d12 d2 + +tests :: TestTree +tests = + localOption (mkTimeout 30_000_000 {- 30 seconds -}) $ + localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator) diff --git a/tests/Tests/Protocols/PacketStream/Packetizers.hs b/tests/Tests/Protocols/PacketStream/Packetizers.hs new file mode 100644 index 00000000..c8400994 --- /dev/null +++ b/tests/Tests/Protocols/PacketStream/Packetizers.hs @@ -0,0 +1,171 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NumericUnderscores #-} + +module Tests.Protocols.PacketStream.Packetizers ( + packetizerModel, + packetizeFromDfModel, + depacketizerModel, + depacketizeToDfModel, + tests, +) where + +-- base +import qualified Data.List as L +import Prelude + +-- clash +import Clash.Prelude +import Clash.Sized.Vector (unsafeFromList) + +-- hedgehog +-- import Hedgehog +-- import qualified Hedgehog.Gen as Gen +-- import qualified Hedgehog.Range as Range + +-- tasty +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) + +-- import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +-- clash-protocols +import Protocols.PacketStream.Base + +-- tests +import Tests.Protocols.PacketStream.Base + +-- | Model of the generic `packetizerC`. +packetizerModel :: + forall + (dataWidth :: Nat) + (headerBytes :: Nat) + (metaIn :: Type) + (header :: Type) + (metaOut :: Type). + (KnownNat dataWidth) => + (KnownNat headerBytes) => + (1 <= dataWidth) => + (1 <= headerBytes) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (metaIn -> metaOut) -> + (metaIn -> header) -> + [PacketStreamM2S dataWidth metaIn] -> + [PacketStreamM2S dataWidth metaOut] +packetizerModel toMetaOut toHeader ps = L.concatMap (upConvert . prependHdr) bytePackets + where + prependHdr :: [PacketStreamM2S 1 metaIn] -> [PacketStreamM2S 1 metaOut] + prependHdr fragments = hdr L.++ L.map (\f -> f{_meta = metaOut}) fragments + where + h = L.head fragments + metaOut = toMetaOut (_meta h) + hdr = L.map go (toList $ bitCoerce (toHeader (_meta h))) + go byte = PacketStreamM2S (singleton byte) Nothing metaOut (_abort h) + + bytePackets :: [[PacketStreamM2S 1 metaIn]] + bytePackets = downConvert . smearAbort <$> chunkByPacket ps + +-- | Model of the generic `packetizeFromDfC`. +packetizeFromDfModel :: + forall + (dataWidth :: Nat) + (headerBytes :: Nat) + (a :: Type) + (header :: Type) + (metaOut :: Type). + (KnownNat dataWidth) => + (KnownNat headerBytes) => + (1 <= dataWidth) => + (1 <= headerBytes) => + (BitPack header) => + (BitSize header ~ headerBytes * 8) => + (a -> metaOut) -> + (a -> header) -> + [a] -> + [PacketStreamM2S dataWidth metaOut] +packetizeFromDfModel toMetaOut toHeader = L.concatMap (upConvert . packetize) + where + packetize :: a -> [PacketStreamM2S 1 metaOut] + packetize d = + fullPackets $ + L.map + (\byte -> PacketStreamM2S (byte :> Nil) Nothing (toMetaOut d) False) + (toList $ bitCoerce (toHeader d)) + +-- | Model of the generic `depacketizerC`. +depacketizerModel :: + forall + (dataWidth :: Nat) + (headerBytes :: Nat) + (metaIn :: Type) + (metaOut :: Type) + (header :: Type). + ( KnownNat dataWidth + , KnownNat headerBytes + , 1 <= dataWidth + , 1 <= headerBytes + , BitPack header + , BitSize header ~ headerBytes * 8 + ) => + (header -> metaIn -> metaOut) -> + [PacketStreamM2S dataWidth metaIn] -> + [PacketStreamM2S dataWidth metaOut] +depacketizerModel toMetaOut ps = L.concat dataWidthPackets + where + hdrbytes = natToNum @headerBytes + + parseHdr :: + ([PacketStreamM2S 1 metaIn], [PacketStreamM2S 1 metaIn]) -> [PacketStreamM2S 1 metaOut] + parseHdr (hdrF, fwdF) = fmap (\f -> f{_meta = metaOut}) fwdF + where + hdr = bitCoerce $ unsafeFromList @headerBytes $ _data <$> hdrF + metaOut = toMetaOut hdr (_meta $ L.head fwdF) + + bytePackets :: [[PacketStreamM2S 1 metaIn]] + bytePackets = + L.filter (\fs -> L.length fs > hdrbytes) $ + L.concatMap chopPacket . smearAbort <$> chunkByPacket ps + + parsedPackets :: [[PacketStreamM2S 1 metaOut]] + parsedPackets = parseHdr . L.splitAt hdrbytes <$> bytePackets + + dataWidthPackets :: [[PacketStreamM2S dataWidth metaOut]] + dataWidthPackets = fmap chunkToPacket . chopBy (natToNum @dataWidth) <$> parsedPackets + +-- | Model of the generic `depacketizeToDfC`. +depacketizeToDfModel :: + forall + (dataWidth :: Nat) + (headerBytes :: Nat) + (meta :: Type) + (a :: Type) + (header :: Type). + ( KnownNat dataWidth + , KnownNat headerBytes + , 1 <= dataWidth + , 1 <= headerBytes + , BitPack header + , BitSize header ~ headerBytes * 8 + ) => + (header -> meta -> a) -> + [PacketStreamM2S dataWidth meta] -> + [a] +depacketizeToDfModel toOut ps = parseHdr <$> bytePackets + where + hdrbytes = natToNum @headerBytes + + parseHdr :: [PacketStreamM2S 1 meta] -> a + parseHdr hdrF = toOut (bitCoerce $ unsafeFromList @headerBytes $ _data <$> hdrF) (_meta $ L.head hdrF) + + bytePackets :: [[PacketStreamM2S 1 meta]] + bytePackets = + L.filter (\fs -> L.length fs >= hdrbytes) $ + L.concatMap chopPacket <$> chunkByPacket (dropAbortedPackets ps) + +tests :: TestTree +tests = + localOption (mkTimeout 12_000_000 {- 12 seconds -}) $ + localOption + (HedgehogTestLimit (Just 1_000_000)) + $(testGroupGenerator) diff --git a/tests/Tests/Protocols/PacketStream/Routing.hs b/tests/Tests/Protocols/PacketStream/Routing.hs new file mode 100644 index 00000000..b1d06788 --- /dev/null +++ b/tests/Tests/Protocols/PacketStream/Routing.hs @@ -0,0 +1,159 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE RecordWildCards #-} + +module Tests.Protocols.PacketStream.Routing where + +-- base +import Data.List (groupBy, sortOn) +import Prelude + +-- clash-prelude +import Clash.Prelude (type (<=)) +import qualified Clash.Prelude as C + +-- hedgehog +import Hedgehog hiding (Parallel) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +-- tasty +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +-- clash-protocols + +import Protocols.Hedgehog +import Protocols.PacketStream.Base +import Protocols.PacketStream.Routing + +-- tests +import Tests.Protocols.PacketStream.Base (chunkByPacket, fullPackets) + +genVec :: (C.KnownNat n, 1 <= n) => Gen a -> Gen (C.Vec n a) +genVec gen = sequence (C.repeat gen) + +-- | Tests the round-robin packet arbiter with one source; essentially an id test +prop_packetarbiter_roundrobin_id :: Property +prop_packetarbiter_roundrobin_id = makePropPacketArbiter C.d1 C.d2 RoundRobin + +-- | Tests the parallel packet arbiter with one source; essentially an id test +prop_packetarbiter_parallel_id :: Property +prop_packetarbiter_parallel_id = makePropPacketArbiter C.d1 C.d2 Parallel + +-- Tests the round-robin arbiter with five sources +prop_packetarbiter_roundrobin :: Property +prop_packetarbiter_roundrobin = makePropPacketArbiter C.d5 C.d2 RoundRobin + +-- Tests the parallel arbiter with five sources +prop_packetarbiter_parallel :: Property +prop_packetarbiter_parallel = makePropPacketArbiter C.d5 C.d2 Parallel + +{- | Tests a packet arbiter for any data width and number of sources. In particular, +tests that packets from all sources are sent out unmodified in the same order +they were in in the source streams. +-} +makePropPacketArbiter :: + forall p n. + ( C.KnownNat p + , 1 <= p + , C.KnownNat n + , 1 <= n + ) => + C.SNat p -> + C.SNat n -> + ArbiterMode -> + Property +makePropPacketArbiter _ _ mode = + propWithModelSingleDomain + @C.System + defExpectOptions + genSources + (C.exposeClockResetEnable concat) + (C.exposeClockResetEnable (packetArbiterC mode)) + (\xs ys -> partitionPackets xs === partitionPackets ys) + where + genSources = mapM (fmap fullPackets . Gen.list (Range.linear 0 100) . genPacket) (C.indicesI @p) + -- TODO use util function from client review branch + genPacket i = + PacketStreamM2S + <$> genVec @n Gen.enumBounded + <*> Gen.maybe Gen.enumBounded + <*> pure i + <*> Gen.enumBounded + + partitionPackets packets = + sortOn (_meta . head . head) $ + groupBy (\a b -> _meta a == _meta b) <$> chunkByPacket packets + +{- | Tests that the packet dispatcher works correctly with one sink that accepts +all packets; essentially an id test. +-} +prop_packetdispatcher_id :: Property +prop_packetdispatcher_id = + makePropPacketDispatcher + C.d4 + ((const True :: Int -> Bool) C.:> C.Nil) + +{- | Tests the packet dispatcher for a data width of four bytes and three +overlapping but incomplete dispatch functions, effectively testing whether +the circuit sends input to the first allowed output channel and drops input +if there are none. +-} +prop_packetdispatcher :: Property +prop_packetdispatcher = makePropPacketDispatcher C.d4 fs + where + fs :: C.Vec 3 (C.Index 4 -> Bool) + fs = + (>= 3) + C.:> (>= 2) + C.:> (>= 1) + C.:> C.Nil + +{- | Generic test function for the packet dispatcher, testing for all data widths, +dispatch functions, and some meta types +-} +makePropPacketDispatcher :: + forall (p :: C.Nat) (dataWidth :: C.Nat) (a :: C.Type). + ( C.KnownNat p + , 1 <= p + , C.KnownNat dataWidth + , 1 <= dataWidth + , TestType a + , Bounded a + , Enum a + ) => + C.SNat dataWidth -> + C.Vec p (a -> Bool) -> + Property +makePropPacketDispatcher _ fs = + idWithModelSingleDomain @C.System + defExpectOptions + (Gen.list (Range.linear 0 100) genPackets) + (C.exposeClockResetEnable (model 0)) + (C.exposeClockResetEnable (packetDispatcherC fs)) + where + model :: + C.Index p -> [PacketStreamM2S dataWidth a] -> C.Vec p [PacketStreamM2S dataWidth a] + model _ [] = pure [] + model i (y : ys) + | (fs C.!! i) (_meta y) = let next = model 0 ys in C.replace i (y : (next C.!! i)) next + | i < maxBound = model (i + 1) (y : ys) + | otherwise = model 0 ys + + -- TODO use util function from client review branch + genPackets = + PacketStreamM2S + <$> genVec @dataWidth Gen.enumBounded + <*> Gen.maybe Gen.enumBounded + <*> Gen.enumBounded + <*> Gen.enumBounded + +tests :: TestTree +tests = + localOption (mkTimeout 12_000_000 {- 12 seconds -}) $ + localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator)