From bfe1baf00764e70434147c338d8a7a38aa92a023 Mon Sep 17 00:00:00 2001
From: Tim Wallet <tw.personal@tutanota.com>
Date: Thu, 10 Oct 2024 17:20:17 +0200
Subject: [PATCH] PacketStream: support zero-byte transfers. (#122)

* Support zero-byte transfers
* Add utility that merges trailing zero-byte transfers
* Make PacketStream test framework more flexible
Now allows users to:
- Set the distribution of abort generation themselves;
- Choose whether to generate zero-byte packets;
- Choose whether to generate trailing zero-byte transfers.
* Converters: remove expensive operations
`mod` and `*` are removed.
---
 clash-protocols/clash-protocols.cabal         |   1 +
 .../src/Protocols/PacketStream/Base.hs        |  72 ++-
 .../src/Protocols/PacketStream/Converters.hs  |  53 ++-
 .../src/Protocols/PacketStream/Delay.hs       |   2 +-
 .../Protocols/PacketStream/Depacketizers.hs   |  41 +-
 .../src/Protocols/PacketStream/Hedgehog.hs    | 412 ++++++++++--------
 .../src/Protocols/PacketStream/PacketFifo.hs  |   2 +-
 .../src/Protocols/PacketStream/Packetizers.hs |  14 +-
 .../tests/Tests/Protocols/PacketStream.hs     |   2 +
 .../Tests/Protocols/PacketStream/AsyncFifo.hs |   3 +-
 .../Tests/Protocols/PacketStream/Base.hs      |  53 +++
 .../Protocols/PacketStream/Converters.hs      |  45 +-
 .../Tests/Protocols/PacketStream/Delay.hs     |   3 +-
 .../Protocols/PacketStream/Depacketizers.hs   |  21 +-
 .../Protocols/PacketStream/PacketFifo.hs      |  27 +-
 .../Protocols/PacketStream/Packetizers.hs     |  48 +-
 .../Tests/Protocols/PacketStream/Routing.hs   |   4 +-
 17 files changed, 514 insertions(+), 289 deletions(-)
 create mode 100644 clash-protocols/tests/Tests/Protocols/PacketStream/Base.hs

diff --git a/clash-protocols/clash-protocols.cabal b/clash-protocols/clash-protocols.cabal
index f264c0da..28aaa9fd 100644
--- a/clash-protocols/clash-protocols.cabal
+++ b/clash-protocols/clash-protocols.cabal
@@ -202,6 +202,7 @@ test-suite unittests
     Tests.Protocols.Wishbone
     Tests.Protocols.PacketStream
     Tests.Protocols.PacketStream.AsyncFifo
+    Tests.Protocols.PacketStream.Base
     Tests.Protocols.PacketStream.Converters
     Tests.Protocols.PacketStream.Delay
     Tests.Protocols.PacketStream.Depacketizers
diff --git a/clash-protocols/src/Protocols/PacketStream/Base.hs b/clash-protocols/src/Protocols/PacketStream/Base.hs
index 9797033c..702d882a 100644
--- a/clash-protocols/src/Protocols/PacketStream/Base.hs
+++ b/clash-protocols/src/Protocols/PacketStream/Base.hs
@@ -24,6 +24,7 @@ module Protocols.PacketStream.Base (
   fanout,
   forceResetSanity,
   zeroOutInvalidBytesC,
+  stripTrailingEmptyC,
   unsafeAbortOnBackpressureC,
 
   -- * Skid buffers
@@ -82,9 +83,11 @@ Heavily inspired by the M2S data of AMBA AXI4-Stream, but simplified:
 data PacketStreamM2S (dataWidth :: Nat) (meta :: Type) = PacketStreamM2S
   { _data :: Vec dataWidth (BitVector 8)
   -- ^ The bytes to be transmitted.
-  , _last :: Maybe (Index dataWidth)
-  -- ^ If this is @Just@ then it signals that this transfer
-  --   is the end of a packet and contains the index of the last valid byte in `_data`.
+  , _last :: Maybe (Index (dataWidth + 1))
+  -- ^ If this is @Just@ then it signals that this transfer is the end of a
+  --   packet and contains the number of valid bytes in '_data', starting from
+  --   index @0@.
+  --
   --   If it is @Nothing@ then this transfer is not yet the end of a packet and all
   --   bytes are valid. This implies that no null bytes are allowed in the middle of
   --   a packet, only after a packet.
@@ -94,7 +97,7 @@ 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 (Bundle, Eq, Functor, Generic, NFData, Show, ShowX)
+  deriving (Eq, Generic, ShowX, Show, NFData, Bundle, Functor)
 
 deriving instance
   (KnownNat dataWidth, NFDataX meta) =>
@@ -134,6 +137,11 @@ Invariants:
 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.
 -}
 data PacketStream (dom :: Domain) (dataWidth :: Nat) (meta :: Type)
 
@@ -278,6 +286,53 @@ forceResetSanity ::
   Circuit (PacketStream dom dataWidth meta) (PacketStream dom dataWidth meta)
 forceResetSanity = forceResetSanityGeneric
 
+{- |
+Strips trailing zero-byte transfers from packets in the stream. That is,
+if a packet consists of more than one transfer and '_last' of the last
+transfer in that packet is @Just 0@, the last transfer of that packet will
+be dropped and '_last' of the transfer before that will be set to @maxBound@.
+If such a trailing zero-byte transfer had '_abort' asserted, it will be
+preserved.
+
+Has one clock cycle latency, but runs at full throughput.
+-}
+stripTrailingEmptyC ::
+  forall (dataWidth :: Nat) (meta :: Type) (dom :: Domain).
+  (HiddenClockResetEnable dom) =>
+  (KnownNat dataWidth) =>
+  (NFDataX meta) =>
+  Circuit
+    (PacketStream dom dataWidth meta)
+    (PacketStream dom dataWidth meta)
+stripTrailingEmptyC = forceResetSanity |> fromSignals (mealyB go (False, False, Nothing))
+ where
+  go (notFirst, flush, cache) (Nothing, bwdIn) =
+    ((notFirst, flush', cache'), (PacketStreamS2M True, fwdOut))
+   where
+    fwdOut = if flush then cache else Nothing
+    (flush', cache')
+      | flush && _ready bwdIn = (False, Nothing)
+      | otherwise = (flush, cache)
+  go (notFirst, flush, cache) (Just transferIn, bwdIn) = (nextStOut, (bwdOut, fwdOut))
+   where
+    (notFirst', flush', cache', fwdOut) = case _last transferIn of
+      Nothing -> (True, False, Just transferIn, cache)
+      Just i ->
+        let trailing = i == 0 && notFirst
+         in ( False
+            , not trailing
+            , if trailing then Nothing else Just transferIn
+            , if trailing
+                then (\x -> x{_last = Just maxBound, _abort = _abort x || _abort transferIn}) <$> cache
+                else cache
+            )
+
+    bwdOut = PacketStreamS2M (Maybe.isNothing cache || _ready bwdIn)
+
+    nextStOut
+      | Maybe.isNothing cache || _ready bwdIn = (notFirst', flush', cache')
+      | otherwise = (notFirst, flush, cache)
+
 -- | Sets data bytes that are not enabled in a @PacketStream@ to @0x00@.
 zeroOutInvalidBytesC ::
   forall (dom :: Domain) (dataWidth :: Nat) (meta :: Type).
@@ -292,11 +347,10 @@ zeroOutInvalidBytesC = Circuit $ \(fwdIn, bwdIn) -> (bwdIn, fmap (go <$>) fwdIn)
    where
     dataOut = case _last transferIn of
       Nothing -> _data transferIn
-      Just i -> a ++ b
-       where
-        -- The first byte is always valid, so we only map over the rest.
-        (a, b') = splitAt d1 (_data transferIn)
-        b = imap (\(j :: Index (dataWidth - 1)) byte -> if resize j < i then byte else 0x00) b'
+      Just i ->
+        imap
+          (\(j :: Index dataWidth) byte -> if resize j < i then byte else 0x00)
+          (_data transferIn)
 
 {- |
 Copy data of a single `PacketStream` to multiple. LHS will only receive
diff --git a/clash-protocols/src/Protocols/PacketStream/Converters.hs b/clash-protocols/src/Protocols/PacketStream/Converters.hs
index 215baf71..ba4f17a1 100644
--- a/clash-protocols/src/Protocols/PacketStream/Converters.hs
+++ b/clash-protocols/src/Protocols/PacketStream/Converters.hs
@@ -13,12 +13,12 @@ module Protocols.PacketStream.Converters (
 
 import Clash.Prelude
 
-import Protocols (CSignal, Circuit (..), fromSignals, idC, (|>))
-import Protocols.PacketStream.Base
-
-import Data.Data ((:~:) (Refl))
 import Data.Maybe (isJust)
 import Data.Maybe.Extra
+import Data.Type.Equality ((:~:) (Refl))
+
+import Protocols (CSignal, Circuit (..), fromSignals, idC, (|>))
+import Protocols.PacketStream.Base
 
 -- | Upconverter state, consisting of at most p `BitVector 8`s and a vector indicating which bytes are valid
 data UpConverterState (dwOut :: Nat) (n :: Nat) (meta :: Type) = UpConverterState
@@ -26,17 +26,21 @@ data UpConverterState (dwOut :: Nat) (n :: Nat) (meta :: Type) = UpConverterStat
   -- ^ The buffer we are filling
   , _ucIdx :: Index n
   -- ^ Where in the buffer we need to write the next element
+  , _ucIdx2 :: Index (dwOut + 1)
+  -- ^ Used when @dwIn@ is not a power of two to determine the adjusted '_last',
+  --   to avoid multiplication (infers an expensive DSP slice).
+  --   If @dwIn@ is a power of two then we can multiply by shifting left.
   , _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 dwOut)
+  , _ucLastIdx :: Maybe (Index (dwOut + 1))
   -- ^ If true the current buffer contains the last byte of the current packet
   , _ucMeta :: meta
   }
-  deriving (Generic, NFDataX)
+  deriving (Generic, NFDataX, Show, ShowX)
 
 toPacketStream :: UpConverterState dwOut n meta -> Maybe (PacketStreamM2S dwOut meta)
 toPacketStream UpConverterState{..} = toMaybe _ucFlush (PacketStreamM2S _ucBuf _ucLastIdx _ucMeta _ucAborted)
@@ -89,14 +93,28 @@ nextState st@(UpConverterState{..}) (Just PacketStreamM2S{..}) (PacketStreamS2M
   nextFlush = isJust _last || bufFull
   nextIdx = if nextFlush then 0 else _ucIdx + 1
 
+  -- If @dwIn@ is not a power of two, we need to do some extra bookkeeping to
+  -- avoid multiplication. If not, _ucIdx2 stays at 0 and is never used, and
+  -- should therefore be optimized out by synthesis tools.
+  (nextIdx2, nextLastIdx) = case sameNat (SNat @(FLog 2 dwIn)) (SNat @(CLog 2 dwIn)) of
+    Just Refl ->
+      ( 0
+      , (\i -> shiftL (resize _ucIdx) (natToNum @(Log 2 dwIn)) + resize i) <$> _last
+      )
+    Nothing ->
+      ( if nextFlush then 0 else _ucIdx2 + natToNum @dwIn
+      , (\i -> _ucIdx2 + resize i) <$> _last
+      )
+
   nextStRaw =
     UpConverterState
       { _ucBuf = nextBuf
       , _ucIdx = nextIdx
+      , _ucIdx2 = nextIdx2
       , _ucFlush = nextFlush
       , _ucFreshBuf = nextFlush
       , _ucAborted = nextAbort
-      , _ucLastIdx = (\i -> resize _ucIdx * natToNum @dwIn + resize i) <$> _last
+      , _ucLastIdx = nextLastIdx
       , _ucMeta = _meta
       }
   nextSt = if outReady then nextStRaw else st
@@ -120,7 +138,17 @@ upConverter ::
   )
 upConverter = mealyB go s0
  where
-  s0 = UpConverterState (repeat undefined) 0 False True False Nothing undefined
+  s0 =
+    UpConverterState
+      { _ucBuf = deepErrorX "upConverterC: undefined initial buffer"
+      , _ucIdx = 0
+      , _ucIdx2 = 0
+      , _ucFlush = False
+      , _ucFreshBuf = True
+      , _ucAborted = False
+      , _ucLastIdx = Nothing
+      , _ucMeta = deepErrorX "upConverterC: undefined initial metadata"
+      }
   go st@(UpConverterState{..}) (fwdIn, bwdIn) =
     (nextState st fwdIn bwdIn, (PacketStreamS2M outReady, toPacketStream st))
    where
@@ -206,7 +234,7 @@ downConverterT st@DownConverterState{..} (Just inPkt, bwdIn) = (nextSt, (PacketS
   -- its corresponding _data. Else, we should use our stored buffer.
   (nextSize, buf) = case (_dcSize == 0, _last inPkt) of
     (True, Nothing) -> (maxBound - natToNum @dwOut, _data inPkt)
-    (True, Just i) -> (satSub SatBound (resize i + 1) (natToNum @dwOut), _data inPkt)
+    (True, Just i) -> (satSub SatBound i (natToNum @dwOut), _data inPkt)
     (False, _) -> (satSub SatBound _dcSize (natToNum @dwOut), _dcBuf)
 
   (newBuf, dataOut) = leToPlus @dwOut @dwIn shiftOutFrom0 (SNat @dwOut) buf
@@ -221,7 +249,10 @@ downConverterT st@DownConverterState{..} (Just inPkt, bwdIn) = (nextSt, (PacketS
 
   (outReady, outLast)
     | nextSize == 0 =
-        (_ready bwdIn, resize . (\i -> i `mod` natToNum @dwOut) <$> _last inPkt)
+        ( _ready bwdIn
+        , (\i -> resize $ if _dcSize == 0 then i else _dcSize)
+            <$> _last inPkt
+        )
     | otherwise = (False, Nothing)
 
   -- Keep the buffer in the state and rotate it once the byte is acknowledged to avoid
@@ -256,6 +287,6 @@ downConverterC = case sameNat (SNat @dwIn) (SNat @dwOut) of
    where
     s0 =
       DownConverterState
-        { _dcBuf = errorX "downConverterC: undefined initial value"
+        { _dcBuf = deepErrorX "downConverterC: undefined initial buffer"
         , _dcSize = 0
         }
diff --git a/clash-protocols/src/Protocols/PacketStream/Delay.hs b/clash-protocols/src/Protocols/PacketStream/Delay.hs
index db47d39e..9741af8b 100644
--- a/clash-protocols/src/Protocols/PacketStream/Delay.hs
+++ b/clash-protocols/src/Protocols/PacketStream/Delay.hs
@@ -18,7 +18,7 @@ import Data.Constraint.Deferrable ((:~:) (Refl))
 import Data.Maybe
 
 type M2SNoMeta dataWidth =
-  (Vec dataWidth (BitVector 8), Maybe (Index dataWidth), Bool)
+  (Vec dataWidth (BitVector 8), Maybe (Index (dataWidth + 1)), Bool)
 
 toPacketstreamM2S :: M2SNoMeta dataWidth -> meta -> PacketStreamM2S dataWidth meta
 toPacketstreamM2S (a, b, c) d = PacketStreamM2S a b d c
diff --git a/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs b/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs
index 5f4c4446..35ca2222 100644
--- a/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs
+++ b/clash-protocols/src/Protocols/PacketStream/Depacketizers.hs
@@ -121,7 +121,7 @@ depacketizerT _ Parse{..} (Just PacketStreamM2S{..}, _) = (nextStOut, (PacketStr
   nextParseBuf = fst (shiftInAtN _buf _data)
 
   prematureEnd idx = case sameNat d0 (SNat @(headerBytes `Mod` dataWidth)) of
-    Just Refl -> True
+    Just Refl -> idx /= maxBound
     _ -> idx < natToNum @(headerBytes `Mod` dataWidth)
 
   -- Upon seeing _last being set, move back to the initial state if the
@@ -150,8 +150,12 @@ depacketizerT toMetaOut st@Forward{..} (Just pkt@PacketStreamM2S{..}, bwdIn) = (
   (dataOut, nextFwdBytes) = splitAt (SNat @dataWidth) (fwdBytes ++ _data)
 
   -- Only use if headerBytes `Mod` dataWidth > 0.
-  adjustLast :: Index dataWidth -> Either (Index dataWidth) (Index dataWidth)
-  adjustLast idx = if idx < x then Left (idx + y) else Right (idx - x)
+  adjustLast ::
+    Index (dataWidth + 1) -> Either (Index (dataWidth + 1)) (Index (dataWidth + 1))
+  adjustLast idx
+    | _lastFwd = Right (idx - x)
+    | idx <= x = Left (idx + y)
+    | otherwise = Right (idx - x)
    where
     x = natToNum @(headerBytes `Mod` dataWidth)
     y = natToNum @(ForwardBytes headerBytes dataWidth)
@@ -159,7 +163,9 @@ depacketizerT toMetaOut st@Forward{..} (Just pkt@PacketStreamM2S{..}, bwdIn) = (
   outPkt = case sameNat d0 (SNat @(headerBytes `Mod` dataWidth)) of
     Just Refl ->
       pkt
-        { _meta = toMetaOut (bitCoerce header) _meta
+        { _data = if _lastFwd then repeat 0x00 else _data
+        , _last = if _lastFwd then Just 0 else _last
+        , _meta = toMetaOut (bitCoerce header) _meta
         , _abort = nextAborted
         }
     Nothing ->
@@ -289,8 +295,8 @@ depacketizeToDfT _ DfParse{..} (Just (PacketStreamM2S{..}), _) = (nextStOut, (Pa
 
   prematureEnd idx =
     case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of
-      SNatGT -> idx < (natToNum @(headerBytes `Mod` dataWidth - 1))
-      _ -> idx < (natToNum @(dataWidth - 1))
+      SNatGT -> idx < (natToNum @(headerBytes `Mod` dataWidth))
+      _ -> idx < (natToNum @dataWidth)
 
   (nextStOut, readyOut) =
     case (_dfCounter == 0, _last) of
@@ -361,7 +367,7 @@ depacketizeToDfC toOut = forceResetSanity |> fromSignals ckt
 data DropTailInfo dataWidth delay = DropTailInfo
   { _dtAborted :: Bool
   -- ^ Whether any fragment of the packet was aborted
-  , _newIdx :: Index dataWidth
+  , _newIdx :: Index (dataWidth + 1)
   -- ^ The adjusted byte enable
   , _drops :: Index (delay + 1)
   -- ^ The amount of transfers to drop from the tail
@@ -395,27 +401,28 @@ transmitDropInfoC SNat = forceResetSanity |> fromSignals (mealyB go False)
     toDropTailInfo i =
       DropTailInfo
         { _dtAborted = aborted || _abort
-        , _newIdx = satSub SatWrap i (natToNum @(n `Mod` dataWidth))
+        , _newIdx = newIdx
         , _drops = drops
         , _wait = wait
         }
      where
-      (drops, wait) = case ( compareSNat (SNat @dataWidth) (SNat @n)
-                           , sameNat d0 (SNat @(n `Mod` dataWidth))
-                           ) of
+      (newIdx, drops, wait) = case ( compareSNat (SNat @dataWidth) (SNat @n)
+                                   , sameNat d0 (SNat @(n `Mod` dataWidth))
+                                   ) of
         (SNatLE, Nothing) ->
-          let smaller = (resize i :: Index n) < natToNum @(n - dataWidth)
-           in ( if smaller
+          let smaller = (resize i :: Index n) <= natToNum @(n - dataWidth)
+           in ( satSub SatWrap i (natToNum @(n `Mod` dataWidth) + (if smaller then 1 else 0))
+              , if smaller
                   then natToNum @(n `DivRU` dataWidth)
                   else natToNum @(n `Div` dataWidth)
               , not smaller
               )
         (SNatLE, Just Refl) ->
-          (natToNum @(n `Div` dataWidth), False)
+          (i, natToNum @(n `Div` dataWidth), False)
         (SNatGT, _) ->
-          if i >= natToNum @n
-            then (0, True)
-            else (1, False)
+          if i > natToNum @n
+            then (i - natToNum @n, 0, True)
+            else (maxBound - (natToNum @n - i), 1, False)
 
 {- |
 Gets a delayed packet stream as input together with non-delayed
diff --git a/clash-protocols/src/Protocols/PacketStream/Hedgehog.hs b/clash-protocols/src/Protocols/PacketStream/Hedgehog.hs
index f69dfcaa..dbfa166b 100644
--- a/clash-protocols/src/Protocols/PacketStream/Hedgehog.hs
+++ b/clash-protocols/src/Protocols/PacketStream/Hedgehog.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE NoImplicitPrelude #-}
 
 {- |
 Copyright   : (C) 2024, QBayLogic B.V.
@@ -29,24 +30,25 @@ module Protocols.PacketStream.Hedgehog (
 
   -- * Hedgehog generators
   AbortMode (..),
+  PacketOptions (..),
+  defPacketOptions,
   genValidPacket,
   genPackets,
 ) where
 
-import Prelude
-
 import Clash.Hedgehog.Sized.Vector (genVec)
-import qualified Clash.Prelude as C
+import Clash.Prelude
 import qualified Clash.Sized.Vector as Vec
 
+import qualified Data.List as L
+import Data.Maybe (fromJust, isJust)
+
 import Hedgehog (Gen, Range)
 import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
 
 import Protocols.PacketStream.Base
 
-import qualified Data.List as L
-import Data.Maybe (fromJust, isJust)
-
 -- | Partition a list based on given function.
 chunkBy :: (a -> Bool) -> [a] -> [[a]]
 chunkBy _ [] = []
@@ -82,28 +84,27 @@ smearAbort (x : xs) = L.reverse $ L.foldl' go [x] xs
 -- | 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
+chopBy n xs = as : chopBy n bs where (as, bs) = L.splitAt n xs
 
 {- |
 Merge a list of `PacketStream` transfers with data width @1@ to
 a single `PacketStream` transfer with data width @dataWidth@.
 -}
 chunkToPacket ::
-  (C.KnownNat dataWidth) =>
+  (KnownNat dataWidth) =>
   [PacketStreamM2S 1 meta] ->
   PacketStreamM2S dataWidth meta
-chunkToPacket l =
+chunkToPacket xs =
   PacketStreamM2S
     { _last =
-        if isJust (_last lastTransfer)
-          then Just (fromIntegral $ L.length l - 1)
-          else Nothing
-    , _abort = any _abort l
+        (\i -> let l = fromIntegral (L.length xs) in if i == 0 then l - 1 else l)
+          <$> _last lastTransfer
+    , _abort = any _abort xs
     , _meta = _meta lastTransfer
-    , _data = foldr ((C.+>>) . C.head . _data) (C.repeat 0) l
+    , _data = L.foldr ((+>>) . head . _data) (repeat 0x00) xs
     }
  where
-  lastTransfer = L.last l
+  lastTransfer = L.last xs
 
 {- |
 Split a single `PacketStream` transfer with data width @dataWidth@ to
@@ -111,41 +112,44 @@ a list of `PacketStream` transfers with data width @1@.
 -}
 chopPacket ::
   forall dataWidth meta.
-  (1 C.<= dataWidth) =>
-  (C.KnownNat dataWidth) =>
+  (1 <= dataWidth) =>
+  (KnownNat dataWidth) =>
   PacketStreamM2S dataWidth 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)]
+    Nothing -> L.repeat Nothing
+    Just size ->
+      if size == 0
+        then [Just 0]
+        else L.replicate (fromIntegral size - 1) Nothing L.++ [Just (1 :: Index 2)]
 
   datas = case _last of
-    Nothing -> C.toList _data
-    Just in' -> take (fromIntegral in' + 1) $ C.toList _data
+    Nothing -> toList _data
+    Just size -> L.take (max 1 (fromIntegral size)) $ toList _data
 
   packets =
-    ( \(idx, dat) ->
-        PacketStreamM2S (pure dat) idx _meta _abort
+    ( \(size, dat) ->
+        PacketStreamM2S (pure dat) size _meta _abort
     )
-      <$> zip lasts datas
+      <$> L.zip lasts datas
 
--- | Set `_last` of the last transfer in the list to @Just 0@
+-- | Set `_last` of the last transfer in the list to @Just 1@
 fullPackets ::
-  (C.KnownNat dataWidth) =>
+  (KnownNat dataWidth) =>
   [PacketStreamM2S dataWidth meta] ->
   [PacketStreamM2S dataWidth meta]
 fullPackets [] = []
 fullPackets fragments =
-  let lastFragment = (last fragments){_last = Just 0}
-   in init fragments ++ [lastFragment]
+  let lastFragment = (L.last fragments){_last = Just 1}
+   in L.init fragments L.++ [lastFragment]
 
 -- | Drops packets if one of the transfers in the packet has `_abort` set.
 dropAbortedPackets ::
   [PacketStreamM2S dataWidth meta] ->
   [PacketStreamM2S dataWidth meta]
-dropAbortedPackets packets = concat $ filter (not . any _abort) (chunkByPacket packets)
+dropAbortedPackets packets = L.concat $ L.filter (not . any _abort) (chunkByPacket packets)
 
 {- |
 Splits a list of `PacketStream` transfers with data width @1@ into
@@ -153,11 +157,11 @@ a list of `PacketStream` transfers with data width @dataWidth@
 -}
 downConvert ::
   forall dataWidth meta.
-  (1 C.<= dataWidth) =>
-  (C.KnownNat dataWidth) =>
+  (1 <= dataWidth) =>
+  (KnownNat dataWidth) =>
   [PacketStreamM2S dataWidth meta] ->
   [PacketStreamM2S 1 meta]
-downConvert = concatMap chopPacket
+downConvert = L.concatMap chopPacket
 
 {- |
 Merges a list of `PacketStream` transfers with data width @dataWidth@ into
@@ -165,51 +169,69 @@ a list of `PacketStream` transfers with data width @1@
 -}
 upConvert ::
   forall dataWidth meta.
-  (1 C.<= dataWidth) =>
-  (C.KnownNat dataWidth) =>
+  (1 <= dataWidth) =>
+  (KnownNat dataWidth) =>
   [PacketStreamM2S 1 meta] ->
   [PacketStreamM2S dataWidth meta]
 upConvert packets =
-  map
+  L.map
     chunkToPacket
-    (chunkByPacket packets >>= chopBy (C.natToNum @dataWidth))
+    (chunkByPacket packets >>= chopBy (natToNum @dataWidth))
 
 -- | Model of the generic `Protocols.PacketStream.depacketizerC`.
 depacketizerModel ::
   forall
-    (dataWidth :: C.Nat)
-    (headerBytes :: C.Nat)
-    (metaIn :: C.Type)
-    (header :: C.Type)
-    (metaOut :: C.Type).
-  (C.KnownNat dataWidth) =>
-  (C.KnownNat headerBytes) =>
-  (1 C.<= dataWidth) =>
-  (1 C.<= headerBytes) =>
-  (C.BitPack header) =>
-  (C.BitSize header ~ headerBytes C.* 8) =>
+    (dataWidth :: Nat)
+    (headerBytes :: Nat)
+    (metaIn :: Type)
+    (header :: Type)
+    (metaOut :: 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 = C.natToNum @headerBytes
+  hdrbytes = natToNum @headerBytes
 
   parseHdr ::
     ([PacketStreamM2S 1 metaIn], [PacketStreamM2S 1 metaIn]) ->
     [PacketStreamM2S 1 metaOut]
-  parseHdr (hdrF, fwdF) = fmap (\f -> f{_meta = metaOut}) fwdF
+  parseHdr (hdrF, fwdF) = fmap (\f -> f{_meta = metaOut}) fwdF'
    where
-    hdr = C.bitCoerce $ Vec.unsafeFromList @headerBytes $ _data <$> hdrF
-    metaOut = toMetaOut hdr (_meta $ L.head fwdF)
+    fwdF' = case fwdF of
+      [] ->
+        [ PacketStreamM2S
+            (Vec.singleton 0x00)
+            (Just 0)
+            (error "depacketizerModel: should be replaced")
+            (_abort (L.last hdrF))
+        ]
+      _ -> fwdF
+
+    hdr = bitCoerce $ Vec.unsafeFromList @headerBytes $ _data <$> hdrF
+    metaOut = toMetaOut hdr (_meta $ L.head hdrF)
 
   bytePackets :: [[PacketStreamM2S 1 metaIn]]
   bytePackets =
-    L.filter (\fs -> L.length fs > hdrbytes) $
-      L.concatMap chopPacket . smearAbort <$> chunkByPacket ps
+    L.filter
+      ( \fs ->
+          let len' = L.length fs
+           in len' > hdrbytes || len' == hdrbytes && _last (L.last fs) == Just 1
+      )
+      $ downConvert
+      . smearAbort
+      <$> chunkByPacket ps
 
   parsedPackets :: [[PacketStreamM2S 1 metaOut]]
-  parsedPackets = parseHdr . L.splitAt hdrbytes <$> bytePackets
+  parsedPackets = L.map go bytePackets
+
+  go = parseHdr . L.splitAt hdrbytes
 
   dataWidthPackets :: [[PacketStreamM2S dataWidth metaOut]]
   dataWidthPackets = L.map upConvert parsedPackets
@@ -217,17 +239,17 @@ depacketizerModel toMetaOut ps = L.concat dataWidthPackets
 -- | Model of the generic `Protocols.PacketStream.depacketizeToDfC`.
 depacketizeToDfModel ::
   forall
-    (dataWidth :: C.Nat)
-    (headerBytes :: C.Nat)
-    (a :: C.Type)
-    (header :: C.Type)
-    (metaIn :: C.Type).
-  (C.KnownNat dataWidth) =>
-  (C.KnownNat headerBytes) =>
-  (1 C.<= dataWidth) =>
-  (1 C.<= headerBytes) =>
-  (C.BitPack header) =>
-  (C.BitSize header ~ headerBytes C.* 8) =>
+    (dataWidth :: Nat)
+    (headerBytes :: Nat)
+    (a :: Type)
+    (header :: Type)
+    (metaIn :: Type).
+  (KnownNat dataWidth) =>
+  (KnownNat headerBytes) =>
+  (1 <= dataWidth) =>
+  (1 <= headerBytes) =>
+  (BitPack header) =>
+  (BitSize header ~ headerBytes * 8) =>
   (header -> metaIn -> a) ->
   [PacketStreamM2S dataWidth metaIn] ->
   [a]
@@ -236,49 +258,53 @@ depacketizeToDfModel toOut ps = L.map parseHdr bytePackets
   parseHdr :: [PacketStreamM2S 1 metaIn] -> a
   parseHdr hdrF =
     toOut
-      (C.bitCoerce $ Vec.unsafeFromList $ _data <$> hdrF)
+      (bitCoerce $ Vec.unsafeFromList $ _data <$> hdrF)
       (_meta $ L.head hdrF)
 
   bytePackets :: [[PacketStreamM2S 1 metaIn]]
   bytePackets =
     L.filter
-      (\pkt -> L.length pkt >= C.natToNum @headerBytes)
+      ( \pkt ->
+          (L.length pkt > natToNum @headerBytes)
+            || (L.length pkt == natToNum @headerBytes && _last (L.last pkt) == Just 1)
+      )
       (chunkByPacket $ downConvert (dropAbortedPackets ps))
 
 -- | Model of 'Protocols.PacketStream.dropTailC'.
 dropTailModel ::
   forall dataWidth meta n.
-  (C.KnownNat dataWidth) =>
-  (1 C.<= dataWidth) =>
-  (1 C.<= n) =>
-  C.SNat n ->
+  (KnownNat dataWidth) =>
+  (1 <= dataWidth) =>
+  (1 <= n) =>
+  SNat n ->
   [PacketStreamM2S dataWidth meta] ->
   [PacketStreamM2S dataWidth meta]
-dropTailModel C.SNat packets = L.concatMap go (chunkByPacket packets)
+dropTailModel SNat packets = L.concatMap go (chunkByPacket packets)
  where
   go :: [PacketStreamM2S dataWidth meta] -> [PacketStreamM2S dataWidth meta]
   go packet =
-    upConvert $
-      L.init trimmed L.++ [(L.last trimmed){_last = Just 0, _abort = aborted}]
+    upConvert
+      $ L.init trimmed
+      L.++ [setNull (L.last trimmed){_last = _last $ L.last bytePkts, _abort = aborted}]
    where
     aborted = L.any _abort packet
     bytePkts = downConvert packet
-    trimmed = L.take (L.length bytePkts - C.natToNum @n) bytePkts
+    trimmed = L.take (L.length bytePkts - natToNum @n) bytePkts
 
 -- | Model of the generic `Protocols.PacketStream.packetizerC`.
 packetizerModel ::
   forall
-    (dataWidth :: C.Nat)
-    (headerBytes :: C.Nat)
-    (metaIn :: C.Type)
-    (header :: C.Type)
-    (metaOut :: C.Type).
-  (C.KnownNat dataWidth) =>
-  (C.KnownNat headerBytes) =>
-  (1 C.<= dataWidth) =>
-  (1 C.<= headerBytes) =>
-  (C.BitPack header) =>
-  (C.BitSize header ~ headerBytes C.* 8) =>
+    (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] ->
@@ -290,8 +316,8 @@ packetizerModel toMetaOut toHeader ps = L.concatMap (upConvert . prependHdr) byt
    where
     h = L.head fragments
     metaOut = toMetaOut (_meta h)
-    hdr = L.map go (C.toList $ C.bitCoerce (toHeader (_meta h)))
-    go byte = PacketStreamM2S (C.singleton byte) Nothing metaOut (_abort 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
@@ -299,17 +325,17 @@ packetizerModel toMetaOut toHeader ps = L.concatMap (upConvert . prependHdr) byt
 -- | Model of the generic `Protocols.PacketStream.packetizeFromDfC`.
 packetizeFromDfModel ::
   forall
-    (dataWidth :: C.Nat)
-    (headerBytes :: C.Nat)
-    (a :: C.Type)
-    (header :: C.Type)
-    (metaOut :: C.Type).
-  (C.KnownNat dataWidth) =>
-  (C.KnownNat headerBytes) =>
-  (1 C.<= dataWidth) =>
-  (1 C.<= headerBytes) =>
-  (C.BitPack header) =>
-  (C.BitSize header ~ headerBytes C.* 8) =>
+    (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] ->
@@ -318,126 +344,166 @@ packetizeFromDfModel toMetaOut toHeader = L.concatMap (upConvert . dfToPacket)
  where
   dfToPacket :: a -> [PacketStreamM2S 1 metaOut]
   dfToPacket d =
-    fullPackets $
-      L.map
-        (\byte -> PacketStreamM2S (C.singleton byte) Nothing (toMetaOut d) False)
-        (C.toList $ C.bitCoerce (toHeader d))
+    fullPackets
+      $ L.map
+        (\byte -> PacketStreamM2S (singleton byte) Nothing (toMetaOut d) False)
+        (toList $ bitCoerce (toHeader d))
+
+-- | Abort generation options for packet generation.
+data AbortMode
+  = Abort
+      { amPacketGen :: Gen Bool
+      -- ^ Determines the chance to generate aborted fragments in a packet.
+      , amTransferGen :: Gen Bool
+      -- ^ Determines the frequency of aborted fragments in a packet.
+      }
+  | NoAbort
+
+-- | Various configuration options for packet generation.
+data PacketOptions = PacketOptions
+  { poAllowEmptyPackets :: Bool
+  -- ^ Whether to allow the generation of zero-byte packets.
+  , poAllowTrailingEmpty :: Bool
+  -- ^ Whether to allow the generation of trailing zero-byte transfers.
+  , poAbortMode :: AbortMode
+  -- ^ If set to @NoAbort@, no transfers in the packet will have '_abort' set.
+  -- Else, randomly generate them according to some distribution. See 'AbortMode'.
+  }
 
 {- |
-If set to @NoAbort@, packets will never contain a transfer with _abort set.
-Otherwise, transfers of roughly 50% of the packets will randomly have _abort set.
+Default packet generation options:
+
+- Allow the generation of a zero-byte packet;
+- Allow the generation of a trailing zero-byte transfer;
+- 50% chance to generate aborted transfers. If aborts are generated, 10% of
+  transfers will be aborted.
 -}
-data AbortMode = Abort | NoAbort
+defPacketOptions :: PacketOptions
+defPacketOptions =
+  PacketOptions
+    { poAllowEmptyPackets = True
+    , poAllowTrailingEmpty = True
+    , poAbortMode =
+        Abort
+          { amPacketGen = Gen.enumBounded
+          , amTransferGen =
+              Gen.frequency
+                [ (90, Gen.constant False)
+                , (10, Gen.constant True)
+                ]
+          }
+    }
 
 {- |
-Generate packets with a user-supplied generator.
+Generate packets with a user-supplied generator and a linear range.
 -}
 genPackets ::
-  forall (dataWidth :: C.Nat) (meta :: C.Type).
-  (1 C.<= dataWidth) =>
-  (C.KnownNat dataWidth) =>
-  -- | The amount of packets to generate.
-  Range Int ->
-  -- | If set to @NoAbort@, always pass @NoAbort@ to the packet generator.
-  --   Else, pass @Abort@ to roughly 50% of the packet generators.
-  AbortMode ->
+  forall (dataWidth :: Nat) (meta :: Type).
+  (1 <= dataWidth) =>
+  (KnownNat dataWidth) =>
+  -- | Minimum amount of packets to generate.
+  Int ->
+  -- | Maximum amount of packets to generate.
+  Int ->
   -- | Packet generator.
-  (AbortMode -> Gen [PacketStreamM2S dataWidth meta]) ->
+  Gen [PacketStreamM2S dataWidth meta] ->
   Gen [PacketStreamM2S dataWidth meta]
-genPackets pkts Abort pktGen =
-  concat
-    <$> Gen.list
-      pkts
-      (Gen.choice [pktGen Abort, pktGen NoAbort])
-genPackets pkts NoAbort pktGen =
-  concat
-    <$> Gen.list
-      pkts
-      (pktGen NoAbort)
+genPackets minB maxB pktGen = L.concat <$> Gen.list (Range.linear minB maxB) pktGen
+{-# INLINE genPackets #-}
 
 {- |
 Generate a valid packet, i.e. a packet of which all transfers carry the same
 `_meta` and with all unenabled bytes in `_data` set to 0x00.
 -}
 genValidPacket ::
-  forall (dataWidth :: C.Nat) (meta :: C.Type).
-  (1 C.<= dataWidth) =>
-  (C.KnownNat dataWidth) =>
+  forall (dataWidth :: Nat) (meta :: Type).
+  (1 <= dataWidth) =>
+  (KnownNat dataWidth) =>
+  -- | Configuration options for packet generation.
+  PacketOptions ->
   -- | Generator for the metadata.
   Gen meta ->
   -- | The amount of transfers with @_last = Nothing@ to generate.
   --   This function will always generate an extra transfer with @_last = Just i@.
   Range Int ->
-  -- | If set to @NoAbort@, no transfers in the packet will have @_abort@ set.
-  --   Else, each transfer has a 10% chance to have @_abort@ set.
-  AbortMode ->
   Gen [PacketStreamM2S dataWidth meta]
-genValidPacket metaGen size abortMode = do
-  meta <- metaGen
-  transfers <- Gen.list size (genTransfer @dataWidth meta abortMode)
-  lastTransfer <- genLastTransfer @dataWidth meta abortMode
-  pure (transfers ++ [lastTransfer])
+genValidPacket PacketOptions{..} metaGen size =
+  let
+    abortGen = case poAbortMode of
+      NoAbort -> Gen.constant False
+      Abort pktGen transferGen -> do
+        allowAborts <- pktGen
+        (if allowAborts then transferGen else Gen.constant False)
+   in
+    do
+      meta <- metaGen
+      transfers <- Gen.list size (genTransfer meta abortGen)
+      lastTransfer <-
+        genLastTransfer
+          meta
+          ( (null transfers && poAllowEmptyPackets)
+              || (not (null transfers) && poAllowTrailingEmpty)
+          )
+          abortGen
+      pure (transfers L.++ [lastTransfer])
 
 -- | Generate a single transfer which is not yet the end of a packet.
 genTransfer ::
-  forall (dataWidth :: C.Nat) (meta :: C.Type).
-  (1 C.<= dataWidth) =>
-  (C.KnownNat dataWidth) =>
+  forall (dataWidth :: Nat) (meta :: Type).
+  (1 <= dataWidth) =>
+  (KnownNat dataWidth) =>
   -- | We need to use the same metadata
   --   for every transfer in a packet to satisfy the protocol
   --   invariant that metadata is constant for an entire packet.
   meta ->
-  -- | If set to @NoAbort@, hardcode @_abort@ to @False@. Else,
-  --   there is a 10% chance for it to be set.
-  AbortMode ->
+  -- | Whether to set '_abort'.
+  Gen Bool ->
   Gen (PacketStreamM2S dataWidth meta)
-genTransfer meta abortMode =
+genTransfer meta abortGen =
   PacketStreamM2S
     <$> genVec Gen.enumBounded
     <*> Gen.constant Nothing
     <*> Gen.constant meta
-    <*> case abortMode of
-      Abort ->
-        Gen.frequency
-          [ (90, Gen.constant False)
-          , (10, Gen.constant True)
-          ]
-      NoAbort -> Gen.constant False
+    <*> 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.
 -}
 genLastTransfer ::
-  forall (dataWidth :: C.Nat) (meta :: C.Type).
-  (1 C.<= dataWidth) =>
-  (C.KnownNat dataWidth) =>
+  forall (dataWidth :: Nat) (meta :: Type).
+  (1 <= dataWidth) =>
+  (KnownNat dataWidth) =>
   -- | We need to use the same metadata
   --   for every transfer in a packet to satisfy the protocol
   --   invariant that metadata is constant for an entire packet.
   meta ->
-  -- | If set to @NoAbort@, hardcode @_abort@ to @False@. Else,
-  --   randomly generate it.
-  AbortMode ->
+  -- | Whether we are allowed to generate a 0-byte transfer.
+  Bool ->
+  -- | Whether to set '_abort'.
+  Gen Bool ->
   Gen (PacketStreamM2S dataWidth meta)
-genLastTransfer meta abortMode =
+genLastTransfer meta allowEmpty abortGen =
   setNull
     <$> ( PacketStreamM2S
             <$> genVec Gen.enumBounded
-            <*> (Just <$> Gen.enumBounded)
+            <*> (Just <$> Gen.enum (if allowEmpty then 0 else 1) maxBound)
             <*> Gen.constant meta
-            <*> case abortMode of
-              Abort -> Gen.enumBounded
-              NoAbort -> Gen.constant False
+            <*> abortGen
         )
- where
-  setNull transfer =
-    let i = fromJust (_last transfer)
-     in transfer
-          { _data =
-              fromJust
-                ( Vec.fromList $
-                    take (1 + fromIntegral i) (C.toList (_data transfer))
-                      ++ replicate ((C.natToNum @dataWidth) - 1 - fromIntegral i) 0x00
-                )
-          }
+
+setNull ::
+  forall (dataWidth :: Nat) (meta :: Type).
+  (KnownNat dataWidth) =>
+  PacketStreamM2S dataWidth meta ->
+  PacketStreamM2S dataWidth meta
+setNull transfer =
+  let i = fromJust (_last transfer)
+   in transfer
+        { _data =
+            fromJust
+              ( Vec.fromList
+                  $ L.take (fromIntegral i) (toList (_data transfer))
+                  L.++ L.replicate ((natToNum @dataWidth) - fromIntegral i) 0x00
+              )
+        }
diff --git a/clash-protocols/src/Protocols/PacketStream/PacketFifo.hs b/clash-protocols/src/Protocols/PacketStream/PacketFifo.hs
index 3b361074..78a55426 100644
--- a/clash-protocols/src/Protocols/PacketStream/PacketFifo.hs
+++ b/clash-protocols/src/Protocols/PacketStream/PacketFifo.hs
@@ -19,7 +19,7 @@ import Data.Maybe
 import Data.Maybe.Extra
 
 type PacketStreamContent (dataWidth :: Nat) (meta :: Type) =
-  (Vec dataWidth (BitVector 8), Maybe (Index dataWidth))
+  (Vec dataWidth (BitVector 8), Maybe (Index (dataWidth + 1)))
 
 toPacketStreamContent ::
   PacketStreamM2S dataWidth meta -> PacketStreamContent dataWidth meta
diff --git a/clash-protocols/src/Protocols/PacketStream/Packetizers.hs b/clash-protocols/src/Protocols/PacketStream/Packetizers.hs
index 716f7e25..84d0e2f0 100644
--- a/clash-protocols/src/Protocols/PacketStream/Packetizers.hs
+++ b/clash-protocols/src/Protocols/PacketStream/Packetizers.hs
@@ -87,7 +87,7 @@ packetizerT1 toMetaOut toHeader st (Just inPkt, bwdIn) =
       (nextSt, newLast) = case _last inPkt of
         Nothing -> (Forward1 nextAborted newBuf, Nothing)
         Just i
-          | i < natToNum @(dataWidth - headerBytes) ->
+          | i <= natToNum @(dataWidth - headerBytes) ->
               (Insert1 False, Just (i + natToNum @headerBytes))
           | otherwise -> (LastForward1 nextAborted newBuf, Nothing)
 
@@ -237,7 +237,7 @@ packetizerT3 toMetaOut _ st@Insert3{..} (Just inPkt, bwdIn) =
     (False, _) -> (Nothing, Insert3 nextAborted newHdrBuf (succ _counter3))
     (True, Nothing) -> (Nothing, Forward3 nextAborted newHdrBuf)
     (True, Just i) ->
-      if i < natToNum @(dataWidth - headerBytes `Mod` dataWidth)
+      if i <= natToNum @(dataWidth - headerBytes `Mod` dataWidth)
         then (Just (i + natToNum @(headerBytes `Mod` dataWidth)), LoadHeader3)
         else (Nothing, LastForward3 nextAborted newHdrBuf)
   nextStOut = if _ready bwdIn then nextSt else st
@@ -266,7 +266,7 @@ packetizerT3 toMetaOut _ st@Forward3{..} (Just inPkt, bwdIn) =
   (lastOut, nextSt) = case _last inPkt of
     Nothing -> (Nothing, Forward3 nextAborted newBuf)
     Just i ->
-      if i < natToNum @(dataWidth - headerBytes `Mod` dataWidth)
+      if i <= natToNum @(dataWidth - headerBytes `Mod` dataWidth)
         then (Just (i + natToNum @(headerBytes `Mod` dataWidth)), LoadHeader3)
         else (Nothing, LastForward3 nextAborted newBuf)
   nextStOut = if _ready bwdIn then nextSt else st
@@ -375,8 +375,8 @@ packetizeFromDfT toMetaOut _ st@DfInsert{..} (Df.Data dataIn, bwdIn) = (nextStOu
   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)
+    SNatGT -> natToNum @(headerBytes `Mod` dataWidth)
+    _ -> natToNum @dataWidth
 
   bwdOut = Ack (_ready bwdIn && _dfCounter == maxBound)
   nextSt = if _dfCounter == maxBound then DfIdle else DfInsert (succ _dfCounter) newHdrBuf
@@ -421,6 +421,6 @@ packetizeFromDfC toMetaOut toHeader = case strictlyPositiveDivRu @headerBytes @d
         outPkt = PacketStreamM2S dataOut (Just l) (toMetaOut dataIn) False
         dataOut = bitCoerce (toHeader dataIn) ++ repeat @(dataWidth - headerBytes) defaultByte
         l = case compareSNat (SNat @(headerBytes `Mod` dataWidth)) d0 of
-          SNatGT -> natToNum @(headerBytes `Mod` dataWidth - 1)
-          _ -> natToNum @(dataWidth - 1)
+          SNatGT -> natToNum @(headerBytes `Mod` dataWidth)
+          _ -> natToNum @dataWidth
     SNatGT -> fromSignals (mealyB (packetizeFromDfT toMetaOut toHeader) DfIdle)
diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream.hs b/clash-protocols/tests/Tests/Protocols/PacketStream.hs
index 7e7ffcb1..f83077f5 100644
--- a/clash-protocols/tests/Tests/Protocols/PacketStream.hs
+++ b/clash-protocols/tests/Tests/Protocols/PacketStream.hs
@@ -3,6 +3,7 @@ module Tests.Protocols.PacketStream (tests) where
 import Test.Tasty
 
 import qualified Tests.Protocols.PacketStream.AsyncFifo
+import qualified Tests.Protocols.PacketStream.Base
 import qualified Tests.Protocols.PacketStream.Converters
 import qualified Tests.Protocols.PacketStream.Delay
 import qualified Tests.Protocols.PacketStream.Depacketizers
@@ -15,6 +16,7 @@ tests =
   testGroup
     "PacketStream"
     [ Tests.Protocols.PacketStream.AsyncFifo.tests
+    , Tests.Protocols.PacketStream.Base.tests
     , Tests.Protocols.PacketStream.Converters.tests
     , Tests.Protocols.PacketStream.Delay.tests
     , Tests.Protocols.PacketStream.Depacketizers.tests
diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/AsyncFifo.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/AsyncFifo.hs
index 393152d8..4da9e9b3 100644
--- a/clash-protocols/tests/Tests/Protocols/PacketStream/AsyncFifo.hs
+++ b/clash-protocols/tests/Tests/Protocols/PacketStream/AsyncFifo.hs
@@ -71,8 +71,7 @@ generateAsyncFifoIdProp ::
 generateAsyncFifoIdProp wClk wRst wEn rClk rRst rEn =
   idWithModel
     defExpectOptions
-    ( genPackets (Range.linear 1 10) Abort (genValidPacket Gen.enumBounded (Range.linear 1 30))
-    )
+    (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 30)))
     id
     (asyncFifoC @wDom @rDom @4 @1 @Int d4 wClk wRst wEn rClk rRst rEn)
 
diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Base.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Base.hs
new file mode 100644
index 00000000..2ef0e311
--- /dev/null
+++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Base.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE NumericUnderscores #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Tests.Protocols.PacketStream.Base (
+  tests,
+) where
+
+import Clash.Prelude
+
+import qualified Data.List as L
+import Data.List.Extra (unsnoc)
+
+import Hedgehog (Property)
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+
+import Test.Tasty (TestTree, localOption, mkTimeout)
+import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit))
+import Test.Tasty.Hedgehog.Extra (testProperty)
+import Test.Tasty.TH (testGroupGenerator)
+
+import Protocols.Hedgehog
+import Protocols.PacketStream.Base
+import Protocols.PacketStream.Hedgehog
+
+prop_strip_trailing_empty :: Property
+prop_strip_trailing_empty =
+  idWithModelSingleDomain
+    @System
+    defExpectOptions
+    (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 10)))
+    (exposeClockResetEnable model')
+    (exposeClockResetEnable (stripTrailingEmptyC @1 @Char))
+ where
+  model' packets = L.concatMap model (chunkByPacket packets)
+
+  model :: [PacketStreamM2S 1 Char] -> [PacketStreamM2S 1 Char]
+  model packet = case unsnoc packet of
+    Nothing -> []
+    Just (xs, l) -> case unsnoc xs of
+      -- Preserve packets that consist of a single zero-byte transfer.
+      Nothing -> [l]
+      Just (ys, l2) ->
+        if _last l == Just 0
+          then ys L.++ [l2{_last = Just maxBound, _abort = _abort l2 || _abort l}]
+          else packet
+
+tests :: TestTree
+tests =
+  localOption (mkTimeout 20_000_000 {- 20 seconds -})
+    $ localOption
+      (HedgehogTestLimit (Just 500))
+      $(testGroupGenerator)
diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Converters.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Converters.hs
index ac48662f..deda660e 100644
--- a/clash-protocols/tests/Tests/Protocols/PacketStream/Converters.hs
+++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Converters.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE NumericUnderscores #-}
 
-module Tests.Protocols.PacketStream.Converters where
+module Tests.Protocols.PacketStream.Converters (
+  tests,
+) where
 
 import Clash.Prelude
 
@@ -30,11 +32,30 @@ generateUpConverterProperty ::
 generateUpConverterProperty SNat SNat =
   idWithModelSingleDomain
     defExpectOptions
-    ( genPackets (Range.linear 1 10) Abort (genValidPacket Gen.enumBounded (Range.linear 1 20))
-    )
+    (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 20)))
     (exposeClockResetEnable (upConvert . downConvert))
     (exposeClockResetEnable @System (upConverterC @dwIn @dwOut @Int))
 
+generateDownConverterProperty ::
+  forall (dwIn :: Nat) (dwOut :: Nat) (n :: Nat).
+  (1 <= dwIn) =>
+  (1 <= dwOut) =>
+  (1 <= n) =>
+  (KnownNat n) =>
+  (dwIn ~ n * dwOut) =>
+  SNat dwIn ->
+  SNat dwOut ->
+  Property
+generateDownConverterProperty SNat SNat =
+  idWithModelSingleDomain
+    defExpectOptions{eoSampleMax = 1000}
+    (genPackets 1 8 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 10)))
+    (exposeClockResetEnable (upConvert . downConvert))
+    (exposeClockResetEnable @System (downConverterC @dwIn @dwOut @Int))
+
+prop_upConverter3to9 :: Property
+prop_upConverter3to9 = generateUpConverterProperty d3 d9
+
 prop_upConverter4to8 :: Property
 prop_upConverter4to8 = generateUpConverterProperty d4 d8
 
@@ -53,22 +74,8 @@ prop_upConverter1to2 = generateUpConverterProperty d1 d2
 prop_upConverter1to1 :: Property
 prop_upConverter1to1 = generateUpConverterProperty d1 d1
 
-generateDownConverterProperty ::
-  forall (dwIn :: Nat) (dwOut :: Nat) (n :: Nat).
-  (1 <= dwIn) =>
-  (1 <= dwOut) =>
-  (1 <= n) =>
-  (KnownNat n) =>
-  (dwIn ~ n * dwOut) =>
-  SNat dwIn ->
-  SNat dwOut ->
-  Property
-generateDownConverterProperty SNat SNat =
-  idWithModelSingleDomain
-    defExpectOptions{eoSampleMax = 1000}
-    (genPackets (Range.linear 1 8) Abort (genValidPacket Gen.enumBounded (Range.linear 1 10)))
-    (exposeClockResetEnable (upConvert . downConvert))
-    (exposeClockResetEnable @System (downConverterC @dwIn @dwOut @Int))
+prop_downConverter9to3 :: Property
+prop_downConverter9to3 = generateDownConverterProperty d9 d3
 
 prop_downConverter8to4 :: Property
 prop_downConverter8to4 = generateDownConverterProperty d8 d4
diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Delay.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Delay.hs
index eff1181e..4f1f8a60 100644
--- a/clash-protocols/tests/Tests/Protocols/PacketStream/Delay.hs
+++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Delay.hs
@@ -24,8 +24,7 @@ prop_delaystream_id =
   idWithModelSingleDomain
     @System
     defExpectOptions
-    ( genPackets (Range.linear 1 10) Abort (genValidPacket Gen.enumBounded (Range.linear 4 20))
-    )
+    (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 4 20)))
     (exposeClockResetEnable id)
     (exposeClockResetEnable (delayStreamC @2 @Int d4))
 
diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Depacketizers.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Depacketizers.hs
index 59d58ab8..f76595b5 100644
--- a/clash-protocols/tests/Tests/Protocols/PacketStream/Depacketizers.hs
+++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Depacketizers.hs
@@ -39,7 +39,7 @@ depacketizerPropertyGenerator SNat SNat =
   idWithModelSingleDomain
     @System
     defExpectOptions{eoSampleMax = 1000, eoStopAfterEmpty = 1000}
-    (genPackets (Range.linear 1 4) Abort (genValidPacket (pure ()) (Range.linear 1 30)))
+    (genPackets 1 4 (genValidPacket defPacketOptions (pure ()) (Range.linear 0 30)))
     (exposeClockResetEnable (depacketizerModel const))
     (exposeClockResetEnable ckt)
  where
@@ -67,7 +67,7 @@ depacketizeToDfPropertyGenerator SNat SNat =
   idWithModelSingleDomain
     @System
     defExpectOptions{eoSampleMax = 1000, eoStopAfterEmpty = 1000}
-    (genPackets (Range.linear 1 10) Abort (genValidPacket (pure ()) (Range.linear 1 20)))
+    (genPackets 1 10 (genValidPacket defPacketOptions (pure ()) (Range.linear 0 20)))
     (exposeClockResetEnable (depacketizeToDfModel const))
     (exposeClockResetEnable ckt)
  where
@@ -90,9 +90,10 @@ dropTailTest SNat n =
     @System
     defExpectOptions
     ( genPackets
-        (Range.linear 1 4)
-        Abort
+        1
+        4
         ( genValidPacket
+            defPacketOptions
             (Gen.int8 Range.linearBounded)
             (Range.linear (natToNum @(n `DivRU` dataWidth)) 20)
         )
@@ -134,17 +135,17 @@ prop_const_depacketize_to_df_d5_d4 = depacketizeToDfPropertyGenerator d5 d4
 
 -- | dataWidth < n && dataWidth % n ~ 0
 prop_droptail_4_bytes_d1 :: Property
-prop_droptail_4_bytes_d1 = dropTailTest d4 d1
+prop_droptail_4_bytes_d1 = dropTailTest d1 d4
 
 prop_droptail_7_bytes_d1 :: Property
-prop_droptail_7_bytes_d1 = dropTailTest d7 d1
+prop_droptail_7_bytes_d1 = dropTailTest d1 d7
 
 -- | dataWidth < n && dataWidth % n > 0
 prop_droptail_4_bytes_d3 :: Property
-prop_droptail_4_bytes_d3 = dropTailTest d4 d3
+prop_droptail_4_bytes_d3 = dropTailTest d3 d4
 
 prop_droptail_7_bytes_d4 :: Property
-prop_droptail_7_bytes_d4 = dropTailTest d7 d4
+prop_droptail_7_bytes_d4 = dropTailTest d4 d7
 
 -- | dataWidth ~ n
 prop_droptail_4_bytes_d4 :: Property
@@ -155,10 +156,10 @@ prop_droptail_7_bytes_d7 = dropTailTest d7 d7
 
 -- | dataWidth > n
 prop_droptail_4_bytes_d7 :: Property
-prop_droptail_4_bytes_d7 = dropTailTest d4 d7
+prop_droptail_4_bytes_d7 = dropTailTest d7 d4
 
 prop_droptail_7_bytes_d12 :: Property
-prop_droptail_7_bytes_d12 = dropTailTest d7 d12
+prop_droptail_7_bytes_d12 = dropTailTest d12 d7
 
 tests :: TestTree
 tests =
diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/PacketFifo.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/PacketFifo.hs
index 9095da0e..75b4ecd0 100644
--- a/clash-protocols/tests/Tests/Protocols/PacketStream/PacketFifo.hs
+++ b/clash-protocols/tests/Tests/Protocols/PacketStream/PacketFifo.hs
@@ -31,8 +31,7 @@ prop_packetFifo_id =
   idWithModelSingleDomain
     @System
     defExpectOptions{eoSampleMax = 1000, eoStopAfterEmpty = 1000}
-    ( genPackets (Range.linear 1 30) Abort (genValidPacket Gen.enumBounded (Range.linear 1 10))
-    )
+    (genPackets 1 30 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 10)))
     (exposeClockResetEnable dropAbortedPackets)
     (exposeClockResetEnable ckt)
  where
@@ -47,8 +46,7 @@ prop_packetFifo_small_buffer_id =
   idWithModelSingleDomain
     @System
     defExpectOptions{eoSampleMax = 1000, eoStopAfterEmpty = 1000}
-    ( genPackets (Range.linear 1 10) Abort (genValidPacket Gen.enumBounded (Range.linear 1 30))
-    )
+    (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 30)))
     (exposeClockResetEnable dropAbortedPackets)
     (exposeClockResetEnable ckt)
  where
@@ -70,9 +68,10 @@ prop_packetFifo_no_gaps = property $ do
           enableGen
       gen =
         genPackets
-          (Range.linear 1 10)
-          NoAbort
-          (genValidPacket Gen.enumBounded (Range.linear 1 10))
+          1
+          10
+          ( genValidPacket defPacketOptions{poAbortMode = NoAbort} Gen.enumBounded (Range.linear 0 10)
+          )
 
   packets :: [PacketStreamM2S 4 Int16] <- forAll gen
 
@@ -93,8 +92,7 @@ prop_overFlowDrop_packetFifo_id =
   idWithModelSingleDomain
     @System
     defExpectOptions{eoSampleMax = 2000, eoStopAfterEmpty = 1000}
-    ( genPackets (Range.linear 1 30) Abort (genValidPacket Gen.enumBounded (Range.linear 1 10))
-    )
+    (genPackets 1 30 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 10)))
     (exposeClockResetEnable dropAbortedPackets)
     (exposeClockResetEnable ckt)
  where
@@ -124,8 +122,13 @@ prop_overFlowDrop_packetFifo_drop =
    where
     packetChunk = chunkByPacket packets
 
-  genSmall = genValidPacket Gen.enumBounded (Range.linear 1 5) NoAbort
-  genBig = genValidPacket Gen.enumBounded (Range.linear 33 33) NoAbort
+  genSmall =
+    genValidPacket defPacketOptions{poAbortMode = NoAbort} Gen.enumBounded (Range.linear 1 5)
+  genBig =
+    genValidPacket
+      defPacketOptions{poAbortMode = NoAbort}
+      Gen.enumBounded
+      (Range.linear 33 33)
 
 -- | test for id using a small metabuffer to ensure backpressure using the metabuffer is tested
 prop_packetFifo_small_metaBuffer :: Property
@@ -133,7 +136,7 @@ prop_packetFifo_small_metaBuffer =
   idWithModelSingleDomain
     @System
     defExpectOptions
-    (genPackets (Range.linear 1 30) Abort (genValidPacket Gen.enumBounded (Range.linear 1 4)))
+    (genPackets 1 30 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 4)))
     (exposeClockResetEnable dropAbortedPackets)
     (exposeClockResetEnable ckt)
  where
diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Packetizers.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Packetizers.hs
index b7d1d742..9edb1c43 100644
--- a/clash-protocols/tests/Tests/Protocols/PacketStream/Packetizers.hs
+++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Packetizers.hs
@@ -24,8 +24,9 @@ import Protocols.PacketStream (packetizeFromDfC, packetizerC)
 import Protocols.PacketStream.Base
 import Protocols.PacketStream.Hedgehog
 
-{- | Test the packetizer with varying datawidth and number of bytes in the header,
-  with metaOut = ().
+{- |
+Test the packetizer with varying datawidth and number of bytes in the header,
+with metaOut = ().
 -}
 packetizerPropertyGenerator ::
   forall
@@ -41,9 +42,9 @@ packetizerPropertyGenerator SNat SNat =
     @System
     defExpectOptions
     ( genPackets
-        (Range.linear 1 10)
-        Abort
-        (genValidPacket (genVec Gen.enumBounded) (Range.linear 1 10))
+        1
+        10
+        (genValidPacket defPacketOptions (genVec Gen.enumBounded) (Range.linear 0 10))
     )
     (exposeClockResetEnable model)
     (exposeClockResetEnable ckt)
@@ -56,24 +57,9 @@ packetizerPropertyGenerator SNat SNat =
       (PacketStream System dataWidth ())
   ckt = packetizerC (const ()) id
 
--- | headerBytes % dataWidth ~ 0
-prop_const_packetizer_d1_d14 :: Property
-prop_const_packetizer_d1_d14 = packetizerPropertyGenerator d1 d14
-
--- | dataWidth < headerBytes
-prop_const_packetizer_d3_d11 :: Property
-prop_const_packetizer_d3_d11 = packetizerPropertyGenerator d3 d11
-
--- | dataWidth ~ header byte size
-prop_const_packetizer_d7_d7 :: Property
-prop_const_packetizer_d7_d7 = packetizerPropertyGenerator d7 d7
-
--- | dataWidth > header byte size
-prop_const_packetizer_d5_d4 :: Property
-prop_const_packetizer_d5_d4 = packetizerPropertyGenerator d5 d4
-
-{- | Test packetizeFromDf with varying datawidth and number of bytes in the header
-  , with metaOut = ().
+{- |
+Test packetizeFromDf with varying datawidth and number of bytes in the header,
+with metaOut = ().
 -}
 packetizeFromDfPropertyGenerator ::
   forall
@@ -98,6 +84,22 @@ packetizeFromDfPropertyGenerator SNat SNat =
     Circuit (Df.Df System (Vec headerBytes (BitVector 8))) (PacketStream System dataWidth ())
   ckt = packetizeFromDfC (const ()) id
 
+-- | headerBytes % dataWidth ~ 0
+prop_const_packetizer_d1_d14 :: Property
+prop_const_packetizer_d1_d14 = packetizerPropertyGenerator d1 d14
+
+-- | dataWidth < headerBytes
+prop_const_packetizer_d3_d11 :: Property
+prop_const_packetizer_d3_d11 = packetizerPropertyGenerator d3 d11
+
+-- | dataWidth ~ header byte size
+prop_const_packetizer_d7_d7 :: Property
+prop_const_packetizer_d7_d7 = packetizerPropertyGenerator d7 d7
+
+-- | dataWidth > header byte size
+prop_const_packetizer_d5_d4 :: Property
+prop_const_packetizer_d5_d4 = packetizerPropertyGenerator d5 d4
+
 -- | headerBytes % dataWidth ~ 0
 prop_const_packetizeFromDf_d1_d14 :: Property
 prop_const_packetizeFromDf_d1_d14 = packetizeFromDfPropertyGenerator d1 d14
diff --git a/clash-protocols/tests/Tests/Protocols/PacketStream/Routing.hs b/clash-protocols/tests/Tests/Protocols/PacketStream/Routing.hs
index e008e8a0..1e962ef9 100644
--- a/clash-protocols/tests/Tests/Protocols/PacketStream/Routing.hs
+++ b/clash-protocols/tests/Tests/Protocols/PacketStream/Routing.hs
@@ -66,7 +66,7 @@ makePropPacketArbiter _ _ mode =
   genSources = mapM setMeta (indicesI @p)
   setMeta j = do
     pkts <-
-      genPackets @n (Range.linear 1 10) Abort (genValidPacket (pure ()) (Range.linear 1 10))
+      genPackets @n 1 10 (genValidPacket defPacketOptions (pure ()) (Range.linear 0 10))
     pure $ L.map (\pkt -> pkt{_meta = j}) pkts
 
   partitionPackets packets =
@@ -117,7 +117,7 @@ makePropPacketDispatcher ::
 makePropPacketDispatcher _ fs =
   idWithModelSingleDomain @System
     defExpectOptions{eoSampleMax = 2000, eoStopAfterEmpty = 1000}
-    (genPackets (Range.linear 1 10) Abort (genValidPacket Gen.enumBounded (Range.linear 1 6)))
+    (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 6)))
     (exposeClockResetEnable (model 0))
     (exposeClockResetEnable (packetDispatcherC fs))
  where