Add Wishbone wrapper for the True Dual Port block ram, issue #472

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 .

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

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 .