Merge pull request #156 from clash-lang/lucas/improve-expect-options

Author: lmbollen

clash-protocols/src/Protocols/Hedgehog.hs

@@ -23,6 +23,7 @@ module Protocols.Hedgehog (
   genStallAck,
   genStallMode,
   genStalls,
+  expectedEmptyCycles,
 ) where
 
 -- base
@@ -64,16 +65,6 @@ 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))
-    ]
-
 {- | Attach a timeout to a property. Fails if the property does not finish in
 the given time. The timeout is given in milliseconds.
 -}
@@ -120,11 +111,12 @@ propWithModel eOpts genData model prot prop =
     when (eoTrace eOpts) $ liftIO $ putStr "propWithModel: dat: " >> print dat
 
     -- TODO: Different 'n's for each output
-    n <- H.forAll (Gen.integral (Range.linear 0 (eoSampleMax eOpts)))
+    n <- H.forAll (Gen.integral (Range.linear 0 (eoStallsMax eOpts)))
     when (eoTrace eOpts) $ liftIO $ putStr "propWithModel: n: " >> print n
 
     -- TODO: Different distributions?
-    let genStall = genSmallInt
+    let
+      genStall = Gen.int (Range.linear 1 eOpts.eoConsecutiveStalls)
 
     -- 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

clash-protocols/src/Protocols/Hedgehog/Internal.hs

@@ -29,9 +29,12 @@ import Clash.Prelude qualified as C
 import Hedgehog qualified as H
 import Hedgehog.Internal.Property qualified as H
 
-{- | Resets for 30 cycles, checks for superfluous data for 50 cycles after
-seeing last valid data cycle, and times out after seeing 1000 consecutive
-empty cycles.
+{- | Conservative settings for `ExpectOptions`:
+- Reset for 30 cycles
+- Insert at most 10 stall moments
+- Every stall moment is at most 10 cycles long
+- Sample at most 1000 cycles
+- Automatically derive when to stop sampling empty samples using `expectedEmptyCycles`.
 -}
 defExpectOptions :: ExpectOptions
 defExpectOptions =
@@ -41,8 +44,10 @@ defExpectOptions =
       --      increase the time it takes to run the tests. This is because
       --      the test will run for at least the number of cycles specified
       --      in 'eoStopAfterEmpty'.
-      eoStopAfterEmpty = 256
-    , eoSampleMax = 256
+      eoStopAfterEmpty = Nothing
+    , eoSampleMax = 1000
+    , eoStallsMax = 10
+    , eoConsecutiveStalls = 10
     , eoResetCycles = 30
     , eoDriveEarly = True
     , eoTimeoutMs = Nothing
@@ -57,9 +62,10 @@ instance (TestType a, C.KnownDomain dom) => Test (Df dom a) where
     ExpectOptions ->
     [Maybe a] ->
     m [a]
-  expectN Proxy (ExpectOptions{eoSampleMax, eoStopAfterEmpty}) sampled = do
-    go eoSampleMax eoStopAfterEmpty sampled
+  expectN Proxy eOpts sampled = do
+    go eOpts.eoSampleMax maxEmptyCycles sampled
    where
+    maxEmptyCycles = expectedEmptyCycles eOpts
     go :: (HasCallStack) => Int -> Int -> [Maybe a] -> m [a]
     go _timeout _n [] =
       -- This really should not happen, protocols should produce data indefinitely
@@ -69,7 +75,7 @@ instance (TestType a, C.KnownDomain dom) => Test (Df dom a) where
       H.failWith
         Nothing
         ( "Sample limit reached after sampling "
-            <> show eoSampleMax
+            <> show eOpts.eoSampleMax
             <> " samples. "
             <> "Consider increasing 'eoSampleMax' in 'ExpectOptions'."
         )
@@ -78,7 +84,7 @@ instance (TestType a, C.KnownDomain dom) => Test (Df dom a) where
       pure []
     go sampleTimeout _emptyTimeout (Just a : as) =
       -- Valid sample
-      (a :) <$> go (sampleTimeout - 1) eoStopAfterEmpty as
+      (a :) <$> go (sampleTimeout - 1) maxEmptyCycles as
     go sampleTimeout emptyTimeout (Nothing : as) =
       -- Empty sample
       go sampleTimeout (emptyTimeout - 1) as

clash-protocols/src/Protocols/Hedgehog/Types.hs

@@ -9,6 +9,7 @@ module Protocols.Hedgehog.Types where
 import Control.DeepSeq
 
 import Clash.Prelude qualified as C
+import Data.Maybe (fromMaybe)
 import Data.Proxy
 import GHC.Stack (HasCallStack)
 import Protocols.Internal.Types
@@ -23,14 +24,16 @@ instance (NFData a, C.NFDataX a, C.ShowX a, C.Show a, Eq a) => TestType a
 
 -- | Options for 'expectN' function. See individual fields for more information.
 data ExpectOptions = ExpectOptions
-  { eoStopAfterEmpty :: Int
-  -- ^ Stop sampling after seeing /n/ consecutive empty samples
+  { eoStopAfterEmpty :: Maybe Int
+  -- ^ Explicitly control the number of samples empty samples simulate before we stop
+  -- the simulation. When set to `Nothing`, this is derived using `expectedEmptyCycles`.
   , eoSampleMax :: Int
   -- ^ Produce an error if the circuit produces more than /n/ valid samples. This
   -- is used to terminate (potentially) infinitely running circuits.
-  --
-  -- This number is used to generate stall information, so setting it to
-  -- unreasonable values will result in long runtimes.
+  , eoStallsMax :: Int
+  -- ^ Generate at most /n/ stall moments of zero or more cycles(set by 'eoConsecutiveStalls').
+  , eoConsecutiveStalls :: Int
+  -- ^ Maximum number of consecutive stalls that are allowed to be inserted.
   , eoResetCycles :: Int
   -- ^ Ignore first /n/ cycles
   , eoDriveEarly :: Bool
@@ -42,6 +45,16 @@ data ExpectOptions = ExpectOptions
   -- ^ Trace data generation for debugging purposes
   }
 
+-- | Default derivation of `eoStopAfterEmpty` when it is set to `Nothing`.
+expectedEmptyCycles :: ExpectOptions -> Int
+expectedEmptyCycles eOpts =
+  -- +2 on `eoStallsMax` to account worst case left side stalling + right side stalling
+  -- +1 on `eoConsecutiveStalls` to consume 1 sample after stalling
+  -- +100 arbitrarily chosen to allow the circuit to have some internal latency.
+  fromMaybe
+    (eOpts.eoStallsMax * (eOpts.eoConsecutiveStalls + 1) + eOpts.eoResetCycles + 100)
+    eOpts.eoStopAfterEmpty
+
 {- | Provides a way of comparing expected data with data produced by a
 protocol component.
 -}

clash-protocols/src/Protocols/Wishbone/Standard/Hedgehog.hs

@@ -670,6 +670,6 @@ sampleUnfiltered ::
   Circuit (Wishbone dom mode addressWidth a) () ->
   [(WishboneM2S addressWidth (BitSize a `DivRU` 8) a, WishboneS2M a)]
 sampleUnfiltered eOpts manager subordinate =
-  takeWhileAnyInWindow (eoStopAfterEmpty eOpts) hasBusActivity $
+  takeWhileAnyInWindow (expectedEmptyCycles eOpts) hasBusActivity $
     uncurry P.zip $
       observeComposedWishboneCircuit manager subordinate

clash-protocols/tests/Tests/Protocols/PacketStream/Converters.hs

@@ -42,7 +42,7 @@ generateDownConverterProperty ::
   Property
 generateDownConverterProperty SNat SNat =
   idWithModelSingleDomain
-    defExpectOptions{eoSampleMax = 1000}
+    defExpectOptions
     (genPackets 1 8 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 10)))
     (exposeClockResetEnable (upConvert . downConvert))
     (exposeClockResetEnable @System (downConverterC @dwOut @n @Int))

clash-protocols/tests/Tests/Protocols/PacketStream/Depacketizers.hs

@@ -44,7 +44,7 @@ depacketizerPropGen ::
 depacketizerPropGen SNat SNat metaGen toMetaOut =
   idWithModelSingleDomain
     @System
-    defExpectOptions{eoSampleMax = 1000, eoStopAfterEmpty = 1000}
+    defExpectOptions
     (genPackets 1 4 (genValidPacket defPacketOptions metaGen (Range.linear 0 30)))
     (exposeClockResetEnable (depacketizerModel toMetaOut))
     (exposeClockResetEnable ckt)
@@ -80,7 +80,7 @@ depacketizeToDfPropGen ::
 depacketizeToDfPropGen SNat SNat metaGen toOut =
   idWithModelSingleDomain
     @System
-    defExpectOptions{eoSampleMax = 1000, eoStopAfterEmpty = 1000}
+    defExpectOptions
     (genPackets 1 10 (genValidPacket defPacketOptions metaGen (Range.linear 0 20)))
     (exposeClockResetEnable (depacketizeToDfModel toOut))
     (exposeClockResetEnable ckt)

clash-protocols/tests/Tests/Protocols/PacketStream/PacketFifo.hs

@@ -55,7 +55,7 @@ prop_packet_fifo_small_buffer_id :: Property
 prop_packet_fifo_small_buffer_id =
   idWithModelSingleDomain
     @System
-    defExpectOptions{eoStopAfterEmpty = 1000}
+    defExpectOptions{eoStopAfterEmpty = Just 500} -- To account for empty cycles due to dropped packets
     (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 30)))
     (exposeClockResetEnable (dropBigPackets d3 . dropAbortedPackets))
     (exposeClockResetEnable (packetFifoC @_ @1 @Int16 d3 d5 Backpressure))
@@ -78,7 +78,7 @@ prop_overFlowDrop_packetFifo_id :: Property
 prop_overFlowDrop_packetFifo_id =
   idWithModelSingleDomain
     @System
-    defExpectOptions{eoStopAfterEmpty = 1000}
+    defExpectOptions
     (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 10)))
     (exposeClockResetEnable dropAbortedPackets)
     (exposeClockResetEnable (packetFifoC @_ @1 @Int16 d10 d10 Drop))

clash-protocols/tests/Tests/Protocols/PacketStream/Routing.hs

@@ -39,7 +39,7 @@ makePropPacketArbiter ::
 makePropPacketArbiter SNat SNat mode =
   propWithModelSingleDomain
     @System
-    defExpectOptions{eoSampleMax = 1000}
+    defExpectOptions
     genSources
     (exposeClockResetEnable L.concat)
     (exposeClockResetEnable (packetArbiterC mode))
@@ -87,7 +87,7 @@ makePropPacketDispatcher ::
   Property
 makePropPacketDispatcher SNat fs =
   idWithModelSingleDomain @System
-    defExpectOptions{eoSampleMax = 2000, eoStopAfterEmpty = 1000}
+    defExpectOptions
     (genPackets 1 10 (genValidPacket defPacketOptions Gen.enumBounded (Range.linear 0 6)))
     (exposeClockResetEnable (model 0))
     (exposeClockResetEnable (packetDispatcherC fs))