forked from Yehowshua/RiscV-Formal
initial support for exceptions
This commit is contained in:
parent
5552ad3d4a
commit
88ec010f98
|
@ -12,7 +12,7 @@ import Data.Maybe (listToMaybe)
|
||||||
import Data.List (isPrefixOf)
|
import Data.List (isPrefixOf)
|
||||||
import Text.Show.Pretty (ppShow)
|
import Text.Show.Pretty (ppShow)
|
||||||
|
|
||||||
import Simulation (simulation, Args(..), Simulation(..))
|
import Simulation (simulation, Args(..), Simulation(..), RISCVCPU(..), Machine(..))
|
||||||
|
|
||||||
main :: IO ()
|
main :: IO ()
|
||||||
main = do
|
main = do
|
||||||
|
@ -23,7 +23,7 @@ main = do
|
||||||
case simResult of
|
case simResult of
|
||||||
Success states -> do
|
Success states -> do
|
||||||
-- mapM_ (putStrLn . ppShow) states -- Uncomment to print each state, if needed.
|
-- mapM_ (putStrLn . ppShow) states -- Uncomment to print each state, if needed.
|
||||||
putStrLn $ "Last state: " ++ show (last states)
|
putStrLn $ "GPR last state: " ++ (show $ gpr $ cpu $ last states)
|
||||||
putStrLn $ "Executed for " ++ show (length states) ++ " cycles"
|
putStrLn $ "Executed for " ++ show (length states) ++ " cycles"
|
||||||
putStrLn "Simulation complete"
|
putStrLn "Simulation complete"
|
||||||
Failure err -> do
|
Failure err -> do
|
||||||
|
|
|
@ -16,7 +16,6 @@ import BusTypes(
|
||||||
BusError(..),
|
BusError(..),
|
||||||
TransactionSize(..),
|
TransactionSize(..),
|
||||||
ReadRequest(..),
|
ReadRequest(..),
|
||||||
BusResponse(..),
|
|
||||||
BusVal(..),
|
BusVal(..),
|
||||||
)
|
)
|
||||||
import Types(Addr,
|
import Types(Addr,
|
||||||
|
|
|
@ -3,7 +3,6 @@ module BusTypes(
|
||||||
BusError(..),
|
BusError(..),
|
||||||
TransactionSize(..),
|
TransactionSize(..),
|
||||||
ReadRequest(..),
|
ReadRequest(..),
|
||||||
BusResponse(..),
|
|
||||||
BusVal(..),
|
BusVal(..),
|
||||||
) where
|
) where
|
||||||
|
|
||||||
|
@ -28,11 +27,6 @@ data TransactionSize
|
||||||
data ReadRequest = Request Addr TransactionSize
|
data ReadRequest = Request Addr TransactionSize
|
||||||
deriving (Generic, Show, Eq, NFDataX)
|
deriving (Generic, Show, Eq, NFDataX)
|
||||||
|
|
||||||
data BusResponse a
|
|
||||||
= Result a
|
|
||||||
| Error BusError
|
|
||||||
deriving (Generic, Show, Eq, NFDataX)
|
|
||||||
|
|
||||||
data BusVal
|
data BusVal
|
||||||
= BusByte Byte
|
= BusByte Byte
|
||||||
| BusHalfWord HalfWord
|
| BusHalfWord HalfWord
|
||||||
|
|
|
@ -24,6 +24,7 @@ data RISCVCPU = RISCVCPU
|
||||||
{ pc :: Pc,
|
{ pc :: Pc,
|
||||||
gpr :: GPR,
|
gpr :: GPR,
|
||||||
fpr :: FPR,
|
fpr :: FPR,
|
||||||
|
csr :: CSR,
|
||||||
privilegeLevel :: PrivilegeLevel
|
privilegeLevel :: PrivilegeLevel
|
||||||
}
|
}
|
||||||
deriving (Generic, Show, Eq, NFDataX)
|
deriving (Generic, Show, Eq, NFDataX)
|
||||||
|
@ -34,4 +35,5 @@ riscvCPUInit =
|
||||||
0
|
0
|
||||||
gprInit
|
gprInit
|
||||||
fprInit
|
fprInit
|
||||||
|
csrInit
|
||||||
MachineMode
|
MachineMode
|
||||||
|
|
34
hs/Exceptions.hs
Normal file
34
hs/Exceptions.hs
Normal file
|
@ -0,0 +1,34 @@
|
||||||
|
{-# LANGUAGE DataKinds #-}
|
||||||
|
{-# LANGUAGE NumericUnderscores #-}
|
||||||
|
|
||||||
|
module Exceptions() where
|
||||||
|
|
||||||
|
import Clash.Prelude
|
||||||
|
|
||||||
|
data Exception =
|
||||||
|
SupervisorSoftwareInterrupt
|
||||||
|
| MachineSoftwareInterrupt
|
||||||
|
| SupervisorTimerInterrupt
|
||||||
|
| MachineTimerInterrupt
|
||||||
|
| SupervisorExternalInterrupt
|
||||||
|
| MachineExternalInterrupt
|
||||||
|
| CounterOverflowInterrupt
|
||||||
|
| InstructionAddressMisaligned
|
||||||
|
| InstructionAccessFault
|
||||||
|
| IllegalInstruction
|
||||||
|
| Breakpoint
|
||||||
|
| LoadAddressMisaligned
|
||||||
|
| LoadAccessFault
|
||||||
|
| StoreAMOAddressMisaligned
|
||||||
|
| StoreAMOAccessFault
|
||||||
|
| EnvironmentCallFromUMode
|
||||||
|
| EnvironmentCallFromSMode
|
||||||
|
| EnvironmentCallFromMMode
|
||||||
|
| InstructionPageFault
|
||||||
|
| LoadPageFault
|
||||||
|
| Reserved
|
||||||
|
| StoreAMOPageFault
|
||||||
|
| DoubleTrap
|
||||||
|
| SoftwareCheck
|
||||||
|
| HardwareError
|
||||||
|
deriving (Generic, Show, Eq, NFDataX)
|
|
@ -14,6 +14,11 @@ import Clash.Prelude
|
||||||
import Types(Mem, Addr, Insn)
|
import Types(Mem, Addr, Insn)
|
||||||
import Util(endianSwapWord)
|
import Util(endianSwapWord)
|
||||||
import Bus(ReadResponse, WriteResponse, read)
|
import Bus(ReadResponse, WriteResponse, read)
|
||||||
|
import Bus(Peripherals(..))
|
||||||
|
import BusTypes(ReadRequest(..), TransactionSize(..))
|
||||||
|
|
||||||
|
import GHC.IO (IO)
|
||||||
|
import GHC.Base (Applicative(pure))
|
||||||
|
|
||||||
data FetchResult = Instruction Insn
|
data FetchResult = Instruction Insn
|
||||||
| Misaligned Addr
|
| Misaligned Addr
|
||||||
|
@ -30,3 +35,7 @@ fetchInstruction mem addr =
|
||||||
case isWordAligned of
|
case isWordAligned of
|
||||||
True -> Instruction insn
|
True -> Instruction insn
|
||||||
False -> Misaligned addr
|
False -> Misaligned addr
|
||||||
|
|
||||||
|
fetchInstruction1 :: Peripherals -> Addr -> IO ReadResponse
|
||||||
|
fetchInstruction1 peripherals addr =
|
||||||
|
read (BusTypes.Request addr BusTypes.SizeFullWord) peripherals
|
||||||
|
|
|
@ -1,6 +1,17 @@
|
||||||
{-# LANGUAGE DataKinds #-}
|
{-# LANGUAGE DataKinds #-}
|
||||||
{-# LANGUAGE NumericUnderscores #-}
|
{-# 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(
|
module RegFiles(
|
||||||
GPR,
|
GPR,
|
||||||
FPR,
|
FPR,
|
||||||
|
@ -12,18 +23,9 @@ module RegFiles(
|
||||||
|
|
||||||
import Clash.Prelude
|
import Clash.Prelude
|
||||||
|
|
||||||
-- In RISC-V, besides the GPR, FPR, and CSR, we may also encounter
|
type GPR = Vec 32 (Unsigned 64) -- General Purpose Registers
|
||||||
-- the following which are not modeled in this codebase.
|
type FPR = Vec 32 (Unsigned 64) -- Floating Point Registers
|
||||||
-- * VRF(Vector Registers File) for vector processing.
|
type CSR = Vec 4096 (Unsigned 64) -- Control and Status Registers
|
||||||
-- * 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.
|
|
||||||
|
|
||||||
type GPR = Vec 32 (Unsigned 64)
|
|
||||||
type FPR = Vec 32 (Unsigned 64)
|
|
||||||
type CSR = Vec 4096 (Unsigned 64)
|
|
||||||
|
|
||||||
gprInit :: GPR
|
gprInit :: GPR
|
||||||
gprInit = repeat 0
|
gprInit = repeat 0
|
||||||
|
@ -31,26 +33,54 @@ gprInit = repeat 0
|
||||||
fprInit :: FPR
|
fprInit :: FPR
|
||||||
fprInit = repeat 0
|
fprInit = repeat 0
|
||||||
|
|
||||||
-- TODO: CSR can't actually be all 0 during initialization.
|
-- | The 'CSRName' data type enumerates a subset of RISC-V CSRs (Control and Status Registers)
|
||||||
-- We need to revisit the following and properly initialize
|
-- that are modeled in this codebase. Each variant represents a particular CSR.
|
||||||
-- various registers later.
|
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 :: CSR
|
||||||
csrInit =
|
csrInit =
|
||||||
replace (0x301 :: Integer) misa_init
|
replace (csrNameToAddr STVEC) stvec_init
|
||||||
$ replace (0x300 :: Integer) mstatus_init
|
$ replace (csrNameToAddr SEPC) sepc_init
|
||||||
$ replace (0x305 :: Integer) mtvec_init
|
$ replace (csrNameToAddr MSTATUS) mstatus_init
|
||||||
$ replace (0xF11 :: Integer) mvendorid_init
|
$ replace (csrNameToAddr MISA) misa_init
|
||||||
$ replace (0xF12 :: Integer) marchid_init
|
$ replace (csrNameToAddr MTVEC) mtvec_init
|
||||||
$ replace (0xF13 :: Integer) mimpid_init
|
$ replace (csrNameToAddr MEPC) mepc_init
|
||||||
$ replace (0x701 :: Integer) mtime_init
|
$ replace (csrNameToAddr MVENDORID) mvendorid_init
|
||||||
$ replace (0x321 :: Integer) mtimecmp_init
|
$ replace (csrNameToAddr MARCHID) marchid_init
|
||||||
|
$ replace (csrNameToAddr MIMPID) mimpid_init
|
||||||
$ repeat 0
|
$ repeat 0
|
||||||
where
|
where
|
||||||
misa_init = 0x8000000000001104 -- `RV64IMAFD`
|
stvec_init = 0x0000000000002000 -- Supervisor mode trap vector base address.
|
||||||
mstatus_init = 0x0000000000001800 -- Default `mstatus`
|
sepc_init = 0x0000000000000000 -- Supervisor Exception PC initial value.
|
||||||
mtvec_init = 0x0000000000001000 -- Trap vector base
|
mstatus_init = 0x0000000000001800 -- Default machine status.
|
||||||
mvendorid_init = 0x00000000
|
misa_init = 0x8000000000001104 -- RV64IMAFD: Machine ISA with standard extensions.
|
||||||
marchid_init = 0x00000000
|
mtvec_init = 0x0000000000001000 -- Machine mode trap vector base address.
|
||||||
mimpid_init = 0x00000000
|
mepc_init = 0x0000000000000000 -- Machine Exception PC initial value.
|
||||||
mtime_init = 0x0000000000000000
|
mvendorid_init = 0x00000000 -- Vendor-specific ID.
|
||||||
mtimecmp_init = 0xFFFFFFFFFFFFFFFF
|
marchid_init = 0x00000000 -- Architecture-specific ID.
|
||||||
|
mimpid_init = 0x00000000 -- Implementation-specific ID.
|
||||||
|
|
|
@ -3,7 +3,13 @@
|
||||||
{-# LANGUAGE TypeOperators #-}
|
{-# LANGUAGE TypeOperators #-}
|
||||||
{-# LANGUAGE ConstraintKinds #-}
|
{-# LANGUAGE ConstraintKinds #-}
|
||||||
|
|
||||||
module Simulation(Args(..), simulation, Simulation(..)) where
|
module Simulation(
|
||||||
|
Args(..),
|
||||||
|
simulation,
|
||||||
|
RISCVCPU(..),
|
||||||
|
Machine(..),
|
||||||
|
Simulation(..)
|
||||||
|
) where
|
||||||
|
|
||||||
import qualified Prelude as P
|
import qualified Prelude as P
|
||||||
import Peripherals.Setup(setupPeripherals, InitializedPeripherals(..))
|
import Peripherals.Setup(setupPeripherals, InitializedPeripherals(..))
|
||||||
|
@ -12,7 +18,6 @@ import Clash.Prelude
|
||||||
import Bus(Peripherals(..))
|
import Bus(Peripherals(..))
|
||||||
import Cpu(
|
import Cpu(
|
||||||
RISCVCPU(..),
|
RISCVCPU(..),
|
||||||
RISCVCPU (RISCVCPU),
|
|
||||||
riscvCPUInit)
|
riscvCPUInit)
|
||||||
import Fetch(fetchInstruction, FetchResult (Instruction, Misaligned))
|
import Fetch(fetchInstruction, FetchResult (Instruction, Misaligned))
|
||||||
import Isa.Decode(decode)
|
import Isa.Decode(decode)
|
||||||
|
|
|
@ -100,6 +100,7 @@ library
|
||||||
Cpu,
|
Cpu,
|
||||||
RegFiles,
|
RegFiles,
|
||||||
Fetch,
|
Fetch,
|
||||||
|
Exceptions,
|
||||||
Util
|
Util
|
||||||
c-sources: c/uart_sim_device.c
|
c-sources: c/uart_sim_device.c
|
||||||
include-dirs: c
|
include-dirs: c
|
||||||
|
|
Loading…
Reference in a new issue