From da5285a52d7e389b29e0792e90345ee3bb104ab1 Mon Sep 17 00:00:00 2001 From: Lucas Bollen Date: Thu, 1 Aug 2024 16:49:35 +0200 Subject: [PATCH] Large Axi4 refactor Fixed up and downscalers Added properties Refactored tests --- bittide/bittide.cabal | 2 + bittide/src/Bittide/Axi4.hs | 110 +++++---- bittide/tests/Tests/Axi4.hs | 298 +++++++++---------------- bittide/tests/Tests/Axi4/Generators.hs | 92 ++++---- bittide/tests/Tests/Axi4/Properties.hs | 189 ++++++++++++++++ bittide/tests/Tests/Axi4/Types.hs | 115 ++++++++++ bittide/tests/UnitTests.hs | 6 +- 7 files changed, 518 insertions(+), 294 deletions(-) create mode 100644 bittide/tests/Tests/Axi4/Properties.hs create mode 100644 bittide/tests/Tests/Axi4/Types.hs diff --git a/bittide/bittide.cabal b/bittide/bittide.cabal index ff5579647..5a8cae4ed 100644 --- a/bittide/bittide.cabal +++ b/bittide/bittide.cabal @@ -229,6 +229,8 @@ test-suite unittests other-modules: Tests.Axi4 Tests.Axi4.Generators + Tests.Axi4.Properties + Tests.Axi4.Types Tests.Calendar Tests.ClockControl.Si539xSpi Tests.Counter diff --git a/bittide/src/Bittide/Axi4.hs b/bittide/src/Bittide/Axi4.hs index be305ebe2..e48ef0924 100644 --- a/bittide/src/Bittide/Axi4.hs +++ b/bittide/src/Bittide/Axi4.hs @@ -34,6 +34,7 @@ module Bittide.Axi4 eqAxi4Stream, axiUserMap, axiUserMapC, + isPackedTransfer, -- * Internal mkKeep @@ -44,7 +45,7 @@ import Clash.Prelude import Bittide.Axi4.Internal import Bittide.Extra.Maybe import Bittide.SharedTypes -import Clash.Cores.Xilinx.Ila +import Clash.Cores.Xilinx.Ila hiding (Data) import Clash.Sized.Internal.BitVector (popCountBV) import Data.Constraint import Data.Constraint.Nat.Extra @@ -57,6 +58,7 @@ import qualified Protocols.DfConv as DfConv {- $setup >>> import Clash.Prelude +>>> import Protocols.Axi4.Stream -} -- | An 'Axi4Stream' without gaps in the data. This means that for each transfer @@ -108,18 +110,22 @@ axiStreamFromByteStream = AS.forceResetSanity |> Circuit (mealyB go Nothing) -- If the head of the pre-shifted axi has its keep bit set, shifting is done. extendedAxi = fmap (axiUserMap (:< undefUser) . extendAxi @_ @1) axiStored axiPreShift = combinedAxi <|> extendedAxi - (axiHead, axiPostShift) = splitAxi4Stream @1 $ + axiPostShift = snd $ splitAxi4Stream @1 $ fmap (axiUserMap (\ v -> (head v, tail v))) axiPreShift -- Output the pre-shifted axi if we can not shift anymore. - output = if not dropInput && isJust axiHead then axiPreShift else Nothing + shiftingDone = not dropInput && maybe False isPackedTransfer axiPreShift + capturedLast = maybe False _tlast axiPreShift + output = if shiftingDone then axiPreShift else Nothing - -- State update + -- Flow control (axiNext, inputReady) - | dropInput = (axiStored, True) - | isJust output && outputReady = (Nothing, isJust combinedAxi) - | isJust output && not outputReady = (axiStored, False) - | otherwise = (axiPostShift, isJust combinedAxi) + | dropInput = (axiStored, True) -- Drop the input + | shiftingDone && outputReady = (Nothing, isJust combinedAxi) -- valid output, accepted + | shiftingDone && not outputReady = (axiStored, False) -- valid output, not accepted + | not shiftingDone && isJust input = (axiPostShift, isJust combinedAxi) -- Shift when input + | not shiftingDone && capturedLast = (axiPostShift, False) -- Shift when captured _tlast + | otherwise = (axiStored, False) -- No input -- TODO: Add test that verifies throughput requirements. -- | Transforms an Axi4 stream of /n/ bytes wide into an Axi4 stream of 1 byte @@ -501,8 +507,8 @@ rxReadMaster# SNat = mealyB go (AwaitingData @fifoDepth @wbBytes, Idle) (ClearingPacketLength, _) -> (bufState, ClearingStatus) (ClearingStatus,_) -> (AwaitingData, Idle) - lastBytes (PacketComplete s) (ReadingPacket i) = s <= (4 * (checkedResize i)) - lastBytes (BufferFull) (ReadingPacket i) = i == maxBound + lastBytes (PacketComplete s) (ReadingPacket i) = s <= (4 * checkedResize i) + lastBytes BufferFull (ReadingPacket i) = i == maxBound lastBytes _ _ = False -- | Convert a @n@ number of bytes to an @m@ byte enable Vector to be used with Axi4Stream. @@ -524,7 +530,6 @@ mkKeep nBytes | nBytes < natToNum @byteEnables = fmap (< checkedResize nBytes) indicesI | otherwise = repeat True - type AxiStreamBytesOnly nBytes = 'Axi4StreamConfig nBytes 0 0 -- TODO: Replace with PacketStream @@ -640,42 +645,35 @@ axiPacking :: (PackedAxi4Stream dom ('Axi4StreamConfig dataWidth idWidth destWidth) ()) axiPacking = AS.forceResetSanity |> Circuit (mealyB go Nothing) where - go axiStored ~(input, Axi4StreamS2M outputReady) = - (newStored, (Axi4StreamS2M consumableInput, output)) + go axiStored ~(input, Axi4StreamS2M{_tready = outputReady}) = + (axiNext, (Axi4StreamS2M inputReady, output)) where + -- undefUser = deepErrorX "axiStreamFromByteStream: _tuser undefined" + + -- Try to append the incoming axi to the stored axi. + dropInput = maybe False (\a -> not (or (_tlast a :> _tkeep a))) input + combinedAxi = axiUserMap (const ()) <$> combineAxi4Stream axiStored input - -- Axi Right - -- Produce when: - -- Data has overflowed into the excess buffer. - -- Output buffer contains the end of a packet. - outputValid = isJust excessBuffer || maybe False _tlast outputBuffer - output = if outputValid then outputBuffer else Nothing - handshakeOutput = outputValid && outputReady - - -- Axi Left - -- Accept input if we can consume the input into the remainder and we don't have valid output being blocked. - consumableInput = isJust packedAxi4Stream - inputReady = consumableInput && not (outputValid && not outputReady) - inputBlock = isJust input && not inputReady - - -- State update - -- Split the state into the output buffer and the excess buffer. - -- Determine the remainder and create a new packed Axi4Stream using the remainder and the input. - (outputBuffer, excessBuffer) = splitAxi4Stream axiStored - remainder = if handshakeOutput then excessBuffer else outputBuffer - packedAxi4Stream = packAxi4Stream <$> combineAxi4Stream remainder input - - newStored - -- The output buffer is consumed and we can add the input to the excess buffer - | handshakeOutput && consumableInput = packedAxi4Stream - -- The output buffer is consumed, but We can not add the input to the excess buffer - | handshakeOutput = combineAxi4Stream excessBuffer Nothing - -- Our output has not been consumed - | outputValid = axiStored - -- We can not consume the input - | inputBlock = axiStored - -- We can consume the input - | otherwise = packedAxi4Stream + -- Shift the internal axi towards HEAD by one position. + -- If the head of the pre-shifted axi has its keep bit set, shifting is done. + extendedAxi = fmap extendAxi axiStored + packedAxi = fmap packAxi4Stream $ combinedAxi <|> extendedAxi + + (outputBuffer, excessBuffer) = splitAxi4Stream $ fmap (axiUserMap (const ((),()))) packedAxi + + -- Output the pre-shifted axi if we can not shift anymore. + shiftingDone = not dropInput && maybe False isPackedTransfer outputBuffer + capturedLast = maybe False _tlast outputBuffer + output = if shiftingDone then outputBuffer else Nothing + + -- Flow control + (axiNext, inputReady) + | dropInput = (axiStored, True) -- Drop the input + | shiftingDone && outputReady = (excessBuffer, isJust combinedAxi) -- valid output, accepted + | shiftingDone && not outputReady = (axiStored, False) -- valid output, not accepted + | not shiftingDone && isJust input = (outputBuffer, isJust combinedAxi) -- Shift when input + | not shiftingDone && capturedLast = (outputBuffer, False) -- Shift when captured _tlast + | otherwise = (axiStored, False) -- No input -- | Integrated logic analyzer for an Axi4Stream bus, it captures the data, keep, ready and last signals. ilaAxi4Stream :: @@ -707,3 +705,25 @@ ilaAxi4Stream stages0 depth0 = Circuit $ \(m2s, s2m) -> (_tready <$> s2m) in ilaInst `hwSeqX` (s2m, m2s) + +-- | A packed transfer is a transfer where either: +-- * _tlast is not set and all _tkeep bits are set. +-- * _tlast is set and only the first n _tkeep bits are set. +-- >>> let mkAxi keep last = Axi4StreamM2S @('Axi4StreamConfig 2 0 0) (repeat 0) keep (repeat True) last 0 0 () +-- >>> isPackedTransfer $ mkAxi (False :> False :> Nil) False +-- False +-- >>> isPackedTransfer $ mkAxi (True :> False :> Nil) False +-- False +-- >>> isPackedTransfer $ mkAxi (True :> True :> Nil) False +-- True +-- >>> isPackedTransfer $ mkAxi (False :> False :> Nil) True +-- True +-- >>> isPackedTransfer $ mkAxi (False :> True :> Nil) True +-- False +isPackedTransfer :: KnownNat (DataWidth conf) => Axi4StreamM2S conf a -> Bool +isPackedTransfer Axi4StreamM2S{..} + | _tlast = not $ hasGaps _tkeep + | otherwise = and _tkeep + where + rising = snd . mapAccumL (\prevKeep keep -> (keep, not prevKeep && keep)) True + hasGaps = or . rising diff --git a/bittide/tests/Tests/Axi4.hs b/bittide/tests/Tests/Axi4.hs index 6b9ff33cc..dd87b4b77 100644 --- a/bittide/tests/Tests/Axi4.hs +++ b/bittide/tests/Tests/Axi4.hs @@ -21,7 +21,7 @@ import Clash.Prelude import Clash.Explicit.Prelude (noReset) import Clash.Hedgehog.Sized.Unsigned -import Clash.Sized.Vector(unsafeFromList) +import Data.Either import Data.Maybe import Data.Proxy import Hedgehog @@ -34,143 +34,75 @@ import Bittide.Axi4 import Bittide.Extra.Maybe import Protocols.Hedgehog import Tests.Axi4.Generators +import Tests.Axi4.Properties +import Tests.Axi4.Types import Tests.Shared import qualified Data.List as L import qualified GHC.TypeNats as TN import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range -import qualified Test.Tasty.HUnit as HU tests :: TestTree tests = testGroup "Tests.Axi4" [ testPropertyNamed - "Read Axi4 Stream packets via Wishbone" "wbAxisRxBufferReadStreams" - wbAxisRxBufferReadStreams - , testPropertyNamed "Various operation on Axi4StreamM2S: splitAxi4Stream combineAxi4Stream packAxi4Stream" "axiOperations" axiOperations - , testPropertyNamed "Packet conversion utilies" "packetConversions" packetConversions - , testPropertyNamed "Axi4StreamPacketFifo as identity" "prop_axi4StreamPacketFifo_id" prop_axi4StreamPacketFifo_id - , testPropertyNamed "Axi4StreamPacketFifo produces uninterrupted packets" "axi4StreamPacketFifoUninterrupted" axi4StreamPacketFifoUninterrupted - , testPropertyNamed "axiStreamToByteStream as identity" "prop_axiStreamToByteStream_id" prop_axiStreamToByteStream_id - , testPropertyNamed "axiStreamToByteStream produces dense streams" "prop_axiStreamToByteStream_dense" prop_axiStreamToByteStream_dense - , testPropertyNamed "axiStreamFromByteStream as identity" "prop_axiStreamFromByteStream_id" prop_axiStreamFromByteStream_id - - -- XXX: This test is disabled because it is failing. It produces something akin: - -- - -- [ M2S(tkeep=[True], tlast=False) - -- , M2S(tkeep=[False], tlast=True) - -- ] - -- - -- , testPropertyNamed "axiStreamFromByteStream produces dense streams" "prop_axiStreamFromByteStream_dense" prop_axiStreamFromByteStream_dense - - , HU.testCase "case_isDenseAxi4Stream" case_isDenseAxi4Stream + "Read Axi4 Stream packets via Wishbone" "prop_wbAxisRxBufferReadStreams" + prop_wbAxisRxBufferReadStreams + , testPropertyNamed "Various operation on Axi4StreamM2S: splitAxi4Stream combineAxi4Stream packAxi4Stream" "prop_axiOperations" prop_axiOperations + , testPropertyNamed "Packet conversion utilies" "prop_packetConversions" prop_packetConversions + , testPropertyNamed "Axi4StreamPacketFifo" "prop_axi4StreamPacketFifo" prop_axi4StreamPacketFifo + , testPropertyNamed "Axi4StreamPacketFifo produces uninterrupted packets" "prop_axi4StreamPacketFifo_Uninterrupted" prop_axi4StreamPacketFifo_Uninterrupted + , testPropertyNamed "axiStreamToByteStream" "prop_axiStreamToByteStream" prop_axiStreamToByteStream + , testPropertyNamed "axiStreamFromByteStream " "prop_axiStreamFromByteStream" prop_axiStreamFromByteStream + , testPropertyNamed "packAxi4Stream" "prop_packAxi4Stream" prop_packAxi4Stream + , testPropertyNamed "prop_axiPacking" "prop_axiPacking" prop_axiPacking ] -type Packet = [Unsigned 8] - --- | Checks if an Axi4Stream transfer is dense, i.e. there are no gaps in the data. --- A transfer can contain null bytes, but only if _tlast is set and they are not followed --- by data bytes or position bytes. -isDenseAxi4Stream :: KnownNat (DataWidth conf) => Axi4StreamM2S conf userType -> Bool -isDenseAxi4Stream Axi4StreamM2S{..} - | _tlast = not $ hasGaps _tkeep - | otherwise = and _tkeep - where - rising = snd . mapAccumL (\prevKeep keep -> (keep, not prevKeep && keep)) True - hasGaps = or . rising - -case_isDenseAxi4Stream :: HU.Assertion -case_isDenseAxi4Stream = do - HU.assertBool "Expected dense" $ go (repeat @1 True) False - HU.assertBool "Expected dense" $ go (repeat @2 True) False - HU.assertBool "Expected dense" $ go (repeat @3 True) False - HU.assertBool "Expected dense" $ go (repeat @1 False) True - HU.assertBool "Expected dense" $ go (repeat @2 False) True - HU.assertBool "Expected dense" $ go (repeat @3 False) True - HU.assertBool "Expected dense" $ go (repeat @1 True ++ repeat @1 False) True - HU.assertBool "Expected dense" $ go (repeat @1 True ++ repeat @2 False) True - HU.assertBool "Expected dense" $ go (repeat @1 True ++ repeat @3 False) True - HU.assertBool "Expected dense" $ go (repeat @2 True ++ repeat @1 False) True - HU.assertBool "Expected dense" $ go (repeat @3 True ++ repeat @2 False) True - - HU.assertBool "Expected sparse" $ not $ go (False :> True :> Nil) True - HU.assertBool "Expected sparse" $ not $ go (False :> True :> False :> Nil) True - HU.assertBool "Expected sparse" $ not $ go (False :> True :> True :> Nil) False - HU.assertBool "Expected sparse" $ not $ go (False :> True :> True :> Nil) False - HU.assertBool "Expected sparse" $ not $ go (True :> False :> True :> Nil) False - HU.assertBool "Expected sparse" $ not $ go (True :> True :> False :> Nil) False - HU.assertBool "Expected sparse" $ not $ go (False :> True :> False :> Nil) False - HU.assertBool "Expected sparse" $ not $ go (False :> False :> False :> Nil) False - - where - go keep last0 = isDenseAxi4Stream $ mkM2S keep last0 - - mkM2S :: KnownNat n => Vec n Bool -> Bool -> Axi4StreamM2S ('Axi4StreamConfig n 0 0 ) () - mkM2S keep last0 = Axi4StreamM2S - { _tdata = repeat 0 - , _tkeep = keep - , _tstrb = repeat True - , _tlast = last0 - , _tid = 0 - , _tdest = 0 - , _tuser = () - } - -prop_axiStreamToByteStream_id :: Property -prop_axiStreamToByteStream_id = - propWithModel defExpectOptions gen model1 impl prop +-- This test only checks that the data and position bytes are not changed by the component, +-- _tdest, _tid and _tuser are not checked. +prop_axiStreamToByteStream :: Property +prop_axiStreamToByteStream = + propWithModel defExpectOptions gen model impl prop where impl = wcre @System axiStreamToByteStream - model1 = L.concatMap (catMaybes . packetToAxiStream d1) . axiStreamToPackets + model = L.concatMap (catMaybes . packetToAxiStream d1) . axiStreamToPackets - packetGen = catMaybes <$> genAxiPacket d4 d0 d0 Sparse - [Null, Data, Position, Reserved] (Range.linear 0 16) (pure ()) + packetGen = catMaybes <$> genRandomAxiPacket d4 d0 d0 + [NullByte, DataByte, PositionByte] (Range.linear 0 16) (pure ()) gen = L.concat <$> Gen.list (Range.linear 0 3) packetGen - prop as bs = axiStreamToPackets as === axiStreamToPackets bs - -prop_axiStreamToByteStream_dense :: Property -prop_axiStreamToByteStream_dense = propWithModel defExpectOptions gen model1 impl prop - where - impl = wcre @System axiStreamToByteStream - - model1 = L.concatMap (catMaybes . packetToAxiStream d1) . axiStreamToPackets + prop expected sampled = do + let bytetypes = fmap getPacketByteTypes $ rights $ separatePackets sampled + footnote $ "expected: " <> show expected + footnote $ "sampled: " <> show sampled + footnote $ "bytetypes: " <> show bytetypes - packetGen = catMaybes <$> genAxiPacket d4 d0 d0 Sparse - [Null, Data, Position, Reserved] (Range.linear 0 16) (pure ()) + -- None of the packets start with null bytes + assert $ not (any hasLeadingNullBytes bytetypes) - gen = L.concat <$> Gen.list (Range.linear 0 3) packetGen + -- All packets are packed + assert $ all isPackedAxi4StreamPacket bytetypes - prop _ bs = assert $ all isDenseAxi4Stream bs + -- The extracted packets are the same for both the expected and sampled data + axiStreamToPackets expected === axiStreamToPackets sampled -prop_axi4StreamPacketFifo_id :: Property -prop_axi4StreamPacketFifo_id = - propWithModel defExpectOptions gen id impl prop +prop_axi4StreamPacketFifo :: Property +prop_axi4StreamPacketFifo = + idWithModel defExpectOptions gen id impl where - impl = wcre @System $ axiStreamPacketFifo d2 d8 + impl = wcre @System $ axiStreamPacketFifo d8 d64 - packetGen = catMaybes <$> genAxiPacket d4 d0 d0 Sparse - [Null, Data, Position, Reserved] (Range.linear 0 32) (pure ()) + packetGen = catMaybes <$> genRandomAxiPacket d4 d0 d0 + [NullByte, DataByte, PositionByte] (Range.linear 0 32) (pure ()) gen = L.concat <$> Gen.list (Range.linear 0 10) packetGen - prop _ bs = axiStreamToPackets bs === axiStreamToPackets bs - --- | Check if a list of Axi4StreamM2S transfers form an uninterrupted stream. --- When a packet transmission is started, all elements should be Just until the --- last transfer of the packet is reached. -unInterruptedAxi4Packets :: [Maybe (Axi4StreamM2S conf userType)] -> Bool -unInterruptedAxi4Packets xs = case break (maybe False _tlast) (dropWhile isNothing xs) of - (packet, lastTransaction : rest) -> - all isJust (packet <> [lastTransaction]) && unInterruptedAxi4Packets rest - (ys, []) -> all isJust ys - -- | Generate a 'axiStreamFromByteStream' component with variable output bus width -- and test if a stream of multiple generated 'Packet's can be routed through it -- without being changed. -axi4StreamPacketFifoUninterrupted :: Property -axi4StreamPacketFifoUninterrupted = property $ do +prop_axi4StreamPacketFifo_Uninterrupted :: Property +prop_axi4StreamPacketFifo_Uninterrupted = property $ do busWidth <- forAll $ Gen.integral $ Range.linear 1 8 extraFifoDepth <- forAll $ Gen.integral $ Range.linear 2 64 case @@ -180,8 +112,8 @@ axi4StreamPacketFifoUninterrupted = property $ do ( SomeNat (Proxy :: Proxy busWidth) ,SomeNat (Proxy :: Proxy extraFifoDepth) ) -> do - let packetGen = genAxiPacket (SNat @busWidth) d0 d0 Sparse - [Null, Data, Position, Reserved] (Range.linear 0 (extraFifoDepth - 2)) (pure ()) + let packetGen = genRandomAxiPacket (SNat @busWidth) d0 d0 + [NullByte, DataByte, PositionByte] (Range.linear 0 (extraFifoDepth - 2)) (pure ()) inputData <- forAll (L.concat <$> Gen.list (Range.linear 0 10) packetGen) let conf = SimulationConfig 0 100 True @@ -194,36 +126,44 @@ axi4StreamPacketFifoUninterrupted = property $ do -- | Verify that the 'axiStreamFromByteStream' component does not change the content of the stream -- when converting 1 byte wide transfers to 4 byte wide transfers. -prop_axiStreamFromByteStream_id :: Property -prop_axiStreamFromByteStream_id = propWithModel defExpectOptions gen model impl prop +prop_axiStreamFromByteStream :: Property +prop_axiStreamFromByteStream = propWithModel defExpectOptions gen model impl prop where impl = wcre @System $ axiUserMapC (const ()) <| axiStreamFromByteStream model = L.concatMap (catMaybes . packetToAxiStream d4) . axiStreamToPackets - packetGen = catMaybes <$> genAxiPacket d1 d0 d0 Sparse - [Null, Data, Position, Reserved] (Range.linear 0 16) (pure ()) + packetGen = catMaybes <$> genRandomAxiPacket d1 d0 d0 + [NullByte, DataByte, PositionByte] (Range.linear 0 16) (pure ()) gen = L.concat <$> Gen.list (Range.linear 0 3) packetGen - prop as (fmap (axiUserMap (const ())) -> bs) = axiStreamToPackets as === axiStreamToPackets bs + prop expected sampled = do + let bytetypes = fmap getPacketByteTypes $ rights $ separatePackets sampled + footnote $ "expected: " <> show expected + footnote $ "sampled: " <> show sampled + footnote $ "bytetypes: " <> show bytetypes --- | Verify that the 'axiStreamFromByteStream' component produces dense streams when converting --- 1 byte wide transfers to 4 byte wide transfers. -prop_axiStreamFromByteStream_dense :: Property -prop_axiStreamFromByteStream_dense = propWithModel defExpectOptions gen model impl prop - where - impl = wcre @System $ axiUserMapC (const ()) <| axiStreamFromByteStream + -- None of the packets start with null bytes + assert $ not (any hasLeadingNullBytes bytetypes) - model = L.concatMap (catMaybes . packetToAxiStream d4) . axiStreamToPackets + -- All packets are packed + assert $ all isPackedAxi4StreamPacket bytetypes - packetGen = catMaybes <$> genAxiPacket d1 d0 d0 Sparse - [Null, Data, Position, Reserved] (Range.linear 0 16) (pure ()) + -- The extracted packets are the same for both the expected and sampled data + axiStreamToPackets expected === axiStreamToPackets sampled - gen = L.concat <$> Gen.list (Range.linear 0 3) packetGen - prop _ bs = do - footnote $ "bs: " <> show bs - footnote $ "bs is dense: " <> show (isDenseAxi4Stream <$> bs) - assert $ all isDenseAxi4Stream bs +prop_packAxi4Stream :: Property +prop_packAxi4Stream = property $ do + -- A transaction can only contain null bytes and be packed if _tlast is True + axiWithNulls <- forAll $ genAxisM2S d8 d0 d0 [NullByte, DataByte, PositionByte] [True] $ pure () + axiWithoutNulls <- forAll $ genAxisM2S d8 d0 d0 [DataByte, PositionByte] [True, False] $ pure () + let + resultWithNulls = packAxi4Stream axiWithNulls + resultWithoutNulls = packAxi4Stream axiWithoutNulls + footnote $ "resultWithNulls: " <> show resultWithNulls + footnote $ "resultWithoutNulls: " <> show resultWithoutNulls + assert (isPackedTransfer resultWithNulls) + assert (isPackedTransfer resultWithoutNulls) -- | Extract the data and strobe bytes. 'Nothing' if the corresponding keep bit -- is low, 'Just' if the keep bit is high. @@ -233,9 +173,9 @@ catKeepBytes :: Vec (DataWidth conf) (Maybe (Unsigned 8, Bool)) catKeepBytes Axi4StreamM2S{..} = orNothing <$> _tkeep <*> zip _tdata _tstrb -axiOperations :: Property -axiOperations = property $ do - axi <- forAll $ genAxisM2S d4 d0 d0 [Null, Data, Position] [True, False] $ pure () +prop_axiOperations :: Property +prop_axiOperations = property $ do + axi <- forAll $ genAxisM2S d4 d0 d0 [NullByte, DataByte, PositionByte] [True, False] $ pure () let keepBytesA = catMaybes $ toList $ catKeepBytes axi keepBytesB = catMaybes $ toList $ catKeepBytes (packAxi4Stream axi) @@ -257,39 +197,39 @@ axiOperations = property $ do -- TODO: Overhaul of `Axi4Stream` representation for correct `Eq` instance assert (maybe False (eqAxi4Stream axi) (uncurry (flip (<|>)) splitConcatB)) -prop_axiPacking_id :: Property -prop_axiPacking_id = propWithModel defExpectOptions gen model impl prop +prop_axiPacking :: Property +prop_axiPacking = propWithModel defExpectOptions gen model impl prop where impl = wcre @System axiPacking - model = L.concatMap (catMaybes . packetToAxiStream d8) . axiStreamToPackets + model = id -- - packetGen = catMaybes <$> genAxiPacket d8 d0 d0 Sparse - [Null, Data, Position, Reserved] (Range.linear 0 16) (pure ()) + packetGen = catMaybes <$> genRandomAxiPacket d1 d0 d0 + [NullByte, DataByte, PositionByte] (Range.linear 0 32) (pure ()) gen = L.concat <$> Gen.list (Range.linear 0 3) packetGen - prop _ bs = axiStreamToPackets bs === axiStreamToPackets bs - -prop_axiPacking_dense :: Property -prop_axiPacking_dense = propWithModel defExpectOptions gen model impl prop - where - impl = wcre @System axiPacking - model = id -- + prop expected sampled = do + let bytetypes = fmap getPacketByteTypes $ rights $ separatePackets sampled + footnote $ "expected: " <> show expected + footnote $ "sampled: " <> show sampled + footnote $ "bytetypes: " <> show bytetypes - packetGen = catMaybes <$> genAxiPacket d8 d0 d0 Sparse - [Null, Data, Position, Reserved] (Range.linear 0 16) (pure ()) + -- None of the packets start with null bytes + assert $ not (any hasLeadingNullBytes bytetypes) - gen = L.concat <$> Gen.list (Range.linear 0 3) packetGen + -- All packets are packed + assert $ all isPackedAxi4StreamPacket bytetypes - prop _ bs = assert $ all isDenseAxi4Stream bs + -- The extracted packets are the same for both the expected and sampled data + axiStreamToPackets expected === axiStreamToPackets sampled -wbAxisRxBufferReadStreams :: Property -wbAxisRxBufferReadStreams = property $ do - let packetGen = genAxiPacket d4 d0 d0 Dense - [Null, Data] (Range.linear 0 16) (pure ()) - inputData <- forAll $ fmap L.concat $ Gen.list (Range.linear 0 3) packetGen +prop_wbAxisRxBufferReadStreams :: Property +prop_wbAxisRxBufferReadStreams = property $ do + let packetGen = Gen.filter (byteTypeFilter conditions . catMaybes) $ genRandomAxiPacket d4 d0 d0 + [NullByte, DataByte] (Range.linear 0 16) (pure ()) + inputData <- forAll (L.concat <$> Gen.list (Range.linear 0 3) packetGen) extraBufferBytes <- forAll $ Gen.integral (Range.linear 31 31) - case (TN.someNatVal extraBufferBytes) of + case TN.someNatVal extraBufferBytes of SomeNat (Proxy :: Proxy extraBufferBytes) -> do let transfers = catMaybes $ wcre $ sampleC conf $ tb (SNat @(1 + extraBufferBytes)) <| driveC conf inputData @@ -297,6 +237,10 @@ wbAxisRxBufferReadStreams = property $ do footnote $ "inputData: " <> show inputData axiStreamToPackets (catMaybes inputData) === axiStreamToPackets transfers where + conditions = + [ isPackedAxi4StreamPacket + , not . hasLeadingNullBytes + ] conf = SimulationConfig 0 500 False tb :: (1 <= bufferBytes, HiddenClockResetEnable System) => SNat bufferBytes -> @@ -309,51 +253,17 @@ wbAxisRxBufferReadStreams = property $ do (wb, axiOut) <- rxReadMasterC bufferBytes -< () idC -< axiOut -packetConversions :: Property -packetConversions = property $ do - packets <- forAll $ Gen.list (Range.linear 1 4) $ Gen.list (Range.linear 1 128) $ genUnsigned Range.constantBounded +prop_packetConversions :: Property +prop_packetConversions = property $ do + packets <- forAll + $ Gen.list (Range.linear 1 4) + $ Gen.list (Range.linear 1 128) + $ genUnsigned Range.constantBounded let transfers = fmap (packetToAxiStream d4) packets footnote $ "transfers:" <> show transfers packets === axiStreamToPackets (L.concatMap catMaybes transfers) -axiStreamToPackets :: - KnownNat nBytes => - [Axi4StreamM2S ('Axi4StreamConfig nBytes 0 0) ()] -> - [Packet] -axiStreamToPackets = L.reverse . snd . L.foldl go ([], []) - where - go (partialPacket, packets) Axi4StreamM2S{..} - | _tlast = ([], L.reverse newPartial : packets) - | otherwise = (newPartial, packets) - where - newPartial = L.reverse (catMaybes (toList $ orNothing <$> _tkeep <*> _tdata)) <> partialPacket - --- Transform a 'Packet' into a list of Axi Stream operations. -packetToAxiStream :: - forall nBytes . - SNat nBytes -> - Packet -> - [Maybe (Axi4StreamM2S ('Axi4StreamConfig nBytes 0 0) ())] -packetToAxiStream w@SNat !bs - | rest /= [] = Just axis : packetToAxiStream w rest - | otherwise = [Just axis] - where - busWidth = natToNum @nBytes - (firstWords, rest) = L.splitAt busWidth bs - word = L.take busWidth (firstWords <> L.repeat 0) - axis = Axi4StreamM2S - { _tdata = unsafeFromList word - , _tkeep = keeps - , _tstrb = repeat True - , _tlast = null rest - , _tid = 0 - , _tdest = 0 - , _tuser = deepErrorX "" - } - keeps = unsafeFromList $ - L.replicate (L.length bs) True <> L.repeat False - -- | Force all invalid bytes to zero. This is useful for a poor man's version -- of '=='. forceKeepLowZero :: Axi4StreamM2S conf userType -> Axi4StreamM2S conf userType diff --git a/bittide/tests/Tests/Axi4/Generators.hs b/bittide/tests/Tests/Axi4/Generators.hs index 1c2d01927..53e5e90a5 100644 --- a/bittide/tests/Tests/Axi4/Generators.hs +++ b/bittide/tests/Tests/Axi4/Generators.hs @@ -9,15 +9,19 @@ module Tests.Axi4.Generators where import Clash.Prelude -import Protocols.Axi4.Stream -import Hedgehog + import Clash.Hedgehog.Sized.Unsigned import Clash.Hedgehog.Sized.Vector (genVec) import Data.Maybe import Data.Proxy +import Hedgehog +import Protocols.Axi4.Stream import Test.Tasty import Test.Tasty.Hedgehog +import Tests.Axi4.Properties +import Tests.Axi4.Types + import qualified GHC.TypeNats as TN import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range @@ -27,36 +31,9 @@ import qualified Hedgehog.Internal.Property as H tests :: TestTree tests = testGroup "Axi4Stream Generators" [ testProperty "genAxisM2S" prop_genAxisM2S + , testProperty "genRandomAxiPacket" prop_genRandomAxiPacket ] --- | Byte types for Axi4StreamM2S transactions -data AxisByteType - = Null - | Data - | Position - | Reserved - deriving (Show, Eq) - -type Keep = Bool -type Strobe = Bool - --- | Get a list of byte types for a given Axi4StreamM2S transaction -getByteTypes :: Axi4StreamM2S conf a -> Vec (DataWidth conf) AxisByteType -getByteTypes Axi4StreamM2S{..} = zipWith getByteType _tkeep _tstrb - --- | Get the byte type based on a keep and strobe value -getByteType :: Keep -> Strobe -> AxisByteType -getByteType True True = Data -getByteType True False = Position -getByteType False False = Null -getByteType False True = Reserved - -getKeepStrobe :: AxisByteType -> (Keep, Strobe) -getKeepStrobe Null = (False, False) -getKeepStrobe Data = (True, True) -getKeepStrobe Position = (True, False) -getKeepStrobe Reserved = (False, True) - -- | Generates a directed Axi4StreamM2S transaction. genAxisM2S :: -- | Data width of the Axi4StreamM2S transaction @@ -66,7 +43,7 @@ genAxisM2S :: -- | Destination width of the Axi4StreamM2S transaction SNat destWidth -> -- | Allowed byte types to generate (can be used to skew the distribution of byte types) - [AxisByteType] -> + [AxiByteType] -> -- | Allowed _tlast values to generate (can be used to skew the distribution of _tlast values) [Bool] -> -- | Generator for user data @@ -84,16 +61,16 @@ genAxisM2S SNat SNat SNat byteTypes lastValues genUser = do prop_genAxisM2S :: Property prop_genAxisM2S = property $ do - dataWidth <- forAll $ Gen.int (Range.constant 1 4) - case TN.someNatVal $ fromIntegral dataWidth of + dataWidth <- forAll (TN.someNatVal . fromIntegral <$> Gen.int (Range.constant 1 4)) + case dataWidth of SomeNat (Proxy :: Proxy dataWidth) -> do let - allowedByteTypes = L.filter (not . null) $ L.subsequences [Null, Data, Position, Reserved] + allowedByteTypes = L.filter (not . null) $ L.subsequences [NullByte, DataByte, PositionByte] allowedLasts = [[False], [True], [False, True]] byteTypes <- forAll $ Gen.choice $ pure <$> allowedByteTypes lastValues <- forAll $ Gen.choice $ fmap pure allowedLasts axi <- forAll $ genAxisM2S (SNat @dataWidth) d8 d8 byteTypes lastValues (pure ()) - let axiBytes = getByteTypes axi + let axiBytes = getByteType <$> getTransferBytes axi cover 40 "tlast" (_tlast axi) cover 40 "not tlast" (not $ _tlast axi) mapM_ (\ byte -> cover 25 (H.LabelName $ "One or more " <> show byte) (isJust $ elemIndex byte axiBytes)) byteTypes @@ -108,35 +85,44 @@ data PacketDensity deriving (Show, Eq) -- | Generate a list of Axi4StreamM2S transactions that form a single packet, only the last transaction --- will have _tlast set to True. When `allowSparse` is set to False, only the last transaction can hold --- null bytes. These null bytes will only appear at the end of the packet. -genAxiPacket :: +-- will have _tlast set to True. The packet +genRandomAxiPacket :: -- | Data width of the Axi4StreamM2S transaction SNat dataWidth -> -- | ID width of the Axi4StreamM2S transaction SNat idWidth -> -- | Destination width of the Axi4StreamM2S transaction SNat destWidth -> - -- | Allow sparse packet - PacketDensity -> -- | Allowed byte types to generate (can be used to skew the distribution of byte types) - -- | A - [AxisByteType] -> + [AxiByteType] -> -- | Range for the length of the packet, excluding the last transaction Range Int -> -- | Generator for user data Gen userType -> -- | Generator for a list of transactions representing a packet Gen [Maybe (Axi4StreamM2S ('Axi4StreamConfig dataWidth idWidth destWidth) userType)] -genAxiPacket SNat SNat SNat density byteTypes range genUser = do - -- Generate init transactions - let initByteTypes = if density == Sparse then byteTypes else L.filter (/= Null) byteTypes - packetInit <- Gen.list range (Gen.maybe $ genAxisM2S SNat SNat SNat initByteTypes [False] genUser) - - -- Generate last transaction - let packetLastGen = genAxisM2S SNat SNat SNat byteTypes [True] genUser - let hasRising axi = or $ snd $ mapAccumL (\prev curr -> (not prev && curr, curr)) True (_tkeep axi) - - -- Filter out transactions that have gaps in the data - packetLast <- if density == Sparse then packetLastGen else Gen.filter (not . hasRising) packetLastGen +genRandomAxiPacket SNat SNat SNat byteTypes range genUser = do + packetInit <- Gen.list range (Gen.maybe $ genAxisM2S SNat SNat SNat byteTypes [False] genUser) + packetLast <- genAxisM2S SNat SNat SNat byteTypes [True] genUser pure (L.tail $ packetInit <> [Just packetLast]) + +prop_genRandomAxiPacket :: Property +prop_genRandomAxiPacket = property $ do + dataWidth <- forAll (TN.someNatVal . fromIntegral <$> Gen.int (Range.constant 1 8)) + case dataWidth of + (SomeNat (Proxy :: Proxy dataWidth)) -> do + let + byteTypes = [NullByte, DataByte, PositionByte] + transfers <- forAll $ genRandomAxiPacket (SNat @dataWidth) d0 d0 byteTypes (Range.constant 1 16) (pure ()) + let + packet = catMaybes transfers + axiBytes = getPacketByteTypes packet + cover 1 "hasLeadingNullBytes" $ hasLeadingNullBytes axiBytes + cover 1 "hasTrailingNullBytes" $ hasTrailingNullBytes axiBytes + cover 1 "isPackedAxi4StreamPacket" $ isPackedAxi4StreamPacket axiBytes + cover 1 "isStrictlySparseAxi4StreamPacket" $ isStrictlySparseAxi4StreamPacket axiBytes + cover 1 "isContinuousAxi4StreamPacket" $ isContinuousAxi4StreamPacket axiBytes + cover 1 "isAlignedAxi4StreamPacket" $ isAlignedAxi4StreamPacket axiBytes + cover 1 "isUnalignedAxi4StreamPacket" $ isUnalignedAxi4StreamPacket axiBytes + cover 1 "unInterruptedAxi4Packets" $ unInterruptedAxi4Packets transfers + assert (isSinglePacket packet) diff --git a/bittide/tests/Tests/Axi4/Properties.hs b/bittide/tests/Tests/Axi4/Properties.hs new file mode 100644 index 000000000..bb3250b17 --- /dev/null +++ b/bittide/tests/Tests/Axi4/Properties.hs @@ -0,0 +1,189 @@ +-- SPDX-FileCopyrightText: 2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 + +{-# LANGUAGE FlexibleContexts #-} + +module Tests.Axi4.Properties where + +import Clash.Prelude +import Protocols.Axi4.Stream + +import Tests.Axi4.Types +import qualified Data.List as L +import qualified Test.Tasty.HUnit as HU +import Test.Tasty +import Data.Maybe + +tests :: TestTree +tests = testGroup "Tests.Axi4.Properties" + [ HU.testCase "case_isPackedAxi4StreamPacket" case_isPackedAxi4StreamPacket + , HU.testCase "case_hasLeadingNullBytes" case_hasLeadingNullBytes + , HU.testCase "case_hasTrailingNullBytes" case_hasTrailingNullBytes + , HU.testCase "case_isSinglePacket" case_isSinglePacket + , HU.testCase "case_isStrictlySparseAxi4StreamPacket" case_isStrictlySparseAxi4StreamPacket + , HU.testCase "case_isUnalignedAxi4StreamPacket" case_isUnalignedAxi4StreamPacket + , HU.testCase "case_unInterruptedAxi4Packets" case_unInterruptedAxi4Packets + ] + +-- | Apply filters to an Axi4StreamM2S packet +byteTypeFilter :: [[AxiByteType] -> Bool] -> [Axi4StreamM2S conf a] -> Bool +byteTypeFilter filters packet = all ($ getPacketByteTypes packet) filters + +-- | A packet does not contain null bytes between the first and last data or position byte +isPackedAxi4StreamPacket :: [AxiByteType] -> Bool +isPackedAxi4StreamPacket = + all (== NullByte) . -- There should not be data or position bytes left + dropWhile (/= NullByte) . -- Find first null byte -- Find first null byte + dropWhile (== NullByte) -- Find first data or position byte + +-- | A strictly sparse packet contains at least one position byte between the first +-- and last data byte +isStrictlySparseAxi4StreamPacket :: [AxiByteType] -> Bool +isStrictlySparseAxi4StreamPacket = + elem DataByte . -- There should still be data bytes left + dropWhile (/= PositionByte) . -- Find first position byte -- Find first position byte + dropWhile (/= DataByte) -- Find first data byte + +-- | Continuous packets do not contain null bytes between the first and last data byte +isContinuousAxi4StreamPacket :: [AxiByteType] -> Bool +isContinuousAxi4StreamPacket = notElem NullByte + +-- | Aligned packets do not contain position bytes +isAlignedAxi4StreamPacket :: [AxiByteType] -> Bool +isAlignedAxi4StreamPacket = notElem PositionByte + +-- | Unaligned packets contain position bytes at the beginning and/or end of the packet, +-- but not between the first and last data byte. +isUnalignedAxi4StreamPacket :: [AxiByteType] -> Bool +isUnalignedAxi4StreamPacket bytes0 + | null bytes1 = False + | otherwise = + ((== PositionByte) (L.head bytes1) || (== PositionByte) (L.last bytes1)) && + not (isStrictlySparseAxi4StreamPacket bytes1) + where + bytes1 = filter (/= NullByte) bytes0 + +-- | Leading null bytes are null bytes that appear before the first data or position byte. +-- If a packet contains only null bytes, this returns @False@. +hasLeadingNullBytes :: [AxiByteType] -> Bool +hasLeadingNullBytes [] = False +hasLeadingNullBytes (x:xs) = x == NullByte && any (/= NullByte) xs + +-- | Trailing null bytes are null bytes at the end of a packet +-- If a packet contains only null bytes, this returns @False@. +hasTrailingNullBytes :: [AxiByteType] -> Bool +hasTrailingNullBytes [] = False +hasTrailingNullBytes xs = (L.last xs == NullByte) && any (/= NullByte) xs + +-- | Check if a list of Axi4StreamM2S transfers form an uninterrupted stream. +-- When a packet transmission is started, all elements should be Just until the +-- last transfer of the packet is reached. +unInterruptedAxi4Packets :: [Maybe (Axi4StreamM2S conf userType)] -> Bool +unInterruptedAxi4Packets xs = case break (maybe False _tlast) (dropWhile isNothing xs) of + (payload, l : rest) -> + all isJust (payload <> [l]) && unInterruptedAxi4Packets rest + (ys, []) -> all isJust ys + +-- | Check if a list of Axi4StreamM2S transfers form a single packet. +-- A list of `Axi4StreamM2S` transfers form a single packet if only the last transfer +-- has `_tlast` set. +isSinglePacket :: [Axi4StreamM2S conf userType] -> Bool +isSinglePacket axis = case break _tlast axis of + (_, [_]) -> True + _ -> False + +case_isPackedAxi4StreamPacket :: HU.Assertion +case_isPackedAxi4StreamPacket = do + HU.assertBool "expected packed" $ isPackedAxi4StreamPacket [] + HU.assertBool "expected packed" $ isPackedAxi4StreamPacket [DataByte] + HU.assertBool "expected packed" $ isPackedAxi4StreamPacket [DataByte, NullByte] + HU.assertBool "expected packed" $ isPackedAxi4StreamPacket [PositionByte, NullByte] + HU.assertBool "expected packed" $ isPackedAxi4StreamPacket [NullByte, DataByte] + HU.assertBool "expected packed" $ isPackedAxi4StreamPacket [DataByte, NullByte] + HU.assertBool "expected packed" $ isPackedAxi4StreamPacket [NullByte, NullByte, NullByte] + HU.assertBool "expected unpacked" $ (not . isPackedAxi4StreamPacket) [DataByte, NullByte, DataByte] + HU.assertBool "expected unpacked" $ (not . isPackedAxi4StreamPacket) [NullByte, PositionByte, NullByte, PositionByte] + HU.assertBool "expected unpacked" $ (not . isPackedAxi4StreamPacket) [NullByte, DataByte, NullByte, PositionByte] + HU.assertBool "expected unpacked" $ (not . isPackedAxi4StreamPacket) [DataByte, NullByte, PositionByte, NullByte] + +case_isStrictlySparseAxi4StreamPacket :: HU.Assertion +case_isStrictlySparseAxi4StreamPacket = do + HU.assertBool "expected not sparse" $ (not . isStrictlySparseAxi4StreamPacket) [] + HU.assertBool "expected not sparse" $ (not . isStrictlySparseAxi4StreamPacket) [DataByte] + HU.assertBool "expected not sparse" $ (not . isStrictlySparseAxi4StreamPacket) [PositionByte] + HU.assertBool "expected not sparse" $ (not . isStrictlySparseAxi4StreamPacket) [DataByte, NullByte] + HU.assertBool "expected not sparse" $ (not . isStrictlySparseAxi4StreamPacket) [PositionByte, NullByte] + HU.assertBool "expected not sparse" $ (not . isStrictlySparseAxi4StreamPacket) [PositionByte, DataByte] + HU.assertBool "expected not sparse" $ (not . isStrictlySparseAxi4StreamPacket) [PositionByte, DataByte, PositionByte] + HU.assertBool "expected sparse" $ isStrictlySparseAxi4StreamPacket [DataByte, PositionByte, DataByte, PositionByte] + HU.assertBool "expected sparse" $ isStrictlySparseAxi4StreamPacket [DataByte, PositionByte, DataByte] + HU.assertBool "expected sparse" $ isStrictlySparseAxi4StreamPacket [DataByte, PositionByte, DataByte, NullByte] + HU.assertBool "expected sparse" $ isStrictlySparseAxi4StreamPacket [PositionByte, DataByte, PositionByte, DataByte] + +case_isUnalignedAxi4StreamPacket :: HU.Assertion +case_isUnalignedAxi4StreamPacket = do + HU.assertBool "expected unaligned" $ isUnalignedAxi4StreamPacket [PositionByte] + HU.assertBool "expected unaligned" $ isUnalignedAxi4StreamPacket [PositionByte, DataByte] + HU.assertBool "expected unaligned" $ isUnalignedAxi4StreamPacket [DataByte, PositionByte] + HU.assertBool "expected unaligned" $ isUnalignedAxi4StreamPacket [PositionByte, DataByte, PositionByte] + HU.assertBool "expected unaligned" $ isUnalignedAxi4StreamPacket [PositionByte, NullByte, DataByte, PositionByte] + HU.assertBool "expected unaligned" $ isUnalignedAxi4StreamPacket [NullByte, DataByte, PositionByte] + HU.assertBool "expected unaligned" $ isUnalignedAxi4StreamPacket [DataByte, PositionByte, NullByte] + HU.assertBool "expected not unaligned" $ not $ isUnalignedAxi4StreamPacket [] + HU.assertBool "expected not unaligned" $ not $ isUnalignedAxi4StreamPacket [DataByte] + HU.assertBool "expected not unaligned" $ not $ isUnalignedAxi4StreamPacket [DataByte, PositionByte, DataByte] + HU.assertBool "expected not unaligned" $ not $ isUnalignedAxi4StreamPacket [PositionByte, DataByte, PositionByte, DataByte] + HU.assertBool "expected not unaligned" $ not $ isUnalignedAxi4StreamPacket [DataByte, PositionByte, DataByte, PositionByte] + +case_unInterruptedAxi4Packets :: HU.Assertion +case_unInterruptedAxi4Packets = do + HU.assertBool "expected uninterrupted" $ unInterruptedAxi4Packets [Nothing, lastTransfer] + HU.assertBool "expected uninterrupted" $ unInterruptedAxi4Packets [Nothing, lastTransfer, Nothing] + HU.assertBool "expected uninterrupted" $ unInterruptedAxi4Packets [Nothing, payloadTransfer, lastTransfer] + HU.assertBool "expected uninterrupted" $ unInterruptedAxi4Packets [payloadTransfer, payloadTransfer, lastTransfer] + HU.assertBool "expected uninterrupted" $ unInterruptedAxi4Packets [lastTransfer, payloadTransfer, lastTransfer] + HU.assertBool "expected not uninterrupted" $ unInterruptedAxi4Packets [lastTransfer, Nothing, payloadTransfer, lastTransfer] + HU.assertBool "expected not uninterrupted" $ not $ unInterruptedAxi4Packets [Nothing, payloadTransfer, Nothing, lastTransfer] + where + payloadTransfer = Just $ mkDummyM2S (repeat True) False + lastTransfer = Just $ mkDummyM2S (repeat True) True + +case_isSinglePacket :: HU.Assertion +case_isSinglePacket = do + HU.assertBool "expected single packet" $ isSinglePacket [lastTransfer] + HU.assertBool "expected single packet" $ isSinglePacket [payloadTransfer, lastTransfer] + HU.assertBool "expected not single packet" $ not $ isSinglePacket [] + HU.assertBool "expected not single packet" $ not $ isSinglePacket [payloadTransfer] + HU.assertBool "expected not single packet" $ not $ isSinglePacket [lastTransfer, payloadTransfer] + HU.assertBool "expected not single packet" $ not $ isSinglePacket [lastTransfer, payloadTransfer, lastTransfer] + where + payloadTransfer = mkDummyM2S (repeat True) False + lastTransfer = mkDummyM2S (repeat True) True + +case_hasLeadingNullBytes :: HU.Assertion +case_hasLeadingNullBytes = do + HU.assertBool "expected leading null bytes" $ hasLeadingNullBytes [NullByte, DataByte] + HU.assertBool "expected not leading null bytes" $ not $ hasLeadingNullBytes [] + HU.assertBool "expected not leading null bytes" $ not $ hasLeadingNullBytes [DataByte] + HU.assertBool "expected not leading null bytes" $ not $ hasLeadingNullBytes [DataByte, NullByte] + HU.assertBool "expected not leading null bytes" $ not $ hasLeadingNullBytes [NullByte] + +case_hasTrailingNullBytes :: HU.Assertion +case_hasTrailingNullBytes = do + HU.assertBool "expected trailing null bytes" $ hasTrailingNullBytes [DataByte, NullByte] + HU.assertBool "expected not trailing null bytes" $ not $ hasTrailingNullBytes [] + HU.assertBool "expected not trailing null bytes" $ not $ hasTrailingNullBytes [DataByte] + HU.assertBool "expected not trailing null bytes" $ not $ hasTrailingNullBytes [NullByte] + HU.assertBool "expected not trailing null bytes" $ not $ hasTrailingNullBytes [NullByte, DataByte] + +mkDummyM2S :: Vec 4 Bool -> Bool -> Axi4StreamM2S ('Axi4StreamConfig 4 0 0 ) () +mkDummyM2S keep last0 = Axi4StreamM2S + { _tdata = repeat 0 + , _tkeep = keep + , _tstrb = repeat True + , _tlast = last0 + , _tid = 0 + , _tdest = 0 + , _tuser = () + } diff --git a/bittide/tests/Tests/Axi4/Types.hs b/bittide/tests/Tests/Axi4/Types.hs new file mode 100644 index 000000000..8040e67a4 --- /dev/null +++ b/bittide/tests/Tests/Axi4/Types.hs @@ -0,0 +1,115 @@ +-- SPDX-FileCopyrightText: 2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 + +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE FlexibleContexts #-} + +module Tests.Axi4.Types where + +import Clash.Prelude + +import Protocols.Axi4.Stream +import Data.Maybe +import Bittide.Extra.Maybe +import Clash.Sized.Vector (unsafeFromList) + +import qualified Data.List as L + +type Packet = [Unsigned 8] + +-- | Bytes in Axi4StreamM2S transfer +data AxiByte + = Null + | Data (Unsigned 8) + | Position (Unsigned 8) + deriving (Generic, NFDataX, Show, Eq) + +-- | Different types of bytes in Axi4StreamM2S transfer +data AxiByteType + = NullByte + | DataByte + | PositionByte + deriving (Generic, NFDataX, Show, Eq) + +type Keep = Bool +type Strobe = Bool + +-- | Get a list of bytes for a given Axi4StreamM2S transaction +getTransferBytes :: Axi4StreamM2S conf a -> Vec (DataWidth conf) AxiByte +getTransferBytes Axi4StreamM2S{..} = zipWith3 getByte _tkeep _tstrb _tdata + +-- | Get a byte based on a keep, strobe and data value +getByte :: Keep -> Strobe -> Unsigned 8 -> AxiByte +getByte True True d = Data d +getByte True False p = Position p +getByte False False _ = Null +getByte False True _ = deepErrorX "Reserved byte" + +-- | Get a list of byte types from an Axi4StreamM2S packet. +-- Input must satisfy `isSinglePacket` +getPacketByteTypes :: [Axi4StreamM2S conf a] -> [AxiByteType] +getPacketByteTypes = L.concatMap (toList . fmap getByteType . getTransferBytes) + +-- | Get the byte type based on a keep and strobe value +getByteType :: AxiByte-> AxiByteType +getByteType (Data _) = DataByte +getByteType (Position _) = PositionByte +getByteType Null = NullByte + +-- | Get the keep and strobe values based on a byte type +getKeepStrobe :: AxiByteType -> (Keep, Strobe) +getKeepStrobe NullByte = (False, False) +getKeepStrobe DataByte = (True, True) +getKeepStrobe PositionByte = (True, False) + +-- | Transform a list of Axi Stream operations into a 'Packet'. +axiStreamToPackets :: + KnownNat nBytes => + [Axi4StreamM2S ('Axi4StreamConfig nBytes 0 0) ()] -> + [Packet] +axiStreamToPackets = L.reverse . snd . L.foldl go ([], []) + where + go (partialPacket, packets) Axi4StreamM2S{..} + | _tlast = ([], L.reverse newPartial : packets) + | otherwise = (newPartial, packets) + where + newPartial = L.reverse (catMaybes (toList $ orNothing <$> _tkeep <*> _tdata)) <> partialPacket + +-- Transform a 'Packet' into a list of Axi Stream operations. +packetToAxiStream :: + forall nBytes . + SNat nBytes -> + Packet -> + [Maybe (Axi4StreamM2S ('Axi4StreamConfig nBytes 0 0) ())] +packetToAxiStream w@SNat !bs + | rest /= [] = Just axis : packetToAxiStream w rest + | otherwise = [Just axis] + where + busWidth = natToNum @nBytes + (firstWords, rest) = L.splitAt busWidth bs + word = L.take busWidth (firstWords <> L.repeat 0) + axis = Axi4StreamM2S + { _tdata = unsafeFromList word + , _tkeep = keeps + , _tstrb = repeat True + , _tlast = null rest + , _tid = 0 + , _tdest = 0 + , _tuser = deepErrorX "" + } + keeps = unsafeFromList $ + L.replicate (L.length bs) True <> L.repeat False + +-- | Separate a list of Axi4Stream operations into a list of Axi4Stream packets. +separatePackets :: + forall nBytes . + KnownNat nBytes => + [Axi4StreamM2S ('Axi4StreamConfig nBytes 0 0) ()] -> + [ Either + [Axi4StreamM2S ('Axi4StreamConfig nBytes 0 0) ()] + [Axi4StreamM2S ('Axi4StreamConfig nBytes 0 0) ()]] +separatePackets [] = [] +separatePackets axis = case L.break _tlast axis of + (payload, l:rest) -> Right (payload <> [l]) : separatePackets rest + (remainder, _) -> [Left remainder] diff --git a/bittide/tests/UnitTests.hs b/bittide/tests/UnitTests.hs index 49850a0d0..adc2f06eb 100644 --- a/bittide/tests/UnitTests.hs +++ b/bittide/tests/UnitTests.hs @@ -10,10 +10,13 @@ import Test.Tasty import Test.Tasty.Hedgehog import qualified Tests.Axi4 +import qualified Tests.Axi4.Generators +import qualified Tests.Axi4.Properties import qualified Tests.Calendar import qualified Tests.ClockControl.Si539xSpi import qualified Tests.DoubleBufferedRam import qualified Tests.ElasticBuffer +import qualified Tests.Haxioms import qualified Tests.Link import qualified Tests.ProcessingElement.ReadElf import qualified Tests.ScatterGather @@ -23,8 +26,6 @@ import qualified Tests.Transceiver import qualified Tests.Transceiver.Prbs import qualified Tests.Transceiver.WordAlign import qualified Tests.Wishbone -import qualified Tests.Axi4.Generators -import qualified Tests.Haxioms tests :: TestTree tests = testGroup "Unittests" @@ -43,6 +44,7 @@ tests = testGroup "Unittests" , Tests.Transceiver.WordAlign.tests , Tests.Wishbone.tests , Tests.Axi4.Generators.tests + , Tests.Axi4.Properties.tests , Tests.Haxioms.tests ]