{-|
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](https://riscv.org/about/) 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
  , defaultCoreConfig
  , P.defaultPipeConfig
  , CoreConfig(..)
  , AluConfig(..)
  , P.PipeConfig(..)
  , FromCore(..)
  , P.ToMem(..)
  , P.MemoryAccess(..)
  , Alu
  ) where

import Clash.Prelude
import Data.Proxy
import Data.Maybe
import Data.Monoid
import Lion.Alu
import Lion.Rvfi
import qualified Lion.Pipe as P
import qualified Lion.Instruction as I (Op(Add))

-- | Core configuration
--
-- ALU configuration default: `Soft`
newtype CoreConfig (startPC :: Nat) (a :: AluConfig) = CoreConfig
  { CoreConfig startPC a -> PipeConfig startPC
pipeConfig :: P.PipeConfig (startPC :: Nat) -- ^ pipeline configuration
  }
  deriving stock ((forall x. CoreConfig startPC a -> Rep (CoreConfig startPC a) x)
-> (forall x. Rep (CoreConfig startPC a) x -> CoreConfig startPC a)
-> Generic (CoreConfig startPC a)
forall x. Rep (CoreConfig startPC a) x -> CoreConfig startPC a
forall x. CoreConfig startPC a -> Rep (CoreConfig startPC a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (startPC :: Nat) (a :: AluConfig) x.
Rep (CoreConfig startPC a) x -> CoreConfig startPC a
forall (startPC :: Nat) (a :: AluConfig) x.
CoreConfig startPC a -> Rep (CoreConfig startPC a) x
$cto :: forall (startPC :: Nat) (a :: AluConfig) x.
Rep (CoreConfig startPC a) x -> CoreConfig startPC a
$cfrom :: forall (startPC :: Nat) (a :: AluConfig) x.
CoreConfig startPC a -> Rep (CoreConfig startPC a) x
Generic, Int -> CoreConfig startPC a -> ShowS
[CoreConfig startPC a] -> ShowS
CoreConfig startPC a -> String
(Int -> CoreConfig startPC a -> ShowS)
-> (CoreConfig startPC a -> String)
-> ([CoreConfig startPC a] -> ShowS)
-> Show (CoreConfig startPC a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (startPC :: Nat) (a :: AluConfig).
Int -> CoreConfig startPC a -> ShowS
forall (startPC :: Nat) (a :: AluConfig).
[CoreConfig startPC a] -> ShowS
forall (startPC :: Nat) (a :: AluConfig).
CoreConfig startPC a -> String
showList :: [CoreConfig startPC a] -> ShowS
$cshowList :: forall (startPC :: Nat) (a :: AluConfig).
[CoreConfig startPC a] -> ShowS
show :: CoreConfig startPC a -> String
$cshow :: forall (startPC :: Nat) (a :: AluConfig).
CoreConfig startPC a -> String
showsPrec :: Int -> CoreConfig startPC a -> ShowS
$cshowsPrec :: forall (startPC :: Nat) (a :: AluConfig).
Int -> CoreConfig startPC a -> ShowS
Show, CoreConfig startPC a -> CoreConfig startPC a -> Bool
(CoreConfig startPC a -> CoreConfig startPC a -> Bool)
-> (CoreConfig startPC a -> CoreConfig startPC a -> Bool)
-> Eq (CoreConfig startPC a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (startPC :: Nat) (a :: AluConfig).
CoreConfig startPC a -> CoreConfig startPC a -> Bool
/= :: CoreConfig startPC a -> CoreConfig startPC a -> Bool
$c/= :: forall (startPC :: Nat) (a :: AluConfig).
CoreConfig startPC a -> CoreConfig startPC a -> Bool
== :: CoreConfig startPC a -> CoreConfig startPC a -> Bool
$c== :: forall (startPC :: Nat) (a :: AluConfig).
CoreConfig startPC a -> CoreConfig startPC a -> Bool
Eq)

-- | Default core configuration
--
-- ALU configuration = `Soft`
--
-- `pipeConfig` = `defaultPipeConfig`
defaultCoreConfig :: CoreConfig 0 'Soft
defaultCoreConfig :: CoreConfig 0 'Soft
defaultCoreConfig = CoreConfig :: forall (startPC :: Nat) (a :: AluConfig).
PipeConfig startPC -> CoreConfig startPC a
CoreConfig
  { pipeConfig :: PipeConfig 0
pipeConfig = PipeConfig 0
P.defaultPipeConfig
  }

-- | 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
  }

-- | RISC-V Core: RV32I
core
  :: forall a startPC dom
   . HiddenClockResetEnable dom
  => Alu a
  => (KnownNat startPC, startPC <= 0xFFFFFFFF)
  => CoreConfig (startPC :: Nat) (a :: AluConfig) -- ^ core configuration
  -> Signal dom (BitVector 32)   -- ^ core input, from memory/peripherals
  -> FromCore dom                -- ^ core output
core :: CoreConfig startPC a -> Signal dom (BitVector 32) -> FromCore dom
core CoreConfig startPC a
config 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
    -- alu connection
    aluOp :: Signal dom Op
aluOp = Op -> Maybe Op -> Op
forall a. a -> Maybe a -> a
fromMaybe Op
I.Add (Maybe Op -> Op) -> (FromPipe -> Maybe Op) -> FromPipe -> Op
forall b c a. (b -> c) -> (a -> b) -> a -> c
. First Op -> Maybe Op
forall a. First a -> Maybe a
getFirst (First Op -> Maybe Op)
-> (FromPipe -> First Op) -> FromPipe -> Maybe Op
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FromPipe -> First Op
P._toAluOp     (FromPipe -> Op) -> Signal dom FromPipe -> Signal dom Op
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom FromPipe
fromPipe
    aluInput1 :: Signal dom (BitVector 32)
aluInput1 = BitVector 32 -> Maybe (BitVector 32) -> BitVector 32
forall a. a -> Maybe a -> a
fromMaybe BitVector 32
0 (Maybe (BitVector 32) -> BitVector 32)
-> (FromPipe -> Maybe (BitVector 32)) -> FromPipe -> BitVector 32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. First (BitVector 32) -> Maybe (BitVector 32)
forall a. First a -> Maybe a
getFirst (First (BitVector 32) -> Maybe (BitVector 32))
-> (FromPipe -> First (BitVector 32))
-> FromPipe
-> Maybe (BitVector 32)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FromPipe -> First (BitVector 32)
P._toAluInput1 (FromPipe -> BitVector 32)
-> Signal dom FromPipe -> Signal dom (BitVector 32)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom FromPipe
fromPipe
    aluInput2 :: Signal dom (BitVector 32)
aluInput2 = BitVector 32 -> Maybe (BitVector 32) -> BitVector 32
forall a. a -> Maybe a -> a
fromMaybe BitVector 32
0 (Maybe (BitVector 32) -> BitVector 32)
-> (FromPipe -> Maybe (BitVector 32)) -> FromPipe -> BitVector 32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. First (BitVector 32) -> Maybe (BitVector 32)
forall a. First a -> Maybe a
getFirst (First (BitVector 32) -> Maybe (BitVector 32))
-> (FromPipe -> First (BitVector 32))
-> FromPipe
-> Maybe (BitVector 32)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FromPipe -> First (BitVector 32)
P._toAluInput2 (FromPipe -> BitVector 32)
-> Signal dom FromPipe -> Signal dom (BitVector 32)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom FromPipe
fromPipe
    aluOutput :: Signal dom (BitVector 32)
aluOutput = Proxy a
-> Signal dom Op
-> Signal dom (BitVector 32)
-> Signal dom (BitVector 32)
-> Signal dom (BitVector 32)
forall (config :: AluConfig) (dom :: Domain).
(Alu config, HiddenClockResetEnable dom) =>
Proxy config
-> Signal dom Op
-> Signal dom (BitVector 32)
-> Signal dom (BitVector 32)
-> Signal dom (BitVector 32)
alu (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Signal dom Op
aluOp Signal dom (BitVector 32)
aluInput1 Signal dom (BitVector 32)
aluInput2
    -- reg bank connection
    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

    -- pipeline connection
    fromPipe :: Signal dom FromPipe
fromPipe = PipeConfig startPC -> Signal dom ToPipe -> Signal dom FromPipe
forall (dom :: Domain) (startPC :: Nat).
(HiddenClockResetEnable dom, KnownNat startPC,
 startPC <= 4294967295) =>
PipeConfig startPC -> Signal dom ToPipe -> Signal dom FromPipe
P.pipe (CoreConfig startPC a -> PipeConfig startPC
forall (startPC :: Nat) (a :: AluConfig).
CoreConfig startPC a -> PipeConfig startPC
pipeConfig CoreConfig startPC a
config) (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 -> BitVector 32 -> ToPipe
P.ToPipe (BitVector 32
 -> BitVector 32 -> BitVector 32 -> BitVector 32 -> ToPipe)
-> Signal dom (BitVector 32)
-> Signal
     dom (BitVector 32 -> 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 -> BitVector 32 -> ToPipe)
-> Signal dom (BitVector 32)
-> Signal dom (BitVector 32 -> 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 -> 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)
aluOutput
                                                     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

-- | 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