Yehowshua/RiscV-Formal
2
0
Fork 1
Code Issues 8 Pull requests Actions Packages Projects Releases Wiki Activity

save progress before switching to new bus architecture

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-03-04 08:12:59 -05:00
parent 88ec010f98
commit d7d698a28c
4 changed files with 80 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
hs/Exceptions.hs
View file

@ -1,7 +1,11 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Exceptions() where
module Exceptions(
Exception(..),
exceptionCode,
isSynchronousException
) where
import Clash.Prelude
@ -32,3 +36,56 @@ data Exception =
| SoftwareCheck
| HardwareError
deriving (Generic, Show, Eq, NFDataX)
exceptionCode :: Exception -> Unsigned 6
exceptionCode SupervisorSoftwareInterrupt = 1
exceptionCode MachineSoftwareInterrupt = 3
exceptionCode SupervisorTimerInterrupt = 5
exceptionCode MachineTimerInterrupt = 7
exceptionCode SupervisorExternalInterrupt = 9
exceptionCode MachineExternalInterrupt = 11
exceptionCode CounterOverflowInterrupt = 13
exceptionCode InstructionAddressMisaligned = 0
exceptionCode InstructionAccessFault = 1
exceptionCode IllegalInstruction = 2
exceptionCode Breakpoint = 3
exceptionCode LoadAddressMisaligned = 4
exceptionCode LoadAccessFault = 5
exceptionCode StoreAMOAddressMisaligned = 6
exceptionCode StoreAMOAccessFault = 7
exceptionCode EnvironmentCallFromUMode = 8
exceptionCode EnvironmentCallFromSMode = 9
exceptionCode EnvironmentCallFromMMode = 11
exceptionCode InstructionPageFault = 12
exceptionCode LoadPageFault = 13
exceptionCode StoreAMOPageFault = 15
exceptionCode DoubleTrap = 16
exceptionCode SoftwareCheck = 18
exceptionCode HardwareError = 19
isSynchronousException :: Exception -> Bool
isSynchronousException SupervisorSoftwareInterrupt = False
isSynchronousException MachineSoftwareInterrupt = False
isSynchronousException SupervisorTimerInterrupt = False
isSynchronousException MachineTimerInterrupt = False
isSynchronousException SupervisorExternalInterrupt = False
isSynchronousException MachineExternalInterrupt = False
isSynchronousException CounterOverflowInterrupt = False
isSynchronousException InstructionAddressMisaligned = True
isSynchronousException InstructionAccessFault = True
isSynchronousException IllegalInstruction = True
isSynchronousException Breakpoint = True
isSynchronousException LoadAddressMisaligned = True
isSynchronousException LoadAccessFault = True
isSynchronousException StoreAMOAddressMisaligned = True
isSynchronousException StoreAMOAccessFault = True
isSynchronousException EnvironmentCallFromUMode = True
isSynchronousException EnvironmentCallFromSMode = True
isSynchronousException EnvironmentCallFromMMode = True
isSynchronousException InstructionPageFault = True
isSynchronousException LoadPageFault = True
isSynchronousException Reserved = True
isSynchronousException StoreAMOPageFault = True
isSynchronousException DoubleTrap = True
isSynchronousException SoftwareCheck = True
isSynchronousException HardwareError = True

30
hs/Fetch.hs
View file

@ -6,16 +6,15 @@ module Fetch(
FetchResult(..)) where
import Clash.Prelude
( Eq((==)),
KnownNat,
Bool(False, True),
(!!),
Bits(shiftR, (.&.)) )
import Types(Mem, Addr, Insn)
import Util(endianSwapWord)
import Bus(ReadResponse, WriteResponse, read)
import Bus(Peripherals(..))
import BusTypes(ReadRequest(..), TransactionSize(..))
import BusTypes(
ReadRequest(..),
TransactionSize(..),
BusVal(..),
BusError(..))
import Exceptions(Exception(..), exceptionCode, isSynchronousException)
import GHC.IO (IO)
import GHC.Base (Applicative(pure))
@ -23,6 +22,9 @@ import GHC.Base (Applicative(pure))
data FetchResult = Instruction Insn
| Misaligned Addr
data FetchResult1 = Instruction1 Insn
| InstructionException Exception
fetchInstruction :: KnownNat n => Mem n -> Addr -> FetchResult
fetchInstruction mem addr =
let
@ -36,6 +38,16 @@ fetchInstruction mem addr =
True -> Instruction insn
False -> Misaligned addr
fetchInstruction1 :: Peripherals -> Addr -> IO ReadResponse
fetchInstruction1 :: Peripherals -> Addr -> IO FetchResult1
fetchInstruction1 peripherals addr =
read (BusTypes.Request addr BusTypes.SizeFullWord) peripherals
do
readReasponse <-Bus.read (BusTypes.Request addr BusTypes.SizeFullWord) peripherals
case readReasponse of
Right (BusFullWord insn) ->
pure $ Instruction1 insn
Left UnAligned ->
pure $ InstructionException InstructionAddressMisaligned
Left UnMapped ->
pure $ InstructionException InstructionAccessFault
Right _ ->
pure $ InstructionException InstructionAccessFault

44
hs/Util.hs
View file

@ -1,44 +0,0 @@
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
module Util(
powerIndex32,
powerIndex64,
endianSwapWord) where
import Clash.Prelude
import Types(FullWord)
data ValidIndex32 (n :: Nat) where
ValidIndex32 :: (0 <= n, n <= 31) => SNat n -> ValidIndex32 n
mkValidIndex32 :: forall n. (KnownNat n, 0 <= n, n <= 31) => ValidIndex32 n
mkValidIndex32 = ValidIndex32 $ SNat @n
powerIndex32 :: forall n. (KnownNat n, 0 <= n, n <= 31) => SNat (31 - n)
powerIndex32 = case mkValidIndex32 @n of
ValidIndex32 _ -> SNat @(31 - n)
data ValidIndex63 (n :: Nat) where
ValidIndex63 :: (0 <= n, n <= 63) => SNat n -> ValidIndex63 n
mkValidIndex64 :: forall n. (KnownNat n, 0 <= n, n <= 63) => ValidIndex63 n
mkValidIndex64 = ValidIndex63 $ SNat @n
powerIndex64 :: forall n. (KnownNat n, 0 <= n, n <= 63) => SNat (63 - n)
powerIndex64 = case mkValidIndex64 @n of
ValidIndex63 _ -> SNat @(63 - n)
endianSwapWord :: FullWord -> FullWord
endianSwapWord x =
(byte0 `shiftL` 24) .|.
(byte1 `shiftL` 16) .|.
(byte2 `shiftL` 8) .|.
byte3
where
byte0 = (x .&. 0x000000FF)
byte1 = (x .&. 0x0000FF00) `shiftR` 8
byte2 = (x .&. 0x00FF0000) `shiftR` 16
byte3 = (x .&. 0xFF000000) `shiftR` 24

3
rv_formal.cabal
View file

@ -100,8 +100,7 @@ library
Cpu,
RegFiles,
Fetch,
Exceptions,
Util
Exceptions
c-sources: c/uart_sim_device.c
include-dirs: c
default-language: Haskell2010