diff --git a/src/Protocols/Wishbone/Standard/Hedgehog.hs b/src/Protocols/Wishbone/Standard/Hedgehog.hs index c9964917..4f1c080d 100644 --- a/src/Protocols/Wishbone/Standard/Hedgehog.hs +++ b/src/Protocols/Wishbone/Standard/Hedgehog.hs @@ -54,8 +54,10 @@ import GHC.Stack (HasCallStack) data WishboneMasterRequest addressWidth dat = Read (BitVector addressWidth) (BitVector (BitSize dat `DivRU` 8)) | Write (BitVector addressWidth) (BitVector (BitSize dat `DivRU` 8)) dat + deriving (Generic) deriving instance (KnownNat addressWidth, KnownNat (BitSize a), Show a) => (Show (WishboneMasterRequest addressWidth a)) +deriving instance (KnownNat addressWidth, KnownNat (BitSize a), ShowX a) => (ShowX (WishboneMasterRequest addressWidth a)) -- -- Validation for (lenient) spec compliance @@ -238,13 +240,13 @@ stallStandard stallsPerCycle = -- tell the master that the slave has no reply yet (emptyWishboneS2M :-) -- tell the slave that the cycle is over - (m :-) + (emptyWishboneM2S :-) (go (st - 1 : stalls) Nothing m2s s2m) -- done stalling, got a reply last second, pass through | busCycle m && strobe m && st == 0 && hasTerminateFlag s = B.bimap (s :-) - (m :-) + (emptyWishboneM2S :-) (go stalls Nothing m2s s2m) -- done stalling but no termination signal yet, just pass through to give the slave -- the chance to reply @@ -284,15 +286,15 @@ driveStandard :: C.KnownNat (C.BitSize a) ) => ExpectOptions -> - -- | Requests to send out - [WishboneMasterRequest addressWidth a] -> + -- | Requests to send out and maximum cycles a transfer is allowed to take + [(WishboneMasterRequest addressWidth a, Int)] -> Circuit () (Wishbone dom 'Standard addressWidth a) driveStandard ExpectOptions {..} reqs = Circuit $ ((),) . C.fromList_lazy . (emptyWishboneM2S :) - . go eoResetCycles reqs + . go eoResetCycles 0 reqs . (\s -> C.sample_lazy s) . snd where @@ -326,22 +328,25 @@ driveStandard ExpectOptions {..} reqs = go :: Int -> - [WishboneMasterRequest addressWidth a] -> + Int -> -- cycles in the current transaction + [(WishboneMasterRequest addressWidth a, Int)] -> [WishboneS2M a] -> [WishboneM2S addressWidth (BitSize a `DivRU` 8) a] - go nResets dat ~(rep : replies) - | nResets > 0 = emptyWishboneM2S : (rep `C.seqX` go (nResets - 1) dat replies) + go nResets _ dat ~(rep : replies) + | nResets > 0 = emptyWishboneM2S : (rep `C.seqX` go (nResets - 1) 0 dat replies) -- no more data to send - go _ [] ~(rep : replies) = emptyWishboneM2S : (rep `C.seqX` go 0 [] replies) - go _ (d : dat) ~(rep : replies) + go _ _ [] ~(rep : replies) = emptyWishboneM2S : (rep `C.seqX` go 0 0 [] replies) + go _ cycles ((d, timeOut) : dat) ~(rep : replies) -- the sent data was acknowledged, end the cycle before continuing - | acknowledge rep || err rep = emptyWishboneM2S : (rep `C.seqX` go 0 dat replies) + | acknowledge rep || err rep = emptyWishboneM2S : (rep `C.seqX` go 0 0 dat replies) -- end cycle, continue but send the previous request again - | retry rep = emptyWishboneM2S : (rep `C.seqX` go 0 (d : dat) replies) - -- not a termination signal, so keep sending the data + | retry rep = emptyWishboneM2S : (rep `C.seqX` go 0 0 ((d, timeOut) : dat) replies) + -- not a termination signal, the transfer timed out + | cycles == timeOut = emptyWishboneM2S : (rep `C.seqX` go 0 0 dat replies) + -- not a termination signal, no timeout, keep sending request | otherwise -- trace "D in-cycle wait for ACK" $ = - transferToSignals d : (rep `C.seqX` go 0 (d : dat) replies) + transferToSignals d : (rep `C.seqX` go 0 (cycles + 1) ((d, timeOut) : dat) replies) -- | Circuit which validates the wishbone communication signals between a -- master and a slave circuit. @@ -410,7 +415,8 @@ validatorCircuitLenient = -- | Test a wishbone 'Standard' circuit against a pure model. wishbonePropWithModel :: forall dom a addressWidth st. - ( Eq a, + ( HasCallStack, + Eq a, C.ShowX a, Show a, C.NFDataX a, @@ -436,36 +442,44 @@ wishbonePropWithModel eOpts model circuit0 inputGen st = H.property $ do let n = P.length input - genStall = Gen.integral (Range.linear 0 10) + genStall = Gen.integral (Range.linear 0 15) + genTimeOut = Gen.integral (Range.linear 1 15) + timeOuts <- H.forAll (Gen.list (Range.singleton n) genTimeOut) stalls <- H.forAll (Gen.list (Range.singleton n) genStall) let resets = 50 - driver = driveStandard @dom (defExpectOptions {eoResetCycles = resets}) input + inputs = P.zip input timeOuts + driver = driveStandard @dom (defExpectOptions {eoResetCycles = resets}) inputs |> validatorCircuit |> stallC stallC = stallStandard stalls - circuit1 = stallC |> validatorCircuit |> circuit0 - (_, _ : s2m) = observeComposedWishboneCircuit (eoTimeout eOpts) driver circuit1 + circuit1 = validatorCircuit |> circuit0 + (m2s, s2m) = observeComposedWishboneCircuit (eoTimeout eOpts) driver circuit1 + + matchModel 0 m2s s2m st === Right () - matchModel 0 s2m input st === Right () where + m2sToReq WishboneM2S{..} + | not (busCycle && strobe) = Nothing + | writeEnable = Just $ Write addr busSelect writeData + | otherwise = Just $ Read addr busSelect + matchModel :: Int -> + [WishboneM2S addressWidth (BitSize a `DivRU` 8) a] -> [WishboneS2M a] -> - [WishboneMasterRequest addressWidth a] -> st -> Either (Int, String) () - matchModel _ [] _ _ = Right () -- so far everything is good but the sampling stopped + matchModel _ [] _ _ = Right () matchModel _ _ [] _ = Right () - matchModel cyc (s : s2m) (req : reqs0) state - | not (hasTerminateFlag s) = s `C.seqX` matchModel (succ cyc) s2m (req : reqs0) state - | otherwise = case model req s state of - Left err -> Left (cyc, err) - Right st1 -> s `C.seqX` matchModel (succ cyc) s2m reqs1 st1 - where - reqs1 - | retry s = req : reqs0 - | otherwise = reqs0 + matchModel cyc (m : m2s) (s : s2m) state + | Nothing <- m2sToReq m, hasTerminateFlag s = + Left (cyc, "Termination flag outside of bus cycle") + | Just req <- m2sToReq m, hasTerminateFlag s = + case model req s state of + Left err -> Left (cyc, err) + Right st1 -> s `C.seqX` matchModel (succ cyc) m2s s2m st1 + | otherwise = s `C.seqX` matchModel (succ cyc) m2s s2m state observeComposedWishboneCircuit :: (KnownDomain dom) => diff --git a/tests/Tests/Protocols/Wishbone.hs b/tests/Tests/Protocols/Wishbone.hs index f4e2801d..3bdcbe73 100644 --- a/tests/Tests/Protocols/Wishbone.hs +++ b/tests/Tests/Protocols/Wishbone.hs @@ -22,6 +22,7 @@ import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) import Test.Tasty.Hedgehog.Extra (testProperty) import Test.Tasty.TH (testGroupGenerator) import Prelude hiding (undefined) +import GHC.Stack (HasCallStack) smallInt :: Range Int smallInt = Range.linear 0 10 @@ -48,7 +49,7 @@ genWishboneTransfer genA = addrReadIdWb :: forall dom addressWidth. - (KnownNat addressWidth) => + (HasCallStack, KnownNat addressWidth) => Circuit (Wishbone dom 'Standard addressWidth (BitVector addressWidth)) () addrReadIdWb = Circuit go where @@ -64,21 +65,41 @@ addrReadIdWb = Circuit go } | otherwise = emptyWishboneS2M +-- | Same as 'addrReadIdWb' but responses are delayed by one cycle. +addrReadIdRegisterWb :: + forall dom addressWidth. + (HasCallStack, KnownNat addressWidth, HiddenClockResetEnable dom) => + Circuit (Wishbone dom 'Standard addressWidth (BitVector addressWidth)) () +addrReadIdRegisterWb = Circuit go + where + go (m2s, ()) = (reply <$> register emptyWishboneM2S m2s <*> m2s, ()) + + reply prev cur + | not (busCycle cur && strobe cur) = emptyWishboneS2M + | busCycle prev && strobe prev && writeEnable prev = + emptyWishboneS2M { acknowledge = True } + | busCycle prev && strobe prev = + (emptyWishboneS2M @(BitVector addressWidth)) + { acknowledge = True, + readData = addr prev + } + | otherwise = emptyWishboneS2M + addrReadIdWbModel :: - (KnownNat addressWidth) => + (HasCallStack, KnownNat addressWidth) => WishboneMasterRequest addressWidth (BitVector addressWidth) -> WishboneS2M (BitVector addressWidth) -> -- | pure state () -> Either String () -addrReadIdWbModel (Read addr _) s@WishboneS2M {..} () - | acknowledge && hasX readData == Right addr = Right () +addrReadIdWbModel req@(Read addr _) s@WishboneS2M {..} () + | acknowledge && not (hasUndefined readData) && readData == addr = Right () | otherwise = - Left $ "Read should have been acknowledged with address as DAT " <> showX s -addrReadIdWbModel Write {} s@WishboneS2M {..} () + Left $ "Read should have been acknowledged with address as DAT " <> showX req <> "\n" <> showX s +addrReadIdWbModel req@Write{} s@WishboneS2M {..} () | acknowledge && hasUndefined readData = Right () | otherwise = - Left $ "Write should have been acknowledged with no DAT " <> showX s + Left $ "Write should have been acknowledged with no DAT " <> showX req <> "\n" <> showX s prop_addrReadIdWb_model :: Property prop_addrReadIdWb_model = withClockResetEnable clockGen resetGen enableGen $ @@ -89,6 +110,15 @@ prop_addrReadIdWb_model = withClockResetEnable clockGen resetGen enableGen $ (genData $ genWishboneTransfer @10 genDefinedBitVector) () +prop_addrReadIdRegisterWb_model :: Property +prop_addrReadIdRegisterWb_model = withClockResetEnable clockGen resetGen enableGen $ + wishbonePropWithModel @System + defExpectOptions + addrReadIdWbModel + addrReadIdRegisterWb + (genData $ genWishboneTransfer @10 genDefinedBitVector) + () + -- -- memory element circuit -- @@ -144,7 +174,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 25_000_000 {- 25 seconds -}) $ localOption (HedgehogTestLimit (Just 1000)) $(testGroupGenerator)