Add tests for switchDemoPe

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

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 ()

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