From f0f6cefa39af66ef1708e2404fd85f786a73fbe2 Mon Sep 17 00:00:00 2001 From: Aleksander Los Date: Thu, 30 May 2024 11:08:33 +0200 Subject: [PATCH] Add Wishbone wrapper for the True Dual Port block ram, issue #472 --- bittide/src/Bittide/DoubleBufferedRam.hs | 157 ++++++++++++++++++++- bittide/tests/Tests/DoubleBufferedRam.hs | 172 +++++++++++++++++++++++ bittide/tests/Tests/Shared.hs | 17 +++ 3 files changed, 345 insertions(+), 1 deletion(-) diff --git a/bittide/src/Bittide/DoubleBufferedRam.hs b/bittide/src/Bittide/DoubleBufferedRam.hs index 476c6e143..c79084927 100644 --- a/bittide/src/Bittide/DoubleBufferedRam.hs +++ b/bittide/src/Bittide/DoubleBufferedRam.hs @@ -1,4 +1,4 @@ --- SPDX-FileCopyrightText: 2022 Google LLC +-- SPDX-FileCopyrightText: 2022-2024 Google LLC -- -- SPDX-License-Identifier: Apache-2.0 @@ -9,10 +9,12 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE NoMonomorphismRestriction #-} module Bittide.DoubleBufferedRam where import Clash.Prelude +import Clash.Cores.Xilinx.BlockRam (tdpbram) import Data.Constraint import Data.Maybe @@ -88,6 +90,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 nAddrs domA domB nBytes a = + forall . + ( 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 (2 ^ nAddrs) domA domB 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 tdpbramModule 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) = tdpbramModule + 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 . diff --git a/bittide/tests/Tests/DoubleBufferedRam.hs b/bittide/tests/Tests/DoubleBufferedRam.hs index 98fb73d0b..e57e7de06 100644 --- a/bittide/tests/Tests/DoubleBufferedRam.hs +++ b/bittide/tests/Tests/DoubleBufferedRam.hs @@ -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 @@ -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" @@ -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) @@ -885,3 +891,169 @@ 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 && + 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 diff --git a/bittide/tests/Tests/Shared.hs b/bittide/tests/Tests/Shared.hs index 845e99b92..7af486090 100644 --- a/bittide/tests/Tests/Shared.hs +++ b/bittide/tests/Tests/Shared.hs @@ -176,6 +176,23 @@ 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) = + 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 .