From c0a95bada5e17c2d9ba62949020eaf974682045f Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Sat, 20 Jul 2024 09:53:02 +0200 Subject: [PATCH] Do not verify lengths in `propWithModel` The input length is not always equal to the output length, nor even predictable. Furthermore, some properties might not be interested in the length in the first place. Fixes #81 --- clash-protocols.cabal | 3 +- src/Protocols/Avalon/Stream.hs | 5 +- src/Protocols/Axi4/Stream.hs | 28 ++-- src/Protocols/Hedgehog.hs | 27 +++- src/Protocols/Hedgehog/Internal.hs | 167 +++++--------------- src/Protocols/Wishbone/Standard/Hedgehog.hs | 10 +- tests/Tests/Protocols/Df.hs | 6 +- tests/Tests/Protocols/DfConv.hs | 2 +- 8 files changed, 89 insertions(+), 159 deletions(-) diff --git a/clash-protocols.cabal b/clash-protocols.cabal index fc216ddb..ab5f0aaa 100644 --- a/clash-protocols.cabal +++ b/clash-protocols.cabal @@ -135,7 +135,8 @@ library build-depends: -- inline-circuit-notation - circuit-notation + , circuit-notation + , clash-prelude-hedgehog , data-default , deepseq , extra diff --git a/src/Protocols/Avalon/Stream.hs b/src/Protocols/Avalon/Stream.hs index acdae9fc..af5167d0 100644 --- a/src/Protocols/Avalon/Stream.hs +++ b/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 diff --git a/src/Protocols/Axi4/Stream.hs b/src/Protocols/Axi4/Stream.hs index e18bf26b..4c093d8d 100644 --- a/src/Protocols/Axi4/Stream.hs +++ b/src/Protocols/Axi4/Stream.hs @@ -17,7 +17,6 @@ import Control.DeepSeq (NFData) 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) @@ -129,7 +128,7 @@ instance 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 @@ instance 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 @@ instance 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 @@ instance ) => 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 diff --git a/src/Protocols/Hedgehog.hs b/src/Protocols/Hedgehog.hs index df016b2f..a348782b 100644 --- a/src/Protocols/Hedgehog.hs +++ b/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 diff --git a/src/Protocols/Hedgehog/Internal.hs b/src/Protocols/Hedgehog/Internal.hs index f7762333..613f5d90 100644 --- a/src/Protocols/Hedgehog/Internal.hs +++ b/src/Protocols/Hedgehog/Internal.hs @@ -11,11 +11,8 @@ Internals for "Protocols.Hedgehog". module Protocols.Hedgehog.Internal where -- base - -import Control.Monad (forM) -import Data.Maybe (fromMaybe) import Data.Proxy (Proxy (Proxy)) -import GHC.Stack (HasCallStack, withFrozenCallStack) +import GHC.Stack (HasCallStack) import Prelude -- clash-protocols @@ -33,17 +30,17 @@ import Control.DeepSeq -- hedgehog import qualified Hedgehog as H import qualified Hedgehog.Internal.Property as H -import qualified Hedgehog.Internal.Show as H - --- pretty-show -import Text.Show.Pretty (ppShow) -- | Options for 'expectN' function. See individual fields for more information. data ExpectOptions = ExpectOptions - { eoEmptyTail :: Int - -- ^ Sample /n/ cycles after last expected value and check for emptiness - , eoTimeout :: Maybe Int - -- ^ Timeout after seeing /n/ empty cycles + { eoStopAfterEmpty :: Int + -- ^ Stop sampling after seeing /n/ consecutive empty samples + , 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. , eoResetCycles :: Int -- ^ Ignore first /n/ cycles , eoDriveEarly :: Bool @@ -58,8 +55,13 @@ empty cycles. defExpectOptions :: ExpectOptions defExpectOptions = ExpectOptions - { eoEmptyTail = 50 - , eoTimeout = Just 1000 + { -- XXX: These numbers are arbitrary, and should be adjusted to fit the + -- protocol being tested. Annoyingly, upping these values will + -- 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 , eoResetCycles = 30 , eoDriveEarly = True } @@ -81,13 +83,6 @@ class ) => Test a where - -- | Get the number of expected valid data cycles for each data channel, - -- given a list of expected data. - expectToLengths :: - Proxy a -> - ExpectType a -> - C.Vec (SimulateChannels a) Int - -- | Trim each channel to the lengths given as the third argument. See -- result documentation for failure modes. expectN :: @@ -95,8 +90,6 @@ class Proxy a -> -- | Options, see 'ExpectOptions' ExpectOptions -> - -- | Number of valid data cycles expected on each channel - C.Vec (SimulateChannels a) Int -> -- | Raw sampled data SimulateFwdType a -> -- | Depending on "ExpectOptions", fails the test if: @@ -113,58 +106,38 @@ class m (ExpectType a) instance (TestType a, C.KnownDomain dom) => Test (Df dom a) where - expectToLengths Proxy = pure . length - expectN :: forall m. (HasCallStack, H.MonadTest m) => Proxy (Df dom a) -> ExpectOptions -> - C.Vec 1 Int -> [Df.Data a] -> m [a] - expectN Proxy (ExpectOptions{eoEmptyTail, eoTimeout}) (C.head -> nExpected) sampled = do - go (fromMaybe maxBound eoTimeout) nExpected sampled + expectN Proxy (ExpectOptions{eoSampleMax, eoStopAfterEmpty}) sampled = do + go eoSampleMax eoStopAfterEmpty sampled where - catDatas [] = [] - catDatas (Df.NoData : xs) = catDatas xs - catDatas (Df.Data x : xs) = x : catDatas xs - - go :: - (HasCallStack) => - -- Timeout counter. If it reaches zero we time out. - Int -> - -- Expected number of values - Int -> - -- Sampled data - [Df.Data a] -> - -- Results - m [a] + go :: (HasCallStack) => Int -> Int -> [Df.Data a] -> m [a] go _timeout _n [] = -- This really should not happen, protocols should produce data indefinitely error "unexpected end of signal" - go _timeout 0 rest = do - -- Check for superfluous output from protocol - case catDatas (take eoEmptyTail rest) of - [] -> pure (take nExpected (catDatas sampled)) - superfluous -> - let err = "Circuit produced more output than expected:" - in H.failWith Nothing (err <> "\n\n" <> ppShow superfluous) - go timeout n _ - | timeout <= 0 = - H.failWith Nothing $ - concat - [ "Circuit did not produce enough output. Expected " - , show n - , " more values. Sampled only " <> show (nExpected - n) <> ":\n\n" - , ppShow (take (nExpected - n) (catDatas sampled)) - ] - go timeout n (Df.NoData : as) = do - -- Circuit did not output valid cycle, just continue - go (pred timeout) n as - go _ n (Df.Data _ : as) = - -- Circuit produced a valid cycle, reset timeout - go (fromMaybe maxBound eoTimeout) (pred n) as + go 0 _ _ = + -- Sample limit reached + H.failWith + Nothing + ( "Sample limit reached after sampling " + <> show eoSampleMax + <> " samples. " + <> "Consider increasing 'eoSampleMax' in 'ExpectOptions'." + ) + go _ 0 _ = + -- Saw enough valid samples, return to user + pure [] + go sampleTimeout _emptyTimeout (Df.Data a : as) = + -- Valid sample + (a :) <$> go (sampleTimeout - 1) eoStopAfterEmpty as + go sampleTimeout emptyTimeout (Df.NoData : as) = + -- Empty sample + go sampleTimeout (emptyTimeout - 1) as instance ( Test a @@ -174,27 +147,16 @@ instance ) => Test (C.Vec n a) where - expectToLengths :: - Proxy (C.Vec n a) -> - ExpectType (C.Vec n a) -> - C.Vec (n * SimulateChannels a) Int - expectToLengths Proxy = - C.concatMap (expectToLengths (Proxy @a)) - expectN :: forall m. (HasCallStack, H.MonadTest m) => Proxy (C.Vec n a) -> ExpectOptions -> - C.Vec (n * SimulateChannels a) Int -> C.Vec n (SimulateFwdType a) -> m (C.Vec n (ExpectType a)) - expectN Proxy opts nExpecteds sampled = do - -- TODO: This creates some pretty terrible error messages, as one - -- TODO: simulate channel is checked at a time. - forM - (C.zip (C.unconcatI nExpecteds) sampled) - (uncurry (expectN (Proxy @a) opts)) + -- TODO: This creates some pretty terrible error messages, as one + -- TODO: simulate channel is checked at a time. + expectN Proxy opts = mapM (expectN (Proxy @a) opts) instance ( Test a @@ -203,59 +165,16 @@ instance ) => Test (a, b) where - expectToLengths :: - Proxy (a, b) -> - (ExpectType a, ExpectType b) -> - C.Vec (SimulateChannels a + SimulateChannels b) Int - expectToLengths Proxy (t1, t2) = - expectToLengths (Proxy @a) t1 C.++ expectToLengths (Proxy @b) t2 - expectN :: forall m. (HasCallStack, H.MonadTest m) => Proxy (a, b) -> ExpectOptions -> - C.Vec (SimulateChannels a + SimulateChannels b) Int -> (SimulateFwdType a, SimulateFwdType b) -> m (ExpectType a, ExpectType b) - expectN Proxy opts nExpecteds (sampledA, sampledB) = do + expectN Proxy opts (sampledA, sampledB) = do -- TODO: This creates some pretty terrible error messages, as one -- TODO: simulate channel is checked at a time. - trimmedA <- expectN (Proxy @a) opts nExpectedsA sampledA - trimmedB <- expectN (Proxy @b) opts nExpectedsB sampledB + trimmedA <- expectN (Proxy @a) opts sampledA + trimmedB <- expectN (Proxy @b) opts sampledB pure (trimmedA, trimmedB) - where - (nExpectedsA, nExpectedsB) = C.splitAtI nExpecteds - --- | Fails with an error that shows the difference between two values. -failDiffWith :: - (H.MonadTest m, Show a, Show b, HasCallStack) => - -- | Additional info for error message - String -> - -- | Expected - a -> - -- | Actual - b -> - m () -failDiffWith msg x y = - case H.valueDiff <$> H.mkValue x <*> H.mkValue y of - Nothing -> - withFrozenCallStack $ - H.failWith Nothing $ - unlines $ - [ msg - , "━━ expected ━━" - , H.showPretty x - , "━━ actual ━━" - , H.showPretty y - ] - Just vdiff@(H.ValueSame _) -> - withFrozenCallStack $ - H.failWith - (Just $ H.Diff "━━━ Failed (" "" "no differences" "" ") ━━━" vdiff) - msg - Just vdiff -> - withFrozenCallStack $ - H.failWith - (Just $ H.Diff "━━━ Failed (" "- expected" ") (" "+ actual" ") ━━━" vdiff) - msg diff --git a/src/Protocols/Wishbone/Standard/Hedgehog.hs b/src/Protocols/Wishbone/Standard/Hedgehog.hs index 9e972f27..65077b3b 100644 --- a/src/Protocols/Wishbone/Standard/Hedgehog.hs +++ b/src/Protocols/Wishbone/Standard/Hedgehog.hs @@ -480,7 +480,7 @@ wishbonePropWithModel eOpts model circuit0 inputGen st = do resets = 5 driver = driveStandard @dom (defExpectOptions{eoResetCycles = resets}) (P.zip input reqStalls) circuit1 = validatorCircuit |> circuit0 - (_, s2m) = observeComposedWishboneCircuit (eoTimeout eOpts) driver circuit1 + (_, s2m) = observeComposedWishboneCircuit (eoSampleMax eOpts) driver circuit1 matchModel 0 s2m input st === Right () where @@ -504,17 +504,13 @@ wishbonePropWithModel eOpts model circuit0 inputGen st = do observeComposedWishboneCircuit :: (KnownDomain dom) => - Maybe Int -> + Int -> Circuit () (Wishbone dom mode addressWidth a) -> Circuit (Wishbone dom mode addressWidth a) () -> ( [WishboneM2S addressWidth (BitSize a `DivRU` 8) a] , [WishboneS2M a] ) -observeComposedWishboneCircuit Nothing (Circuit master) (Circuit slave) = - let ~((), m2s) = master ((), s2m) - ~(s2m, ()) = slave (m2s, ()) - in (sample_lazy m2s, sample_lazy s2m) -observeComposedWishboneCircuit (Just n) (Circuit master) (Circuit slave) = +observeComposedWishboneCircuit n (Circuit master) (Circuit slave) = let ~((), m2s) = master ((), s2m) ~(s2m, ()) = slave (m2s, ()) in (sampleN_lazy n m2s, sampleN_lazy n s2m) diff --git a/tests/Tests/Protocols/Df.hs b/tests/Tests/Protocols/Df.hs index 8e994514..a20ef0a7 100644 --- a/tests/Tests/Protocols/Df.hs +++ b/tests/Tests/Protocols/Df.hs @@ -69,7 +69,11 @@ smallInt :: Range Int smallInt = Range.linear 0 10 genSmallInt :: Gen Int -genSmallInt = Gen.integral smallInt +genSmallInt = + Gen.frequency + [ (90, Gen.integral smallInt) + , (10, Gen.constant (Range.lowerBound 99 smallInt)) + ] genSmallPlusInt :: Gen PlusInt genSmallPlusInt = coerce <$> genSmallInt diff --git a/tests/Tests/Protocols/DfConv.hs b/tests/Tests/Protocols/DfConv.hs index 23bb728a..776ae787 100644 --- a/tests/Tests/Protocols/DfConv.hs +++ b/tests/Tests/Protocols/DfConv.hs @@ -257,7 +257,7 @@ tests :: TestTree tests = -- TODO: Move timeout option to hedgehog for better error messages. -- TODO: Does not seem to work for combinatorial loops like @let x = x in x@?? - localOption (mkTimeout 12_000_000 {- 12 seconds -}) $ + localOption (mkTimeout 20_000_000 {- 20 seconds -}) $ localOption (HedgehogTestLimit (Just 1000)) $(testGroupGenerator)