Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add timeout to driveStandard function #49

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

add timeout to driveStandard function #49

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
76 changes: 45 additions & 31 deletions src/Protocols/Wishbone/Standard/Hedgehog.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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,
Expand All @@ -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) =>
Expand Down
46 changes: 38 additions & 8 deletions tests/Tests/Protocols/Wishbone.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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 $
Expand All @@ -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
--
Expand Down Expand Up @@ -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)