Do not verify lengths in propWithModel

clash-protocols.cabal

@@ -135,7 +135,8 @@ library
 
   build-depends:
       -- inline-circuit-notation
-      circuit-notation
+    , circuit-notation
+    , clash-prelude-hedgehog
     , data-default
     , deepseq
     , extra

src/Protocols/Avalon/Stream.hs

@@ -251,9 +251,8 @@ instance
   ) =>
   Test (AvalonStream dom conf dataType)
   where
-  expectToLengths Proxy = pure . P.length
-  expectN Proxy options nExpected sampled =
-    expectN (Proxy @(Df.Df dom _)) options nExpected
+  expectN Proxy options sampled =
+    expectN (Proxy @(Df.Df dom _)) options
       $ Df.maybeToData
       <$> sampled
 

src/Protocols/Axi4/Stream.hs

@@ -17,7 +17,6 @@
 import Data.Hashable (Hashable, hashWithSalt)
 import qualified Data.Maybe as Maybe
 import Data.Proxy
-import qualified Prelude as P
 
 -- clash-prelude
 import Clash.Prelude hiding (concat, length, take)
@@ -103,7 +102,7 @@
 the '_tready' signal.
 -}
 newtype Axi4StreamS2M = Axi4StreamS2M {_tready :: Bool}
   deriving (Generic, C.NFDataX, C.ShowX, Eq, NFData, Show, Bundle)
 
 -- | Type for AXI4 Stream protocol.
 data Axi4Stream (dom :: Domain) (conf :: Axi4StreamConfig) (userType :: Type)
@@ -129,7 +128,7 @@
     s0 = ()
     blankOtp = Nothing
     stateFn ack _ otpItem =
-      pure (otpItem, Nothing, Maybe.isJust otpItem && _tready ack)
+      pure (otpItem, Nothing, Maybe.isJust otpItem C.&& _tready ack)
 
   fromDfCircuit proxy = DfConv.fromDfCircuitHelper proxy s0 blankOtp stateFn
    where
@@ -153,9 +152,9 @@
   sigToSimFwd _ s = sample_lazy s
   sigToSimBwd _ s = sample_lazy s
 
-  stallC conf (head -> (stallAck, stalls)) =
-    withClockResetEnable clockGen resetGen enableGen
-      $ DfConv.stall Proxy Proxy conf stallAck stalls
+  stallC conf (C.head -> (stallAck, stalls)) =
+    withClockResetEnable clockGen resetGen enableGen $
+      DfConv.stall Proxy Proxy conf stallAck stalls
 
 instance
   (KnownAxi4StreamConfig conf, NFDataX userType, KnownDomain dom) =>
@@ -169,12 +168,12 @@
   fromSimulateType Proxy = Maybe.catMaybes
 
   driveC conf vals =
-    withClockResetEnable clockGen resetGen enableGen
-      $ DfConv.drive Proxy conf vals
+    withClockResetEnable clockGen resetGen enableGen $
+      DfConv.drive Proxy conf vals
   sampleC conf ckt =
-    withClockResetEnable clockGen resetGen enableGen
-      $ DfConv.sample Proxy conf
-      $ ckt
+    withClockResetEnable clockGen resetGen enableGen $
+      DfConv.sample Proxy conf $
+        ckt
 
 instance
   ( KnownAxi4StreamConfig conf
@@ -187,11 +186,10 @@
   ) =>
   Test (Axi4Stream dom conf userType)
   where
-  expectToLengths Proxy = pure . P.length
-  expectN Proxy options nExpected sampled =
-    expectN (Proxy @(Df.Df dom _)) options nExpected
-      $ Df.maybeToData
-      <$> sampled
+  expectN Proxy options sampled =
+    expectN (Proxy @(Df.Df dom _)) options $
+      Df.maybeToData
+        <$> sampled
 
 instance IdleCircuit (Axi4Stream dom conf userType) where
   idleFwd Proxy = C.pure Nothing

src/Protocols/Hedgehog.hs

@@ -41,8 +41,10 @@ import Protocols.Hedgehog.Internal
 -- clash-prelude
 import qualified Clash.Prelude as C
 
--- hedgehog
+-- clash-prelude-hedgehog
+import Clash.Hedgehog.Sized.Vector (genVec)
 
+-- hedgehog
 import Hedgehog ((===))
 import qualified Hedgehog as H
 import qualified Hedgehog.Gen as Gen
@@ -60,6 +62,16 @@ resetGen n =
   C.unsafeFromActiveHigh
     (C.fromList (replicate n True <> repeat False))
 
+smallInt :: H.Range Int
+smallInt = Range.linear 0 10
+
+genSmallInt :: H.Gen Int
+genSmallInt =
+  Gen.frequency
+    [ (90, Gen.integral smallInt)
+    , (10, Gen.constant (Range.lowerBound 99 smallInt))
+    ]
+
 {- | Test a protocol against a pure model implementation. Circuit under test will
 be arbitrarily stalled on the left hand and right hand side and tested for
 a number of properties:
@@ -89,21 +101,23 @@ propWithModel ::
   H.Property
 propWithModel eOpts genData model prot prop = H.property $ do
   dat <- H.forAll genData
-  let n = maximum (expectToLengths (Proxy @a) dat)
+
+  -- TODO: Different 'n's for each output
+  n <- H.forAll (Gen.integral (Range.linear 0 (eoSampleMax eOpts)))
 
   -- TODO: Different distributions?
-  let genStall = Gen.integral (Range.linear 0 10)
+  let genStall = genSmallInt
 
   -- Generate stalls for LHS part of the protocol. The first line determines
   -- whether to stall or not. The second determines how many cycles to stall
   -- on each _valid_ cycle.
-  lhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels a) genStallMode))
+  lhsStallModes <- H.forAll (genVec genStallMode)
   lhsStalls <- H.forAll (traverse (genStalls genStall n) lhsStallModes)
 
   -- Generate stalls for RHS part of the protocol. The first line determines
   -- whether to stall or not. The second determines how many cycles to stall
   -- on each _valid_ cycle.
-  rhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels b) genStallMode))
+  rhsStallModes <- H.forAll (genVec genStallMode)
   rhsStalls <- H.forAll (traverse (genStalls genStall n) rhsStallModes)
 
   let
@@ -121,10 +135,9 @@ propWithModel eOpts genData model prot prop = H.property $ do
         |> prot
         |> rhsStallC
     sampled = sampleC simConfig stalledProtocol
-    lengths = expectToLengths (Proxy @b) expected
 
   -- expectN errors if circuit does not produce enough data
-  trimmed <- expectN (Proxy @b) eOpts lengths sampled
+  trimmed <- expectN (Proxy @b) eOpts sampled
 
   _ <- H.evalNF trimmed
   _ <- H.evalNF expected