-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | RISC-V Core
--   
--   Lion is a formally verified, 5-stage pipeline <a>RISC-V</a> core. Lion
--   targets the <a>VELDT FPGA development board</a> and is written in
--   Haskell using <a>Clash</a>.
@package lion
@version 0.4.0.0


-- | As the pipeline processes instructions, it populates the fields of the
--   Rvfi data. When the instruction reaches the end of the pipeline, the
--   core retires the instruction and writes the Rvfi data to output. This
--   output is inspected and verified by the riscv-formal framework. See
--   <a>riscv-formal</a> for more information about the interface. To
--   verify the Lion core, see <a>lion-formal</a>.
module Lion.Rvfi

-- | RISC-V Formal Csr Interface
data RvfiCsr n
RvfiCsr :: ("wdata" ::: BitVector n) -> ("rdata" ::: BitVector n) -> ("wmask" ::: BitVector n) -> ("rmask" ::: BitVector n) -> RvfiCsr n
[_wdataCsr] :: RvfiCsr n -> "wdata" ::: BitVector n
[_rdataCsr] :: RvfiCsr n -> "rdata" ::: BitVector n
[_wmaskCsr] :: RvfiCsr n -> "wmask" ::: BitVector n
[_rmaskCsr] :: RvfiCsr n -> "rmask" ::: BitVector n
wmaskCsr :: forall n_aGXz. Lens' (RvfiCsr n_aGXz) ((:::) "wmask" (BitVector n_aGXz))
wdataCsr :: forall n_aGXz. Lens' (RvfiCsr n_aGXz) ((:::) "wdata" (BitVector n_aGXz))
rmaskCsr :: forall n_aGXz. Lens' (RvfiCsr n_aGXz) ((:::) "rmask" (BitVector n_aGXz))
rdataCsr :: forall n_aGXz. Lens' (RvfiCsr n_aGXz) ((:::) "rdata" (BitVector n_aGXz))

-- | RISC-V Formal Interface
data Rvfi
Rvfi :: ("valid" ::: Bool) -> ("order" ::: BitVector 64) -> ("insn" ::: BitVector 32) -> ("trap" ::: Bool) -> ("halt" ::: Bool) -> ("intr" ::: Bool) -> ("mode" ::: BitVector 2) -> ("ixl" ::: BitVector 2) -> ("rs1_addr" ::: Unsigned 5) -> ("rs2_addr" ::: Unsigned 5) -> ("rs1_rdata" ::: BitVector 32) -> ("rs2_rdata" ::: BitVector 32) -> ("rd_addr" ::: Unsigned 5) -> ("rd_wdata" ::: BitVector 32) -> ("pc_rdata" ::: BitVector 32) -> ("pc_wdata" ::: BitVector 32) -> ("mem_addr" ::: BitVector 32) -> ("mem_rmask" ::: BitVector 4) -> ("mem_wmask" ::: BitVector 4) -> ("mem_rdata" ::: BitVector 32) -> ("mem_wdata" ::: BitVector 32) -> ("csr_minstret" ::: RvfiCsr 64) -> ("csr_mcycle" ::: RvfiCsr 64) -> ("csr_mscratch" ::: RvfiCsr 32) -> ("csr_mstatus" ::: RvfiCsr 32) -> ("csr_misa" ::: RvfiCsr 32) -> Rvfi

-- | When the core retires an instruction, it asserts the <a>rvfiValid</a>
--   signal and uses the signals described in Rvfi to output the details of
--   the retired instruction. The signals below are only valid during such
--   a cycle and can be driven to arbitrary values in a cycle in which
--   `_rvfiValid is not asserted.
[_rvfiValid] :: Rvfi -> "valid" ::: Bool

-- | The <a>rvfiOrder</a> field must be set to the instruction index. No
--   indices must be used twice and there must be no gaps. Instructions may
--   be retired in a reordered fashion, as long as causality is preserved
--   (register nad memory write operations must be retired before the read
--   operations that depend on them).
[_rvfiOrder] :: Rvfi -> "order" ::: BitVector 64

-- | <a>rvfiInsn</a> is the instruction word for the retired instruction.
--   In case of an instruction with fewer than ILEN bits, the upper bits of
--   this output must all be zero. For compressed instructions the
--   compressed instruction word must be output on this port. For fused
--   instructions the complete fused instruciton sequence must be output
[_rvfiInsn] :: Rvfi -> "insn" ::: BitVector 32

-- | <a>rvfiTrap</a> must be set for an instruction that cannot be decoded
--   as a legal instruction, such as 0x00000000.
[_rvfiTrap] :: Rvfi -> "trap" ::: Bool

-- | The signal <a>rvfiHalt</a> must be set when the instruction is the
--   last instruction that the core retires before halting execution. It
--   should not be set for an instruction that triggers a trap condition if
--   the CPU reacts to the trap by executing a trap handler. This signal
--   enable verification of liveness properties.
[_rvfiHalt] :: Rvfi -> "halt" ::: Bool

-- | <a>rvfiIntr</a> must be set for the first instruction that is part of
--   a trap handler, i.e. an instruction that has a <a>rvfiPcRData</a> that
--   does not match the <a>rvfiPcWData</a> of the previous instruction.
[_rvfiIntr] :: Rvfi -> "intr" ::: Bool

-- | <a>rvfiMode</a> must be set to the current privilege level, using the
--   following encoding: 0=U-Mode, 1=S-Mode, 2=Reserved, 3=M-Mode
[_rvfiMode] :: Rvfi -> "mode" ::: BitVector 2

-- | <a>rvfiIxl</a> must be set to the value of MXL<i>SXL</i>UXL in the
--   current privilege level, using the following encoding: 1=32, 2=64
[_rvfiIxl] :: Rvfi -> "ixl" ::: BitVector 2

-- | <a>rvfiRs1Addr</a> and <a>rvfiRs2Addr</a> are the decoded rs1 and rs2
--   register addresses for the retired instruction. For an instruction
--   that reads no rs1/rs2 register, this output can have an arbitrary
--   value. However if this output is nonzero then <a>rvfiRs1Data</a> or
--   <a>rvfiRs2Data</a> must carry the value stored in that register in the
--   pre-state.
[_rvfiRs1Addr] :: Rvfi -> "rs1_addr" ::: Unsigned 5
[_rvfiRs2Addr] :: Rvfi -> "rs2_addr" ::: Unsigned 5

-- | <a>rvfiRs1Data</a> and <a>rvfiRs2Data</a> are the values of the
--   register addressed by rs1 and rs2 before execute of this instruction.
--   This output must be zero when rs1/rs2 is zero.
[_rvfiRs1Data] :: Rvfi -> "rs1_rdata" ::: BitVector 32
[_rvfiRs2Data] :: Rvfi -> "rs2_rdata" ::: BitVector 32

-- | <a>rvfiRdAddr</a> is the decoded rd register address for the retired
--   instruction. For an instruction that writes no rd register, this
--   output must always be zero.
[_rvfiRdAddr] :: Rvfi -> "rd_addr" ::: Unsigned 5

-- | <a>rvfiRdWData</a> is the value of the register addressed by rd after
--   execution of this instruction. This output must be zero when rd is
--   zero.
[_rvfiRdWData] :: Rvfi -> "rd_wdata" ::: BitVector 32

-- | This is the program counter (pc) before (<a>rvfiPcRData</a>) and after
--   (<a>rvfiPcWData</a>) execution of this instruciton. I.e. this is the
--   address of the retired instruction and the address of the next
--   instruction.
[_rvfiPcRData] :: Rvfi -> "pc_rdata" ::: BitVector 32
[_rvfiPcWData] :: Rvfi -> "pc_wdata" ::: BitVector 32

-- | For memory operations (<a>rvfiMemRMask</a> and/or <a>rvfiMemWMask</a>
--   are non-zero), <a>rvfiMemAddr</a> holds the accessed memory location.
[_rvfiMemAddr] :: Rvfi -> "mem_addr" ::: BitVector 32

-- | <a>rvfiMemRMask</a> is a bitmask that specifies which bytes in
--   <a>rvfiMemRData</a> contain valid read data from <a>rvfiMemAddr</a>.
[_rvfiMemRMask] :: Rvfi -> "mem_rmask" ::: BitVector 4

-- | <a>rvfiMemWMask</a> is a bitmask that specifies which bytes in
--   <a>rvfiMemWData</a> contain valid data this is written to
--   <a>rvfiMemAddr</a>.
[_rvfiMemWMask] :: Rvfi -> "mem_wmask" ::: BitVector 4

-- | <a>rvfiMemRData</a> is the pre-state data read from
--   <a>rvfiMemAddr</a>. <a>rvfiMemRMask</a> specifies which bytes are
--   valid.
[_rvfiMemRData] :: Rvfi -> "mem_rdata" ::: BitVector 32

-- | <a>rvfiMemWData</a> is the post-state data written to
--   <a>rvfiMemAddr</a>. <a>rvfiMemWMask</a> specifies which bytes are
--   valid.
[_rvfiMemWData] :: Rvfi -> "mem_wdata" ::: BitVector 32
[_rvfiCsrMinstret] :: Rvfi -> "csr_minstret" ::: RvfiCsr 64
[_rvfiCsrMcycle] :: Rvfi -> "csr_mcycle" ::: RvfiCsr 64
[_rvfiCsrMscratch] :: Rvfi -> "csr_mscratch" ::: RvfiCsr 32
[_rvfiCsrMstatus] :: Rvfi -> "csr_mstatus" ::: RvfiCsr 32
[_rvfiCsrMisa] :: Rvfi -> "csr_misa" ::: RvfiCsr 32
rvfiValid :: Lens' Rvfi ((:::) "valid" Bool)
rvfiTrap :: Lens' Rvfi ((:::) "trap" Bool)
rvfiRs2Data :: Lens' Rvfi ((:::) "rs2_rdata" (BitVector 32))
rvfiRs2Addr :: Lens' Rvfi ((:::) "rs2_addr" (Unsigned 5))
rvfiRs1Data :: Lens' Rvfi ((:::) "rs1_rdata" (BitVector 32))
rvfiRs1Addr :: Lens' Rvfi ((:::) "rs1_addr" (Unsigned 5))
rvfiRdWData :: Lens' Rvfi ((:::) "rd_wdata" (BitVector 32))
rvfiRdAddr :: Lens' Rvfi ((:::) "rd_addr" (Unsigned 5))
rvfiPcWData :: Lens' Rvfi ((:::) "pc_wdata" (BitVector 32))
rvfiPcRData :: Lens' Rvfi ((:::) "pc_rdata" (BitVector 32))
rvfiOrder :: Lens' Rvfi ((:::) "order" (BitVector 64))
rvfiMode :: Lens' Rvfi ((:::) "mode" (BitVector 2))
rvfiMemWMask :: Lens' Rvfi ((:::) "mem_wmask" (BitVector 4))
rvfiMemWData :: Lens' Rvfi ((:::) "mem_wdata" (BitVector 32))
rvfiMemRMask :: Lens' Rvfi ((:::) "mem_rmask" (BitVector 4))
rvfiMemRData :: Lens' Rvfi ((:::) "mem_rdata" (BitVector 32))
rvfiMemAddr :: Lens' Rvfi ((:::) "mem_addr" (BitVector 32))
rvfiIxl :: Lens' Rvfi ((:::) "ixl" (BitVector 2))
rvfiIntr :: Lens' Rvfi ((:::) "intr" Bool)
rvfiInsn :: Lens' Rvfi ((:::) "insn" (BitVector 32))
rvfiHalt :: Lens' Rvfi ((:::) "halt" Bool)
rvfiCsrMstatus :: Lens' Rvfi ((:::) "csr_mstatus" (RvfiCsr 32))
rvfiCsrMscratch :: Lens' Rvfi ((:::) "csr_mscratch" (RvfiCsr 32))
rvfiCsrMisa :: Lens' Rvfi ((:::) "csr_misa" (RvfiCsr 32))
rvfiCsrMinstret :: Lens' Rvfi ((:::) "csr_minstret" (RvfiCsr 64))
rvfiCsrMcycle :: Lens' Rvfi ((:::) "csr_mcycle" (RvfiCsr 64))

-- | Unwrap Rvfi from First monoid
fromRvfi :: First Rvfi -> Rvfi

-- | Construct the RISC-V Formal Interface
mkRvfi :: Rvfi
instance Clash.XException.NFDataX Lion.Rvfi.Rvfi
instance GHC.Classes.Eq Lion.Rvfi.Rvfi
instance GHC.Show.Show Lion.Rvfi.Rvfi
instance GHC.Generics.Generic Lion.Rvfi.Rvfi
instance GHC.TypeNats.KnownNat n => Clash.XException.NFDataX (Lion.Rvfi.RvfiCsr n)
instance GHC.TypeNats.KnownNat n => GHC.Classes.Eq (Lion.Rvfi.RvfiCsr n)
instance GHC.TypeNats.KnownNat n => GHC.Show.Show (Lion.Rvfi.RvfiCsr n)
instance GHC.Generics.Generic (Lion.Rvfi.RvfiCsr n)


-- | The Lion core is a 32-bit <a>RISC-V</a> processor written in Haskell
--   using <a>Clash</a>. Note, all peripherals and memory must have single
--   cycle latency. See <a>lion-soc</a> for an example of using the Lion
--   core in a system.
module Lion.Core

-- | RISC-V Core: RV32I
core :: HiddenClockResetEnable dom => CoreConfig -> Signal dom (BitVector 32) -> FromCore dom

-- | Default core configuration
--   
--   <a>aluConfig</a> = <a>Soft</a>
--   
--   <a>pipeConfig</a> = <a>defaultPipeConfig</a>
defaultCoreConfig :: CoreConfig

-- | Default pipeline configuration
--   
--   <a>startPC</a> = 0
defaultPipeConfig :: PipeConfig

-- | Core configuration
data CoreConfig
CoreConfig :: AluConfig -> PipeConfig -> CoreConfig

-- | ALU configuration, default: <a>Soft</a>
[aluConfig] :: CoreConfig -> AluConfig

-- | pipeline configuration
[pipeConfig] :: CoreConfig -> PipeConfig

-- | ALU configuration
data AluConfig

-- | use hard adder and subtractor from iCE40 SB_MAC16
Hard :: AluConfig

-- | use generic adder and subtractor: (+) and (-)
Soft :: AluConfig

-- | Pipeline configuration
newtype PipeConfig
PipeConfig :: BitVector 32 -> PipeConfig

-- | start program counter
[startPC] :: PipeConfig -> BitVector 32

-- | Core outputs
data FromCore dom
FromCore :: Signal dom (Maybe ToMem) -> Signal dom Rvfi -> FromCore dom

-- | shared memory and instruction bus, output from core to memory and
--   peripherals
[toMem] :: FromCore dom -> Signal dom (Maybe ToMem)

-- | formal verification interface output, see <a>lion-formal</a> for usage
[toRvfi] :: FromCore dom -> Signal dom Rvfi

-- | Memory bus
data ToMem
ToMem :: MemoryAccess -> BitVector 32 -> BitVector 4 -> Maybe (BitVector 32) -> ToMem

-- | memory access type
[memAccess] :: ToMem -> MemoryAccess

-- | memory address
[memAddress] :: ToMem -> BitVector 32

-- | memory byte mask
[memByteMask] :: ToMem -> BitVector 4

-- | read=Nothing write=Just wr
[memWrite] :: ToMem -> Maybe (BitVector 32)

-- | Memory access - Lion has a shared instruction/memory bus
data MemoryAccess

-- | instruction access
InstrMem :: MemoryAccess

-- | data access
DataMem :: MemoryAccess
instance GHC.Classes.Eq Lion.Core.CoreConfig
instance GHC.Show.Show Lion.Core.CoreConfig
instance GHC.Generics.Generic Lion.Core.CoreConfig