    {-|
    Copyright  :  (C) 2023, QBayLogic B.V.
    License    :  BSD2 (see the file LICENSE)
    Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>

    Configurable model for true dual-port block RAM
    -}

    {-# LANGUAGE BangPatterns #-}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE RecordWildCards #-}

    module Clash.Explicit.BlockRam.Model where

    #if !MIN_VERSION_base(4,18,0)
    import Control.Applicative (liftA2)
    #endif
    import Control.Exception (throw)
    import Data.Sequence (Seq)
    import GHC.Stack (HasCallStack)
    import GHC.TypeNats (KnownNat)

    import Clash.Promoted.Nat (SNat(..), natToNum)
    import Clash.Signal.Bundle (Bundle(bundle))
    import Clash.Signal.Internal
      (KnownDomain(..), Clock (..), Signal (..), ClockAB (..), clockTicks)
    import Clash.Sized.Index (Index)
    import Clash.XException (XException(..), NFDataX(..), seqX)
    import Clash.XException.MaybeX (MaybeX(..), toMaybeX, andX)

    import qualified Clash.XException.MaybeX as MaybeX

    import qualified Data.Sequence as Seq

    -- | Helper used in 'getConflict'
    data Conflict = Conflict
      { Conflict -> MaybeX Bool
    cfRWA :: !(MaybeX Bool) -- ^ Read/Write conflict for output A
      , Conflict -> MaybeX Bool
    cfRWB :: !(MaybeX Bool) -- ^ Read/Write conflict for output B
      , Conflict -> MaybeX Bool
    cfWW  :: !(MaybeX Bool) -- ^ Write/Write conflict
      } deriving (Int -> Conflict -> ShowS
    [Conflict] -> ShowS
    Conflict -> String
    (Int -> Conflict -> ShowS)
    -> (Conflict -> String) -> ([Conflict] -> ShowS) -> Show Conflict
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Conflict -> ShowS
    showsPrec :: Int -> Conflict -> ShowS
    $cshow :: Conflict -> String
    show :: Conflict -> String
    $cshowList :: [Conflict] -> ShowS
    showList :: [Conflict] -> ShowS
    Show)

    -- | Determines whether there was a write-write or read-write conflict. A conflict
    -- occurs when two ports tried to (potentially, in case of undefined values)
    -- access the same address and one or both tried to write to it. See documentation
    -- of 'Conflict' for more information.
    getConflict ::
      -- | Port A: enable, write enable, address
      (MaybeX Bool, MaybeX Bool, MaybeX Int) ->
      -- | Port B: enable, write enable, address
      (MaybeX Bool, MaybeX Bool, MaybeX Int) ->
      -- | 'Just' if there is a (potential) write conflict, otherwise 'Nothing'
      Maybe Conflict
    getConflict :: (MaybeX Bool, MaybeX Bool, MaybeX Int)
    -> (MaybeX Bool, MaybeX Bool, MaybeX Int) -> Maybe Conflict
    getConflict (MaybeX Bool
    enA, MaybeX Bool
    wenA, MaybeX Int
    addrA) (MaybeX Bool
    enB, MaybeX Bool
    wenB, MaybeX Int
    addrB)
      | IsDefined Bool
    False <- MaybeX Bool
    sameAddrX = Maybe Conflict
    forall a. Maybe a
    Nothing
      | Bool
    otherwise                    = Conflict -> Maybe Conflict
    forall a. a -> Maybe a
    Just Conflict
    conflict
     where
      sameAddrX :: MaybeX Bool
    sameAddrX = (Int -> Int -> Bool) -> MaybeX Int -> MaybeX Int -> MaybeX Bool
    forall a b c. (a -> b -> c) -> MaybeX a -> MaybeX b -> MaybeX c
    forall (f :: Type -> Type) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) MaybeX Int
    addrA MaybeX Int
    addrB

      conflict :: Conflict
    conflict = Conflict
        { cfRWA :: MaybeX Bool
    cfRWA = MaybeX Bool
    enA MaybeX Bool -> MaybeX Bool -> MaybeX Bool
    `andX` (MaybeX Bool
    enB MaybeX Bool -> MaybeX Bool -> MaybeX Bool
    `andX` MaybeX Bool
    wenB)
        , cfRWB :: MaybeX Bool
    cfRWB = MaybeX Bool
    enB MaybeX Bool -> MaybeX Bool -> MaybeX Bool
    `andX` (MaybeX Bool
    enA MaybeX Bool -> MaybeX Bool -> MaybeX Bool
    `andX` MaybeX Bool
    wenA)
        , cfWW :: MaybeX Bool
    cfWW  = (MaybeX Bool
    enA MaybeX Bool -> MaybeX Bool -> MaybeX Bool
    `andX` MaybeX Bool
    enB) MaybeX Bool -> MaybeX Bool -> MaybeX Bool
    `andX` (MaybeX Bool
    wenA MaybeX Bool -> MaybeX Bool -> MaybeX Bool
    `andX` MaybeX Bool
    wenB)
        }

    -- | Step through a cycle of a TDP block RAM where only one clock is active. Like
    -- 'accessRam', it accounts for 'Clash.XException.XException' in all values
    -- supplied by the user of the block RAM.
    cycleOne ::
      forall nAddrs a writeEnable .
      ( HasCallStack
      , NFDataX a
      ) =>
      SNat nAddrs ->
      TdpbramModelConfig writeEnable a ->
      -- | Previous value
      a ->
      -- | Memory
      Seq a ->
      -- | Port: enable, address, write enable, write data
      (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a) ->
      -- | Updated memory, output value
      (Seq a, a)
    cycleOne :: forall (nAddrs :: Nat) a writeEnable.
    (HasCallStack, NFDataX a) =>
    SNat nAddrs
    -> TdpbramModelConfig writeEnable a
    -> a
    -> Seq a
    -> (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    -> (Seq a, a)
    cycleOne SNat nAddrs
    SNat TdpbramModelConfig{Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    MaybeX writeEnable -> MaybeX Bool
    MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
    tdpIsActiveWriteEnable :: MaybeX writeEnable -> MaybeX Bool
    tdpMergeWriteEnable :: MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
    tdpUpdateRam :: Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    tdpUpdateRam :: forall writeEnable a.
    TdpbramModelConfig writeEnable a
    -> Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    tdpMergeWriteEnable :: forall writeEnable a.
    TdpbramModelConfig writeEnable a
    -> MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
    tdpIsActiveWriteEnable :: forall writeEnable a.
    TdpbramModelConfig writeEnable a
    -> MaybeX writeEnable -> MaybeX Bool
    ..} a
    prev Seq a
    ram0 = \case
      -- RAM is disabled, so we do nothing
      (IsDefined Bool
    False, MaybeX Int
    _, MaybeX writeEnable
    _, a
    _) ->
        (Seq a
    ram0, a
    prev)

      -- RAM is (potentially) enabled, so we run write RAM logic
      (MaybeX Bool
    ena, MaybeX Int
    addr, MaybeX writeEnable
    byteEna0, a
    dat) ->
        let
          byteEna1 :: MaybeX writeEnable
    byteEna1 = MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
    tdpMergeWriteEnable MaybeX Bool
    ena MaybeX writeEnable
    byteEna0
          (a
    out0, !Seq a
    ram1) =
            SNat nAddrs
    -> (MaybeX writeEnable -> MaybeX Bool)
    -> (Int -> MaybeX writeEnable -> a -> Seq a -> Seq a)
    -> MaybeX Int
    -> MaybeX writeEnable
    -> a
    -> Seq a
    -> (a, Seq a)
    forall (nAddrs :: Nat) a writeEnable.
    (NFDataX a, HasCallStack) =>
    SNat nAddrs
    -> (MaybeX writeEnable -> MaybeX Bool)
    -> (Int -> MaybeX writeEnable -> a -> Seq a -> Seq a)
    -> MaybeX Int
    -> MaybeX writeEnable
    -> a
    -> Seq a
    -> (a, Seq a)
    accessRam (forall (n :: Nat). KnownNat n => SNat n
    SNat @nAddrs) MaybeX writeEnable -> MaybeX Bool
    tdpIsActiveWriteEnable Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    tdpUpdateRam MaybeX Int
    addr MaybeX writeEnable
    byteEna1 a
    dat Seq a
    ram0

          out1 :: a
    out1 = (String -> a) -> (Bool -> a) -> MaybeX Bool -> a
    forall b a. (String -> b) -> (a -> b) -> MaybeX a -> b
    MaybeX.maybeX (XException -> a
    forall a e. (HasCallStack, Exception e) => e -> a
    throw (XException -> a) -> (String -> XException) -> String -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> XException
    XException) (a -> Bool -> a
    forall a b. a -> b -> a
    const a
    out0) MaybeX Bool
    ena
        in
          (Seq a
    ram1, a
    out1)

    -- | Step through a cycle of a TDP block RAM where the clock edges of port A and
    -- port B coincided. Like 'accessRam', it accounts for 'Clash.XException.XException'
    -- in all values supplied by the user of the block RAM.
    cycleBoth ::
      forall nAddrs a writeEnable.
      ( NFDataX a
      , HasCallStack
      ) =>
      SNat nAddrs ->
      TdpbramModelConfig writeEnable a ->
      -- | Previous value for port A
      a ->
      -- | Previous value for port B
      a ->
      -- | Memory
      Seq a ->
      -- | Port A: enable, address, write enable, write data
      (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a) ->
      -- | Port B: enable, address, write enable, write data
      (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a) ->
      -- | Updated memory, output value A, output value B
      (Seq a, a, a)
    cycleBoth :: forall (nAddrs :: Nat) a writeEnable.
    (NFDataX a, HasCallStack) =>
    SNat nAddrs
    -> TdpbramModelConfig writeEnable a
    -> a
    -> a
    -> Seq a
    -> (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    -> (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    -> (Seq a, a, a)
    cycleBoth
      SNat nAddrs
    SNat TdpbramModelConfig{Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    MaybeX writeEnable -> MaybeX Bool
    MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
    tdpUpdateRam :: forall writeEnable a.
    TdpbramModelConfig writeEnable a
    -> Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    tdpMergeWriteEnable :: forall writeEnable a.
    TdpbramModelConfig writeEnable a
    -> MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
    tdpIsActiveWriteEnable :: forall writeEnable a.
    TdpbramModelConfig writeEnable a
    -> MaybeX writeEnable -> MaybeX Bool
    tdpIsActiveWriteEnable :: MaybeX writeEnable -> MaybeX Bool
    tdpMergeWriteEnable :: MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
    tdpUpdateRam :: Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    ..} a
    prevA a
    prevB Seq a
    ram0
      (MaybeX Bool
    enAx, MaybeX Int
    addrAx, MaybeX writeEnable
    byteEnaAx0, a
    datA)
      (MaybeX Bool
    enBx, MaybeX Int
    addrBx, MaybeX writeEnable
    byteEnaBx0, a
    datB) = (Seq a
    ram2, a
    outA2, a
    outB2)
     where
      conflict :: Maybe Conflict
    conflict =
        (MaybeX Bool, MaybeX Bool, MaybeX Int)
    -> (MaybeX Bool, MaybeX Bool, MaybeX Int) -> Maybe Conflict
    getConflict
          (MaybeX Bool
    enAx, MaybeX writeEnable -> MaybeX Bool
    tdpIsActiveWriteEnable MaybeX writeEnable
    byteEnaAx1, MaybeX Int
    addrAx)
          (MaybeX Bool
    enBx, MaybeX writeEnable -> MaybeX Bool
    tdpIsActiveWriteEnable MaybeX writeEnable
    byteEnaBx1, MaybeX Int
    addrBx)

      writeWriteError :: a
    writeWriteError = String -> a
    forall a. (NFDataX a, HasCallStack) => String -> a
    deepErrorX String
    "conflicting write/write queries"
      readWriteError :: a
    readWriteError = String -> a
    forall a. (NFDataX a, HasCallStack) => String -> a
    deepErrorX String
    "conflicting read/write queries"

      byteEnaAx1 :: MaybeX writeEnable
    byteEnaAx1 = MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
    tdpMergeWriteEnable MaybeX Bool
    enAx MaybeX writeEnable
    byteEnaAx0
      byteEnaBx1 :: MaybeX writeEnable
    byteEnaBx1 = MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
    tdpMergeWriteEnable MaybeX Bool
    enBx MaybeX writeEnable
    byteEnaBx0

      (a
    datA1, a
    datB1) = case Maybe Conflict
    conflict of
        Just Conflict{cfWW :: Conflict -> MaybeX Bool
    cfWW=IsDefined Bool
    True} -> (a
    writeWriteError, a
    writeWriteError)
        Just Conflict{cfWW :: Conflict -> MaybeX Bool
    cfWW=IsX String
    _} -> (a
    writeWriteError, a
    writeWriteError)
        Maybe Conflict
    _ -> (a
    datA, a
    datB)

      (a
    outA0, Seq a
    ram1) =
        SNat nAddrs
    -> (MaybeX writeEnable -> MaybeX Bool)
    -> (Int -> MaybeX writeEnable -> a -> Seq a -> Seq a)
    -> MaybeX Int
    -> MaybeX writeEnable
    -> a
    -> Seq a
    -> (a, Seq a)
    forall (nAddrs :: Nat) a writeEnable.
    (NFDataX a, HasCallStack) =>
    SNat nAddrs
    -> (MaybeX writeEnable -> MaybeX Bool)
    -> (Int -> MaybeX writeEnable -> a -> Seq a -> Seq a)
    -> MaybeX Int
    -> MaybeX writeEnable
    -> a
    -> Seq a
    -> (a, Seq a)
    accessRam (forall (n :: Nat). KnownNat n => SNat n
    SNat @nAddrs) MaybeX writeEnable -> MaybeX Bool
    tdpIsActiveWriteEnable Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    tdpUpdateRam MaybeX Int
    addrAx MaybeX writeEnable
    byteEnaAx1 a
    datA1 Seq a
    ram0
      (a
    outB0, Seq a
    ram2) =
        SNat nAddrs
    -> (MaybeX writeEnable -> MaybeX Bool)
    -> (Int -> MaybeX writeEnable -> a -> Seq a -> Seq a)
    -> MaybeX Int
    -> MaybeX writeEnable
    -> a
    -> Seq a
    -> (a, Seq a)
    forall (nAddrs :: Nat) a writeEnable.
    (NFDataX a, HasCallStack) =>
    SNat nAddrs
    -> (MaybeX writeEnable -> MaybeX Bool)
    -> (Int -> MaybeX writeEnable -> a -> Seq a -> Seq a)
    -> MaybeX Int
    -> MaybeX writeEnable
    -> a
    -> Seq a
    -> (a, Seq a)
    accessRam (forall (n :: Nat). KnownNat n => SNat n
    SNat @nAddrs) MaybeX writeEnable -> MaybeX Bool
    tdpIsActiveWriteEnable Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    tdpUpdateRam MaybeX Int
    addrBx MaybeX writeEnable
    byteEnaBx1 a
    datB1 Seq a
    ram1

      outA1 :: a
    outA1 = case Maybe Conflict
    conflict of
        Just Conflict{cfRWA :: Conflict -> MaybeX Bool
    cfRWA=IsDefined Bool
    True} -> a
    readWriteError
        Just Conflict{cfRWA :: Conflict -> MaybeX Bool
    cfRWA=IsX String
    _} -> a
    readWriteError
        Maybe Conflict
    _ -> a
    outA0

      outB1 :: a
    outB1 = case Maybe Conflict
    conflict of
        Just Conflict{cfRWB :: Conflict -> MaybeX Bool
    cfRWB=IsDefined Bool
    True} -> a
    readWriteError
        Just Conflict{cfRWB :: Conflict -> MaybeX Bool
    cfRWB=IsX String
    _} -> a
    readWriteError
        Maybe Conflict
    _ -> a
    outB0

      outA2 :: a
    outA2 = if MaybeX Bool -> Bool
    forall a. MaybeX a -> a
    MaybeX.fromMaybeX MaybeX Bool
    enAx then a
    outA1 else a
    prevA
      outB2 :: a
    outB2 = if MaybeX Bool -> Bool
    forall a. MaybeX a -> a
    MaybeX.fromMaybeX MaybeX Bool
    enBx then a
    outB1 else a
    prevB

    -- | Access a RAM and account for undefined values in the address, write enable,
    -- and data to write. Return read after write value.
    accessRam ::
      forall nAddrs a writeEnable .
      ( NFDataX a
      , HasCallStack ) =>
      SNat nAddrs ->
      -- | Determine whether a write enable is active
      (MaybeX writeEnable -> MaybeX Bool) ->
      -- | Update memory with a defined address
      (Int -> MaybeX writeEnable -> a -> Seq a -> Seq a) ->
      -- | Address
      MaybeX Int ->
      -- | Byte enable
      MaybeX writeEnable ->
      -- | Data to write
      a ->
      -- | Memory to write to
      Seq a ->
      -- | (Read after write value, new memory)
      (a, Seq a)
    accessRam :: forall (nAddrs :: Nat) a writeEnable.
    (NFDataX a, HasCallStack) =>
    SNat nAddrs
    -> (MaybeX writeEnable -> MaybeX Bool)
    -> (Int -> MaybeX writeEnable -> a -> Seq a -> Seq a)
    -> MaybeX Int
    -> MaybeX writeEnable
    -> a
    -> Seq a
    -> (a, Seq a)
    accessRam SNat nAddrs
    SNat MaybeX writeEnable -> MaybeX Bool
    tdpIsActiveWriteEnable Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    updateMem MaybeX Int
    addrX MaybeX writeEnable
    byteEnableX a
    dat Seq a
    mem0
      -- Read (do nothing)
      | IsDefined Bool
    False <- MaybeX writeEnable -> MaybeX Bool
    tdpIsActiveWriteEnable MaybeX writeEnable
    byteEnableX
      = (Seq a
    mem0 Seq a -> Int -> a
    forall a. Seq a -> Int -> a
    `Seq.index` MaybeX Int -> Int
    forall a. MaybeX a -> a
    MaybeX.fromMaybeX MaybeX Int
    addrX, Seq a
    mem0)

      -- Undefined address and write enable or (partially) unknown
      | IsX String
    addrMsg <- MaybeX Int
    addrX
      = ( String -> a
    forall a. (NFDataX a, HasCallStack) => String -> a
    deepErrorX (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    "Unknown address" String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> String
    "\nAddress error message: " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> String
    addrMsg
        , Int -> (Int -> a) -> Seq a
    forall a. Int -> (Int -> a) -> Seq a
    Seq.fromFunction (forall (n :: Nat) a. (Num a, KnownNat n) => a
    natToNum @nAddrs) (String -> Int -> a
    unknownAddr String
    addrMsg) )

      -- Write with defined address
      | IsDefined Int
    addr <- MaybeX Int
    addrX
      , Seq a
    mem1 <- Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    updateMem Int
    addr MaybeX writeEnable
    byteEnableX a
    dat Seq a
    mem0
      = (Seq a
    mem1 Seq a -> Int -> a
    forall a. Seq a -> Int -> a
    `Seq.index` Int
    addr, Seq a
    mem1)
     where
      unknownAddr :: String -> Int -> a
      unknownAddr :: String -> Int -> a
    unknownAddr String
    msg Int
    n =
        String -> a
    forall a. (NFDataX a, HasCallStack) => String -> a
    deepErrorX (String
    "Write enabled or undefined, but address unknown; position " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> Int -> String
    forall a. Show a => a -> String
    show Int
    n String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <>
                    String
    "\nAddress error message: " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> String
    msg)

    data TdpbramModelConfig writeEnable a = TdpbramModelConfig
      { forall writeEnable a.
    TdpbramModelConfig writeEnable a
    -> MaybeX writeEnable -> MaybeX Bool
    tdpIsActiveWriteEnable :: MaybeX writeEnable -> MaybeX Bool
      -- ^ Determine whether a write enable is active

      , forall writeEnable a.
    TdpbramModelConfig writeEnable a
    -> MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
    tdpMergeWriteEnable :: MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
      -- ^ Merge global enable with write enable

      , forall writeEnable a.
    TdpbramModelConfig writeEnable a
    -> Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
    tdpUpdateRam :: Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
      -- ^ Update memory with a defined address
      }

    -- | Haskell model for a true dual-port block RAM which is polymorphic in its
    -- write enables
    --
    tdpbramModel ::
      forall nAddrs domA domB a writeEnable .
      ( HasCallStack
      , KnownNat nAddrs
      , KnownDomain domA
      , KnownDomain domB
      , NFDataX a
      ) =>
      TdpbramModelConfig writeEnable a ->

      Clock domA ->
      -- | Enable
      Signal domA Bool ->
      -- | Address
      Signal domA (Index nAddrs) ->
      -- | Write enable
      Signal domA writeEnable ->
      -- | Write data
      Signal domA a ->

      Clock domB ->
      -- | Enable
      Signal domB Bool ->
      -- | Address
      Signal domB (Index nAddrs) ->
      -- | Write byte enable
      Signal domB writeEnable ->
      -- | Write data
      Signal domB a ->

      (Signal domA a, Signal domB a)
    tdpbramModel :: forall (nAddrs :: Nat) (domA :: Domain) (domB :: Domain) a
           writeEnable.
    (HasCallStack, KnownNat nAddrs, KnownDomain domA, KnownDomain domB,
     NFDataX a) =>
    TdpbramModelConfig writeEnable a
    -> Clock domA
    -> Signal domA Bool
    -> Signal domA (Index nAddrs)
    -> Signal domA writeEnable
    -> Signal domA a
    -> Clock domB
    -> Signal domB Bool
    -> Signal domB (Index nAddrs)
    -> Signal domB writeEnable
    -> Signal domB a
    -> (Signal domA a, Signal domB a)
    tdpbramModel
      TdpbramModelConfig writeEnable a
    config
      Clock domA
    clkA Signal domA Bool
    enA Signal domA (Index nAddrs)
    addrA Signal domA writeEnable
    byteEnaA Signal domA a
    datA
      Clock domB
    clkB Signal domB Bool
    enB Signal domB (Index nAddrs)
    addrB Signal domB writeEnable
    byteEnaB Signal domB a
    datB =
      ( a
    startA a -> Signal domA a -> Signal domA a
    forall (dom :: Domain) a. a -> Signal dom a -> Signal dom a
    :- Signal domA a
    outA
      , a
    startB a -> Signal domB a -> Signal domB a
    forall (dom :: Domain) a. a -> Signal dom a -> Signal dom a
    :- Signal domB a
    outB )
     where
      (Signal domA a
    outA, Signal domB a
    outB) =
        Seq a
    -> [ClockAB]
    -> Signal domA (Bool, writeEnable, Int, a)
    -> Signal domB (Bool, writeEnable, Int, a)
    -> a
    -> a
    -> (Signal domA a, Signal domB a)
    go
          (Int -> (Int -> a) -> Seq a
    forall a. Int -> (Int -> a) -> Seq a
    Seq.fromFunction (forall (n :: Nat) a. (Num a, KnownNat n) => a
    natToNum @nAddrs) Int -> a
    initElement)
          (Clock domA -> Clock domB -> [ClockAB]
    forall (domA :: Domain) (domB :: Domain).
    (KnownDomain domA, KnownDomain domB) =>
    Clock domA -> Clock domB -> [ClockAB]
    clockTicks Clock domA
    clkA Clock domB
    clkB)
          (Unbundled domA (Bool, writeEnable, Int, a)
    -> Signal domA (Bool, writeEnable, Int, a)
    forall a (dom :: Domain).
    Bundle a =>
    Unbundled dom a -> Signal dom a
    forall (dom :: Domain).
    Unbundled dom (Bool, writeEnable, Int, a)
    -> Signal dom (Bool, writeEnable, Int, a)
    bundle (Signal domA Bool
    enA, Signal domA writeEnable
    byteEnaA, Index nAddrs -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Index nAddrs -> Int)
    -> Signal domA (Index nAddrs) -> Signal domA Int
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Signal domA (Index nAddrs)
    addrA, Signal domA a
    datA))
          (Unbundled domB (Bool, writeEnable, Int, a)
    -> Signal domB (Bool, writeEnable, Int, a)
    forall a (dom :: Domain).
    Bundle a =>
    Unbundled dom a -> Signal dom a
    forall (dom :: Domain).
    Unbundled dom (Bool, writeEnable, Int, a)
    -> Signal dom (Bool, writeEnable, Int, a)
    bundle (Signal domB Bool
    enB, Signal domB writeEnable
    byteEnaB, Index nAddrs -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Index nAddrs -> Int)
    -> Signal domB (Index nAddrs) -> Signal domB Int
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Signal domB (Index nAddrs)
    addrB, Signal domB a
    datB))
          a
    startA a
    startB

      startA :: a
    startA = String -> a
    forall a. (NFDataX a, HasCallStack) => String -> a
    deepErrorX (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    "Port A: First value undefined"
      startB :: a
    startB = String -> a
    forall a. (NFDataX a, HasCallStack) => String -> a
    deepErrorX (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    "Port B: First value undefined"

      initElement :: Int -> a
      initElement :: Int -> a
    initElement Int
    n =
        String -> a
    forall a. (NFDataX a, HasCallStack) => String -> a
    deepErrorX (String
    "Unknown initial element; position " String -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> Int -> String
    forall a. Show a => a -> String
    show Int
    n)

      go ::
        Seq a ->
        [ClockAB] ->
        Signal domA (Bool, writeEnable, Int, a) ->
        Signal domB (Bool, writeEnable, Int, a) ->
        a -> a ->
        (Signal domA a, Signal domB a)
      go :: Seq a
    -> [ClockAB]
    -> Signal domA (Bool, writeEnable, Int, a)
    -> Signal domB (Bool, writeEnable, Int, a)
    -> a
    -> a
    -> (Signal domA a, Signal domB a)
    go Seq a
    _ [] Signal domA (Bool, writeEnable, Int, a)
    _ Signal domB (Bool, writeEnable, Int, a)
    _ =
        String -> a -> a -> (Signal domA a, Signal domB a)
    forall a. HasCallStack => String -> a
    error String
    "tdpbramModel#.go: `ticks` should have been an infinite list"
      go Seq a
    ram0 (ClockAB
    tick:[ClockAB]
    ticks) Signal domA (Bool, writeEnable, Int, a)
    as0 Signal domB (Bool, writeEnable, Int, a)
    bs0 =
        case ClockAB
    tick of
          ClockAB
    ClockA -> a -> a -> (Signal domA a, Signal domB a)
    goA
          ClockAB
    ClockB -> a -> a -> (Signal domA a, Signal domB a)
    goB
          ClockAB
    ClockAB -> a -> a -> (Signal domA a, Signal domB a)
    goBoth
       where
        (  Bool -> MaybeX Bool
    forall a. a -> MaybeX a
    toMaybeX -> MaybeX Bool
    enAx
         , writeEnable -> MaybeX writeEnable
    forall a. a -> MaybeX a
    toMaybeX -> MaybeX writeEnable
    byteEnaAx
         , Int -> MaybeX Int
    forall a. a -> MaybeX a
    toMaybeX -> MaybeX Int
    addrAx
         , a
    datA0
         ) :- Signal domA (Bool, writeEnable, Int, a)
    as1 = Signal domA (Bool, writeEnable, Int, a)
    as0

        (  Bool -> MaybeX Bool
    forall a. a -> MaybeX a
    toMaybeX -> MaybeX Bool
    enBx
         , writeEnable -> MaybeX writeEnable
    forall a. a -> MaybeX a
    toMaybeX -> MaybeX writeEnable
    byteEnaBx
         , Int -> MaybeX Int
    forall a. a -> MaybeX a
    toMaybeX -> MaybeX Int
    addrBx
         , a
    datB0
         ) :- Signal domB (Bool, writeEnable, Int, a)
    bs1 = Signal domB (Bool, writeEnable, Int, a)
    bs0

        portA :: (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    portA = (MaybeX Bool
    enAx, MaybeX Int
    addrAx, MaybeX writeEnable
    byteEnaAx, a
    datA0)
        portB :: (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    portB = (MaybeX Bool
    enBx, MaybeX Int
    addrBx, MaybeX writeEnable
    byteEnaBx, a
    datB0)

        goBoth :: a -> a -> (Signal domA a, Signal domB a)
    goBoth a
    prevA a
    prevB = a
    outA1 a
    -> (Signal domA a, Signal domB a) -> (Signal domA a, Signal domB a)
    forall a b. a -> b -> b
    `seqX` a
    outB1 a
    -> (Signal domA a, Signal domB a) -> (Signal domA a, Signal domB a)
    forall a b. a -> b -> b
    `seqX` (a
    outA1 a -> Signal domA a -> Signal domA a
    forall (dom :: Domain) a. a -> Signal dom a -> Signal dom a
    :- Signal domA a
    as2, a
    outB1 a -> Signal domB a -> Signal domB a
    forall (dom :: Domain) a. a -> Signal dom a -> Signal dom a
    :- Signal domB a
    bs2)
         where
          (Seq a
    ram1, a
    outA1, a
    outB1) =
            SNat nAddrs
    -> TdpbramModelConfig writeEnable a
    -> a
    -> a
    -> Seq a
    -> (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    -> (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    -> (Seq a, a, a)
    forall (nAddrs :: Nat) a writeEnable.
    (NFDataX a, HasCallStack) =>
    SNat nAddrs
    -> TdpbramModelConfig writeEnable a
    -> a
    -> a
    -> Seq a
    -> (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    -> (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    -> (Seq a, a, a)
    cycleBoth
              (forall (n :: Nat). KnownNat n => SNat n
    SNat @nAddrs) TdpbramModelConfig writeEnable a
    config
              a
    prevA a
    prevB Seq a
    ram0 (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    portA (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    portB
          (Signal domA a
    as2, Signal domB a
    bs2) = Seq a
    -> [ClockAB]
    -> Signal domA (Bool, writeEnable, Int, a)
    -> Signal domB (Bool, writeEnable, Int, a)
    -> a
    -> a
    -> (Signal domA a, Signal domB a)
    go Seq a
    ram1 [ClockAB]
    ticks Signal domA (Bool, writeEnable, Int, a)
    as1 Signal domB (Bool, writeEnable, Int, a)
    bs1 a
    outA1 a
    outB1

        goA :: a -> a -> (Signal domA a, Signal domB a)
    goA a
    prevA a
    prevB = a
    out a
    -> (Signal domA a, Signal domB a) -> (Signal domA a, Signal domB a)
    forall a b. a -> b -> b
    `seqX` (a
    out a -> Signal domA a -> Signal domA a
    forall (dom :: Domain) a. a -> Signal dom a -> Signal dom a
    :- Signal domA a
    as2, Signal domB a
    bs2)
         where
          (Seq a
    ram1, a
    out) = SNat nAddrs
    -> TdpbramModelConfig writeEnable a
    -> a
    -> Seq a
    -> (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    -> (Seq a, a)
    forall (nAddrs :: Nat) a writeEnable.
    (HasCallStack, NFDataX a) =>
    SNat nAddrs
    -> TdpbramModelConfig writeEnable a
    -> a
    -> Seq a
    -> (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    -> (Seq a, a)
    cycleOne (forall (n :: Nat). KnownNat n => SNat n
    SNat @nAddrs) TdpbramModelConfig writeEnable a
    config a
    prevA Seq a
    ram0 (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    portA
          (Signal domA a
    as2, Signal domB a
    bs2) = Seq a
    -> [ClockAB]
    -> Signal domA (Bool, writeEnable, Int, a)
    -> Signal domB (Bool, writeEnable, Int, a)
    -> a
    -> a
    -> (Signal domA a, Signal domB a)
    go Seq a
    ram1 [ClockAB]
    ticks Signal domA (Bool, writeEnable, Int, a)
    as1 Signal domB (Bool, writeEnable, Int, a)
    bs0 a
    out a
    prevB

        goB :: a -> a -> (Signal domA a, Signal domB a)
    goB a
    prevA a
    prevB = a
    out a
    -> (Signal domA a, Signal domB a) -> (Signal domA a, Signal domB a)
    forall a b. a -> b -> b
    `seqX` (Signal domA a
    as2, a
    out a -> Signal domB a -> Signal domB a
    forall (dom :: Domain) a. a -> Signal dom a -> Signal dom a
    :- Signal domB a
    bs2)
         where
          (Seq a
    ram1, a
    out) = SNat nAddrs
    -> TdpbramModelConfig writeEnable a
    -> a
    -> Seq a
    -> (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    -> (Seq a, a)
    forall (nAddrs :: Nat) a writeEnable.
    (HasCallStack, NFDataX a) =>
    SNat nAddrs
    -> TdpbramModelConfig writeEnable a
    -> a
    -> Seq a
    -> (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    -> (Seq a, a)
    cycleOne (forall (n :: Nat). KnownNat n => SNat n
    SNat @nAddrs) TdpbramModelConfig writeEnable a
    config a
    prevB Seq a
    ram0 (MaybeX Bool, MaybeX Int, MaybeX writeEnable, a)
    portB
          (Signal domA a
    as2, Signal domB a
    bs2) = Seq a
    -> [ClockAB]
    -> Signal domA (Bool, writeEnable, Int, a)
    -> Signal domB (Bool, writeEnable, Int, a)
    -> a
    -> a
    -> (Signal domA a, Signal domB a)
    go Seq a
    ram1 [ClockAB]
    ticks Signal domA (Bool, writeEnable, Int, a)
    as0 Signal domB (Bool, writeEnable, Int, a)
    bs1 a
    prevA a
    out