{-|
Module      : Lion.Core
Description : Lion RISC-V Core
Copyright   : (c) David Cox, 2021
License     : BSD-3-Clause
Maintainer  : standardsemiconductor@gmail.com

The Lion core is a 32-bit RISC-V processor written in Haskell using [Clash](https://clash-lang.org). Note, all peripherals and memory must have single cycle latency. See [lion-soc](https://github.com/standardsemiconductor/lion/tree/main/lion-soc) for an example of using the Lion core in a system.
-}

module Lion.Core 
  ( core
  , FromCore(..)
  , toMem
  , toRvfi
  , P.ToMem(..)
  ) where

import Clash.Prelude
import Control.Lens
import Data.Maybe
import Data.Monoid
import Lion.Rvfi
import qualified Lion.Pipe as P

-- | Core outputs
data FromCore dom = FromCore
  { FromCore dom -> Signal dom (Maybe ToMem)
_toMem  :: Signal dom (Maybe P.ToMem) -- ^ shared memory and instruction bus, output from core to memory and peripherals
  , FromCore dom -> Signal dom Rvfi
_toRvfi :: Signal dom Rvfi -- ^ formal verification interface output, see [lion-formal](https://github.com/standardsemiconductor/lion/tree/main/lion-formal) for usage
  }
makeLenses ''FromCore

-- | RISC-V Core
core
  :: HiddenClockResetEnable dom
  => BitVector 32               -- ^ start address
  -> Signal dom (BitVector 32)  -- ^ core input, from memory/peripherals
  -> FromCore dom               -- ^ core output
core :: BitVector 32 -> Signal dom (BitVector 32) -> FromCore dom
core BitVector 32
start Signal dom (BitVector 32)
toCore = FromCore :: forall (dom :: Domain).
Signal dom (Maybe ToMem) -> Signal dom Rvfi -> FromCore dom
FromCore
  { _toMem :: Signal dom (Maybe ToMem)
_toMem  = First ToMem -> Maybe ToMem
forall a. First a -> Maybe a
getFirst (First ToMem -> Maybe ToMem)
-> (FromPipe -> First ToMem) -> FromPipe -> Maybe ToMem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FromPipe -> First ToMem
P._toMem (FromPipe -> Maybe ToMem)
-> Signal dom FromPipe -> Signal dom (Maybe ToMem)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom FromPipe
fromPipe
  , _toRvfi :: Signal dom Rvfi
_toRvfi = Rvfi -> Maybe Rvfi -> Rvfi
forall a. a -> Maybe a -> a
fromMaybe Rvfi
mkRvfi (Maybe Rvfi -> Rvfi)
-> (FromPipe -> Maybe Rvfi) -> FromPipe -> Rvfi
forall b c a. (b -> c) -> (a -> b) -> a -> c
. First Rvfi -> Maybe Rvfi
forall a. First a -> Maybe a
getFirst (First Rvfi -> Maybe Rvfi)
-> (FromPipe -> First Rvfi) -> FromPipe -> Maybe Rvfi
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FromPipe -> First Rvfi
P._toRvfi (FromPipe -> Rvfi) -> Signal dom FromPipe -> Signal dom Rvfi
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom FromPipe
fromPipe
  }
  where
    fromPipe :: Signal dom FromPipe
fromPipe = BitVector 32 -> Signal dom ToPipe -> Signal dom FromPipe
forall (dom :: Domain).
HiddenClockResetEnable dom =>
BitVector 32 -> Signal dom ToPipe -> Signal dom FromPipe
P.pipe BitVector 32
start (Signal dom ToPipe -> Signal dom FromPipe)
-> Signal dom ToPipe -> Signal dom FromPipe
forall a b. (a -> b) -> a -> b
$ BitVector 32 -> BitVector 32 -> BitVector 32 -> ToPipe
P.ToPipe (BitVector 32 -> BitVector 32 -> BitVector 32 -> ToPipe)
-> Signal dom (BitVector 32)
-> Signal dom (BitVector 32 -> BitVector 32 -> ToPipe)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (BitVector 32)
rs1Data Signal dom (BitVector 32 -> BitVector 32 -> ToPipe)
-> Signal dom (BitVector 32) -> Signal dom (BitVector 32 -> ToPipe)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Signal dom (BitVector 32)
rs2Data Signal dom (BitVector 32 -> ToPipe)
-> Signal dom (BitVector 32) -> Signal dom ToPipe
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Signal dom (BitVector 32)
toCore
    rs1Addr :: Signal dom (Unsigned 5)
rs1Addr = Unsigned 5 -> Maybe (Unsigned 5) -> Unsigned 5
forall a. a -> Maybe a -> a
fromMaybe Unsigned 5
0 (Maybe (Unsigned 5) -> Unsigned 5)
-> (FromPipe -> Maybe (Unsigned 5)) -> FromPipe -> Unsigned 5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. First (Unsigned 5) -> Maybe (Unsigned 5)
forall a. First a -> Maybe a
getFirst (First (Unsigned 5) -> Maybe (Unsigned 5))
-> (FromPipe -> First (Unsigned 5))
-> FromPipe
-> Maybe (Unsigned 5)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FromPipe -> First (Unsigned 5)
P._toRs1Addr (FromPipe -> Unsigned 5)
-> Signal dom FromPipe -> Signal dom (Unsigned 5)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom FromPipe
fromPipe
    rs2Addr :: Signal dom (Unsigned 5)
rs2Addr = Unsigned 5 -> Maybe (Unsigned 5) -> Unsigned 5
forall a. a -> Maybe a -> a
fromMaybe Unsigned 5
0 (Maybe (Unsigned 5) -> Unsigned 5)
-> (FromPipe -> Maybe (Unsigned 5)) -> FromPipe -> Unsigned 5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. First (Unsigned 5) -> Maybe (Unsigned 5)
forall a. First a -> Maybe a
getFirst (First (Unsigned 5) -> Maybe (Unsigned 5))
-> (FromPipe -> First (Unsigned 5))
-> FromPipe
-> Maybe (Unsigned 5)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FromPipe -> First (Unsigned 5)
P._toRs2Addr (FromPipe -> Unsigned 5)
-> Signal dom FromPipe -> Signal dom (Unsigned 5)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom FromPipe
fromPipe
    rdWrM :: Signal dom (Maybe (Unsigned 5, BitVector 32))
rdWrM = First (Unsigned 5, BitVector 32)
-> Maybe (Unsigned 5, BitVector 32)
forall a. First a -> Maybe a
getFirst (First (Unsigned 5, BitVector 32)
 -> Maybe (Unsigned 5, BitVector 32))
-> (FromPipe -> First (Unsigned 5, BitVector 32))
-> FromPipe
-> Maybe (Unsigned 5, BitVector 32)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FromPipe -> First (Unsigned 5, BitVector 32)
P._toRd (FromPipe -> Maybe (Unsigned 5, BitVector 32))
-> Signal dom FromPipe
-> Signal dom (Maybe (Unsigned 5, BitVector 32))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom FromPipe
fromPipe
    (Signal dom (BitVector 32)
rs1Data, Signal dom (BitVector 32)
rs2Data) = Signal dom (Unsigned 5)
-> Signal dom (Unsigned 5)
-> Signal dom (Maybe (Unsigned 5, BitVector 32))
-> Unbundled dom (BitVector 32, BitVector 32)
forall (dom :: Domain).
HiddenClockResetEnable dom =>
Signal dom (Unsigned 5)
-> Signal dom (Unsigned 5)
-> Signal dom (Maybe (Unsigned 5, BitVector 32))
-> Unbundled dom (BitVector 32, BitVector 32)
regBank Signal dom (Unsigned 5)
rs1Addr Signal dom (Unsigned 5)
rs2Addr Signal dom (Maybe (Unsigned 5, BitVector 32))
rdWrM

-- | Register bank
regBank
  :: HiddenClockResetEnable dom
  => Signal dom (Unsigned 5)                        -- ^ Rs1 Addr
  -> Signal dom (Unsigned 5)                        -- ^ Rs2 Addr
  -> Signal dom (Maybe (Unsigned 5, BitVector 32))  -- ^ Rd Write
  -> Unbundled dom (BitVector 32, BitVector 32)     -- ^ (Rs1Data, Rs2Data)
regBank :: Signal dom (Unsigned 5)
-> Signal dom (Unsigned 5)
-> Signal dom (Maybe (Unsigned 5, BitVector 32))
-> Unbundled dom (BitVector 32, BitVector 32)
regBank Signal dom (Unsigned 5)
rs1Addr Signal dom (Unsigned 5)
rs2Addr Signal dom (Maybe (Unsigned 5, BitVector 32))
rdWrM = (Signal dom (Unsigned 5) -> Signal dom (BitVector 32)
regFile Signal dom (Unsigned 5)
rs1Addr, Signal dom (Unsigned 5) -> Signal dom (BitVector 32)
regFile Signal dom (Unsigned 5)
rs2Addr)
  where
    regFile :: Signal dom (Unsigned 5) -> Signal dom (BitVector 32)
regFile = (Signal dom (Unsigned 5)
 -> Signal dom (Maybe (Unsigned 5, BitVector 32))
 -> Signal dom (BitVector 32))
-> Signal dom (Maybe (Unsigned 5, BitVector 32))
-> Signal dom (Unsigned 5)
-> Signal dom (BitVector 32)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Signal dom (Unsigned 5)
 -> Signal dom (Maybe (Unsigned 5, BitVector 32))
 -> Signal dom (BitVector 32))
-> Signal dom (Unsigned 5)
-> Signal dom (Maybe (Unsigned 5, BitVector 32))
-> Signal dom (BitVector 32)
forall (dom :: Domain) a addr.
(HiddenClockResetEnable dom, NFDataX a, Eq addr) =>
(Signal dom addr -> Signal dom (Maybe (addr, a)) -> Signal dom a)
-> Signal dom addr -> Signal dom (Maybe (addr, a)) -> Signal dom a
readNew (Vec (2 ^ 5) (BitVector 32)
-> Signal dom (Unsigned 5)
-> Signal dom (Maybe (Unsigned 5, BitVector 32))
-> Signal dom (BitVector 32)
forall (dom :: Domain) a (n :: Nat).
(HasCallStack, HiddenClock dom, HiddenEnable dom, NFDataX a,
 KnownNat n) =>
Vec (2 ^ n) a
-> Signal dom (Unsigned n)
-> Signal dom (Maybe (Unsigned n, a))
-> Signal dom a
blockRamPow2 (BitVector 32 -> Vec 32 (BitVector 32)
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat BitVector 32
0))) Signal dom (Maybe (Unsigned 5, BitVector 32))
rdWrM