Add prop_fanin

Author: lmbollen

bittide-extra/src/Protocols/BiDf.hs

@@ -130,7 +130,10 @@ dimap ::
   Circuit (BiDf dom req resp') (BiDf dom req' resp)
 dimap f g = mapC (Df.map f) (Df.map g)
 
--- | Merge a number of 'BiDf's, preferring requests from the last channel.
+{- | Merge a number of 'BiDf's, preferring requests from the last channel.
+TODO: Check why this does not work if we insert delays on the individual `Df` channels of the
+right hand side `BiDf`s. See `Tests.Protocols.BiDf.prop_fanin`.
+-}
 fanin ::
   forall n dom req resp.
   ( KnownNat n

bittide-extra/tests/unittests/Tests/Protocols/BiDf.hs

@@ -10,17 +10,20 @@ import Clash.Hedgehog.Sized.Vector (genVec)
 import Hedgehog (Gen, Property)
 import Protocols
 import Protocols.BiDf as BiDf
+import Protocols.Extra (fmapC)
 import Protocols.Hedgehog (ExpectOptions (eoResetCycles), defExpectOptions)
 import Test.Tasty (TestTree)
 import Test.Tasty.Hedgehog.Extra (testProperty)
 import Test.Tasty.TH (testGroupGenerator)
 
+import qualified Data.List as L
 import qualified Hedgehog as H
 import qualified Hedgehog.Gen as Gen
 import qualified Hedgehog.Range as Range
 import qualified Protocols.Df as Df
 import qualified Protocols.Df.Extra as Df
 import qualified Protocols.Hedgehog as PH
+import qualified Protocols.Vec as Vec
 
 smallInt :: Gen Int
 smallInt = Gen.integral (Range.linear 0 10)
@@ -75,5 +78,31 @@ prop_fromDfs_toDfs_id = H.property $ do
   gen :: Gen [Int]
   gen = Gen.list (Range.linear 0 10) smallInt
 
+prop_fanin :: Property
+prop_fanin = H.property $ do
+  -- stalls <- H.forAll genStalls
+  let
+    impl ::
+      forall dom.
+      (HiddenClockResetEnable dom) =>
+      Circuit (Vec 3 (Df dom Int)) (Vec 3 (Df dom Int))
+    impl = circuit $ \reqs -> do
+      (biDfs, resps) <- Vec.unzip <| fmapC (BiDf.fromDfs) -< reqs
+      respBiDf <- BiDf.fanin -< biDfs
+      resp0 <- BiDf.toDfs -< (respBiDf, resp0)
+      -- resp1 <- Df.bypassFifo d2 (Df.fifo d8) -< resp0
+      idC -< resps
+  PH.propWithModelSingleDomainT @System
+    defExpectOptions
+    gen
+    (\_ _ _ -> id)
+    (exposeClockResetEnable impl)
+    prop
+ where
+  gen :: Gen (Vec 3 [Int])
+  gen = genVec (Gen.list (Range.linear 0 10) smallInt)
+  -- Since stalling can change the order of the samples, we only check if they are all present
+  prop expected sampled = L.sort (L.concat (toList sampled)) H.=== L.sort (L.concat (toList expected))
+
 tests :: TestTree
 tests = $(testGroupGenerator)