Merge pull request #51 from clash-lang/wishbonePropWithModel-as-Prope…

…rtyT

change `wishbonePropWithModel` to use `PropertyT` instead of `Property`

src/Protocols/Wishbone/Standard/Hedgehog.hs

@@ -409,15 +409,16 @@ validatorCircuitLenient =
 
 -- | Test a wishbone 'Standard' circuit against a pure model.
 wishbonePropWithModel ::
-  forall dom a addressWidth st.
+  forall dom a addressWidth st m.
   ( Eq a,
     C.ShowX a,
     Show a,
     C.NFDataX a,
     C.KnownNat addressWidth,
     C.HiddenClockResetEnable dom,
     C.KnownNat (C.BitSize a),
-    C.BitPack a
+    C.BitPack a,
+    Monad m
   ) =>
   ExpectOptions ->
   -- | Check whether a S2M signal for a given request is matching a pure model using @st@
@@ -430,8 +431,8 @@ wishbonePropWithModel ::
   H.Gen [WishboneMasterRequest addressWidth a] ->
   -- | Initial state of the model
   st ->
-  H.Property
-wishbonePropWithModel eOpts model circuit0 inputGen st = H.property $ do
+  H.PropertyT m ()
+wishbonePropWithModel eOpts model circuit0 inputGen st = do
   input <- H.forAll inputGen
 
   let

tests/Tests/Protocols/Wishbone.hs

@@ -81,13 +81,14 @@ addrReadIdWbModel Write {} s@WishboneS2M {..} ()
     Left $ "Write should have been acknowledged with no DAT " <> showX s
 
 prop_addrReadIdWb_model :: Property
-prop_addrReadIdWb_model = withClockResetEnable clockGen resetGen enableGen $
-  wishbonePropWithModel @System
-    defExpectOptions
-    addrReadIdWbModel
-    addrReadIdWb
-    (genData $ genWishboneTransfer @10 genDefinedBitVector)
-    ()
+prop_addrReadIdWb_model = property $
+  withClockResetEnable clockGen resetGen enableGen $
+    wishbonePropWithModel @System
+      defExpectOptions
+      addrReadIdWbModel
+      addrReadIdWb
+      (genData $ genWishboneTransfer @10 genDefinedBitVector)
+      ()
 
 --
 -- memory element circuit
@@ -131,7 +132,7 @@ memoryWbModel (Write addr sel a) s st
   | otherwise = Left $ "Write should be acked : " <> showX s
 
 prop_memoryWb_model :: Property
-prop_memoryWb_model =
+prop_memoryWb_model = property $
   withClockResetEnable clockGen resetGen enableGen $
     wishbonePropWithModel @System
       defExpectOptions