{-|
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
showList :: [Conflict] -> ShowS
$cshowList :: [Conflict] -> ShowS
show :: Conflict -> String
$cshow :: Conflict -> String
showsPrec :: Int -> Conflict -> ShowS
$cshowsPrec :: Int -> 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 (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 :: MaybeX Bool -> MaybeX Bool -> MaybeX Bool -> 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 :: 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
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
tdpUpdateRam :: Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
tdpMergeWriteEnable :: MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
tdpIsActiveWriteEnable :: 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 (KnownNat nAddrs => SNat nAddrs
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. 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 :: 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 :: Int -> MaybeX writeEnable -> a -> Seq a -> Seq a
tdpMergeWriteEnable :: MaybeX Bool -> MaybeX writeEnable -> MaybeX writeEnable
tdpIsActiveWriteEnable :: MaybeX writeEnable -> MaybeX Bool
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
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 (KnownNat nAddrs => SNat nAddrs
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 (KnownNat nAddrs => SNat nAddrs
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 :: 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 a. (Num a, KnownNat nAddrs) => a
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
  { TdpbramModelConfig writeEnable a
-> MaybeX writeEnable -> MaybeX Bool
tdpIsActiveWriteEnable :: MaybeX writeEnable -> MaybeX Bool
  -- ^ Determine whether a write enable is active

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

  , 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 :: 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 a. (Num a, KnownNat nAddrs) => a
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
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
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
          (KnownNat nAddrs => SNat nAddrs
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 (KnownNat nAddrs => SNat nAddrs
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 (KnownNat nAddrs => SNat nAddrs
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