Merge pull request #184 from clash-lang/specialize-wishbone

Specialize payload of `Wishbone` to be `BitVector (w * 8)`.

Author: lmbollen

clash-protocols/src/Data/Constraint/Nat/Extra.hs

@@ -12,12 +12,6 @@ import Clash.Prelude
 import Data.Constraint
 import Unsafe.Coerce (unsafeCoerce)
 
-{- | Postulates that multiplying some number /a/ by some constant /b/, and
-subsequently dividing that result by /b/ equals /a/.
--}
-cancelMulDiv :: forall a b. (1 <= b) => Dict (DivRU (a * b) b ~ a)
-cancelMulDiv = unsafeCoerce (Dict :: Dict (0 ~ 0))
-
 -- | if (1 <= b) then (Mod a b + 1 <= b)
 leModulusDivisor :: forall a b. (1 <= b) => Dict (Mod a b + 1 <= b)
 leModulusDivisor = unsafeCoerce (Dict :: Dict (0 <= 0))

clash-protocols/src/Protocols/Wishbone.hs

@@ -8,7 +8,7 @@ Types modelling the Wishbone bus protocol.
 -}
 module Protocols.Wishbone where
 
-import Clash.Prelude (DivRU, Nat, Type, (:::))
+import Clash.Prelude (Nat, (:::))
 import Prelude hiding (head, not, (&&))
 
 import Clash.Signal.Internal (Signal (..))
@@ -19,17 +19,17 @@ import Protocols.Idle
 import Clash.Prelude qualified as C
 
 -- | Data communicated from a Wishbone Master to a Wishbone Slave
-data WishboneM2S addressWidth selWidth dat = WishboneM2S
-  { addr :: "ADR" ::: C.BitVector addressWidth
+data WishboneM2S addressBits dataBytes = WishboneM2S
+  { addr :: "ADR" ::: C.BitVector addressBits
   -- ^ The address output array [ADR_O()] is used to pass a binary address. The higher array
   --   boundary is specific to the address width of the core, and the lower array boundary is
   --   determined by the data port size and granularity. For example the array size on a 32-bit
   --   data port with BYTE granularity is [ADR_O(n..2)]. In some cases (such as FIFO
   --   interfaces) the array may not be present on the interface.
-  , writeData :: "DAT_MOSI" ::: dat
+  , writeData :: "DAT_MOSI" ::: C.BitVector (dataBytes C.* 8)
   -- ^ The data output array [DAT_O()] is used to pass binary data. The array boundaries are
   --   determined by the port size, with a maximum port size of 64-bits (e.g. [DAT_I(63..0)]).
-  , busSelect :: "SEL" ::: C.BitVector selWidth
+  , busSelect :: "SEL" ::: C.BitVector dataBytes
   -- ^ The select output array [SEL_O()] indicates where valid data is expected on the [DAT_I()]
   --   signal array during READ cycles, and where it is placed on the [DAT_O()] signal array
   --   during WRITE cycles. The array boundaries are determined by the granularity of a port.
@@ -69,16 +69,16 @@ data WishboneM2S addressWidth selWidth dat = WishboneM2S
   deriving (NFData, C.Generic, C.NFDataX, Eq, C.BitPack)
 
 instance
-  (C.ShowX dat, C.KnownNat addressWidth, C.KnownNat selWidth) =>
-  C.ShowX (WishboneM2S addressWidth selWidth dat)
+  (C.KnownNat addressBits, C.KnownNat dataBytes) =>
+  C.ShowX (WishboneM2S addressBits dataBytes)
   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)
+  (C.KnownNat addressBits, C.KnownNat dataBytes) =>
+  Show (WishboneM2S addressBits dataBytes)
   where
   show WishboneM2S{..} =
     "WishboneM2S [ "
@@ -121,8 +121,8 @@ instance
       CycleTypeIdentifier val -> "reserved (" <> C.showX val <> ")"
 
 -- | Data communicated from a Wishbone Slave to a Wishbone Master
-data WishboneS2M dat = WishboneS2M
-  { readData :: "DAT_MISO" ::: dat
+data WishboneS2M dataBytes = WishboneS2M
+  { readData :: "DAT_MISO" ::: C.BitVector (dataBytes C.* 8)
   -- ^ The data output array [DAT_O()] is used to pass binary data. The array boundaries are
   --   determined by the port size, with a maximum port size of 64-bits (e.g. [DAT_I(63..0)]).
   , acknowledge :: "ACK" ::: Bool
@@ -143,12 +143,12 @@ data WishboneS2M dat = WishboneS2M
   }
   deriving (NFData, C.Generic, C.NFDataX, Eq, C.BitPack)
 
-instance (C.ShowX dat) => C.ShowX (WishboneS2M dat) where
+instance (C.KnownNat dataBytes) => C.ShowX (WishboneS2M dataBytes) where
   showX = show
 
 -- Compact printing for S2M values. This handles undefined values in the
 -- structure too.
-instance (C.ShowX dat) => Show (WishboneS2M dat) where
+instance (C.KnownNat dataBytes) => Show (WishboneS2M dataBytes) where
   show WishboneS2M{..} =
     "WishboneS2M [ "
       <> prefix acknowledge
@@ -217,27 +217,27 @@ data
   Wishbone
     (dom :: C.Domain)
     (mode :: WishboneMode)
-    (addressWidth :: Nat)
-    (userType :: Type)
+    (addressBits :: Nat)
+    (dataBytes :: Nat)
 
-instance Protocol (Wishbone dom mode addressWidth dat) where
+instance Protocol (Wishbone dom mode addressBits dataBytes) where
   type
-    Fwd (Wishbone dom mode addressWidth dat) =
-      Signal dom (WishboneM2S addressWidth (C.BitSize dat `DivRU` 8) dat)
+    Fwd (Wishbone dom mode addressBits dataBytes) =
+      Signal dom (WishboneM2S addressBits dataBytes)
 
-  type Bwd (Wishbone dom mode addressWidth dat) = Signal dom (WishboneS2M dat)
+  type Bwd (Wishbone dom mode addressBits dataBytes) = Signal dom (WishboneS2M dataBytes)
 
 instance
-  (C.KnownNat aw, C.KnownNat (C.BitSize dat), C.NFDataX dat) =>
-  IdleCircuit (Wishbone dom mode aw dat)
+  (C.KnownNat aw, C.KnownNat dw) =>
+  IdleCircuit (Wishbone dom mode aw dw)
   where
   idleFwd _ = C.pure emptyWishboneM2S
   idleBwd _ = C.pure emptyWishboneS2M
 
 -- | Construct "default" Wishbone M2S signals
 emptyWishboneM2S ::
-  (C.KnownNat addressWidth, C.KnownNat (C.BitSize dat), C.NFDataX dat) =>
-  WishboneM2S addressWidth (C.BitSize dat `DivRU` 8) dat
+  (C.KnownNat addressBits, C.KnownNat dataBytes) =>
+  WishboneM2S addressBits dataBytes
 emptyWishboneM2S =
   WishboneM2S
     { addr = C.deepErrorX "M2S address not defined"
@@ -252,7 +252,7 @@ emptyWishboneM2S =
     }
 
 -- | Construct "default" Wishbone S2M signals
-emptyWishboneS2M :: (C.NFDataX dat) => WishboneS2M dat
+emptyWishboneS2M :: (C.KnownNat dataBytes) => WishboneS2M dataBytes
 emptyWishboneS2M =
   WishboneS2M
     { readData = C.deepErrorX "S2M readData not defined"
@@ -267,56 +267,55 @@ whether transactions are in progress(returns true for any 'hasTerminateFlag').
 This is useful to determine whether a Wishbone bus is active.
 
 >>> :{
-let m2s = (emptyWishboneM2S @32 @()){busCycle = True, strobe = True}
+let m2s = (emptyWishboneM2S @32 @4){busCycle = True, strobe = True}
     s2m = emptyWishboneS2M{acknowledge = True}
   in hasBusActivity (m2s, s2m)
 :}
 True
 
 >>> :{
-let m2s = (emptyWishboneM2S @32 @()){busCycle = True, strobe = True}
+let m2s = (emptyWishboneM2S @32 @4){busCycle = True, strobe = True}
     s2m = emptyWishboneS2M{retry = True}
   in hasBusActivity (m2s, s2m)
 :}
 True
 
 >>> :{
-let m2s = (emptyWishboneM2S @32 @()){busCycle = True}
+let m2s = (emptyWishboneM2S @32 @4){busCycle = True}
     s2m = emptyWishboneS2M{acknowledge = True}
   in hasBusActivity (m2s, s2m)
 :}
 False
 
 >>> :{
-let m2s = (emptyWishboneM2S @32 @()){busCycle = True, strobe = True}
+let m2s = (emptyWishboneM2S @32 @4){busCycle = True, strobe = True}
     s2m = emptyWishboneS2M
   in hasBusActivity (m2s, s2m)
 :}
 False
 
 >>> :{
-let m2s = emptyWishboneM2S @32 @()
+let m2s = emptyWishboneM2S @32 @4
     s2m = emptyWishboneS2M{acknowledge = True}
   in hasBusActivity (m2s, s2m)
 :}
 False
 -}
-hasBusActivity :: (WishboneM2S addressWidth sel dat, WishboneS2M dat) -> Bool
+hasBusActivity :: (WishboneM2S addressBits dataBytes, WishboneS2M dataBytes) -> Bool
 hasBusActivity (m2s, s2m) = busCycle m2s C.&& strobe m2s C.&& hasTerminateFlag s2m
 
 -- | Helper function to determine whether a Slave signals the termination of a cycle.
-hasTerminateFlag :: WishboneS2M dat -> Bool
+hasTerminateFlag :: WishboneS2M dataBytes -> Bool
 hasTerminateFlag s2m = acknowledge s2m || err s2m || retry s2m
 
 {- | Force a /nack/ on the backward channel and /no data/ on the forward
 channel if reset is asserted.
 -}
 forceResetSanity ::
-  forall dom mode aw a.
+  forall dom mode aw dw.
   ( C.HiddenClockResetEnable dom
   , C.KnownNat aw
-  , C.KnownNat (C.BitSize a)
-  , C.NFDataX a
+  , C.KnownNat dw
   ) =>
-  Circuit (Wishbone dom mode aw a) (Wishbone dom mode aw a)
+  Circuit (Wishbone dom mode aw dw) (Wishbone dom mode aw dw)
 forceResetSanity = forceResetSanityGeneric

clash-protocols/src/Protocols/Wishbone/Standard.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE ApplicativeDo #-}
-{-# LANGUAGE RecordWildCards #-}
 {-# OPTIONS_GHC -fconstraint-solver-iterations=10 #-}
 
 -- | Circuits and utils for working with Standard mode wishbone circuits.
@@ -13,17 +12,16 @@ import Prelude hiding (head, not, repeat, (!!), (&&), (||))
 
 -- | Distribute requests amongst N slave circuits
 roundrobin ::
-  forall n dom addressWidth a.
+  forall n dom addressBits dataBytes.
   ( KnownNat n
   , HiddenClockResetEnable dom
-  , KnownNat addressWidth
-  , KnownNat (BitSize a)
-  , NFDataX a
+  , KnownNat addressBits
+  , KnownNat dataBytes
   , 1 <= n
   ) =>
   Circuit
-    (Wishbone dom 'Standard addressWidth a)
-    (Vec n (Wishbone dom 'Standard addressWidth a))
+    (Wishbone dom 'Standard addressBits dataBytes)
+    (Vec n (Wishbone dom 'Standard addressBits dataBytes))
 roundrobin = Circuit $ \(m2s, s2ms) -> B.first head $ fn (singleton m2s, s2ms)
  where
   Circuit fn = sharedBus selectFn
@@ -35,26 +33,25 @@ roundrobin = Circuit $ \(m2s, s2ms) -> B.first head $ fn (singleton m2s, s2ms)
   A selector signal is used to compute the next M-S pair.
 -}
 sharedBus ::
-  forall n m dom addressWidth a.
+  forall n m dom addressBits dataBytes.
   ( KnownNat n
   , KnownNat m
   , HiddenClockResetEnable dom
-  , KnownNat addressWidth
-  , KnownNat (BitSize a)
-  , NFDataX a
+  , KnownNat addressBits
+  , KnownNat dataBytes
   ) =>
   -- | Funcion to select which M-S pair should be connected next.
   ( Signal
       dom
       ( Index n
       , Index m
-      , Vec n (WishboneM2S addressWidth (BitSize a `DivRU` 8) a)
+      , Vec n (WishboneM2S addressBits dataBytes)
       ) ->
     Signal dom (Index n, Index m)
   ) ->
   Circuit
-    (Vec n (Wishbone dom 'Standard addressWidth a))
-    (Vec m (Wishbone dom 'Standard addressWidth a))
+    (Vec n (Wishbone dom 'Standard addressBits dataBytes))
+    (Vec m (Wishbone dom 'Standard addressBits dataBytes))
 sharedBus selectFn = Circuit go
  where
   go (bundle -> m2ss0, bundle -> s2ms0) = (unbundle s2ms1, unbundle m2ss1)
@@ -74,19 +71,18 @@ sharedBus selectFn = Circuit go
 
 -- | Crossbar-Switch circuit, allowing to dynamically route N masters to N slaves
 crossbarSwitch ::
-  forall n m dom addressWidth a.
+  forall n m dom addressBits dataBytes.
   ( KnownNat n
   , KnownNat m
   , KnownDomain dom
-  , KnownNat addressWidth
-  , NFDataX a
-  , KnownNat (BitSize a)
+  , KnownNat addressBits
+  , KnownNat dataBytes
   ) =>
   Circuit
     ( CSignal dom (Vec n (Index m)) -- route
-    , Vec n (Wishbone dom 'Standard addressWidth a) -- masters
+    , Vec n (Wishbone dom 'Standard addressBits dataBytes) -- masters
     )
-    (Vec m (Wishbone dom 'Standard addressWidth a)) -- slaves
+    (Vec m (Wishbone dom 'Standard addressBits dataBytes)) -- slaves
 crossbarSwitch = Circuit go
  where
   go ((route, bundle -> m2ss0), bundle -> s2ms0) =
@@ -108,26 +104,24 @@ data MemoryDelayState = Wait | AckRead
   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
+  Since the underlying block RAM operates on the whole bitvector, 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.
-  ( BitPack a
-  , NFDataX a
-  , KnownDomain dom
-  , KnownNat addressWidth
+  forall dom addressBits dataBytes.
+  ( KnownDomain dom
+  , KnownNat addressBits
+  , KnownNat dataBytes
   , HiddenClockResetEnable dom
-  , Default a
   ) =>
-  ( Signal dom (BitVector addressWidth) ->
-    Signal dom (Maybe (BitVector addressWidth, a)) ->
-    Signal dom a
+  ( Signal dom (BitVector addressBits) ->
+    Signal dom (Maybe (BitVector addressBits, BitVector (dataBytes * 8))) ->
+    Signal dom (BitVector (dataBytes * 8))
   ) ->
-  Circuit (Wishbone dom 'Standard addressWidth a) ()
+  Circuit (Wishbone dom 'Standard addressBits dataBytes) ()
 memoryWb ram = Circuit go
  where
   go (m2s, ()) = (s2m1, ())
@@ -136,7 +130,7 @@ memoryWb ram = Circuit go
     s2m1 = (\s2m dat -> s2m{readData = dat}) <$> s2m0 <*> readValue
     readValue = ram readAddr write
 
-  fsm st m2s
+  fsm st (m2s :: WishboneM2S addressBits dataBytes)
     -- Manager must be active if we're in this state
     | AckRead <- st = (Wait, (0, Nothing, noS2M{acknowledge = True}))
     -- Stay in Wait for invalid transactions
@@ -147,7 +141,7 @@ memoryWb ram = Circuit go
     | isRead = (AckRead, (m2s.addr, Nothing, noS2M))
     | otherwise = (Wait, (0, Nothing, noS2M))
    where
-    noS2M = emptyWishboneS2M @()
+    noS2M = emptyWishboneS2M :: WishboneS2M dataBytes
     managerActive = m2s.busCycle && m2s.strobe
     isError = managerActive && (m2s.busSelect /= maxBound)
     isWrite = managerActive && m2s.writeEnable