From e5adc935f786239a203a6f8820f99a324a3706ab Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Fri, 7 Feb 2025 16:32:13 +0100 Subject: [PATCH] Add tests for `switchDemoPe` --- bittide/bittide.cabal | 1 + .../Tests/SwitchDemoProcessingElement.hs | 140 ++++++++++++++++++ bittide/tests/UnitTests.hs | 2 + 3 files changed, 143 insertions(+) create mode 100644 bittide/tests/Tests/SwitchDemoProcessingElement.hs diff --git a/bittide/bittide.cabal b/bittide/bittide.cabal index 877082310..45b2883fc 100644 --- a/bittide/bittide.cabal +++ b/bittide/bittide.cabal @@ -222,6 +222,7 @@ test-suite unittests Tests.Shared Tests.StabilityChecker Tests.Switch + Tests.SwitchDemoProcessingElement Tests.Transceiver Tests.Transceiver.Prbs Tests.Transceiver.WordAlign diff --git a/bittide/tests/Tests/SwitchDemoProcessingElement.hs b/bittide/tests/Tests/SwitchDemoProcessingElement.hs new file mode 100644 index 000000000..700b2cd22 --- /dev/null +++ b/bittide/tests/Tests/SwitchDemoProcessingElement.hs @@ -0,0 +1,140 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE NumericUnderscores #-} + +module Tests.SwitchDemoProcessingElement where + +import Clash.Prelude hiding (someNatVal, withSomeSNat) + +import Test.Tasty +import Test.Tasty.Hedgehog + +import Data.Proxy (Proxy (..)) +import GHC.TypeNats (someNatVal) + +import Bittide.SwitchDemoProcessingElement + +import qualified Hedgehog as H +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import qualified Clash.Explicit.Prelude as E +import qualified Data.List as L + +import Clash.Explicit.Reset (noReset) +import Clash.Hedgehog.Sized.BitVector (genDefinedBitVector) +import Clash.Hedgehog.Sized.Index (genIndex) +import Clash.Hedgehog.Sized.Unsigned (genUnsigned) +import Hedgehog ((===)) + +main :: IO () +main = defaultMain tests + +tests :: TestTree +tests = + testGroup + "SwitchDemoProcessingElement" + [ testPropertyNamed "prop_writeAfterRead" "prop_writeAfterRead" prop_writeAfterRead + ] + +withSomeSNat :: Natural -> (forall (n :: Nat). SNat n -> r) -> r +withSomeSNat n f = case someNatVal n of + SomeNat (_ :: Proxy n) -> f (SNat @n) + +linearLength :: (Integral a) => a -> a -> Range.Range a +linearLength start len = Range.linear start (start + len) + +singletonInt :: (Integral a) => a -> Range.Range Int +singletonInt = Range.singleton . fromIntegral + +prop_writeAfterRead :: H.Property +prop_writeAfterRead = H.property $ do + nNodesMinusOne <- H.forAll $ Gen.integral (Range.linear 0 10) + withSomeSNat nNodesMinusOne $ \(succSNat -> nNodesSNat@(SNat :: SNat nNodes)) -> do + nReadTriCycles <- H.forAll $ genIndex Range.linearBounded + nWriteTriCycles <- H.forAll $ genIndex Range.linearBounded + + let + cyclesPerNode = 3 :: Unsigned 64 + nReadCycles = cyclesPerNode * fromIntegral nReadTriCycles + nWriteCycles = cyclesPerNode * fromIntegral nWriteTriCycles + maxIdle1 = 100 + maxIdle2 = 100 + + -- Notice that the PE needs a single clock cycle in its idle state to function + -- correctly. Hence, we always start reading a minimum at clockStart+1. + readData <- H.forAll $ Gen.list (singletonInt nReadCycles) genDefinedBitVector + clockStart <- H.forAll $ genUnsigned @_ @64 (Range.linear 0 100) + readStart <- H.forAll $ genUnsigned @_ @64 (linearLength (clockStart+1) maxIdle1) + let readEnd = readStart + fromIntegral nReadCycles + writeStart <- H.forAll $ genUnsigned @_ @64 (linearLength readEnd maxIdle2) + deviceDna <- H.forAll genDefinedBitVector + + let + idle1length = readStart - clockStart + idle2length = writeStart - readEnd + idle1in = L.replicate (fromIntegral idle1length) 0 + crossBarIn = fromList (idle1in <> readData <> L.repeat 0) + + out = + E.sample + $ bundle + $ withClockResetEnable @System clockGen noReset enableGen + $ switchDemoPe + nNodesSNat + (fromList [clockStart ..]) + crossBarIn + (pure (Just deviceDna)) + (pure readStart) + (pure nReadTriCycles) + (pure writeStart) + (pure nWriteTriCycles) + + (idle1out, rest0) = L.splitAt (fromIntegral idle1length) out + (readOut, rest1) = L.splitAt (fromIntegral nReadCycles) rest0 + (idle2out, rest2) = L.splitAt (fromIntegral idle2length) rest1 + (writeOut, rest3) = L.splitAt (fromIntegral nWriteCycles) rest2 + + (idle1outs, _idle1buffers) = L.unzip idle1out + (readOuts, _readBuffers) = L.unzip readOut + (idle2outs, _idle2buffers) = L.unzip idle2out + (writeOuts, _writeBuffers) = L.unzip writeOut + (_restOuts, restBuffers) = L.unzip rest3 + + H.footnote $ "idle1in: " <> show idle1in + H.footnote $ "idle1length: " <> show idle1length + H.footnote $ "idle2length: " <> show idle2length + H.footnote $ "nReadCycles: " <> show nReadCycles + H.footnote $ "nWriteCycles: " <> show nWriteCycles + H.footnote $ "readData: " <> show readData + H.footnote $ "readEnd: " <> show readEnd + H.footnote $ "readStart: " <> show readStart + H.footnote $ "writeStart: " <> show writeStart + H.footnote $ "clockStart: " <> show clockStart + H.footnote $ "idle2outs: " <> showX idle2outs + H.footnote $ "nNodesSNat: " <> show nNodesSNat + + -- Check that at the end of the simulation the buffer is what we expect it + -- to be. The buffer should be equal to the data we send to the PE. We don't + -- care about data we don't write, hence we truncate (L.take) the buffer to + -- match the number of read cycles. + case restBuffers of + [] -> error "Unexpected end of output" + (buffer : _) -> do + H.footnote $ "buffer: " <> show buffer + L.take (fromIntegral nReadCycles) (toList buffer) === readData + + -- Check that idle value is written at correct times + let idleValue = 0xAAAA_BBBB_AAAA_BBBB + idle1outs === L.replicate (L.length idle1outs) idleValue + readOuts === L.replicate (L.length readOuts) idleValue + idle2outs === L.replicate (L.length idle2outs) idleValue + + -- Check that the right data is written the crossbar link at the time we + -- expect it to. + let + relevantOutCycles = fromIntegral (min nWriteCycles nReadCycles) + deviceDnaVec = bitCoerce @_ @(Vec 2 (BitVector 64)) (zeroExtend deviceDna) + expectedOutData = toList (pack writeStart :> deviceDnaVec) <> readData + L.take relevantOutCycles writeOuts === L.take relevantOutCycles expectedOutData + + pure () diff --git a/bittide/tests/UnitTests.hs b/bittide/tests/UnitTests.hs index e4fa57950..40f7587b7 100644 --- a/bittide/tests/UnitTests.hs +++ b/bittide/tests/UnitTests.hs @@ -21,6 +21,7 @@ import qualified Tests.ProcessingElement.ReadElf import qualified Tests.ScatterGather import qualified Tests.StabilityChecker import qualified Tests.Switch +import qualified Tests.SwitchDemoProcessingElement import qualified Tests.Transceiver import qualified Tests.Transceiver.Prbs import qualified Tests.Transceiver.WordAlign @@ -36,6 +37,7 @@ tests = , Tests.DoubleBufferedRam.tests , Tests.ElasticBuffer.tests , Tests.ProcessingElement.ReadElf.tests + , Tests.SwitchDemoProcessingElement.tests , Tests.ScatterGather.tests , Tests.StabilityChecker.tests , Tests.Switch.tests