{-|
Copyright  :  (C) 2015-2016, University of Twente,
                  2017     , Google Inc.
                  2019     , Myrtle Software Ltd
License    :  BSD2 (see the file LICENSE)
Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>

ROMs
-}

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

{-# LANGUAGE Trustworthy #-}

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

module Clash.Explicit.ROM
  ( -- * Synchronous ROM synchronized to an arbitrary clock
    rom
  , romPow2
    -- * Internal
  , rom#
  )
where

import Data.Array             ((!),listArray)
import GHC.Stack              (withFrozenCallStack)
import GHC.TypeLits           (KnownNat, type (^))
import Prelude hiding         (length)

import Clash.Signal.Internal
  (Clock (..), KnownDomain, Signal (..), Enable, fromEnable)
import Clash.Sized.Unsigned   (Unsigned)
import Clash.Sized.Vector     (Vec, length, toList)
import Clash.XException       (deepErrorX, seqX, NFDataX)

-- | A ROM with a synchronous read port, with space for 2^@n@ elements
--
-- * __NB__: Read value is delayed by 1 cycle
-- * __NB__: Initial output value is 'undefined'
--
-- Additional helpful information:
--
-- * See "Clash.Sized.Fixed#creatingdatafiles" and "Clash.Explicit.BlockRam#usingrams"
-- for ideas on how to use ROMs and RAMs
romPow2
  :: (KnownDomain dom, KnownNat n, NFDataX a)
  => Clock dom
  -- ^ 'Clock' to synchronize to
  -> Enable dom
  -- ^ Global enable
  -> Vec (2^n) a
  -- ^ ROM content
  --
  -- __NB:__ must be a constant
  -> Signal dom (Unsigned n)
  -- ^ Read address @rd@
  -> Signal dom a
  -- ^ The value of the ROM at address @rd@
romPow2 :: Clock dom
-> Enable dom
-> Vec (2 ^ n) a
-> Signal dom (Unsigned n)
-> Signal dom a
romPow2 = Clock dom
-> Enable dom
-> Vec (2 ^ n) a
-> Signal dom (Unsigned n)
-> Signal dom a
forall (dom :: Domain) (n :: Nat) a addr.
(KnownDomain dom, KnownNat n, NFDataX a, Enum addr) =>
Clock dom
-> Enable dom -> Vec n a -> Signal dom addr -> Signal dom a
rom
{-# INLINE romPow2 #-}

-- | A ROM with a synchronous read port, with space for @n@ elements
--
-- * __NB__: Read value is delayed by 1 cycle
-- * __NB__: Initial output value is 'undefined'
--
-- Additional helpful information:
--
-- * See "Clash.Sized.Fixed#creatingdatafiles" and "Clash.Explicit.BlockRam#usingrams"
-- for ideas on how to use ROMs and RAMs
rom
  :: (KnownDomain dom, KnownNat n, NFDataX a, Enum addr)
  => Clock dom
  -- ^ 'Clock' to synchronize to
  -> Enable dom
  -- ^ Global enable
  -> Vec n a
  -- ^ ROM content
  --
  -- __NB:__ must be a constant
  -> Signal dom addr
  -- ^ Read address @rd@
  -> Signal dom a
  -- ^ The value of the ROM at address @rd@ from the previous clock cycle
rom :: Clock dom
-> Enable dom -> Vec n a -> Signal dom addr -> Signal dom a
rom = \clk :: Clock dom
clk en :: Enable dom
en content :: Vec n a
content rd :: Signal dom addr
rd -> Clock dom
-> Enable dom -> Vec n a -> Signal dom Int -> Signal dom a
forall (dom :: Domain) (n :: Nat) a.
(KnownDomain dom, KnownNat n, NFDataX a) =>
Clock dom
-> Enable dom -> Vec n a -> Signal dom Int -> Signal dom a
rom# Clock dom
clk Enable dom
en Vec n a
content (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)
{-# INLINE rom #-}

-- | ROM primitive
rom#
  :: forall dom n a
   . (KnownDomain dom, KnownNat n, NFDataX a)
  => Clock dom
  -- ^ 'Clock' to synchronize to
  -> Enable dom
  -- ^ Global enable
  -> Vec n a
  -- ^ ROM content
  --
  -- __NB:__ must be a constant
  -> Signal dom Int
  -- ^ Read address @rd@
  -> Signal dom a
  -- ^ The value of the ROM at address @rd@ from the previous clock cycle
rom# :: Clock dom
-> Enable dom -> Vec n a -> Signal dom Int -> Signal dom a
rom# _ en :: Enable dom
en content :: Vec n a
content =
  a -> Signal dom Bool -> Signal dom Int -> Signal dom a
go
    ((HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack (String -> a
forall a. (NFDataX a, HasCallStack) => String -> a
deepErrorX "rom: initial value undefined"))
    (Enable dom -> Signal dom Bool
forall (dom :: Domain). Enable dom -> Signal dom Bool
fromEnable Enable dom
en)
 where
  szI :: Int
szI = Vec n a -> Int
forall (n :: Nat) a. KnownNat n => Vec n a -> Int
length Vec n a
content
  arr :: Array Int a
arr = (Int, Int) -> [a] -> Array Int a
forall i e. Ix i => (i, i) -> [e] -> Array i e
listArray (0,Int
szIInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) (Vec n a -> [a]
forall (n :: Nat) a. Vec n a -> [a]
toList Vec n a
content)

  go :: a -> Signal dom Bool -> Signal dom Int -> Signal dom a
go o :: a
o (e :: Bool
e :- es :: Signal dom Bool
es) rd :: Signal dom Int
rd@(~(r :: Int
r :- rs :: Signal dom Int
rs)) =
    let o1 :: a
o1 = if Bool
e then Array Int a
arr Array Int a -> Int -> a
forall i e. Ix i => Array i e -> i -> e
! Int
r else a
o
    -- See [Note: register strictness annotations]
    in  a
o a -> Signal dom a -> Signal dom a
forall a b. a -> b -> b
`seqX` a
o a -> Signal dom a -> Signal dom a
forall (dom :: Domain) a. a -> Signal dom a -> Signal dom a
:- (Signal dom Int
rd Signal dom Int -> Signal dom a -> Signal dom a
forall a b. a -> b -> b
`seq` a -> Signal dom Bool -> Signal dom Int -> Signal dom a
go a
o1 Signal dom Bool
es Signal dom Int
rs)
{-# NOINLINE rom# #-}