Remove null-byte restriction

Forcing bytes in PacketStream _data to be 0x00 turned out to be too restrictive. Allowing them to be undefined makes a lot of components more efficient: depacketizers, packetizers, dropTail, and upConverter. It also strengthens the test framework as we can now force un-enabled bytes to throw an error when evaluated.

clash-protocols/src/Protocols/PacketStream/Base.hs

@@ -16,6 +16,9 @@ module Protocols.PacketStream.Base (
   PacketStreamS2M (..),
   PacketStream,
 
+  -- * Constants
+  nullByte,
+
   -- * CSignal conversion
   toCSignal,
   unsafeFromCSignal,
@@ -102,12 +105,60 @@ data PacketStreamM2S (dataWidth :: Nat) (meta :: Type) = PacketStreamM2S
   -- ^ Iff true, the packet corresponding to this transfer is invalid. The subordinate
   --   must either drop the packet or forward the `_abort`.
   }
-  deriving (Eq, Generic, ShowX, Show, NFData, Bundle, Functor)
+  deriving (Generic, ShowX, Show, NFData, Bundle, Functor)
 
 deriving instance
   (KnownNat dataWidth, NFDataX meta) =>
   NFDataX (PacketStreamM2S dataWidth meta)
 
+{- |
+Two PacketStream transfers are equal if and only if:
+
+1. They have the same `_last`
+2. They have the same `_meta`.
+3. They have the same `_abort`.
+4. All bytes in `_data` which are enabled by `_last` are equal.
+
+Data bytes that are not enabled are not considered in the equality check,
+because the protocol allows them to be /undefined/.
+
+=== Examples
+
+>>> t1 = PacketStreamM2S (0x11 :> 0x22 :> 0x33 :> Nil) Nothing () False
+>>> t2 = PacketStreamM2S (0x11 :> 0x22 :> 0x33 :> Nil) (Just 2) () False
+>>> t3 = PacketStreamM2S (0x11 :> 0x22 :> 0xFF :> Nil) (Just 2) () False
+>>> t4 = PacketStreamM2S (0x11 :> 0x22 :> undefined :> Nil) (Just 2) () False
+
+>>> t1 == t1
+True
+>>> t2 == t3
+True
+>>> t1 /= t2
+True
+>>> t3 == t4
+True
+-}
+instance (KnownNat dataWidth, Eq meta) => Eq (PacketStreamM2S dataWidth meta) where
+  t1 == t2 = lastEq && metaEq && abortEq && dataEq
+   where
+    lastEq = _last t1 == _last t2
+    metaEq = _meta t1 == _meta t2
+    abortEq = _abort t1 == _abort t2
+
+    -- Bitmask used for data equality. If the index of a data byte is larger
+    -- than or equal to the size of `_data`, it is a null byte and must be
+    -- disregarded in the equality check.
+    mask = case _last t1 of
+      Nothing -> repeat False
+      Just size -> imap (\i _ -> resize i >= size) (_data t1)
+
+    dataEq = case compareSNat (SNat @dataWidth) d0 of
+      SNatLE -> True
+      SNatGT ->
+        leToPlus @1 @dataWidth
+          $ fold (&&)
+          $ zipWith3 (\b1 b2 isNull -> isNull || b1 == b2) (_data t1) (_data t2) mask
+
 -- | Used by circuit-notation to create an empty stream
 instance Default (Maybe (PacketStreamM2S dataWidth meta)) where
   def = Nothing
@@ -141,12 +192,13 @@ Invariants:
 3. A manager must keep the metadata (`_meta`) of an entire packet it sends constant.
 4. A subordinate which receives a transfer with `_abort` asserted must either forward this `_abort` or drop the packet.
 5. A packet may not be interrupted by another packet.
-6. All bytes in `_data` which are not enabled must be 0x00.
 
 This protocol allows the last transfer of a packet to have zero valid bytes in
 '_data', so it also allows 0-byte packets. Note that concrete implementations
 of the protocol are free to disallow 0-byte packets or packets with a trailing
 zero-byte transfer for whatever reason.
+
+The value of data bytes which are not enabled is /undefined/.
 -}
 data PacketStream (dom :: Domain) (dataWidth :: Nat) (meta :: Type)
 
@@ -240,6 +292,13 @@ instance
       $ Df.maybeToData
       <$> sampled
 
+-- | Undefined PacketStream null byte. Will throw an error if evaluated.
+nullByte :: BitVector 8
+nullByte =
+  deepErrorX
+    $ "value of PacketStream null byte is undefined. "
+    <> "Data bytes that are not enabled must not be evaluated."
+
 {- |
 Circuit to convert a 'CSignal' into a 'PacketStream'.
 This is unsafe, because it ignores all incoming backpressure.

clash-protocols/src/Protocols/PacketStream/Converters.hs

@@ -38,12 +38,10 @@ data UpConverterState (dwOut :: Nat) (n :: Nat) (meta :: Type) = UpConverterStat
   --   a constant, which is free in hardware in terms of resource usage.
   , _ucFlush :: Bool
   -- ^ If true, we should output the current state as a PacketStream transfer.
-  , _ucFreshBuf :: Bool
-  -- ^ If true, we need to start a fresh buffer (all zeroes).
   , _ucAborted :: Bool
   -- ^ Whether the current transfer we are building is aborted.
   , _ucLastIdx :: Maybe (Index (dwOut + 1))
-  -- ^ If true, the current buffer contains the last byte of the current packet.
+  -- ^ If Just, the current buffer contains the last byte of the current packet.
   , _ucMeta :: meta
   -- ^ Metadata of the current transfer we are a building.
   }
@@ -86,14 +84,13 @@ nextState st@(UpConverterState{..}) (Just PacketStreamM2S{..}) (PacketStreamS2M
   -- output fragment is accepted by the sink
   outReady = not _ucFlush || inReady
   bufFull = _ucIdx == maxBound
-  currBuf = if _ucFreshBuf then repeat 0 else _ucBuf
 
   nextBuf =
     bitCoerce
       $ replace
         _ucIdx
         (bitCoerce _data :: BitVector (8 * dwIn))
-        (bitCoerce currBuf :: Vec n (BitVector (8 * dwIn)))
+        (bitCoerce _ucBuf :: Vec n (BitVector (8 * dwIn)))
 
   nextFlush = isJust _last || bufFull
   nextIdx = if nextFlush then 0 else _ucIdx + 1
@@ -117,7 +114,6 @@ nextState st@(UpConverterState{..}) (Just PacketStreamM2S{..}) (PacketStreamS2M
       , _ucIdx = nextIdx
       , _ucIdx2 = nextIdx2
       , _ucFlush = nextFlush
-      , _ucFreshBuf = nextFlush
       , _ucAborted = nextAbort
       , _ucLastIdx = nextLastIdx
       , _ucMeta = _meta
@@ -146,11 +142,10 @@ upConverter = mealyB go s0
   errPrefix = "upConverterT: undefined initial "
   s0 =
     UpConverterState
-      { _ucBuf = deepErrorX (errPrefix <> " _ucBuf")
+      { _ucBuf = repeat nullByte
       , _ucIdx = 0
       , _ucIdx2 = 0
       , _ucFlush = False
-      , _ucFreshBuf = True
       , _ucAborted = False
       , _ucLastIdx = deepErrorX (errPrefix <> " _ucLastIdx")
       , _ucMeta = deepErrorX (errPrefix <> " _ucMeta")

clash-protocols/src/Protocols/PacketStream/Depacketizers.hs

@@ -32,9 +32,6 @@ import Data.Constraint.Nat.Extra
 import Data.Data ((:~:) (Refl))
 import Data.Maybe
 
-defaultByte :: BitVector 8
-defaultByte = 0x00
-
 {- | Vectors of this size are able to hold @headerBytes `DivRU` dataWidth@
      transfers of size @dataWidth@, which is bigger than or equal to @headerBytes@.
 -}
@@ -167,17 +164,14 @@ depacketizerT toMetaOut st@Forward{..} (Just pkt@PacketStreamM2S{..}, bwdIn) = (
   outPkt = case sameNat d0 (SNat @(headerBytes `Mod` dataWidth)) of
     Just Refl ->
       pkt
-        { _data = if _lastFwd then repeat 0x00 else _data
+        { _data = _data
         , _last = if _lastFwd then Just 0 else _last
         , _meta = toMetaOut (bitCoerce header) _meta
         , _abort = nextAborted
         }
     Nothing ->
       pkt
-        { _data =
-            if _lastFwd
-              then fwdBytes ++ repeat @(dataWidth - ForwardBytes headerBytes dataWidth) defaultByte
-              else dataOut
+        { _data = dataOut
         , _last =
             if _lastFwd
               then either Just Just =<< newLast
@@ -497,6 +491,5 @@ dropTailC SNat = case strictlyPositiveDivRu @n @dataWidth of
             [s1, s2] <- fanout -< stream
             delayed <- delayStreamC (SNat @(n `DivRU` dataWidth)) -< s1
             info <- transmitDropInfoC @dataWidth @(n `DivRU` dataWidth) (SNat @n) -< s2
-            dropped <- dropTailC' @dataWidth @(n `DivRU` dataWidth) -< (delayed, info)
-            zeroOutInvalidBytesC -< dropped
+            dropTailC' @dataWidth @(n `DivRU` dataWidth) -< (delayed, info)
         )

clash-protocols/src/Protocols/PacketStream/Hedgehog.hs

@@ -101,7 +101,7 @@ chunkToPacket xs =
           <$> _last lastTransfer
     , _abort = any _abort xs
     , _meta = _meta lastTransfer
-    , _data = L.foldr ((+>>) . head . _data) (repeat 0x00) xs
+    , _data = L.foldr ((+>>) . head . _data) (repeat nullByte) xs
     }
  where
   lastTransfer = L.last xs
@@ -207,7 +207,7 @@ depacketizerModel toMetaOut ps = L.concat dataWidthPackets
     fwdF' = case fwdF of
       [] ->
         [ PacketStreamM2S
-            (Vec.singleton 0x00)
+            (Vec.singleton nullByte)
             (Just 0)
             (error "depacketizerModel: should be replaced")
             (_abort (L.last hdrF))
@@ -285,7 +285,7 @@ dropTailModel SNat packets = L.concatMap go (chunkByPacket packets)
   go packet =
     upConvert
       $ L.init trimmed
-      L.++ [setNull (L.last trimmed){_last = _last $ L.last bytePkts, _abort = aborted}]
+      L.++ [(L.last trimmed){_last = _last $ L.last bytePkts, _abort = aborted}]
    where
     aborted = L.any _abort packet
     bytePkts = downConvert packet
@@ -468,7 +468,7 @@ genTransfer meta abortGen =
 
 {- |
 Generate the last transfer of a packet, i.e. a transfer with @_last@ set as @Just@.
-All bytes which are not enabled are set to 0x00.
+All bytes which are not enabled are forced /undefined/.
 -}
 genLastTransfer ::
   forall (dataWidth :: Nat) (meta :: Type).
@@ -504,6 +504,6 @@ setNull transfer =
             fromJust
               ( Vec.fromList
                   $ L.take (fromIntegral i) (toList (_data transfer))
-                  L.++ L.replicate ((natToNum @dataWidth) - fromIntegral i) 0x00
+                  L.++ L.replicate ((natToNum @dataWidth) - fromIntegral i) nullByte
               )
         }

clash-protocols/src/Protocols/PacketStream/Packetizers.hs

@@ -28,9 +28,6 @@ import Data.Constraint.Nat.Extra (leModulusDivisor, leZeroIsZero, strictlyPositi
 import Data.Maybe
 import Data.Maybe.Extra
 
-defaultByte :: BitVector 8
-defaultByte = 0x00
-
 type PacketizerCt (header :: Type) (headerBytes :: Nat) (dataWidth :: Nat) =
   ( BitPack header
   , BitSize header ~ headerBytes * 8
@@ -107,7 +104,7 @@ packetizerT1 toMetaOut toHeader st (Just inPkt, bwdIn) =
        where
         outPkt =
           inPkt
-            { _data = _hdrBuf1 ++ repeat defaultByte
+            { _data = _hdrBuf1 ++ repeat nullByte
             , _last = (\i -> i - natToNum @(dataWidth - headerBytes)) <$> _last inPkt
             , _meta = toMetaOut (_meta inPkt)
             , _abort = _aborted1 || _abort inPkt
@@ -256,7 +253,7 @@ packetizerT3 toMetaOut _ st@Forward3{..} (Just inPkt, bwdIn) =
   buf :: Vec (headerBytes `Mod` dataWidth) (BitVector 8)
   (bytesOut, buf) = splitAt (SNat @(dataWidth - headerBytes `Mod` dataWidth)) (_data inPkt)
   newBuf :: Vec (headerBytes + dataWidth) (BitVector 8)
-  newBuf = buf ++ repeat @(headerBytes + dataWidth - headerBytes `Mod` dataWidth) defaultByte
+  newBuf = buf ++ repeat @(headerBytes + dataWidth - headerBytes `Mod` dataWidth) nullByte
   nextAborted = _aborted3 || _abort inPkt
 
   outPkt =
@@ -375,7 +372,7 @@ packetizeFromDfT toMetaOut toHeader DfIdle (Df.Data dataIn, bwdIn) = (nextStOut,
 -- Thus, we don't need to store the metadata in the state.
 packetizeFromDfT toMetaOut _ st@DfInsert{..} (Df.Data dataIn, bwdIn) = (nextStOut, (bwdOut, Just outPkt))
  where
-  (dataOut, newHdrBuf) = splitAt (SNat @dataWidth) (_dfHdrBuf ++ repeat @dataWidth defaultByte)
+  (dataOut, newHdrBuf) = splitAt (SNat @dataWidth) (_dfHdrBuf ++ repeat @dataWidth nullByte)
   outPkt = PacketStreamM2S dataOut newLast (toMetaOut dataIn) False
 
   newLast = toMaybe (_dfCounter == maxBound) $ case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of
@@ -423,7 +420,7 @@ packetizeFromDfC toMetaOut toHeader = case strictlyPositiveDivRu @headerBytes @d
       go (Df.Data dataIn, bwdIn) = (Ack (_ready bwdIn), Just outPkt)
        where
         outPkt = PacketStreamM2S dataOut (Just l) (toMetaOut dataIn) False
-        dataOut = bitCoerce (toHeader dataIn) ++ repeat @(dataWidth - headerBytes) defaultByte
+        dataOut = bitCoerce (toHeader dataIn) ++ repeat @(dataWidth - headerBytes) nullByte
         l = case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of
           SNatGT -> natToNum @(headerBytes `Mod` dataWidth)
           _ -> natToNum @dataWidth

clash-protocols/tests/Tests/Protocols/PacketStream/PacketFifo.hs

@@ -77,7 +77,7 @@ prop_overFlowDrop_packetFifo_id :: Property
 prop_overFlowDrop_packetFifo_id =
   idWithModelSingleDomain
     @System
-    defExpectOptions
+    defExpectOptions{eoStopAfterEmpty = 1000}
     (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 10)))
     (exposeClockResetEnable dropAbortedPackets)
     (exposeClockResetEnable (packetFifoC @_ @1 @Int16 d10 d10 Drop))