RiscV-Formal/hs/RegFiles.hs
2025-03-10 17:46:06 -04:00

99 lines
4.4 KiB
Haskell

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
-- | This module defines the register files used in a RISC-V core, including:
-- General Purpose Registers (GPR), Floating Point Registers (FPR), and Control & Status Registers (CSR).
--
-- In RISC-V, besides the GPR, FPR, and CSR, we may also encounter
-- the following which are not modeled in this codebase:
-- * VRF (Vector Registers File) for vector processing.
-- * Debug Registers (DBR) for hardware debugging.
-- * Shadow Registers for fast context switching (optional).
-- * MPU Registers for memory protection.
-- * Counter/Timer Registers for time/cycle counting.
-- * Hypervisor Registers (HPR) for guest virtualization.
module RegFiles(
RegFileIdx,
RegVal(..),
GPR,
FPR,
CSR,
gprInit,
fprInit,
csrInit
) where
import Clash.Prelude
import Util((|>))
import Types(DoubleWord)
type RegFileIdx = Unsigned 5
data RegVal = Value {
regFileIdx :: RegFileIdx,
regVal :: DoubleWord
}
| Unpopulated {regFileIdx :: RegFileIdx}
deriving (Generic, Show, Eq, NFDataX)
type GPR = Vec 32 (Unsigned 64) -- General Purpose Registers
type FPR = Vec 32 (Unsigned 64) -- Floating Point Registers
type CSR = Vec 4096 (Unsigned 64) -- Control and Status Registers
gprInit :: GPR
gprInit = repeat 0
fprInit :: FPR
fprInit = repeat 0
-- | The 'CSRName' data type enumerates a subset of RISC-V CSRs (Control and Status Registers)
-- that are modeled in this codebase. Each variant represents a particular CSR.
data CSRName =
STVEC -- ^ Supervisor Trap-Vector Base Address: Base address for supervisor mode exception handlers.
| SEPC -- ^ Supervisor Exception Program Counter: Holds the return address for supervisor mode exceptions.
| MSTATUS -- ^ Machine Status Register: Contains global machine status flags and control bits.
| MISA -- ^ Machine ISA Register: Indicates the supported ISA extensions and width.
| MTVEC -- ^ Machine Trap-Vector Base Address: Base address for machine mode exception handlers.
| MEPC -- ^ Machine Exception Program Counter: Holds the return address for machine mode exceptions.
| MVENDORID -- ^ Machine Vendor ID: Identifies the vendor of the processor.
| MARCHID -- ^ Machine Architecture ID: Identifies the architecture of the processor.
| MIMPID -- ^ Machine Implementation ID: Identifies the implementation of the processor.
deriving (Generic, Show, Eq, NFDataX)
-- | Map each 'CSRName' variant to its corresponding CSR address.
csrNameToAddr :: CSRName -> Integer
csrNameToAddr STVEC = 0x105 -- Address for Supervisor Trap-Vector
csrNameToAddr SEPC = 0x141 -- Address for Supervisor Exception PC
csrNameToAddr MSTATUS = 0x300
csrNameToAddr MISA = 0x301
csrNameToAddr MTVEC = 0x305
csrNameToAddr MEPC = 0x341 -- Address for Machine Exception PC
csrNameToAddr MVENDORID = 0xF11
csrNameToAddr MARCHID = 0xF12
csrNameToAddr MIMPID = 0xF13
-- | Initial CSR values.
-- Note: The CSR registers are not all zero during proper initialization; these values
-- are placeholders to be revisited for proper initialization later.
csrInit :: CSR
csrInit =
replace (csrNameToAddr STVEC) stvec_init |>
replace (csrNameToAddr SEPC) sepc_init |>
replace (csrNameToAddr MSTATUS) mstatus_init |>
replace (csrNameToAddr MISA) misa_init |>
replace (csrNameToAddr MTVEC) mtvec_init |>
replace (csrNameToAddr MEPC) mepc_init |>
replace (csrNameToAddr MVENDORID) mvendorid_init |>
replace (csrNameToAddr MARCHID) marchid_init |>
replace (csrNameToAddr MIMPID) mimpid_init |>
repeat 0
where
stvec_init = 0x0000000000002000 -- Supervisor mode trap vector base address.
sepc_init = 0x0000000000000000 -- Supervisor Exception PC initial value.
mstatus_init = 0x0000000000001800 -- Default machine status.
misa_init = 0x8000000000001104 -- RV64IMAFD: Machine ISA with standard extensions.
mtvec_init = 0x0000000000001000 -- Machine mode trap vector base address.
mepc_init = 0x0000000000000000 -- Machine Exception PC initial value.
mvendorid_init = 0x00000000 -- Vendor-specific ID.
marchid_init = 0x00000000 -- Architecture-specific ID.
mimpid_init = 0x00000000 -- Implementation-specific ID.