Skip to content

Commit

Permalink
Add Wishbone wrapper for the True Dual Port block ram, issue #472
Browse files Browse the repository at this point in the history
  • Loading branch information
Losiek committed May 30, 2024
1 parent 703b881 commit a5a2e56
Show file tree
Hide file tree
Showing 3 changed files with 349 additions and 0 deletions.
156 changes: 156 additions & 0 deletions bittide/src/Bittide/DoubleBufferedRam.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,13 @@
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

module Bittide.DoubleBufferedRam where

import Clash.Prelude
import Clash.Explicit.Prelude (noReset)
import Clash.Cores.Xilinx.BlockRam (tdpbram)

import Data.Constraint
import Data.Maybe
Expand Down Expand Up @@ -88,6 +91,159 @@ contentGenerator content = case compareSNat d1 (SNat @romSize) of
element = initializedRam content (bitCoerce <$> romAddr1) (pure Nothing)
_ -> (pure Nothing, pure True)

-- | Circuit wrapper around `wbStorageTDP`.
wbStorageTDPC ::
forall domA domB nAddrs .
( KnownDomain domA
, KnownDomain domB
, KnownNat nAddrs
) =>
Clock domA ->
Reset domA ->
Enable domA ->
Clock domB ->
Reset domB ->
Enable domB ->
Circuit
(
Wishbone domA 'Standard nAddrs (Bytes 4)
, Wishbone domB 'Standard nAddrs (Bytes 4)
)
()
wbStorageTDPC clkA rstA enA clkB rstB enB = Circuit go
where
go ::
( (
Signal domA (WishboneM2S nAddrs 4 (BitVector 32))
, Signal domB (WishboneM2S nAddrs 4 (BitVector 32)))
, ()
) ->
( ( Signal domA (WishboneS2M (BitVector 32))
, Signal domB (WishboneS2M (BitVector 32)))
, ()
)
go ((m2sA, m2sB), ()) = ((s2mA, s2mB),())
where
(s2mA, s2mB) = wbStorageTDP clkA rstA enA clkB rstB enB m2sA m2sB

-- | Create a type synonym
type TdpbramType nAddres domA nBytes a =
forall nAddrs domA domB nBytes .
( KnownNat nAddrs
, KnownDomain domA
, KnownDomain domB
, KnownNat nBytes
, BitSize a ~ (8 * nBytes)
, NFDataX a
, BitPack a
, Num a
) =>

Clock domA ->
-- | Port enable
Enable domA ->
-- | Address
Signal domA (Index nAddrs) ->
-- | Write byte enable
Signal domA (BitVector nBytes) ->
-- | Write data
Signal domA a ->

Clock domB ->
-- | Port enable
Enable domB ->
-- | Address
Signal domB (Index nAddrs) ->
-- | Write byte enable
Signal domB (BitVector nBytes) ->
-- | Write data
Signal domB a ->

( Signal domA a
, Signal domB a
)

-- | Wrapper for the True Dual Port block ram
wbStorageTDP ::
forall domA domB nAddrs .
( KnownDomain domA
, KnownDomain domB
, KnownNat nAddrs
) =>
Clock domA ->
Reset domA ->
Enable domA ->
Clock domB ->
Reset domB ->
Enable domB ->
Signal domA (WishboneM2S nAddrs 4 (Bytes 4)) ->
Signal domB (WishboneM2S nAddrs 4 (Bytes 4)) ->
(Signal domA (WishboneS2M (Bytes 4)), Signal domB (WishboneS2M (Bytes 4)))
wbStorageTDP = wbStorageTDPM tdpbram

-- | Wrapper for the True Dual Port block ram with model
wbStorageTDPM ::
forall domA domB nAddrs .
( KnownDomain domA
, KnownDomain domB
, KnownNat nAddrs
) =>
(TdpbramType nAddrs domA (Bytes 4) (BitVector 32)) ->
Clock domA ->
Reset domA ->
Enable domA ->
Clock domB ->
Reset domB ->
Enable domB ->
Signal domA (WishboneM2S nAddrs 4 (Bytes 4)) ->
Signal domB (WishboneM2S nAddrs 4 (Bytes 4)) ->
(Signal domA (WishboneS2M (Bytes 4)), Signal domB (WishboneS2M (Bytes 4)))
wbStorageTDPM tdpbram clkA rstA enA clkB rstB enB aM2S bM2S =
(responseWb clkA rstA enA aM2S datA, responseWb clkB rstB enB bM2S datB)
where
addrBitToIndex :: forall dom n . (KnownDomain dom, KnownNat n) =>
Signal dom (WishboneM2S n 4 (Bytes 4)) -> Signal dom (Index (2 ^ n))
addrBitToIndex wbM2S = bv2i . addr <$> wbM2S
writeDataWb :: forall dom . (KnownDomain dom) =>
Signal dom (WishboneM2S nAddrs 4 (Bytes 4)) -> Signal dom (BitVector 32)
writeDataWb wbM2S = writeData <$> wbM2S
byteEna :: forall dom . (KnownDomain dom) =>
Signal dom (WishboneM2S nAddrs 4 (Bytes 4)) -> Signal dom (BitVector 4)
byteEna wbM2S = (\wb -> if writeEnable wb then busSelect wb else 0 :: BitVector 4) <$> wbM2S
enableWb :: forall dom . (KnownDomain dom) =>
Signal dom (WishboneM2S nAddrs 4 (Bytes 4)) -> Enable dom
enableWb wbM2S = toEnable $ (\wb -> busCycle wb && strobe wb) <$> wbM2S
(datA, datB) = tdpbram
clkA
(enableWb aM2S) (addrBitToIndex aM2S) (byteEna aM2S) (writeDataWb aM2S)
clkB
(enableWb bM2S) (addrBitToIndex bM2S) (byteEna bM2S) (writeDataWb bM2S)

-- | Create a response on the wishbone bus from wishbone request and
-- data from the tdpbram
responseWb ::
forall dom a .
( KnownDomain dom
, BitSize a ~ 32
, NFDataX a
, BitPack a
) =>
Clock dom ->
Reset dom ->
Enable dom ->
Signal dom (WishboneM2S nAddrs 4 a) -> -- current M2S signal
Signal dom a -> -- data from tdpbram
Signal dom (WishboneS2M a) -- S2M signal
responseWb clk rst en m2s dat = mux inCycle s2m (pure emptyWishboneS2M)
where
inCycle = (busCycle <$> m2s) .&&. (strobe <$> m2s)
-- It takes a single cycle to lookup elements in a block ram. We can therfore
-- only process a request every other clock cycle.
ack = (not <$> delayedAck) .&&. inCycle
delayedAck = withClockResetEnable clk rst en $ register False ack
s2m = (\newAck newDat-> (emptyWishboneS2M @(Bytes 4)){acknowledge = newAck, readData = newDat})
<$> delayedAck <*> dat

-- | Circuit wrapper around `wbStorageDP`.
wbStorageDPC ::
forall dom depth awA awB .
Expand Down
174 changes: 174 additions & 0 deletions bittide/tests/Tests/DoubleBufferedRam.hs
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ import Data.Type.Equality (type (:~:)(Refl))
import Hedgehog
import Hedgehog.Range as Range
import Numeric (showHex)
import Protocols
import Protocols.Hedgehog.Internal
import Protocols.Wishbone
import Protocols.Wishbone.Standard.Hedgehog
Expand All @@ -43,6 +44,9 @@ import qualified Data.Set as Set
import qualified GHC.TypeNats as TN
import qualified Hedgehog.Gen as Gen hiding (resize)
import qualified Prelude as P
import qualified Data.Map as Map
import qualified Clash.Sized.Internal.BitVector as BV
import qualified Data.Foldable as F

tests :: TestTree
tests = testGroup "Tests.DoubleBufferedRam"
Expand Down Expand Up @@ -78,6 +82,8 @@ tests = testGroup "Tests.DoubleBufferedRam"
"wbStorageRangeErrors" wbStorageRangeErrors
, testPropertyNamed "Test whether wbStorage acts the same its Behavioral model (clash-protocols)"
"wbStorageProtocolsModel" wbStorageProtocolsModel
, testPropertyNamed "Test whether wbStorageTDPBehavior acts the same its Behavioral model"
"wbStorageTDPBehavior" wbStorageTDPBehavior
]

genRamContents :: (MonadGen m, Integral i) => i -> m a -> m (SomeVec 1 a)
Expand Down Expand Up @@ -885,3 +891,171 @@ wbStorageProtocolsModel = property $ do
Right $ I.insert modelAddr wr st0
where
modelAddr = fromIntegral $ addr `div` 4

-- | Compare transaction with undefined value in the Read data field
compareTransWithUndef :: (KnownNat addrW, KnownNat selWidth, KnownNat n) =>
(Transaction addrW selWidth (BitVector n)) -> (Transaction addrW selWidth (BitVector n)) -> Bool
compareTransWithUndef transA transB =
case (transA, transB) of
((WriteSuccess mA _), (WriteSuccess mB _)) ->
checkField "addr" addr mA mB &&
checkField "buSelect" busSelect mA mB &&
checkField "writeData" writeData mA mB
((ReadSuccess mA sA), (ReadSuccess mB sB)) ->
checkField "addr" addr mA mB &&
checkField "busSelect" busSelect mA mB &&
-- checkField "readData" readData sA sB
checkBitVectorField readData sA sB
((Error _), (Error _)) -> True
((Retry _), (Retry _)) -> True
((Stall _), (Stall _)) -> True
((Illegal _ _), (Illegal _ _)) -> True
((Ignored _), (Ignored _)) -> True
(_, _) -> False

checkBitVectorField :: (KnownNat n) => (t -> BitVector n) -> t -> t -> Bool
checkBitVectorField f a b =
(f a) `eqBitVec` (f b)


-- | Behavioral test for 'wbStorageTDP', it checks whether the behavior of
-- 'wbStorageTDP' matches the 'wbStorageTDPBehaviorModel'.
wbStorageTDPBehavior :: Property
wbStorageTDPBehavior = verifiedTermination . withTests 1000 . property $ do
nWordsA <- forAll $ Gen.enum 2 32
nWordsB <- forAll $ Gen.enum 2 32
case (TN.someNatVal (nWordsA - 2), TN.someNatVal (nWordsB - 2)) of
(SomeNat (addSNat d2 . snatProxy -> nWordsA0), SomeNat (addSNat d2 . snatProxy -> nWordsB0)) -> go nWordsA0 nWordsB0
where
go :: forall wordsA wordsB m . (KnownNat wordsA, 2 <= wordsA, KnownNat wordsB, 2 <= wordsB, Monad m) => SNat wordsA -> SNat wordsB -> PropertyT m ()
go SNat SNat = do
wbRequestsNum <- forAll $ Gen.integral (Range.linearFrom 0 (0) 32)
wbRequestsA <- forAll $ Gen.list (Range.singleton wbRequestsNum)
(genWishboneTransfer @32 (natToNum @wordsA) (genDefinedBitVector @32))
wbRequestsB <- forAll $ Gen.list (Range.singleton wbRequestsNum)
(genWishboneTransfer @32 (natToNum @wordsB) (genDefinedBitVector @32))

cover 5 "equal address" $ or (L.zipWith checkAddressEqual (L.map fst wbRequestsA) (L.map fst wbRequestsB))

F.for_ (L.map (getAddressWbRequest . fst) (wbRequestsA L.++ wbRequestsB)) $ \x -> do
classify "low address" $ x == minBound
classify "mid address" $ x > minBound && x < maxBound
classify "high address" $ x == maxBound

F.for_ (L.map (getByteEnableWbRequest . fst) (wbRequestsA L.++ wbRequestsB)) $ \x -> do
classify "ByteEnable: 0000" $ x == 0
classify "ByteEnable: 0001" $ x == 1
classify "ByteEnable: 0010" $ x == 2
classify "ByteEnable: 0100" $ x == 4
classify "ByteEnable: 1000" $ x == 8

let
masterA = driveStandard defExpectOptions wbRequestsA
masterB = driveStandard defExpectOptions wbRequestsB
master = prod2C masterA masterB
slave = wbStorageTDPC @System @System @32 clockGen resetGen enableGen clockGen resetGen enableGen
(simTransactionsA, simTransactionsB) = exposeDoubleWbTransactions (Just 1000) master slave
(goldenTransactionsA, goldenTransactionsB) = L.unzip (wbStorageTDPBehaviorModel (fmap fst wbRequestsA) (fmap fst wbRequestsB))

footnote $ "simTransactionsA" <> show simTransactionsA
footnote $ "simTransactionsB" <> show simTransactionsB
footnote $ "wbRequestsA" <> show wbRequestsA
footnote $ "wbRequestsB" <> show wbRequestsB
footnote $ "goldenTransactionsA" <> show goldenTransactionsA
footnote $ "goldenTransactionsB" <> show goldenTransactionsB

assert $ and (L.zipWith compareTransWithUndef simTransactionsA goldenTransactionsA)
assert $ and (L.zipWith compareTransWithUndef simTransactionsB goldenTransactionsB)

where
genWishboneTransfer ::
(KnownNat addressWidth, KnownNat (BitSize a)) =>
Int -> -- ^ size
Gen a ->
Gen (WishboneMasterRequest addressWidth a, Int)
genWishboneTransfer size genA =
let
validAddr = (4 *) . fromIntegral <$> Gen.enum 0 (size - 1)
-- Make wbOps that won't be repeated
mkRead address bs = (Read address bs, 0)
mkWrite address bs a = (Write address bs a, 0)
in
-- Generate valid operations. The boolean represents the validity of the operation.
Gen.choice
[ (mkRead <$> validAddr <*> genDefinedBitVector)
, (mkWrite <$> validAddr <*> genDefinedBitVector <*> genA)
]

checkAddressEqual :: (KnownNat addressWidth, KnownNat (BitSize a)) =>
WishboneMasterRequest addressWidth a ->
WishboneMasterRequest addressWidth a ->
Bool
checkAddressEqual req1 req2 = extractAddress req1 == extractAddress req2
where
extractAddress :: WishboneMasterRequest addressWidth a -> BitVector addressWidth
extractAddress (Read addr _) = addr
extractAddress (Write addr _ _) = addr

getAddressWbRequest :: (KnownNat addressWidth, KnownNat (BitSize a)) =>
WishboneMasterRequest addressWidth a -> Unsigned addressWidth
getAddressWbRequest (Read addr _) = unpack addr
getAddressWbRequest (Write addr _ _) = unpack addr

getByteEnableWbRequest :: (KnownNat addressWidth, KnownNat (BitSize a)) =>
WishboneMasterRequest addressWidth a -> Unsigned (BitSize a `DivRU` 8)
getByteEnableWbRequest (Read _ be) = unpack be
getByteEnableWbRequest (Write _ be _) = unpack be

-- | Memory Model
type MemoryModel a b = Map.Map a b

-- | Behavioral model for 'wbStorageTDPM'.
wbStorageTDPBehaviorModel ::
forall addrW bytes .
( 1 <= addrW, KnownNat bytes) =>
(KnownNat addrW) =>
[WishboneMasterRequest addrW (Bytes bytes)] -> [WishboneMasterRequest addrW (Bytes bytes)] ->
[(Transaction addrW bytes (Bytes bytes),Transaction addrW bytes (Bytes bytes))]
wbStorageTDPBehaviorModel initWbOpsA initWbOpsB = case (cancelMulDiv @bytes @8) of
Dict -> snd $ L.mapAccumL g emptyMemoryMap (L.zipWith (\wbA wbB -> (wbA, wbB)) initWbOpsA initWbOpsB)
where
emptyMemoryMap = Map.empty :: MemoryModel (BitVector addrW) (Bytes bytes)

fromMaybeBytes :: Maybe (Bytes bytes) -> Bytes bytes
fromMaybeBytes x = case x of
Just a -> a
Nothing -> 0

g storedMap (opA, opB) = (storedMapB, (transA, transB))
where
(storedMapA, transA) = f storedMap opA
(storedMapB, transB) = f storedMapA opB

-- Successful Read
f storedMap op@(Read i _) = (storedMap, ReadSuccess wbM2S wbS2M)
where
dat = fromMaybeBytes $ Map.lookup i storedMap
wbM2S = wbMasterRequestToM2S op
wbS2M = (emptyWishboneS2M @(Bytes bytes)){acknowledge = True, readData = dat}

-- Successful Write
f storedMap op@(Write i bs a) = (updatedStoredMap, WriteSuccess wbM2S wbS2M)
where
wbM2S = wbMasterRequestToM2S op
wbS2M = emptyWishboneS2M{acknowledge = True}
dat = fromMaybeBytes $ Map.lookup i storedMap
updatedStoredMap = Map.insert i (pack newEntry) storedMap

newEntry :: Vec bytes Byte
newEntry = zipWith3 (\ b old new -> if b then new else old)
(unpack bs) (unpack dat) (unpack a)

-- | Check equiality of two BitVectors containing the undefined values ('.')
-- Example:
-- x: "000111..."
-- y: "01.01.01."
-- result: False
eqBitVec :: (KnownNat n) => BitVector n -> BitVector n -> Bool
eqBitVec x@(BV.BV xMask _) y =
case (x `xor` y) of
BV.BV m v -> xMask == m && v == 0
19 changes: 19 additions & 0 deletions bittide/tests/Tests/Shared.hs
Original file line number Diff line number Diff line change
Expand Up @@ -176,6 +176,25 @@ exposeWbTransactions maybeSampleLength (Circuit master) (Circuit slave) =
Just n -> sampleN_lazy n
Nothing -> sample_lazy

exposeDoubleWbTransactions ::
(KnownDomain dom, Eq a, KnownNat addrW, ShowX a, KnownNat (BitSize a)) =>
Maybe Int ->
Circuit ((),()) (Wishbone dom mode addrW a, Wishbone dom mode addrW a) ->
Circuit (Wishbone dom mode addrW a, Wishbone dom mode addrW a) () ->
( [Transaction addrW (DivRU (BitSize a) 8) a]
, [Transaction addrW (DivRU (BitSize a) 8) a] )
exposeDoubleWbTransactions maybeSampleLength (Circuit master) (Circuit slave) =
-- bundle :: (Signal dom a, Signal dom b) -> Signal dom (a, b)
-- unbundle :: Signal dom (a, b) -> (Signal dom a, Signal dom b)
let ~((_), (m2sA, m2sB)) = master (((), ()), (s2mA, s2mB))
~((s2mA, s2mB), ()) = slave ((m2sA, m2sB), ())
in ( uncurry wbToTransaction $ L.unzip $ sampleF $ bundle (m2sA, s2mA)
, uncurry wbToTransaction $ L.unzip $ sampleF $ bundle (m2sB, s2mB))
where
sampleF = case maybeSampleLength of
Just n -> sampleN_lazy n
Nothing -> sample_lazy

-- | Transform a `WishboneMasterRequest` into `WishboneM2S`
wbMasterRequestToM2S ::
forall addrW a .
Expand Down

0 comments on commit a5a2e56

Please sign in to comment.