Safe Haskell	None
Language	GHC2021

Protocols.Experimental.Hedgehog

Contents

Types
Test functions
Monadic test functions
Internals

Description

A collection of Hedgehog helpers to test Circuit components. To test a protocol component against a combinatorial model, see idWithModel. To write your own tester, see Test.

Synopsis

data ExpectOptions = ExpectOptions {
- eoStopAfterEmpty :: Maybe Int
- eoSampleMax :: Int
- eoStallsMax :: Int
- eoConsecutiveStalls :: Int
- eoResetCycles :: Int
- eoDriveEarly :: Bool
- eoTimeoutMs :: Maybe Int
- eoTrace :: Bool
}
defExpectOptions :: ExpectOptions
data StallMode
- = NoStall
- | Stall
class (Drivable a, TestType (SimulateFwdType a), TestType (ExpectType a)) => Test a where
- expectN :: (HasCallStack, MonadTest m) => Proxy a -> ExpectOptions -> SimulateFwdType a -> m (ExpectType a)
class (NFData a, NFDataX a, ShowX a, Show a, Eq a) => TestType a
idWithModel :: (Test a, Test b, HasCallStack) => ExpectOptions -> Gen (ExpectType a) -> (ExpectType a -> ExpectType b) -> Circuit a b -> Property
idWithModelSingleDomain :: forall (dom :: Domain) a b. (Test a, Test b, KnownDomain dom, HasCallStack) => ExpectOptions -> Gen (ExpectType a) -> (Clock dom -> Reset dom -> Enable dom -> ExpectType a -> ExpectType b) -> (Clock dom -> Reset dom -> Enable dom -> Circuit a b) -> Property
propWithModel :: (Test a, Test b, HasCallStack) => ExpectOptions -> Gen (ExpectType a) -> (ExpectType a -> ExpectType b) -> Circuit a b -> (ExpectType b -> ExpectType b -> PropertyT IO ()) -> Property
propWithModelSingleDomain :: forall (dom :: Domain) a b. (Test a, Test b, KnownDomain dom, HasCallStack) => ExpectOptions -> Gen (ExpectType a) -> (Clock dom -> Reset dom -> Enable dom -> ExpectType a -> ExpectType b) -> (Clock dom -> Reset dom -> Enable dom -> Circuit a b) -> (ExpectType b -> ExpectType b -> PropertyT IO ()) -> Property
idWithModelT :: forall a b (m :: Type -> Type). (Test a, Test b, HasCallStack, Monad m, MonadIO m, MonadBaseControl IO m) => ExpectOptions -> Gen (ExpectType a) -> (ExpectType a -> ExpectType b) -> Circuit a b -> PropertyT m ()
idWithModelSingleDomainT :: forall (dom :: Domain) a b (m :: Type -> Type). (Test a, Test b, KnownDomain dom, HasCallStack, Monad m, MonadIO m, MonadBaseControl IO m) => ExpectOptions -> Gen (ExpectType a) -> (Clock dom -> Reset dom -> Enable dom -> ExpectType a -> ExpectType b) -> (Clock dom -> Reset dom -> Enable dom -> Circuit a b) -> PropertyT m ()
propWithModelT :: forall a b (m :: Type -> Type). (Test a, Test b, HasCallStack, Monad m, MonadIO m, MonadBaseControl IO m) => ExpectOptions -> Gen (ExpectType a) -> (ExpectType a -> ExpectType b) -> Circuit a b -> (ExpectType b -> ExpectType b -> PropertyT m ()) -> PropertyT m ()
propWithModelSingleDomainT :: forall (dom :: Domain) a b (m :: Type -> Type). (Test a, Test b, KnownDomain dom, HasCallStack, Monad m, MonadIO m, MonadBaseControl IO m) => ExpectOptions -> Gen (ExpectType a) -> (Clock dom -> Reset dom -> Enable dom -> ExpectType a -> ExpectType b) -> (Clock dom -> Reset dom -> Enable dom -> Circuit a b) -> (ExpectType b -> ExpectType b -> PropertyT m ()) -> PropertyT m ()
genStallAck :: Gen StallAck
genStallMode :: Gen StallMode
genStalls :: Gen Int -> Int -> StallMode -> Gen (StallAck, [Int])
expectedEmptyCycles :: ExpectOptions -> Int

Types

data ExpectOptions Source #

Options for expectN function. See individual fields for more information.

Constructors

ExpectOptions

Fields

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.
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
Start driving the circuit with its reset asserted. Circuits should never acknowledge data while this is happening.
eoTimeoutMs :: Maybe Int
Terminate the test after n milliseconds.
eoTrace :: Bool
Trace data generation for debugging purposes

defExpectOptions :: ExpectOptions Source #

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.

data StallMode Source #

Whether to stall or not. Used in idWithModel.

Constructors

NoStall
Stall

Instances

Instances details

Bounded StallMode Source #
Instance details Defined in Protocols.Experimental.Hedgehog Methods minBound :: StallMode # maxBound :: StallMode #
Enum StallMode Source #
Instance details Defined in Protocols.Experimental.Hedgehog Methods succ :: StallMode -> StallMode # pred :: StallMode -> StallMode # toEnum :: Int -> StallMode # fromEnum :: StallMode -> Int # enumFrom :: StallMode -> [StallMode] # enumFromThen :: StallMode -> StallMode -> [StallMode] # enumFromTo :: StallMode -> StallMode -> [StallMode] # enumFromThenTo :: StallMode -> StallMode -> StallMode -> [StallMode] #
Show StallMode Source #
Instance details Defined in Protocols.Experimental.Hedgehog Methods showsPrec :: Int -> StallMode -> ShowS # show :: StallMode -> String # showList :: [StallMode] -> ShowS #

class (Drivable a, TestType (SimulateFwdType a), TestType (ExpectType a)) => Test a where Source #

Provides a way of comparing expected data with data produced by a protocol component.

Methods

expectN Source #

Arguments

:: (HasCallStack, MonadTest m)
=> Proxy a
-> ExpectOptions	Options, see `ExpectOptions`
-> SimulateFwdType a	Raw sampled data
-> m (ExpectType a)	Depending on ExpectOptions, fails the test if: Circuit produced less data than expected Circuit produced more data than expected If it does not fail, SimulateFwdType a will contain exactly the number of expected data packets. TODO: Should probably return a 'Vec (SimulateChannels) Failures' in order to produce pretty reports.

Trim each channel to the lengths given as the third argument. See result documentation for failure modes.

Instances

Instances details

Test () Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Internal Methods expectN :: (HasCallStack, MonadTest m) => Proxy () -> ExpectOptions -> SimulateFwdType () -> m (ExpectType ()) Source #
(Test a, KnownNat n, 1 <= (n * SimulateChannels a), 1 <= n) => Test (Vec n a) Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Internal Methods expectN :: (HasCallStack, MonadTest m) => Proxy (Vec n a) -> ExpectOptions -> SimulateFwdType (Vec n a) -> m (ExpectType (Vec n a)) Source #
(TestType a, KnownDomain dom) => Test (Df dom a) Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Internal Methods expectN :: (HasCallStack, MonadTest m) => Proxy (Df dom a) -> ExpectOptions -> SimulateFwdType (Df dom a) -> m (ExpectType (Df dom a)) Source #
(Test a, Test b, 1 <= (SimulateChannels a + SimulateChannels b)) => Test (a, b) Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Internal Methods expectN :: (HasCallStack, MonadTest m) => Proxy (a, b) -> ExpectOptions -> SimulateFwdType (a, b) -> m (ExpectType (a, b)) Source #
(ReadyLatency conf ~ 0, KnownAvalonStreamConfig conf, NFDataX dataType, NFData dataType, ShowX dataType, Show dataType, Eq dataType, KnownDomain dom) => Test (AvalonStream dom conf dataType) Source #
Instance details Defined in Protocols.Experimental.Avalon.Stream Methods expectN :: (HasCallStack, MonadTest m) => Proxy (AvalonStream dom conf dataType) -> ExpectOptions -> SimulateFwdType (AvalonStream dom conf dataType) -> m (ExpectType (AvalonStream dom conf dataType)) Source #
(KnownAxi4StreamConfig conf, NFDataX userType, NFData userType, ShowX userType, Show userType, Eq userType, KnownDomain dom) => Test (Axi4Stream dom conf userType) Source #
Instance details Defined in Protocols.Experimental.Axi4.Stream Methods expectN :: (HasCallStack, MonadTest m) => Proxy (Axi4Stream dom conf userType) -> ExpectOptions -> SimulateFwdType (Axi4Stream dom conf userType) -> m (ExpectType (Axi4Stream dom conf userType)) Source #
(KnownNat dataWidth, NFDataX meta, NFData meta, ShowX meta, Show meta, Eq meta, KnownDomain dom) => Test (PacketStream dom dataWidth meta) Source #
Instance details Defined in Protocols.Experimental.PacketStream Methods expectN :: (HasCallStack, MonadTest m) => Proxy (PacketStream dom dataWidth meta) -> ExpectOptions -> SimulateFwdType (PacketStream dom dataWidth meta) -> m (ExpectType (PacketStream dom dataWidth meta)) Source #
(Test c1, Test c2, Test c3) => Test (c1, c2, c3) Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Internal Methods expectN :: (HasCallStack, MonadTest m) => Proxy (c1, c2, c3) -> ExpectOptions -> SimulateFwdType (c1, c2, c3) -> m (ExpectType (c1, c2, c3)) Source #
(Test c1, Test c2, Test c3, Test c4) => Test (c1, c2, c3, c4) Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Internal Methods expectN :: (HasCallStack, MonadTest m) => Proxy (c1, c2, c3, c4) -> ExpectOptions -> SimulateFwdType (c1, c2, c3, c4) -> m (ExpectType (c1, c2, c3, c4)) Source #
(Test c1, Test c2, Test c3, Test c4, Test c5) => Test (c1, c2, c3, c4, c5) Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Internal Methods expectN :: (HasCallStack, MonadTest m) => Proxy (c1, c2, c3, c4, c5) -> ExpectOptions -> SimulateFwdType (c1, c2, c3, c4, c5) -> m (ExpectType (c1, c2, c3, c4, c5)) Source #
(Test c1, Test c2, Test c3, Test c4, Test c5, Test c6) => Test (c1, c2, c3, c4, c5, c6) Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Internal Methods expectN :: (HasCallStack, MonadTest m) => Proxy (c1, c2, c3, c4, c5, c6) -> ExpectOptions -> SimulateFwdType (c1, c2, c3, c4, c5, c6) -> m (ExpectType (c1, c2, c3, c4, c5, c6)) Source #
(Test c1, Test c2, Test c3, Test c4, Test c5, Test c6, Test c7) => Test (c1, c2, c3, c4, c5, c6, c7) Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Internal Methods expectN :: (HasCallStack, MonadTest m) => Proxy (c1, c2, c3, c4, c5, c6, c7) -> ExpectOptions -> SimulateFwdType (c1, c2, c3, c4, c5, c6, c7) -> m (ExpectType (c1, c2, c3, c4, c5, c6, c7)) Source #
(Test c1, Test c2, Test c3, Test c4, Test c5, Test c6, Test c7, Test c8) => Test (c1, c2, c3, c4, c5, c6, c7, c8) Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Internal Methods expectN :: (HasCallStack, MonadTest m) => Proxy (c1, c2, c3, c4, c5, c6, c7, c8) -> ExpectOptions -> SimulateFwdType (c1, c2, c3, c4, c5, c6, c7, c8) -> m (ExpectType (c1, c2, c3, c4, c5, c6, c7, c8)) Source #
(Test c1, Test c2, Test c3, Test c4, Test c5, Test c6, Test c7, Test c8, Test c9) => Test (c1, c2, c3, c4, c5, c6, c7, c8, c9) Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Internal Methods expectN :: (HasCallStack, MonadTest m) => Proxy (c1, c2, c3, c4, c5, c6, c7, c8, c9) -> ExpectOptions -> SimulateFwdType (c1, c2, c3, c4, c5, c6, c7, c8, c9) -> m (ExpectType (c1, c2, c3, c4, c5, c6, c7, c8, c9)) Source #

class (NFData a, NFDataX a, ShowX a, Show a, Eq a) => TestType a Source #

Superclass class to reduce syntactical noise.

Instances

Instances details

(NFData a, NFDataX a, ShowX a, Show a, Eq a) => TestType a Source #
Instance details Defined in Protocols.Experimental.Hedgehog.Types

Test functions

idWithModel Source #

Arguments

:: (Test a, Test b, HasCallStack)
=> ExpectOptions	Options, see `ExpectOptions`
-> Gen (ExpectType a)	Test data generator
-> (ExpectType a -> ExpectType b)	Model
-> Circuit a b	Implementation
-> Property

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:

Whether it does not produce too little data
Whether it does not produce more data than expected
Whether the expected data corresponds to the sampled data
Whether it responds to backpressure correctly
Whether it (eventually) drives a nack while in reset

For testing custom properties, see propWithModel.

idWithModelSingleDomain Source #

Arguments

:: forall (dom :: Domain) a b. (Test a, Test b, KnownDomain dom, HasCallStack)
=> ExpectOptions	Options, see `ExpectOptions`
-> Gen (ExpectType a)	Test data generator
-> (Clock dom -> Reset dom -> Enable dom -> ExpectType a -> ExpectType b)	Model
-> (Clock dom -> Reset dom -> Enable dom -> Circuit a b)	Implementation
-> Property

Same as propWithModel, but with single clock, reset, and enable.

propWithModel Source #

Arguments

:: (Test a, Test b, HasCallStack)
=> ExpectOptions	Options, see `ExpectOptions`
-> Gen (ExpectType a)	Test data generator
-> (ExpectType a -> ExpectType b)	Model
-> Circuit a b	Implementation
-> (ExpectType b -> ExpectType b -> PropertyT IO ())	Property to test for. Function is given the data produced by the model as a first argument, and the sampled data as a second argument.
-> Property

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:

Whether it does not produce too little data.
Whether it does not produce more data than expected.
Whether it responds to backpressure correctly
Whether it (eventually) drives a nack while in reset.

Finally, the data will be tested against the property supplied in the last argument.

propWithModelSingleDomain Source #

Arguments

:: forall (dom :: Domain) a b. (Test a, Test b, KnownDomain dom, HasCallStack)
=> ExpectOptions	Options, see `ExpectOptions`
-> Gen (ExpectType a)	Test data generator
-> (Clock dom -> Reset dom -> Enable dom -> ExpectType a -> ExpectType b)	Model
-> (Clock dom -> Reset dom -> Enable dom -> Circuit a b)	Implementation
-> (ExpectType b -> ExpectType b -> PropertyT IO ())	Property to test for. Function is given the data produced by the model as a first argument, and the sampled data as a second argument.
-> Property

Same as propWithModel, but with single clock, reset, and enable.

Monadic test functions

idWithModelT Source #

Arguments

:: forall a b (m :: Type -> Type). (Test a, Test b, HasCallStack, Monad m, MonadIO m, MonadBaseControl IO m)
=> ExpectOptions	Options, see `ExpectOptions`
-> Gen (ExpectType a)	Test data generator
-> (ExpectType a -> ExpectType b)	Model
-> Circuit a b	Implementation
-> PropertyT m ()

Monadic version of idWithModel. Runs the protocol-vs-model test using the default equality property (===) in any monad supporting MonadIO and 'MonadBaseControl IO'. Use this when you want to run the test in a monadic context or need additional effects.

idWithModelSingleDomainT Source #

Arguments

:: forall (dom :: Domain) a b (m :: Type -> Type). (Test a, Test b, KnownDomain dom, HasCallStack, Monad m, MonadIO m, MonadBaseControl IO m)
=> ExpectOptions	Options, see `ExpectOptions`
-> Gen (ExpectType a)	Test data generator
-> (Clock dom -> Reset dom -> Enable dom -> ExpectType a -> ExpectType b)	Model
-> (Clock dom -> Reset dom -> Enable dom -> Circuit a b)	Implementation
-> PropertyT m ()

Monadic version of idWithModelSingleDomain. Runs the single-domain protocol-vs-model test using the default equality property (===) in any monad supporting MonadIO and 'MonadBaseControl IO'. Use this for monadic test frameworks or when additional effects are needed.

propWithModelT Source #

Arguments

:: forall a b (m :: Type -> Type). (Test a, Test b, HasCallStack, Monad m, MonadIO m, MonadBaseControl IO m)
=> ExpectOptions	Options, see `ExpectOptions`
-> Gen (ExpectType a)	Test data generator
-> (ExpectType a -> ExpectType b)	Model
-> Circuit a b	Implementation
-> (ExpectType b -> ExpectType b -> PropertyT m ())	Property to test for. Function is given the data produced by the model as a first argument, and the sampled data as a second argument.
-> PropertyT m ()

Monadic version of propWithModel. Allows property-based protocol testing in any monad supporting MonadIO and 'MonadBaseControl IO'. This is useful for integrating with monadic test frameworks or when additional effects are needed during testing.

propWithModelSingleDomainT Source #

Arguments

:: forall (dom :: Domain) a b (m :: Type -> Type). (Test a, Test b, KnownDomain dom, HasCallStack, Monad m, MonadIO m, MonadBaseControl IO m)
=> ExpectOptions	Options, see `ExpectOptions`
-> Gen (ExpectType a)	Test data generator
-> (Clock dom -> Reset dom -> Enable dom -> ExpectType a -> ExpectType b)	Model
-> (Clock dom -> Reset dom -> Enable dom -> Circuit a b)	Implementation
-> (ExpectType b -> ExpectType b -> PropertyT m ())	Property to test for. Function is given the data produced by the model as a first argument, and the sampled data as a second argument.
-> PropertyT m ()

Monadic version of propWithModelSingleDomain. Allows property-based protocol testing for single-domain circuits in any monad supporting MonadIO and 'MonadBaseControl IO'. This is useful for monadic test integration or when effects are required during testing.

Internals

genStallAck :: Gen StallAck Source #

Generator for StallMode. Shrinks towards StallWithNack.

genStallMode :: Gen StallMode Source #

Generator for StallMode. Shrinks towards NoStall.

genStalls :: Gen Int -> Int -> StallMode -> Gen (StallAck, [Int]) Source #

Generator for stall information for stallC. Generates stalls according to distribution given in first argument. The second argument indicates how many cycles the component is expecting / is producing data for. If the last argument is NoStall, no stalls will be generated at all.

expectedEmptyCycles :: ExpectOptions -> Int Source #

Default derivation of eoStopAfterEmpty when it is set to Nothing.