add 'common sense' wishbone validation (#47)

* add 'common sense' wishbone validation

* expose validator circuits

clash-protocols.cabal

@@ -132,7 +132,6 @@ library
     , hedgehog >= 1.0.2
     , pretty-show
     , strict-tuple
-
     , mtl
     , hashable
 

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)

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