From 4c9520d60b7e7b6c2e98e721f21fdaa1d8745cee Mon Sep 17 00:00:00 2001 From: Lara Herzog <74796302+cuddlefishie@users.noreply.github.com> Date: Wed, 24 Aug 2022 15:12:58 +0200 Subject: [PATCH] add 'common sense' wishbone validation (#47) * add 'common sense' wishbone validation * expose validator circuits --- clash-protocols.cabal | 1 - src/Protocols/Wishbone/Standard.hs | 12 +- src/Protocols/Wishbone/Standard/Hedgehog.hs | 277 ++++++++++++++++---- tests/Tests/Protocols/Wishbone.hs | 103 ++++---- 4 files changed, 290 insertions(+), 103 deletions(-) diff --git a/clash-protocols.cabal b/clash-protocols.cabal index 0464e3e5..fc096f24 100644 --- a/clash-protocols.cabal +++ b/clash-protocols.cabal @@ -132,7 +132,6 @@ library , hedgehog >= 1.0.2 , pretty-show , strict-tuple - , mtl , hashable diff --git a/src/Protocols/Wishbone/Standard.hs b/src/Protocols/Wishbone/Standard.hs index ba1a4f76..2dad39b4 100644 --- a/src/Protocols/Wishbone/Standard.hs +++ b/src/Protocols/Wishbone/Standard.hs @@ -104,6 +104,10 @@ crossbarSwitch = Circuit go -- The data rate could be increased by using registered feedback cycles or -- by using a pipelined circuit which would eliminate one wait cycle. -- +-- Since the underlying block RAM operates on values of @a@ directly, the only +-- accepted bus selector value is 'maxBound'. All other bus selector values +-- will cause an ERR response. +-- -- TODO create pipelined memory circuit memoryWb :: forall dom a addressWidth. @@ -124,9 +128,10 @@ memoryWb ram = Circuit go Signal dom (WishboneM2S addressWidth (BitSize a `DivRU` 8) a) -> Signal dom (WishboneS2M a) reply request = do - ack <- writeAck .||. readAck + ack <- (writeAck .||. readAck) .&&. (not <$> isError) .&&. requestValid + errVal <- isError val <- readValue - pure $ (emptyWishboneS2M @a) {acknowledge = ack, readData = val} + pure $ (emptyWishboneS2M @a) {acknowledge = ack, err = errVal, readData = val} where addr1 = addr <$> request writeData1 = writeData <$> request @@ -142,6 +147,9 @@ memoryWb ram = Circuit go isReadRequest = (\WishboneM2S {..} -> writeEnable && strobe && busCycle) <$> request justReadRequest = isRising False isReadRequest + 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 11f5984e..3c2d30c2 100644 --- a/src/Protocols/Wishbone/Standard/Hedgehog.hs +++ b/src/Protocols/Wishbone/Standard/Hedgehog.hs @@ -1,21 +1,44 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE MultiWayIf #-} -- | -- Types and functions to aid with testing Wishbone circuits. +-- +-- This module provides two "modes" of Wishbone Specification compliance checks: +-- +-- * "lenient" mode +-- +-- * "common sense" mode +-- +-- __\"lenient\" mode__ +-- +-- The Wishbone spec mostly specifies the handshake protocols but does not make many +-- assumptions about which signals *should* be valid in response to what. This is +-- presumably done so to allow circuits to be very flexible, however it makes for +-- a relatively weak validation tool. +-- +-- __\"common sense\" mode__ +-- +-- The Wishbone spec itself makes very little assumptions about how interactions +-- should look like outside of basic hand-shaking. +-- This "common sense" compliance checking additionally checks for: +-- - A read request is acked with defined data +-- - response data respects the 'busSelect' signal +-- - A write request must contain valid data according to the 'busSelect' signal module Protocols.Wishbone.Standard.Hedgehog ( WishboneMasterRequest (..), stallStandard, driveStandard, wishbonePropWithModel, + validatorCircuit, + validatorCircuitLenient ) where -import Clash.Prelude as C hiding (cycle, not, (&&), (||)) +import Clash.Prelude as C hiding (cycle, not, (&&), (||), indices) import Clash.Signal.Internal (Signal ((:-))) --- hedgehog -import Control.DeepSeq (NFData) --- me import qualified Data.Bifunctor as B import Hedgehog ((===)) import qualified Hedgehog as H @@ -25,63 +48,142 @@ import Protocols hiding (stallC, circuit) import Protocols.Hedgehog import Protocols.Wishbone import Prelude as P hiding (cycle) +import GHC.Stack (HasCallStack) -- | Datatype representing a single transaction request sent from a Wishbone Master to a Wishbone Slave data WishboneMasterRequest addressWidth dat - = Read (BitVector addressWidth) - | Write (BitVector addressWidth) dat - deriving (Show) + = Read (BitVector addressWidth) (BitVector (BitSize dat `DivRU` 8)) + | Write (BitVector addressWidth) (BitVector (BitSize dat `DivRU` 8)) dat -data WishboneStandardState - = WSSQuiet - | WSSInCycleNoStrobe - | WSSWaitForSlave +deriving instance (KnownNat addressWidth, KnownNat (BitSize a), Show a) => (Show (WishboneMasterRequest addressWidth a)) --- TODO add a SlaveHolding state? Spec seems unclear +-- +-- Validation for (lenient) spec compliance +-- -data WishboneStandardError - = WSEMoreThanOneTerminationSignalAsserted - | WSETerminationSignalOutsideOfCycle - deriving (NFData, Generic, NFDataX, Show, ShowX, Eq) +data LenientValidationState + = LVSQuiet + | LVSInCycleNoStrobe + | LVSWaitForSlave + deriving (Generic, NFDataX) -nextStateStandard :: - WishboneStandardState -> + +nextStateLenient :: + LenientValidationState -> WishboneM2S addressWidth (BitSize a `DivRU` 8) a -> WishboneS2M a -> - Either WishboneStandardError WishboneStandardState -nextStateStandard _ m2s s2m + Either String LenientValidationState +nextStateLenient _ m2s s2m | P.length (filter ($ s2m) [acknowledge, err, retry]) > 1 = - Left WSEMoreThanOneTerminationSignalAsserted + Left "More than one termination signal asserted" | not (busCycle m2s) && (acknowledge s2m || err s2m || retry s2m) = - Left WSETerminationSignalOutsideOfCycle -nextStateStandard WSSQuiet m2s _ - | busCycle m2s && P.not (strobe m2s) = Right WSSInCycleNoStrobe - | busCycle m2s && strobe m2s = Right WSSWaitForSlave - | otherwise = Right WSSQuiet -nextStateStandard WSSInCycleNoStrobe m2s _ - | not (busCycle m2s) = Right WSSQuiet - | busCycle m2s && strobe m2s = Right WSSWaitForSlave - | otherwise = Right WSSInCycleNoStrobe -nextStateStandard WSSWaitForSlave m2s s2m - | busCycle m2s && P.not (strobe m2s) = Right WSSInCycleNoStrobe - | not (busCycle m2s) = Right WSSQuiet - | acknowledge s2m || err s2m || retry s2m = Right WSSQuiet - | otherwise = Right WSSWaitForSlave + Left "Termination signals outside of a bus cycle" +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 + LVSInCycleNoStrobe -> + if + | not (busCycle m2s) -> Right LVSQuiet + | busCycle m2s && strobe m2s -> Right LVSWaitForSlave + | otherwise -> Right 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 + --- | Validate the input/output streams of a standard wishbone interface -- --- Returns 'Right ()' when the interactions comply with the spec. --- Returns 'Left (cycle, err)' when a spec violation was found. -validateStandard :: - [WishboneM2S addressWidth (BitSize a `DivRU` 8) a] -> - [WishboneS2M a] -> - Either (Int, WishboneStandardError) () -validateStandard m2s s2m = go 0 (P.zip m2s s2m) WSSQuiet +-- Validation for "common sense" compliance +-- + +type CommonSenseValidationError = String + +data CommonSenseValidationState + = CSVSQuiet + | CSVSInCycleNoStrobe + | CSVSReadCycle + | CSVSWriteCycle + deriving (Eq, Show, Generic, NFDataX) + +nextStateCommonSense :: + forall a addressWidth. + (BitPack a) => + CommonSenseValidationState -> + WishboneM2S addressWidth (BitSize a `DivRU` 8) a -> + WishboneS2M a -> + Either CommonSenseValidationError (Bool, CommonSenseValidationState) +-- ^ go to next cycle +nextStateCommonSense _ _ s2m + | P.length (filter ($ s2m) [acknowledge, err, retry]) > 1 = + Left "More than one termination signal asserted" +nextStateCommonSense state m2s@WishboneM2S{..} s2m@WishboneS2M{..} = case state of + CSVSQuiet -> + if + | busCycle && not strobe -> Right (True, CSVSInCycleNoStrobe) + | busCycle && strobe && writeEnable -> Right (False, CSVSWriteCycle) + | busCycle && strobe && not writeEnable -> Right (False, CSVSReadCycle) + | hasTerminateFlag s2m -> Left "Termination signals outside of a bus cycle" + | otherwise -> Right (True, CSVSQuiet) + CSVSInCycleNoStrobe -> + if + | not busCycle -> Right (True, CSVSQuiet) + | not strobe -> Right (True, CSVSInCycleNoStrobe) + | writeEnable -> Right (False, CSVSWriteCycle) + | not writeEnable -> Right (False, CSVSReadCycle) + | otherwise -> C.error "Should not happen" + CSVSReadCycle -> + if + | not busCycle -> Right (True, CSVSQuiet) + | not strobe -> Right (True, CSVSInCycleNoStrobe) + | acknowledge -> + if responseValid m2s s2m + then Right (True, CSVSQuiet) + else Left "read-response does not respect SEL" + | err || retry -> Right (True, CSVSQuiet) + | writeEnable -> Left "asserted WE while in a read cycle" + | otherwise -> Right (True, CSVSReadCycle) + CSVSWriteCycle -> + if + | not busCycle -> Right (True, CSVSQuiet) + | not strobe -> Right (True, CSVSInCycleNoStrobe) + | not writeEnable -> Left "deasserted WE while in a write cycle" + | not $ requestValid m2s -> Left "write request does not respect SEL" + | err || retry -> Right (True, CSVSQuiet) + | acknowledge -> Right (True, CSVSQuiet) + | otherwise -> Right (True, CSVSWriteCycle) + where + responseValid WishboneM2S{busSelect=sel} WishboneS2M{readData=dat} = selectValidData sel dat + requestValid WishboneM2S{busSelect=sel, writeData=dat} = selectValidData sel dat + +-- | This function checks whether all bytes selected by \"SEL\" in a value +-- contain defined data. +selectValidData :: + forall a. + (HasCallStack, KnownNat (BitSize a), BitPack a) => + BitVector (BitSize a `DivRU` 8) -> + a -> + Bool +selectValidData byteSelect rawDat = + all + (== False) + [ hasUndefined part + | idx <- indices byteSelect, + let part = dat ! idx + ] where - go _ [] _ = Right () - go n ((fwd, bwd) : rest) st0 = case nextStateStandard st0 fwd bwd of - Left e -> Left (n, e) - Right st1 -> go (n + 1) rest st1 + dat :: C.Vec (BitSize a `DivRU` 8) (BitVector 8) + dat = case maybeIsX rawDat of + Just val -> bitCoerce $ resize (bitCoerce val :: BitVector (BitSize a)) + Nothing -> C.deepErrorX "value to be 'select-checked' has an undefined spine" + + indices :: forall n. (KnownNat n) => BitVector n -> [Index n] + indices bv = filter (testBit bv . fromIntegral) [0 .. maxBound] + -- | Create a stalling wishbone 'Standard' circuit. stallStandard :: @@ -204,18 +306,20 @@ driveStandard ExpectOptions {..} reqs = ) => WishboneMasterRequest addrWidth b -> WishboneM2S addrWidth (BitSize b `DivRU` 8) b - transferToSignals (Read addr) = + transferToSignals (Read addr sel) = (emptyWishboneM2S @addrWidth @b) { busCycle = True, strobe = True, addr = addr, + busSelect = sel, writeEnable = False } - transferToSignals (Write addr dat) = + transferToSignals (Write addr sel dat) = (emptyWishboneM2S @addrWidth @b) { busCycle = True, strobe = True, addr = addr, + busSelect = sel, writeEnable = True, writeData = dat } @@ -239,6 +343,70 @@ driveStandard ExpectOptions {..} reqs = = transferToSignals d : (rep `C.seqX` go 0 (d : dat) replies) +-- | Circuit which validates the wishbone communication signals between a +-- master and a slave circuit. +-- +-- Halts execution using 'error' when a "common sense" spec validation occurs. +-- +-- N.B. Not synthesisable. +validatorCircuit :: + forall dom addressWidth a. + ( HasCallStack, + HiddenClockResetEnable dom, + KnownNat addressWidth, + BitPack a, + NFDataX a, + ShowX a + ) => + Circuit (Wishbone dom 'Standard addressWidth a) (Wishbone dom 'Standard addressWidth a) +validatorCircuit = + Circuit $ mealyB go (0 :: Integer, (emptyWishboneM2S, emptyWishboneS2M), CSVSQuiet) + where + go (cycle, (m2s0, s2m0), state0) (m2s1, s2m1) = + case nextStateCommonSense state0 m2s0 s2m0 of + Left err -> + error $ + "Wishbone common-sense validation error on cycle " + <> show cycle + <> ": " <> err + <> "\n\n" + <> "M2S: " <> show m2s0 <> "\n" + <> "S2M: " <> show s2m0 + Right (True, state1) -> ((cycle + 1, (m2s1, s2m1), state1), (s2m1, m2s1)) + Right (False, state1) -> go (cycle, (m2s0, s2m0), state1) (m2s1, s2m1) + + +-- | Circuit which validates the wishbone communication signals between a +-- master and a slave circuit. +-- +-- Halts execution using 'error' when a spec validation occurs. +-- +-- N.B. Not synthesisable. +validatorCircuitLenient :: + forall dom addressWidth a. + ( HasCallStack, + HiddenClockResetEnable dom, + KnownNat addressWidth, + BitPack a, + NFDataX a, + ShowX a + ) => + Circuit (Wishbone dom 'Standard addressWidth a) (Wishbone dom 'Standard addressWidth a) +validatorCircuitLenient = + Circuit $ mealyB go (0 :: Integer, (emptyWishboneM2S, emptyWishboneS2M), LVSQuiet) + where + go (cycle, (m2s0, s2m0), state0) (m2s1, s2m1) = + case nextStateLenient state0 m2s0 s2m0 of + Left err -> + error $ + "Wishbone lenient validation error on cycle " + <> show cycle + <> ": " <> err + <> "\n\n" + <> "M2S: " <> show m2s0 <> "\n" + <> "S2M: " <> show s2m0 + Right state1 -> ((cycle + 1, (m2s1, s2m1), state1), (s2m1, m2s1)) + -- | Test a wishbone 'Standard' circuit against a pure model. wishbonePropWithModel :: forall dom a addressWidth st. @@ -247,8 +415,9 @@ wishbonePropWithModel :: Show a, C.NFDataX a, C.KnownNat addressWidth, - C.KnownDomain dom, - C.KnownNat (C.BitSize a) + C.HiddenClockResetEnable dom, + C.KnownNat (C.BitSize a), + C.BitPack a ) => ExpectOptions -> -- | Check whether a S2M signal for a given request is matching a pure model using @st@ @@ -275,10 +444,8 @@ wishbonePropWithModel eOpts model circuit0 inputGen st = H.property $ do resets = 50 driver = driveStandard @dom (defExpectOptions {eoResetCycles = resets}) input stallC = stallStandard stalls - circuit1 = stallC |> circuit0 - (m2s, _ : s2m) = observeComposedWishboneCircuit (eoTimeout eOpts) driver circuit1 - - validateStandard m2s s2m === Right () + circuit1 = stallC |> 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 36db1f15..f4e2801d 100644 --- a/tests/Tests/Protocols/Wishbone.hs +++ b/tests/Tests/Protocols/Wishbone.hs @@ -7,9 +7,8 @@ module Tests.Protocols.Wishbone where import Clash.Hedgehog.Sized.BitVector -import Clash.Prelude hiding ((&&)) +import Clash.Prelude hiding (not, (&&)) import Control.DeepSeq (NFData) -import Data.Either (isLeft) import Hedgehog import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range @@ -34,59 +33,60 @@ genData :: Gen a -> Gen [a] genData = Gen.list (Range.linear 0 150) genWishboneTransfer :: - (KnownNat addressWidth) => + (KnownNat addressWidth, KnownNat (BitSize a)) => Gen a -> Gen (WishboneMasterRequest addressWidth a) genWishboneTransfer genA = Gen.choice - [ Read <$> genDefinedBitVector, - Write <$> genDefinedBitVector <*> genA + [ Read <$> genDefinedBitVector <*> genDefinedBitVector , + Write <$> genDefinedBitVector <*> genDefinedBitVector <*> genA ] -- --- 'id' circuit +-- 'addrReadId' circuit -- -idWriteWbSt :: - forall a dom addressWidth. - (BitPack a, NFDataX a) => - Circuit (Wishbone dom 'Standard addressWidth a) () -idWriteWbSt = Circuit go +addrReadIdWb :: + forall dom addressWidth. + (KnownNat addressWidth) => + Circuit (Wishbone dom 'Standard addressWidth (BitVector addressWidth)) () +addrReadIdWb = Circuit go where go (m2s, ()) = (reply <$> m2s, ()) reply WishboneM2S {..} | busCycle && strobe && writeEnable = - (emptyWishboneS2M @a) + emptyWishboneS2M { acknowledge = True } + | busCycle && strobe = + (emptyWishboneS2M @(BitVector addressWidth)) { acknowledge = True, - readData = writeData + readData = addr } - | busCycle && strobe = emptyWishboneS2M {acknowledge = True} | otherwise = emptyWishboneS2M -idWriteStModel :: - (NFData a, Eq a, ShowX a) => - WishboneMasterRequest addressWidth a -> - WishboneS2M a -> +addrReadIdWbModel :: + (KnownNat addressWidth) => + WishboneMasterRequest addressWidth (BitVector addressWidth) -> + WishboneS2M (BitVector addressWidth) -> -- | pure state () -> Either String () -idWriteStModel (Read _) s@WishboneS2M {..} () - | acknowledge && isLeft (hasX readData) = Right () +addrReadIdWbModel (Read addr _) s@WishboneS2M {..} () + | acknowledge && hasX readData == Right addr = Right () | otherwise = - Left $ "Read should have been acknowledged with no DAT " <> showX s -idWriteStModel (Write _ a) s@WishboneS2M {..} () - | acknowledge && hasX readData == Right a = Right () + Left $ "Read should have been acknowledged with address as DAT " <> showX s +addrReadIdWbModel Write {} s@WishboneS2M {..} () + | acknowledge && hasUndefined readData = Right () | otherwise = - Left $ "Write should have been acknowledged with write-data as DAT " <> showX s + Left $ "Write should have been acknowledged with no DAT " <> showX s -prop_idWriteSt_model :: Property -prop_idWriteSt_model = +prop_addrReadIdWb_model :: Property +prop_addrReadIdWb_model = withClockResetEnable clockGen resetGen enableGen $ wishbonePropWithModel @System defExpectOptions - idWriteStModel - idWriteWbSt - (genData $ genWishboneTransfer @10 genSmallInt) + addrReadIdWbModel + addrReadIdWb + (genData $ genWishboneTransfer @10 genDefinedBitVector) () -- @@ -94,26 +94,39 @@ prop_idWriteSt_model = -- memoryWbModel :: - (KnownNat addressWidth, Eq a, ShowX a, NFDataX a, NFData a, Default a) => + ( KnownNat addressWidth, + Eq a, + ShowX a, + NFDataX a, + NFData a, + Default a, + KnownNat (BitSize a) + ) => WishboneMasterRequest addressWidth a -> WishboneS2M a -> [(BitVector addressWidth, a)] -> Either String [(BitVector addressWidth, a)] -memoryWbModel (Read addr) s st - = case lookup addr st of - Just x | readData s == x && acknowledge s -> Right st - Just x | otherwise -> - Left $ - "Read from a known address did not yield the same value " - <> showX x - <> " : " - <> showX 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 -memoryWbModel (Write addr a) s st +memoryWbModel (Read addr sel) s st + | sel /= maxBound && err s = Right st + | sel /= maxBound && not (err s) = + Left "Read with non maxBound SEL should cause ERR response" + | otherwise = case lookup addr st of + Just x | readData s == x && acknowledge s -> Right st + Just x | otherwise -> + Left $ + "Read from a known address did not yield the same value " + <> showX x + <> " : " + <> showX 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 +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