From 8b9afba1bc2efa1bd92cffa9fae29aeb5560cac3 Mon Sep 17 00:00:00 2001 From: Lara Herzog Date: Fri, 27 Jan 2023 13:52:17 +0100 Subject: [PATCH 1/2] make wishbone lenient checking more robust, add tests for validators --- src/Protocols/Wishbone/Standard/Hedgehog.hs | 26 ++-- tests/Tests/Protocols/Wishbone.hs | 138 +++++++++++++++++++- 2 files changed, 149 insertions(+), 15 deletions(-) diff --git a/src/Protocols/Wishbone/Standard/Hedgehog.hs b/src/Protocols/Wishbone/Standard/Hedgehog.hs index 7c5b5882..5e70426e 100644 --- a/src/Protocols/Wishbone/Standard/Hedgehog.hs +++ b/src/Protocols/Wishbone/Standard/Hedgehog.hs @@ -72,7 +72,8 @@ nextStateLenient :: LenientValidationState -> WishboneM2S addressWidth (BitSize a `DivRU` 8) a -> WishboneS2M a -> - Either String LenientValidationState + Either String (Bool, LenientValidationState) +-- ^ go to next cycle nextStateLenient _ m2s s2m | P.length (filter ($ s2m) [acknowledge, err, retry]) > 1 = Left "More than one termination signal asserted" @@ -81,20 +82,20 @@ nextStateLenient _ m2s s2m nextStateLenient state m2s s2m = case state of LVSQuiet -> if - | busCycle m2s && P.not (strobe m2s) -> Right LVSInCycleNoStrobe - | busCycle m2s && strobe m2s -> Right LVSWaitForSlave - | otherwise -> Right LVSQuiet + | busCycle m2s && P.not (strobe m2s) -> Right (False, LVSInCycleNoStrobe) + | busCycle m2s && strobe m2s -> Right (False, LVSWaitForSlave) + | otherwise -> Right (True, LVSQuiet) LVSInCycleNoStrobe -> if - | not (busCycle m2s) -> Right LVSQuiet - | busCycle m2s && strobe m2s -> Right LVSWaitForSlave - | otherwise -> Right LVSInCycleNoStrobe + | not (busCycle m2s) -> Right (False, LVSQuiet) + | busCycle m2s && strobe m2s -> Right (False, LVSWaitForSlave) + | otherwise -> Right (True, LVSInCycleNoStrobe) LVSWaitForSlave -> if - | busCycle m2s && P.not (strobe m2s) -> Right LVSInCycleNoStrobe - | not (busCycle m2s) -> Right LVSQuiet - | acknowledge s2m || err s2m || retry s2m -> Right LVSQuiet - | otherwise -> Right LVSWaitForSlave + | busCycle m2s && P.not (strobe m2s) -> Right (False, LVSInCycleNoStrobe) + | not (busCycle m2s) -> Right (False, LVSQuiet) + | acknowledge s2m || err s2m || retry s2m -> Right (True, LVSQuiet) + | otherwise -> Right (True, LVSWaitForSlave) -- @@ -405,7 +406,8 @@ validatorCircuitLenient = <> "\n\n" <> "M2S: " <> show m2s0 <> "\n" <> "S2M: " <> show s2m0 - Right state1 -> ((cycle + 1, (m2s1, s2m1), state1), (s2m1, m2s1)) + Right (True, state1) -> ((cycle + 1, (m2s1, s2m1), state1), (s2m1, m2s1)) + Right (False, state1) -> go (cycle, (m2s0, s2m0), state1) (m2s1, s2m1) -- | Test a wishbone 'Standard' circuit against a pure model. wishbonePropWithModel :: diff --git a/tests/Tests/Protocols/Wishbone.hs b/tests/Tests/Protocols/Wishbone.hs index 68e030d2..84a3e699 100644 --- a/tests/Tests/Protocols/Wishbone.hs +++ b/tests/Tests/Protocols/Wishbone.hs @@ -8,10 +8,11 @@ module Tests.Protocols.Wishbone where import Clash.Hedgehog.Sized.BitVector import Clash.Prelude hiding (not, (&&)) -import Control.DeepSeq (NFData) +import Control.DeepSeq (NFData, force) import Hedgehog import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range +import qualified Data.List as L import Protocols import Protocols.Hedgehog (defExpectOptions) import Protocols.Wishbone @@ -22,6 +23,9 @@ import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) import Test.Tasty.Hedgehog.Extra (testProperty) import Test.Tasty.TH (testGroupGenerator) import Prelude hiding (undefined) +import Control.Exception (evaluate, try, SomeException) +import Control.Monad.IO.Class (MonadIO(liftIO)) +import Data.Either (isLeft) smallInt :: Range Int smallInt = Range.linear 0 10 @@ -30,7 +34,7 @@ genSmallInt :: Gen Int genSmallInt = Gen.integral smallInt genData :: Gen a -> Gen [a] -genData = Gen.list (Range.linear 0 150) +genData = Gen.list (Range.linear 0 300) genWishboneTransfer :: (KnownNat addressWidth, KnownNat (BitSize a)) => @@ -141,11 +145,139 @@ prop_memoryWb_model = property $ (genData (genWishboneTransfer @8 genSmallInt)) [] -- initial state + +-- +-- Helpers +-- + +(|>>) :: Circuit () b -> Circuit b () -> (Fwd b, Bwd b) +Circuit aFn |>> Circuit bFn = (s2rAb, r2sBc) + where + ~((), s2rAb) = aFn ((), r2sBc) + ~(r2sBc, ()) = bFn (s2rAb, ()) + +evaluateUnitCircuit :: + (KnownDomain dom, KnownNat (BitSize a), KnownNat addressWidth, NFDataX a) => + Int -> + Circuit () (Wishbone dom 'Standard addressWidth a) -> + Circuit (Wishbone dom 'Standard addressWidth a) () -> + Int +evaluateUnitCircuit n a b = + let (bundle -> signals) = a |>> b + in L.length $ sampleN n signals + +-- +-- validatorCircuit +-- + +prop_addrReadId_validator :: Property +prop_addrReadId_validator = property $ do + reqs <- forAll $ genData (genWishboneTransfer @8 genDefinedBitVector) + + let + circuitSignalsN = withClockResetEnable @System clockGen resetGen enableGen $ + let + driver = driveStandard @System @(BitVector 8) @8 defExpectOptions reqs + addrRead = addrReadIdWb @System @8 + in evaluateUnitCircuit sampleNumber driver (validatorCircuit @System @8 @(BitVector 8) |> addrRead) + + -- force evalution of sampling somehow + assert (circuitSignalsN == sampleNumber) + +prop_memoryWb_validator :: Property +prop_memoryWb_validator = property $ do + reqs <- forAll $ genData (genWishboneTransfer @8 genDefinedBitVector) + + let + circuitSignalsN = withClockResetEnable @System clockGen resetGen enableGen $ + let + driver = driveStandard @System @(BitVector 8) @8 defExpectOptions reqs + memory = memoryWb @System @(BitVector 8) @8 (blockRamU ClearOnReset (SNat @256) (const def)) + + in evaluateUnitCircuit sampleNumber driver (validatorCircuit @System @8 @(BitVector 8) |> memory) + + -- force evalution of sampling somehow + assert (circuitSignalsN == sampleNumber) + + +-- +-- validatorCircuitLenient +-- + +prop_addrReadId_validator_lenient :: Property +prop_addrReadId_validator_lenient = property $ do + reqs <- forAll $ genData (genWishboneTransfer @8 genDefinedBitVector) + + let + circuitSignalsN = withClockResetEnable @System clockGen resetGen enableGen $ + let + driver = driveStandard @System @(BitVector 8) @8 defExpectOptions reqs + addrRead = addrReadIdWb @System @8 + + in evaluateUnitCircuit sampleNumber driver (validatorCircuitLenient @System @8 @(BitVector 8) |> addrRead) + + -- force evalution of sampling somehow + assert (circuitSignalsN == sampleNumber) + +prop_memoryWb_validator_lenient :: Property +prop_memoryWb_validator_lenient = property $ do + reqs <- forAll $ genData (genWishboneTransfer @8 genDefinedBitVector) + + let + circuitSignalsN = withClockResetEnable @System clockGen resetGen enableGen $ + let + driver = driveStandard @System @(BitVector 8) @8 defExpectOptions reqs + memory = memoryWb @System @(BitVector 8) @8 (blockRamU ClearOnReset (SNat @256) (const def)) + + in evaluateUnitCircuit sampleNumber driver (validatorCircuitLenient @System @8 @(BitVector 8) |> memory) + + -- force evalution of sampling somehow + assert (circuitSignalsN == sampleNumber) + +prop_specViolation_lenient :: Property +prop_specViolation_lenient = property $ do + -- need AT LEAST one transaction so that multiple termination signals can be emitted + reqs <- forAll $ Gen.list (Range.linear 1 500) (genWishboneTransfer @8 genDefinedBitVector) + + let + circuitSignalsN = withClockResetEnable @System clockGen resetGen enableGen $ + let + driver = driveStandard @System @(BitVector 8) @8 defExpectOptions reqs + invalid = invalidCircuit + + in evaluateUnitCircuit sampleNumber driver (validatorCircuitLenient @System @8 @(BitVector 8) |> invalid) + + -- an ErrorCall is expected, but really *any* exception is expected + -- from the validator circuit + res <- liftIO $ try @SomeException (evaluate (force circuitSignalsN)) + + assert $ isLeft res + where + -- a circuit that terminates a cycle with more than one termination signal + invalidCircuit :: Circuit (Wishbone dom 'Standard 8 (BitVector 8)) () + invalidCircuit = Circuit go + where + go (m2s, ()) = (reply <$> m2s, ()) + + reply WishboneM2S {..} + | busCycle && strobe && writeEnable = + emptyWishboneS2M { acknowledge = True, err = True } + | busCycle && strobe = + (emptyWishboneS2M @(BitVector 8)) + { acknowledge = True, + err = True, + readData = addr + } + | otherwise = emptyWishboneS2M + +sampleNumber :: Int +sampleNumber = 1000 + 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 60_000_000 {- 60 seconds -}) $ localOption (HedgehogTestLimit (Just 1000)) $(testGroupGenerator) From cce5c068bcf95dcd92797d0f284aed0b13eb9e3b Mon Sep 17 00:00:00 2001 From: Lara Herzog Date: Thu, 2 Feb 2023 15:58:15 +0100 Subject: [PATCH 2/2] add stall-length to `driveCircuit` This allows a test to control the "downtime" between two transactions. The `stallCircuit` does not yet work with "zero-downtime" transactions. It also only used to test the compliance of the Wishbone master, which in `wishbonePropWithModel` was only ever `driveCircuit`. This was removed for now because it doesn't add trust to the circuit-under-test. This commit also adds more compact `Show` and `ShowX` instances for Wishbone{S2M|M2S} values. --- src/Protocols/Wishbone.hs | 61 ++++++++++++++++-- src/Protocols/Wishbone/Standard.hs | 32 +++++++--- src/Protocols/Wishbone/Standard/Hedgehog.hs | 71 +++++++++++++-------- tests/Tests/Protocols/Wishbone.hs | 26 +++++--- 4 files changed, 137 insertions(+), 53 deletions(-) diff --git a/src/Protocols/Wishbone.hs b/src/Protocols/Wishbone.hs index 7a2940f1..d466eb17 100644 --- a/src/Protocols/Wishbone.hs +++ b/src/Protocols/Wishbone.hs @@ -2,6 +2,7 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fconstraint-solver-iterations=10 #-} +{-# LANGUAGE RecordWildCards #-} -- | -- Types modelling the Wishbone bus protocol. @@ -62,14 +63,48 @@ data WishboneM2S addressWidth selWidth dat = WishboneM2S -- signals. burstTypeExtension :: "BTE" ::: BurstTypeExtension } - deriving (NFData, C.Generic, C.NFDataX, C.ShowX, Eq, C.BitPack) + deriving (NFData, C.Generic, C.NFDataX, Eq, C.BitPack) --- M2S signals can contain undefined values, hence 'Show' is implemented through 'ShowX' +instance + (C.ShowX dat, C.KnownNat addressWidth, C.KnownNat selWidth) => + C.ShowX (WishboneM2S addressWidth selWidth dat) + where + showX = show + +-- Compact printing for M2S values. This handles undefined values in the +-- structure too. instance (C.ShowX dat, C.KnownNat addressWidth, C.KnownNat selWidth) => Show (WishboneM2S addressWidth selWidth dat) where - show = C.showX + + show WishboneM2S{..} = + "WishboneM2S [ " <> + prefix busCycle <> "CYC " <> + prefix strobe <> "STB " <> + prefix writeEnable <> "WE, " <> + "ADR = " <> C.showX addr <> ", " <> + "DAT = " <> C.showX writeData <> ", " <> + "SEL = " <> C.showX busSelect <> ", " <> + "CTE = " <> cycle' <> ", " <> + "BTE = " <> burst <> + " ]" + where + prefix True = " " + prefix False = "!" + + burst = case burstTypeExtension of + LinearBurst -> "linear" + Beat4Burst -> "beat 4" + Beat8Burst -> "beat 8" + Beat16Burst -> "beat 16" + + cycle' = case cycleTypeIdentifier of + Classic -> "classic" + ConstantAddressBurst -> "constant addr" + IncrementingBurst -> "incrementing" + EndOfBurst -> "end-of-burst" + CycleTypeIdentifier val -> "reserved (" <> C.showX val <> ")" -- | Data communicated from a Wishbone Slave to a Wishbone Master data WishboneS2M dat = WishboneS2M @@ -92,11 +127,25 @@ data WishboneS2M dat = WishboneS2M -- is defined by the IP core supplier. Also see the [ERR_O] and [RTY_O] signal descriptions. retry :: "RTY" ::: Bool } - deriving (NFData, C.Generic, C.NFDataX, C.ShowX, Eq, C.BitPack) + deriving (NFData, C.Generic, C.NFDataX, Eq, C.BitPack) + +instance (C.ShowX dat) => C.ShowX (WishboneS2M dat) where + showX = show --- S2M signals can contain undefined values, hence 'Show' is implemented through 'ShowX' +-- Compact printing for S2M values. This handles undefined values in the +-- structure too. instance (C.ShowX dat) => Show (WishboneS2M dat) where - show = C.showX + show WishboneS2M{..} = + "WishboneS2M [ " <> + prefix acknowledge <> "ACK " <> + prefix err <> "ERR " <> + prefix stall <> "STALL " <> + prefix stall <> "RETRY, " <> + "DAT = " <> C.showX readData <> + " ]" + where + prefix True = " " + prefix False = "!" -- | Identifier for different types of cycle-modes, used to potentially -- increase throughput by reducing handshake-overhead diff --git a/src/Protocols/Wishbone/Standard.hs b/src/Protocols/Wishbone/Standard.hs index 2dad39b4..7e0a4c42 100644 --- a/src/Protocols/Wishbone/Standard.hs +++ b/src/Protocols/Wishbone/Standard.hs @@ -10,7 +10,7 @@ import qualified Data.Bifunctor as B import Protocols import Protocols.Internal import Protocols.Wishbone -import Prelude hiding (head, not, repeat, (!!), (&&)) +import Prelude hiding (head, not, repeat, (!!), (&&), (||)) -- | Distribute requests amongst N slave circuits roundrobin :: @@ -95,6 +95,10 @@ crossbarSwitch = Circuit go m2ss1 = scatter @_ @_ @_ @_ @0 (repeat emptyWishboneM2S) <$> route <*> m2ss0 s2ms1 = gather <$> s2ms0 <*> route +-- | State for making guaranteeing correct timing of responses in 'memoryWb' +data MemoryDelayState = Wait | AckRead + deriving (Generic, NFDataX) + -- | Memory component circuit using a specific RAM function -- -- This circuit uses 'Standard' mode and only supports the classic cycle type. @@ -122,7 +126,20 @@ memoryWb :: Circuit (Wishbone dom 'Standard addressWidth a) () memoryWb ram = Circuit go where - go (m2s, ()) = (reply m2s, ()) + go (m2s, ()) = (mux inCycle s2m1 (pure emptyWishboneS2M), ()) + where + inCycle = (busCycle <$> m2s) .&&. (strobe <$> m2s) + s2m0 = reply m2s + s2m1 = mealy delayControls Wait (bundle (m2s, s2m0)) + + delayControls st (m2s, s2m) + -- no need to delay non-ACK responses + | err s2m || retry s2m = (Wait, s2m) + -- write requests can be ACKed directly + | Wait <- st, writeEnable m2s = (Wait, emptyWishboneS2M { acknowledge = True }) + -- read ACKs need to be delayed one cycle + | Wait <- st, otherwise = (AckRead, emptyWishboneS2M) + | AckRead <- st = (Wait, s2m) reply :: Signal dom (WishboneM2S addressWidth (BitSize a `DivRU` 8) a) -> @@ -135,21 +152,16 @@ memoryWb ram = Circuit go where addr1 = addr <$> request writeData1 = writeData <$> request - isWriteRequest = (\WishboneM2S {..} -> writeEnable && strobe && busCycle) <$> request + writeAck = (\WishboneM2S {..} -> writeEnable && strobe && busCycle) <$> request write = mux - isWriteRequest + writeAck (Just <$> ((,) <$> addr1 <*> writeData1)) (pure Nothing) - writeAck = isRising False isWriteRequest - - isReadRequest = (\WishboneM2S {..} -> writeEnable && strobe && busCycle) <$> request - justReadRequest = isRising False isReadRequest + readAck = (\WishboneM2S {..} -> writeEnable && strobe && busCycle) <$> request requestValid = (busCycle <$> request) .&&. (strobe <$> request) - readAck = register False justReadRequest - readValue = ram addr1 write isError = requestValid .&&. (/= maxBound) <$> (busSelect <$> request) diff --git a/src/Protocols/Wishbone/Standard/Hedgehog.hs b/src/Protocols/Wishbone/Standard/Hedgehog.hs index 5e70426e..4a66d71c 100644 --- a/src/Protocols/Wishbone/Standard/Hedgehog.hs +++ b/src/Protocols/Wishbone/Standard/Hedgehog.hs @@ -206,6 +206,7 @@ stallStandard stallsPerCycle = B.second (emptyWishboneM2S :-) . uncurry (go stallsPerCycle Nothing) where + go :: [Int] -> Maybe (WishboneS2M a) -> @@ -274,6 +275,19 @@ stallStandard stallsPerCycle = -- master cancelled cycle | otherwise = B.bimap (emptyWishboneS2M :-) (m :-) (go stalls Nothing m2s s2m) + +data DriverState addressWidth a + = -- | State in which the driver still needs to perform N resets + DSReset Int [(WishboneMasterRequest addressWidth a, Int)] + -- | State in which the driver is issuing a new request to the slave + | DSNewRequest (WishboneMasterRequest addressWidth a) Int [(WishboneMasterRequest addressWidth a, Int)] + -- | State in which the driver is waiting (and holding the request) for the slave to reply + | DSWaitForReply (WishboneMasterRequest addressWidth a) Int [(WishboneMasterRequest addressWidth a, Int)] + -- | State in which the driver is waiting for N cycles before starting a new request + | DSStall Int [(WishboneMasterRequest addressWidth a, Int)] + -- | State in which the driver has no more work to do + | DSDone + -- | Create a wishbone 'Standard' circuit to drive other circuits. driveStandard :: forall dom a addressWidth. @@ -286,17 +300,22 @@ driveStandard :: ) => ExpectOptions -> -- | Requests to send out - [WishboneMasterRequest addressWidth a] -> + [(WishboneMasterRequest addressWidth a, Int)] -> Circuit () (Wishbone dom 'Standard addressWidth a) -driveStandard ExpectOptions {..} reqs = +driveStandard ExpectOptions {..} requests = Circuit $ ((),) . C.fromList_lazy . (emptyWishboneM2S :) - . go eoResetCycles reqs + . go (DSReset eoResetCycles requests) . (\s -> C.sample_lazy s) . snd where + + go st0 ~(s2m : s2ms) = + let (st1, m2s) = step st0 s2m + in m2s : (s2m `C.seqX` go st1 s2ms) + transferToSignals :: forall b addrWidth. ( C.ShowX b, @@ -325,24 +344,23 @@ driveStandard ExpectOptions {..} reqs = writeData = dat } - go :: - Int -> - [WishboneMasterRequest addressWidth a] -> - [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) - -- no more data to send - go _ [] ~(rep : replies) = emptyWishboneM2S : (rep `C.seqX` go 0 [] replies) - go _ (d : 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) - -- 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 - | otherwise -- trace "D in-cycle wait for ACK" $ - = - transferToSignals d : (rep `C.seqX` go 0 (d : dat) replies) + step :: + DriverState addressWidth a -> + -- | respone from *last* cycle + WishboneS2M a -> + (DriverState addressWidth a, WishboneM2S addressWidth (BitSize a `DivRU` 8) a) + step (DSReset _ []) _s2m = (DSDone, emptyWishboneM2S) + step (DSReset 0 ((req, n):reqs)) s2m = step (DSNewRequest req n reqs) s2m + step (DSReset n reqs) _s2m = (DSReset (n - 1) reqs, emptyWishboneM2S) + step (DSNewRequest req n reqs) _s2m = (DSWaitForReply req n reqs, transferToSignals req) + step (DSWaitForReply req n reqs) s2m + | acknowledge s2m || err s2m = step (DSStall n reqs) s2m + | retry s2m = (DSNewRequest req n reqs, emptyWishboneM2S) + | otherwise = (DSWaitForReply req n reqs, transferToSignals req) + step (DSStall 0 []) _s2m = (DSDone, emptyWishboneM2S) + step (DSStall 0 ((req, n):reqs)) s2m = step (DSNewRequest req n reqs) s2m + step (DSStall n reqs) _s2m = (DSStall (n - 1) reqs, emptyWishboneM2S) + step DSDone _s2m = (DSDone, emptyWishboneM2S) -- | Circuit which validates the wishbone communication signals between a -- master and a slave circuit. @@ -441,14 +459,13 @@ wishbonePropWithModel eOpts model circuit0 inputGen st = do n = P.length input genStall = Gen.integral (Range.linear 0 10) - stalls <- H.forAll (Gen.list (Range.singleton n) genStall) + reqStalls <- H.forAll (Gen.list (Range.singleton n) genStall) let - resets = 50 - driver = driveStandard @dom (defExpectOptions {eoResetCycles = resets}) input - stallC = stallStandard stalls - circuit1 = stallC |> validatorCircuit |> circuit0 - (_, _ : s2m) = observeComposedWishboneCircuit (eoTimeout eOpts) driver circuit1 + resets = 5 + driver = driveStandard @dom (defExpectOptions {eoResetCycles = resets}) (P.zip input reqStalls) + circuit1 = validatorCircuit |> circuit0 + (_, s2m) = observeComposedWishboneCircuit (eoTimeout eOpts) driver circuit1 matchModel 0 s2m input st === Right () where diff --git a/tests/Tests/Protocols/Wishbone.hs b/tests/Tests/Protocols/Wishbone.hs index 84a3e699..1998dc3c 100644 --- a/tests/Tests/Protocols/Wishbone.hs +++ b/tests/Tests/Protocols/Wishbone.hs @@ -46,6 +46,12 @@ genWishboneTransfer genA = Write <$> genDefinedBitVector <*> genDefinedBitVector <*> genA ] +genWbTransferPair :: + (KnownNat addressWidth, KnownNat (BitSize a)) => + Gen a -> + Gen (WishboneMasterRequest addressWidth a, Int) +genWbTransferPair genA = liftA2 (,) (genWishboneTransfer genA) genSmallInt + -- -- 'addrReadId' circuit -- @@ -78,11 +84,11 @@ addrReadIdWbModel :: addrReadIdWbModel (Read addr _) s@WishboneS2M {..} () | acknowledge && hasX readData == Right addr = Right () | otherwise = - Left $ "Read should have been acknowledged with address as DAT " <> showX s + Left $ "Read should have been acknowledged with address as DAT " <> show s addrReadIdWbModel 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 " <> show s prop_addrReadIdWb_model :: Property prop_addrReadIdWb_model = property $ @@ -122,18 +128,18 @@ memoryWbModel (Read addr sel) s st "Read from a known address did not yield the same value " <> showX x <> " : " - <> showX s + <> show s Nothing | acknowledge s && hasX (readData s) == Right def -> Right st Nothing | otherwise -> Left $ "Read from unknown address did no ACK with undefined result : " - <> showX s + <> show s memoryWbModel (Write addr sel a) s st | sel /= maxBound && err s = Right st | sel /= maxBound && not (err s) = Left "Write with non maxBound SEL should cause ERR response" | acknowledge s = Right ((addr, a) : st) - | otherwise = Left $ "Write should be acked : " <> showX s + | otherwise = Left $ "Write should be acked : " <> show s prop_memoryWb_model :: Property prop_memoryWb_model = property $ @@ -172,7 +178,7 @@ evaluateUnitCircuit n a b = prop_addrReadId_validator :: Property prop_addrReadId_validator = property $ do - reqs <- forAll $ genData (genWishboneTransfer @8 genDefinedBitVector) + reqs <- forAll $ genData (genWbTransferPair @8 genDefinedBitVector) let circuitSignalsN = withClockResetEnable @System clockGen resetGen enableGen $ @@ -186,7 +192,7 @@ prop_addrReadId_validator = property $ do prop_memoryWb_validator :: Property prop_memoryWb_validator = property $ do - reqs <- forAll $ genData (genWishboneTransfer @8 genDefinedBitVector) + reqs <- forAll $ genData (genWbTransferPair @8 genDefinedBitVector) let circuitSignalsN = withClockResetEnable @System clockGen resetGen enableGen $ @@ -206,7 +212,7 @@ prop_memoryWb_validator = property $ do prop_addrReadId_validator_lenient :: Property prop_addrReadId_validator_lenient = property $ do - reqs <- forAll $ genData (genWishboneTransfer @8 genDefinedBitVector) + reqs <- forAll $ genData (genWbTransferPair @8 genDefinedBitVector) let circuitSignalsN = withClockResetEnable @System clockGen resetGen enableGen $ @@ -221,7 +227,7 @@ prop_addrReadId_validator_lenient = property $ do prop_memoryWb_validator_lenient :: Property prop_memoryWb_validator_lenient = property $ do - reqs <- forAll $ genData (genWishboneTransfer @8 genDefinedBitVector) + reqs <- forAll $ genData (genWbTransferPair @8 genDefinedBitVector) let circuitSignalsN = withClockResetEnable @System clockGen resetGen enableGen $ @@ -237,7 +243,7 @@ prop_memoryWb_validator_lenient = property $ do prop_specViolation_lenient :: Property prop_specViolation_lenient = property $ do -- need AT LEAST one transaction so that multiple termination signals can be emitted - reqs <- forAll $ Gen.list (Range.linear 1 500) (genWishboneTransfer @8 genDefinedBitVector) + reqs <- forAll $ Gen.list (Range.linear 1 500) (genWbTransferPair @8 genDefinedBitVector) let circuitSignalsN = withClockResetEnable @System clockGen resetGen enableGen $