{-|
Copyright  :  (C) 2015-2016, University of Twente,
                  2017     , Google Inc.,
                  2019     , Myrtle Software Ltd,
                  2021-2022, QBayLogic B.V.
License    :  BSD2 (see the file LICENSE)
Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>

= Initializing a BlockRAM with a data file #usingramfiles#

BlockRAM primitives that can be initialized with a data file. The BNF grammar
for this data file is simple:

@
FILE = LINE+
LINE = BIT+
BIT  = '0'
     | '1'
@

Consecutive @LINE@s correspond to consecutive memory addresses starting at @0@.
For example, a data file @memory.bin@ containing the 9-bit unsigned number
@7@ to @13@ looks like:

@
000000111
000001000
000001001
000001010
000001011
000001100
000001101
@

Such a file can be produced with 'memFile':

@
writeFile "memory.bin" (memFile Nothing [7 :: Unsigned 9 .. 13])
@

We can instantiate a BlockRAM using the content of the above file like so:

@
f :: Clock  dom
  -> Enable dom
  -> Signal dom (Unsigned 3)
  -> Signal dom (Unsigned 9)
f clk ena rd = 'Clash.Class.BitPack.unpack' '<$>' 'blockRamFile' clk ena d7 \"memory.bin\" rd (signal Nothing)
@

In the example above, we basically treat the BlockRAM as an synchronous ROM.
We can see that it works as expected:

@
__>>> import qualified Data.List as L__
__>>> L.tail $ sampleN 4 $ f systemClockGen enableGen (fromList [3..5])__
[10,11,12]
@

However, we can also interpret the same data as a tuple of a 6-bit unsigned
number, and a 3-bit signed number:

@
g :: Clock  dom
  -> Enable dom
  -> Signal dom (Unsigned 3)
  -> Signal dom (Unsigned 6,Signed 3)
g clk ena rd = 'Clash.Class.BitPack.unpack' '<$>' 'blockRamFile' clk ena d7 \"memory.bin\" rd (signal Nothing)
@

And then we would see:

@
__>>> import qualified Data.List as L__
__>>> L.tail $ sampleN 4 $ g systemClockGen enableGen (fromList [3..5])__
[(1,2),(1,3)(1,-4)]
@

-}

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}

{-# LANGUAGE Unsafe #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_HADDOCK show-extensions #-}

-- See: https://github.com/clash-lang/clash-compiler/commit/721fcfa9198925661cd836668705f817bddaae3c
-- as to why we need this.
{-# OPTIONS_GHC -fno-cpr-anal #-}

module Clash.Explicit.BlockRam.File
  ( -- * BlockRAM synchronized to an arbitrary clock
    blockRamFile
  , blockRamFilePow2
    -- * Producing files
  , memFile
    -- * Internal
  , blockRamFile#
  , initMem
  )
where

import Control.Exception     (catch, throw)
import Control.Monad         (forM_)
import Control.Monad.ST      (ST, runST)
import Control.Monad.ST.Unsafe (unsafeInterleaveST, unsafeIOToST, unsafeSTToIO)
import Data.Array.MArray     (newArray_)
import Data.Bits             ((.&.), (.|.), shiftL, xor)
import Data.Char             (digitToInt)
import Data.Maybe            (isJust, listToMaybe)
import GHC.Arr               (STArray, unsafeReadSTArray, unsafeWriteSTArray)
import GHC.Stack             (HasCallStack, withFrozenCallStack)
import GHC.TypeLits          (KnownNat)
import Numeric               (readInt)
import System.IO

import Clash.Annotations.Primitive (hasBlackBox)
import Clash.Class.BitPack   (BitPack, BitSize, pack)
import Clash.Promoted.Nat    (SNat (..), pow2SNat, natToNum, snatToNum)
import Clash.Sized.Internal.BitVector (Bit(..), BitVector(..), undefined#)
import Clash.Signal.Internal
  (Clock(..), Signal (..), Enable, KnownDomain, fromEnable, (.&&.))
import Clash.Signal.Bundle   (unbundle)
import Clash.Sized.Unsigned  (Unsigned)
import Clash.XException      (errorX, maybeIsX, seqX, fromJustX, XException (..))

-- start benchmark only
-- import GHC.Arr (unsafeFreezeSTArray, unsafeThawSTArray)
-- end benchmark only

-- $setup
-- >>> :m -Prelude
-- >>> :set -fplugin GHC.TypeLits.Normalise
-- >>> :set -fplugin GHC.TypeLits.KnownNat.Solver
-- >>> import Clash.Prelude
-- >>> import Clash.Prelude.BlockRam.File


-- | Create a blockRAM with space for 2^@n@ elements
--
-- * __NB__: Read value is delayed by 1 cycle
-- * __NB__: Initial output value is /undefined/, reading it will throw an
-- 'XException'
-- * __NB__: This function might not work for specific combinations of
-- code-generation backends and hardware targets. Please check the support table
-- below:
--
--     @
--                    | VHDL     | Verilog  | SystemVerilog |
--     ===============+==========+==========+===============+
--     Altera/Quartus | Broken   | Works    | Works         |
--     Xilinx/ISE     | Works    | Works    | Works         |
--     ASIC           | Untested | Untested | Untested      |
--     ===============+==========+==========+===============+
--     @
--
-- Additional helpful information:
--
-- * See "Clash.Prelude.BlockRam#usingrams" for more information on how to use a
-- Block RAM.
-- * Use the adapter 'Clash.Explicit.BlockRam.readNew' for obtaining write-before-read semantics like this: @'Clash.Explicit.BlockRam.readNew' clk rst en (blockRamFilePow2' clk en file) rd wrM@.
-- * See "Clash.Explicit.BlockRam.File#usingramfiles" for more information on how
-- to instantiate a Block RAM with the contents of a data file.
-- * See 'memFile' for creating a data file with Clash.
-- * See "Clash.Explicit.Fixed#creatingdatafiles" for more ideas on how to
-- create your own data files.
blockRamFilePow2
  :: forall dom n m
   . (KnownDomain dom, KnownNat m, KnownNat n, HasCallStack)
  => Clock dom
  -- ^ 'Clock' to synchronize to
  -> Enable dom
  -- ^ Global enable
  -> FilePath
  -- ^ File describing the initial content of the blockRAM
  -> Signal dom (Unsigned n)
  -- ^ Read address @r@
  -> Signal dom (Maybe (Unsigned n, BitVector m))
  -- ^ (write address @w@, value to write)
  -> Signal dom (BitVector m)
  -- ^ Value of the @blockRAM@ at address @r@ from the previous clock cycle
blockRamFilePow2 :: Clock dom
-> Enable dom
-> FilePath
-> Signal dom (Unsigned n)
-> Signal dom (Maybe (Unsigned n, BitVector m))
-> Signal dom (BitVector m)
blockRamFilePow2 = \Clock dom
clk Enable dom
en FilePath
file Signal dom (Unsigned n)
rd Signal dom (Maybe (Unsigned n, BitVector m))
wrM -> (HasCallStack => Signal dom (BitVector m))
-> Signal dom (BitVector m)
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack
  (Clock dom
-> Enable dom
-> SNat (2 ^ n)
-> FilePath
-> Signal dom (Unsigned n)
-> Signal dom (Maybe (Unsigned n, BitVector m))
-> Signal dom (BitVector m)
forall (dom :: Domain) (m :: Nat) addr (n :: Nat).
(KnownDomain dom, KnownNat m, Enum addr, HasCallStack) =>
Clock dom
-> Enable dom
-> SNat n
-> FilePath
-> Signal dom addr
-> Signal dom (Maybe (addr, BitVector m))
-> Signal dom (BitVector m)
blockRamFile Clock dom
clk Enable dom
en (SNat n -> SNat (2 ^ n)
forall (a :: Nat). SNat a -> SNat (2 ^ a)
pow2SNat (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat @n)) FilePath
file Signal dom (Unsigned n)
rd Signal dom (Maybe (Unsigned n, BitVector m))
wrM)
{-# INLINE blockRamFilePow2 #-}

-- | Create a blockRAM with space for @n@ elements
--
-- * __NB__: Read value is delayed by 1 cycle
-- * __NB__: Initial output value is /undefined/, reading it will throw an
-- 'XException'
-- * __NB__: This function might not work for specific combinations of
-- code-generation backends and hardware targets. Please check the support table
-- below:
--
--     @
--                    | VHDL     | Verilog  | SystemVerilog |
--     ===============+==========+==========+===============+
--     Altera/Quartus | Broken   | Works    | Works         |
--     Xilinx/ISE     | Works    | Works    | Works         |
--     ASIC           | Untested | Untested | Untested      |
--     ===============+==========+==========+===============+
--     @
--
-- Additional helpful information:
--
-- * See "Clash.Explicit.BlockRam#usingrams" for more information on how to use a
-- Block RAM.
-- * Use the adapter 'Clash.Explicit.BlockRam.readNew' for obtaining write-before-read semantics like this: @'Clash.Explicit.BlockRam.readNew' clk rst en ('blockRamFile' clk en size file) rd wrM@.
-- * See "Clash.Explicit.BlockRam.File#usingramfiles" for more information on how
-- to instantiate a Block RAM with the contents of a data file.
-- * See 'memFile' for creating a data file with Clash.
-- * See "Clash.Sized.Fixed#creatingdatafiles" for more ideas on how to create
-- your own data files.
blockRamFile
  :: (KnownDomain dom, KnownNat m, Enum addr, HasCallStack)
  => Clock dom
  -- ^ 'Clock' to synchronize to
  -> Enable dom
  -- ^ Global enable
  -> SNat n
  -- ^ Size of the blockRAM
  -> FilePath
  -- ^ File describing the initial content of the blockRAM
  -> Signal dom addr
  -- ^ Read address @r@
  -> Signal dom (Maybe (addr, BitVector m))
  -- ^ (write address @w@, value to write)
  -> Signal dom (BitVector m)
  -- ^ Value of the @blockRAM@ at address @r@ from the previous
  -- clock cycle
blockRamFile :: Clock dom
-> Enable dom
-> SNat n
-> FilePath
-> Signal dom addr
-> Signal dom (Maybe (addr, BitVector m))
-> Signal dom (BitVector m)
blockRamFile = \Clock dom
clk Enable dom
gen SNat n
sz FilePath
file Signal dom addr
rd Signal dom (Maybe (addr, BitVector m))
wrM ->
  let en :: Signal dom Bool
en       = Maybe (addr, BitVector m) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (addr, BitVector m) -> Bool)
-> Signal dom (Maybe (addr, BitVector m)) -> Signal dom Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (Maybe (addr, BitVector m))
wrM
      (Signal dom addr
wr,Signal dom (BitVector m)
din) = Signal dom (addr, BitVector m) -> Unbundled dom (addr, BitVector m)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
unbundle (Maybe (addr, BitVector m) -> (addr, BitVector m)
forall a. HasCallStack => Maybe a -> a
fromJustX (Maybe (addr, BitVector m) -> (addr, BitVector m))
-> Signal dom (Maybe (addr, BitVector m))
-> Signal dom (addr, BitVector m)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (Maybe (addr, BitVector m))
wrM)
  in  (HasCallStack => Signal dom (BitVector m))
-> Signal dom (BitVector m)
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack
      (Clock dom
-> Enable dom
-> SNat n
-> FilePath
-> Signal dom Int
-> Signal dom Bool
-> Signal dom Int
-> Signal dom (BitVector m)
-> Signal dom (BitVector m)
forall (m :: Nat) (dom :: Domain) (n :: Nat).
(KnownDomain dom, KnownNat m, HasCallStack) =>
Clock dom
-> Enable dom
-> SNat n
-> FilePath
-> Signal dom Int
-> Signal dom Bool
-> Signal dom Int
-> Signal dom (BitVector m)
-> Signal dom (BitVector m)
blockRamFile# Clock dom
clk Enable dom
gen SNat n
sz FilePath
file (addr -> Int
forall a. Enum a => a -> Int
fromEnum (addr -> Int) -> Signal dom addr -> Signal dom Int
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom addr
rd) Signal dom Bool
en (addr -> Int
forall a. Enum a => a -> Int
fromEnum (addr -> Int) -> Signal dom addr -> Signal dom Int
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom addr
wr) Signal dom (BitVector m)
din)
{-# INLINE blockRamFile #-}

-- | Convert data to the String contents of a memory file.
--
-- * __NB:__ Not synthesizable
-- * The following document the several ways to instantiate components with
-- files:
--
--     * "Clash.Prelude.BlockRam.File#usingramfiles"
--     * "Clash.Prelude.ROM.File#usingromfiles"
--     * "Clash.Explicit.BlockRam.File#usingramfiles"
--     * "Clash.Explicit.ROM.File#usingromfiles"
--
-- * See "Clash.Sized.Fixed#creatingdatafiles" for more ideas on how to create
-- your own data files.
--
-- = Example
--
-- The @Maybe@ datatype has don't care bits, where the actual value does not
-- matter. But the bits need a defined value in the memory. Either 0 or 1 can be
-- used, and both are valid representations of the data.
--
-- >>> let es = [ Nothing, Just (7 :: Unsigned 8), Just 8]
-- >>> mapM_ (putStrLn . show . pack) es
-- 0b0_...._....
-- 0b1_0000_0111
-- 0b1_0000_1000
-- >>> putStr (memFile (Just 0) es)
-- 000000000
-- 100000111
-- 100001000
-- >>> putStr (memFile (Just 1) es)
-- 011111111
-- 100000111
-- 100001000
--
memFile
  :: forall a f
   . ( BitPack a
     , Foldable f
     , HasCallStack)
  => Maybe Bit
  -- ^ Value to map don't care bits to. Nothing means throwing an error on
  -- don't care bits.
  -> f a
  -- ^ Values to convert.
  -> String
  -- ^ Contents of the memory file.
memFile :: Maybe Bit -> f a -> FilePath
memFile Maybe Bit
care = (a -> FilePath -> FilePath) -> FilePath -> f a -> FilePath
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
e -> BitVector (BitSize a) -> FilePath -> FilePath
showsBV (BitVector (BitSize a) -> FilePath -> FilePath)
-> BitVector (BitSize a) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ a -> BitVector (BitSize a)
forall a. BitPack a => a -> BitVector (BitSize a)
pack a
e) FilePath
""
 where
  showsBV :: BitVector (BitSize a) -> String -> String
  showsBV :: BitVector (BitSize a) -> FilePath -> FilePath
showsBV (BV Natural
mask Natural
val) FilePath
s =
    if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then
      Char
'0' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: Char
'\n' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
s
    else
      case Maybe Bit
care of
        Just (Bit Word
0 Word
0) -> Int -> Natural -> FilePath -> FilePath
forall t a.
(Integral t, Num a, Eq a) =>
a -> t -> FilePath -> FilePath
go Int
n (Natural
val Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. (Natural
mask Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
`xor` Natural
fullMask)) (Char
'\n' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
s)
        Just (Bit Word
0 Word
1)  -> Int -> Natural -> FilePath -> FilePath
forall t a.
(Integral t, Num a, Eq a) =>
a -> t -> FilePath -> FilePath
go Int
n (Natural
val Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
mask) (Char
'\n' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
s)
        Maybe Bit
_ -> if Natural
mask Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
/= Natural
0 then
               FilePath
forall a. a
err
             else
               Int -> Natural -> FilePath -> FilePath
forall t a.
(Integral t, Num a, Eq a) =>
a -> t -> FilePath -> FilePath
go Int
n Natural
val (Char
'\n' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
s)
   where
    n :: Int
n = (Num Int, KnownNat (BitSize a)) => Int
forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @(BitSize a) @Int
    fullMask :: Natural
fullMask = (Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Int
n) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1
    err :: a
err = (HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => a) -> a) -> (HasCallStack => a) -> a
forall a b. (a -> b) -> a -> b
$ FilePath -> a
forall a. HasCallStack => FilePath -> a
error (FilePath -> a) -> FilePath -> a
forall a b. (a -> b) -> a -> b
$
            FilePath
"memFile: cannot convert don't-care values. "
            FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"Please specify mapping to definite value."
    go :: a -> t -> FilePath -> FilePath
go a
0  t
_ FilePath
s0 = FilePath
s0
    go a
n0 t
v FilePath
s0 =
      let (!t
v0, !t
vBit) = t -> t -> (t, t)
forall a. Integral a => a -> a -> (a, a)
quotRem t
v t
2
      in if t
vBit t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 then
           a -> t -> FilePath -> FilePath
go (a
n0 a -> a -> a
forall a. Num a => a -> a -> a
- a
1) t
v0 (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Char
'0' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
s0
         else
           a -> t -> FilePath -> FilePath
go (a
n0 a -> a -> a
forall a. Num a => a -> a -> a
- a
1) t
v0 (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Char
'1' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
s0

-- | blockRamFile primitive
blockRamFile#
  :: forall m dom n
   . (KnownDomain dom, KnownNat m, HasCallStack)
  => Clock dom
  -- ^ 'Clock' to synchronize to
  -> Enable dom
  -- ^ Global enable
  -> SNat n
  -- ^ Size of the blockRAM
  -> FilePath
  -- ^ File describing the initial content of the blockRAM
  -> Signal dom Int
  -- ^ Read address @r@
  -> Signal dom Bool
  -- ^ Write enable
  -> Signal dom Int
  -- ^ Write address @w@
  -> Signal dom (BitVector m)
  -- ^ Value to write (at address @w@)
  -> Signal dom (BitVector m)
  -- ^ Value of the @blockRAM@ at address @r@ from the previous clock cycle
blockRamFile# :: Clock dom
-> Enable dom
-> SNat n
-> FilePath
-> Signal dom Int
-> Signal dom Bool
-> Signal dom Int
-> Signal dom (BitVector m)
-> Signal dom (BitVector m)
blockRamFile# (Clock SSymbol dom
_) Enable dom
ena SNat n
sz FilePath
file = \Signal dom Int
rd Signal dom Bool
wen Signal dom Int
waS Signal dom (BitVector m)
wd -> (forall s. ST s (Signal dom (BitVector m)))
-> Signal dom (BitVector m)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Signal dom (BitVector m)))
 -> Signal dom (BitVector m))
-> (forall s. ST s (Signal dom (BitVector m)))
-> Signal dom (BitVector m)
forall a b. (a -> b) -> a -> b
$ do
  STArray s Int (BitVector m)
ramStart <- (Int, Int) -> ST s (STArray s Int (BitVector m))
forall (a :: Type -> Type -> Type) e (m :: Type -> Type) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Int
0,Int
szI)
  IO () -> ST s ()
forall a s. IO a -> ST s a
unsafeIOToST (FilePath -> IOMode -> (Handle -> IO ()) -> IO ()
forall r. FilePath -> IOMode -> (Handle -> IO r) -> IO r
withFile FilePath
file IOMode
ReadMode (\Handle
h ->
    [Int] -> (Int -> IO ()) -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
0..(Int
szIInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] (\Int
i -> do
      FilePath
l <- Handle -> IO FilePath
hGetLine Handle
h
      let bv :: BitVector m
bv = FilePath -> BitVector m
parseBV FilePath
l
      BitVector m
bv BitVector m -> IO () -> IO ()
`seq` ST s () -> IO ()
forall s a. ST s a -> IO a
unsafeSTToIO (STArray s Int (BitVector m) -> Int -> BitVector m -> ST s ()
forall s i e. STArray s i e -> Int -> e -> ST s ()
unsafeWriteSTArray STArray s Int (BitVector m)
ramStart Int
i BitVector m
bv)
      )))
  -- start benchmark only
  -- ramStart <- unsafeThawSTArray ramArr
  -- end benchmark only
  STArray s Int (BitVector m)
-> BitVector m
-> Signal dom Bool
-> Signal dom Int
-> Signal dom Bool
-> Signal dom Int
-> Signal dom (BitVector m)
-> ST s (Signal dom (BitVector m))
forall s.
STArray s Int (BitVector m)
-> BitVector m
-> Signal dom Bool
-> Signal dom Int
-> Signal dom Bool
-> Signal dom Int
-> Signal dom (BitVector m)
-> ST s (Signal dom (BitVector m))
go
    STArray s Int (BitVector m)
ramStart
    ((HasCallStack => BitVector m) -> BitVector m
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack (FilePath -> BitVector m
forall a. HasCallStack => FilePath -> a
errorX FilePath
"blockRamFile: intial value undefined"))
    (Enable dom -> Signal dom Bool
forall (dom :: Domain). Enable dom -> Signal dom Bool
fromEnable Enable dom
ena)
    Signal dom Int
rd
    (Enable dom -> Signal dom Bool
forall (dom :: Domain). Enable dom -> Signal dom Bool
fromEnable Enable dom
ena Signal dom Bool -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type).
Applicative f =>
f Bool -> f Bool -> f Bool
.&&. Signal dom Bool
wen)
    Signal dom Int
waS
    Signal dom (BitVector m)
wd
 where
  szI :: Int
szI = SNat n -> Int
forall a (n :: Nat). Num a => SNat n -> a
snatToNum SNat n
sz :: Int
  -- start benchmark only
  -- ramArr = runST $ do
  --             ram <- newArray_ (0,szI-1) -- 0 -- (error "QQ")
  --             unsafeIOToST (withFile file ReadMode (\h ->
  --               forM_ [0..(szI-1)] (\i -> do
  --                 l <- hGetLine h
  --                 let bv = parseBV l
  --                 bv `seq` unsafeSTToIO (unsafeWriteSTArray ram i bv))
  --               ))
  --             unsafeFreezeSTArray ram
  -- end benchmark only

  go :: STArray s Int (BitVector m) -> (BitVector m) -> Signal dom Bool -> Signal dom Int
    -> Signal dom Bool -> Signal dom Int -> Signal dom (BitVector m)
    -> ST s (Signal dom (BitVector m))
  go :: STArray s Int (BitVector m)
-> BitVector m
-> Signal dom Bool
-> Signal dom Int
-> Signal dom Bool
-> Signal dom Int
-> Signal dom (BitVector m)
-> ST s (Signal dom (BitVector m))
go !STArray s Int (BitVector m)
ram BitVector m
o ret :: Signal dom Bool
ret@(~(Bool
re :- Signal dom Bool
res)) rt :: Signal dom Int
rt@(~(Int
r :- Signal dom Int
rs)) et :: Signal dom Bool
et@(~(Bool
e :- Signal dom Bool
en)) wt :: Signal dom Int
wt@(~(Int
w :- Signal dom Int
wr)) dt :: Signal dom (BitVector m)
dt@(~(BitVector m
d :- Signal dom (BitVector m)
din)) = do
    BitVector m
o BitVector m
-> ST s (Signal dom (BitVector m))
-> ST s (Signal dom (BitVector m))
forall a b. a -> b -> b
`seqX` (BitVector m
o BitVector m -> Signal dom (BitVector m) -> Signal dom (BitVector m)
forall (dom :: Domain) a. a -> Signal dom a -> Signal dom a
:-) (Signal dom (BitVector m) -> Signal dom (BitVector m))
-> ST s (Signal dom (BitVector m))
-> ST s (Signal dom (BitVector m))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Signal dom Bool
ret Signal dom Bool
-> ST s (Signal dom (BitVector m))
-> ST s (Signal dom (BitVector m))
`seq` Signal dom Int
rt Signal dom Int
-> ST s (Signal dom (BitVector m))
-> ST s (Signal dom (BitVector m))
`seq` Signal dom Bool
et Signal dom Bool
-> ST s (Signal dom (BitVector m))
-> ST s (Signal dom (BitVector m))
`seq` Signal dom Int
wt Signal dom Int
-> ST s (Signal dom (BitVector m))
-> ST s (Signal dom (BitVector m))
`seq` Signal dom (BitVector m)
dt Signal dom (BitVector m)
-> ST s (Signal dom (BitVector m))
-> ST s (Signal dom (BitVector m))
`seq`
      ST s (Signal dom (BitVector m)) -> ST s (Signal dom (BitVector m))
forall s a. ST s a -> ST s a
unsafeInterleaveST
        (do BitVector m
o' <- IO (BitVector m) -> ST s (BitVector m)
forall a s. IO a -> ST s a
unsafeIOToST
                    (IO (BitVector m)
-> (XException -> IO (BitVector m)) -> IO (BitVector m)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch (if Bool
re then ST s (BitVector m) -> IO (BitVector m)
forall s a. ST s a -> IO a
unsafeSTToIO (STArray s Int (BitVector m)
ram STArray s Int (BitVector m) -> Int -> ST s (BitVector m)
forall s.
HasCallStack =>
STArray s Int (BitVector m) -> Int -> ST s (BitVector m)
`safeAt` Int
r) else BitVector m -> IO (BitVector m)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BitVector m
o)
                    (\err :: XException
err@XException {} -> BitVector m -> IO (BitVector m)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (XException -> BitVector m
forall a e. Exception e => e -> a
throw XException
err)))
            BitVector m
d BitVector m -> ST s () -> ST s ()
forall a b. a -> b -> b
`seqX` STArray s Int (BitVector m)
-> Bool -> Int -> BitVector m -> ST s ()
forall s.
STArray s Int (BitVector m)
-> Bool -> Int -> BitVector m -> ST s ()
upd STArray s Int (BitVector m)
ram Bool
e (Int -> Int
forall a. Enum a => a -> Int
fromEnum Int
w) BitVector m
d
            STArray s Int (BitVector m)
-> BitVector m
-> Signal dom Bool
-> Signal dom Int
-> Signal dom Bool
-> Signal dom Int
-> Signal dom (BitVector m)
-> ST s (Signal dom (BitVector m))
forall s.
STArray s Int (BitVector m)
-> BitVector m
-> Signal dom Bool
-> Signal dom Int
-> Signal dom Bool
-> Signal dom Int
-> Signal dom (BitVector m)
-> ST s (Signal dom (BitVector m))
go STArray s Int (BitVector m)
ram BitVector m
o' Signal dom Bool
res Signal dom Int
rs Signal dom Bool
en Signal dom Int
wr Signal dom (BitVector m)
din))

  upd :: STArray s Int (BitVector m) -> Bool -> Int -> (BitVector m) -> ST s ()
  upd :: STArray s Int (BitVector m)
-> Bool -> Int -> BitVector m -> ST s ()
upd STArray s Int (BitVector m)
ram Bool
we Int
waddr BitVector m
d = case Bool -> Maybe Bool
forall a. a -> Maybe a
maybeIsX Bool
we of
    Maybe Bool
Nothing -> case Int -> Maybe Int
forall a. a -> Maybe a
maybeIsX Int
waddr of
      Maybe Int
Nothing -> -- Put the XException from `waddr` as the value in all
                 -- locations of `ram`.
                 [Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
0..(Int
szIInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] (\Int
i -> STArray s Int (BitVector m) -> Int -> BitVector m -> ST s ()
forall s i e. STArray s i e -> Int -> e -> ST s ()
unsafeWriteSTArray STArray s Int (BitVector m)
ram Int
i (Int -> BitVector m -> BitVector m
seq Int
waddr BitVector m
d))
      Just Int
wa -> -- Put the XException from `we` as the value at address
                 -- `waddr`.
                 Int -> BitVector m -> STArray s Int (BitVector m) -> ST s ()
forall a s. HasCallStack => Int -> a -> STArray s Int a -> ST s ()
safeUpdate Int
wa (Bool -> BitVector m -> BitVector m
seq Bool
we BitVector m
d) STArray s Int (BitVector m)
ram
    Just Bool
True -> case Int -> Maybe Int
forall a. a -> Maybe a
maybeIsX Int
waddr of
      Maybe Int
Nothing -> -- Put the XException from `waddr` as the value in all
                 -- locations of `ram`.
                 [Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
0..(Int
szIInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] (\Int
i -> STArray s Int (BitVector m) -> Int -> BitVector m -> ST s ()
forall s i e. STArray s i e -> Int -> e -> ST s ()
unsafeWriteSTArray STArray s Int (BitVector m)
ram Int
i (Int -> BitVector m -> BitVector m
seq Int
waddr BitVector m
d))
      Just Int
wa -> Int -> BitVector m -> STArray s Int (BitVector m) -> ST s ()
forall a s. HasCallStack => Int -> a -> STArray s Int a -> ST s ()
safeUpdate Int
wa BitVector m
d STArray s Int (BitVector m)
ram
    Maybe Bool
_ -> () -> ST s ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

  safeAt :: HasCallStack => STArray s Int (BitVector m) -> Int -> ST s (BitVector m)
  safeAt :: STArray s Int (BitVector m) -> Int -> ST s (BitVector m)
safeAt STArray s Int (BitVector m)
s Int
i =
    if (Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i) Bool -> Bool -> Bool
&& (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
szI) then
      STArray s Int (BitVector m) -> Int -> ST s (BitVector m)
forall s i e. STArray s i e -> Int -> ST s e
unsafeReadSTArray STArray s Int (BitVector m)
s Int
i
    else BitVector m -> ST s (BitVector m)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BitVector m -> ST s (BitVector m))
-> BitVector m -> ST s (BitVector m)
forall a b. (a -> b) -> a -> b
$
      (HasCallStack => BitVector m) -> BitVector m
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack
        (FilePath -> BitVector m
forall a. HasCallStack => FilePath -> a
errorX (FilePath
"blockRamFile: read address " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<>
                FilePath
" not in range [0.." FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Int -> FilePath
forall a. Show a => a -> FilePath
show Int
szI FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
")"))
  {-# INLINE safeAt #-}

  safeUpdate :: HasCallStack => Int -> a -> STArray s Int a -> ST s ()
  safeUpdate :: Int -> a -> STArray s Int a -> ST s ()
safeUpdate Int
i a
a STArray s Int a
s =
    if (Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i) Bool -> Bool -> Bool
&& (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
szI) then
      STArray s Int a -> Int -> a -> ST s ()
forall s i e. STArray s i e -> Int -> e -> ST s ()
unsafeWriteSTArray STArray s Int a
s Int
i a
a
    else
      let d :: a
d = (HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack
                (FilePath -> a
forall a. HasCallStack => FilePath -> a
errorX (FilePath
"blockRamFile: write address " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<>
                        FilePath
" not in range [0.." FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Int -> FilePath
forall a. Show a => a -> FilePath
show Int
szI FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
")"))
      in [Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
0..(Int
szIInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] (\Int
j -> STArray s Int a -> Int -> a -> ST s ()
forall s i e. STArray s i e -> Int -> e -> ST s ()
unsafeWriteSTArray STArray s Int a
s Int
j a
d)
  {-# INLINE safeUpdate #-}

  parseBV :: String -> BitVector m
  parseBV :: FilePath -> BitVector m
parseBV FilePath
s = case FilePath -> Maybe Integer
parseBV' FilePath
s of
                Just Integer
i  -> Integer -> BitVector m
forall a. Num a => Integer -> a
fromInteger Integer
i
                Maybe Integer
Nothing -> BitVector m
forall (n :: Nat). KnownNat n => BitVector n
undefined#
  parseBV' :: FilePath -> Maybe Integer
parseBV' = ((Integer, FilePath) -> Integer)
-> Maybe (Integer, FilePath) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer, FilePath) -> Integer
forall a b. (a, b) -> a
fst (Maybe (Integer, FilePath) -> Maybe Integer)
-> (FilePath -> Maybe (Integer, FilePath))
-> FilePath
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Integer, FilePath)] -> Maybe (Integer, FilePath)
forall a. [a] -> Maybe a
listToMaybe ([(Integer, FilePath)] -> Maybe (Integer, FilePath))
-> (FilePath -> [(Integer, FilePath)])
-> FilePath
-> Maybe (Integer, FilePath)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer
-> (Char -> Bool)
-> (Char -> Int)
-> FilePath
-> [(Integer, FilePath)]
forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
readInt Integer
2 (Char -> FilePath -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` FilePath
"01") Char -> Int
digitToInt
{-# NOINLINE blockRamFile# #-}
{-# ANN blockRamFile# hasBlackBox #-}

-- | __NB:__ Not synthesizable
initMem :: KnownNat n => FilePath -> IO [BitVector n]
initMem :: FilePath -> IO [BitVector n]
initMem = (FilePath -> [BitVector n]) -> IO FilePath -> IO [BitVector n]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FilePath -> BitVector n) -> [FilePath] -> [BitVector n]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> BitVector n
parseBV ([FilePath] -> [BitVector n])
-> (FilePath -> [FilePath]) -> FilePath -> [BitVector n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
lines) (IO FilePath -> IO [BitVector n])
-> (FilePath -> IO FilePath) -> FilePath -> IO [BitVector n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> IO FilePath
readFile
  where
    parseBV :: FilePath -> BitVector n
parseBV FilePath
s = case FilePath -> Maybe Integer
parseBV' FilePath
s of
                  Just Integer
i  -> Integer -> BitVector n
forall a. Num a => Integer -> a
fromInteger Integer
i
                  Maybe Integer
Nothing -> FilePath -> BitVector n
forall a. HasCallStack => FilePath -> a
error (FilePath
"Failed to parse: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s)
    parseBV' :: FilePath -> Maybe Integer
parseBV' = ((Integer, FilePath) -> Integer)
-> Maybe (Integer, FilePath) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer, FilePath) -> Integer
forall a b. (a, b) -> a
fst (Maybe (Integer, FilePath) -> Maybe Integer)
-> (FilePath -> Maybe (Integer, FilePath))
-> FilePath
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Integer, FilePath)] -> Maybe (Integer, FilePath)
forall a. [a] -> Maybe a
listToMaybe ([(Integer, FilePath)] -> Maybe (Integer, FilePath))
-> (FilePath -> [(Integer, FilePath)])
-> FilePath
-> Maybe (Integer, FilePath)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer
-> (Char -> Bool)
-> (Char -> Int)
-> FilePath
-> [(Integer, FilePath)]
forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
readInt Integer
2 (Char -> FilePath -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` FilePath
"01") Char -> Int
digitToInt
{-# NOINLINE initMem #-}