Add PacketStream protocol.

Co-authored-by: Jasmijn Bookelmann <[email protected]>
Co-authored-by: Cato van Ojen <[email protected]>>
Co-authored-by: MatthijsMu <[email protected]>
Co-authored-by: t-wallet <[email protected]>
Co-authored-by: Jasper Laumen <[email protected]>
Co-authored-by: Mart Koster <[email protected]>
Co-authored-by: Bryan Rinders <[email protected]>
Co-authored-by: Daan Weessies <[email protected]>

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
 

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

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

src/Protocols/PacketStream/AsyncFifo.hs

@@ -0,0 +1,57 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+{- |
+Provides `asyncFifoC` for crossing clock domains in the packet stream protocol.
+-}
+module Protocols.PacketStream.AsyncFifo (asyncFifoC) where
+
+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, empty, full) = asyncFIFOSynchronizer depth wClk rClk wRst rRst wEn rEn readReq fwdIn
+    -- If the FIFO is empty, we output Nothing. Else, we output the oldest element.
+    fwdOut = mux empty (pure Nothing) (Just <$> element)
+    -- Assert backpressure when the FIFO is full.
+    bwdOut = PacketStreamS2M . not <$> full
+    -- Next component is ready to read if the fifo is not empty and it does not assert backpressure.
+    readReq = (not <$> empty) .&&. (_ready <$> bwdIn)

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)