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

bus architecture re-built I think

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-02-26 13:05:02 -05:00
parent c8b192cade
commit 5552ad3d4a
9 changed files with 144 additions and 115 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
hs/Bus.hs
View file

@ -1,25 +1,45 @@
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
module Bus() where
module Bus(
Peripherals(..),
ReadResponse,
WriteResponse,
Bus.read,
Bus.write,
) where
import Clash.Prelude
import Peripherals.Ram(Ram, RamLine, read, RamAddr)
import Peripherals.Uart(UartAddr, read, write)
import Machine(Peripherals(..))
import BusTypes(
BusError(..),
TransactionSize(..),
ReadRequest(..),
BusResponse(..),
BusVal(..),
ReadResponse(..),
WriteResponse(..)
)
import Types(Addr,
Byte, HalfWord, FullWord, DoubleWord, QuadWord)
import Peripherals.Ram(read, bytesInRam)
import Peripherals.Ram(read, write, bytesInRam)
import Distribution.Types.UnitId (DefUnitId(unDefUnitId))
data Peripherals = Peripherals
{
ram :: Ram
}
deriving (Generic, Show, Eq, NFDataX)
type ReadResponse = Either BusError BusVal
type WriteResponse = Either BusError Peripherals
busValToTransactionSize :: BusVal -> TransactionSize
busValToTransactionSize (BusByte _) = SizeByte
busValToTransactionSize (BusHalfWord _) = SizeHalfWord
busValToTransactionSize (BusFullWord _) = SizeFullWord
busValToTransactionSize (BusDoubleWord _) = SizeDoubleWord
busValToTransactionSize (BusQuadWord _) = SizeQuadWord
alignCheck :: Addr -> TransactionSize -> Bool
alignCheck addr SizeByte = True
alignCheck addr SizeHalfWord = addr `mod` 2 == 0
@ -50,15 +70,24 @@ read (Request addr size) peripherals
uartAddr :: UartAddr
uartAddr = resize uartAddrNoOffset
-- write :: BusVal -> Addr -> Peripherals -> IO WriteResponse
-- write val addr peripherals
-- | (addr >= uartStart) && (addr <= uartEnd) =
-- WriteResponse . Result <$> Peripherals.Uart.write val uartAddr
-- where
-- ramAddrNoOffset = addr - ramStart
-- ramAddr :: RamAddr
-- ramAddr = resize ramAddrNoOffset
write :: BusVal -> Addr -> Peripherals -> IO WriteResponse
write val addr peripherals
| not (alignCheck addr $ busValToTransactionSize val) = return $ Left UnAligned
| (addr >= uartStart) && (addr <= uartEnd) =
do
Peripherals.Uart.write val uartAddr
return $ Right peripherals
| (addr >= ramStart) && (addr <= ramEnd) =
return $ Right $
peripherals {
ram = Peripherals.Ram.write val ramAddr (ram peripherals)
}
| otherwise = return $ Left UnMapped
where
ramAddrNoOffset = addr - ramStart
ramAddr :: RamAddr
ramAddr = resize ramAddrNoOffset
-- uartAddrNoOffset = addr - uartStart
-- uartAddr :: UartAddr
-- uartAddr = resize uartAddrNoOffset
uartAddrNoOffset = addr - uartStart
uartAddr :: UartAddr
uartAddr = resize uartAddrNoOffset

10
hs/BusTypes.hs
View file

@ -5,8 +5,6 @@ module BusTypes(
ReadRequest(..),
BusResponse(..),
BusVal(..),
ReadResponse(..),
WriteResponse(..)
) where
import Clash.Prelude
@ -42,11 +40,3 @@ data BusVal
| BusDoubleWord DoubleWord
| BusQuadWord QuadWord
deriving (Generic, Show, Eq, NFDataX)
-- newtype ReadResponse = ReadResponse (BusResponse BusVal)
-- deriving (Generic, Show, Eq, NFDataX)
type ReadResponse = Either BusError BusVal
newtype WriteResponse = WriteResponse (BusResponse ())
deriving (Generic, Show, Eq, NFDataX)

37
hs/Cpu.hs Normal file
View file

@ -0,0 +1,37 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Cpu(
RISCVCPU(..),
Endian(..),
riscvCPUInit) where
import Clash.Prelude
import Types(Pc, Mem)
import RegFiles(GPR, FPR, CSR, gprInit, fprInit, csrInit)
import Peripherals.Ram(Ram)
data Endian = Big | Little
deriving (Generic, Show, Eq, NFDataX)
data PrivilegeLevel
= MachineMode
| SuperVisorMode
| UserMode
deriving (Generic, Show, Eq, NFDataX)
data RISCVCPU = RISCVCPU
{ pc :: Pc,
gpr :: GPR,
fpr :: FPR,
privilegeLevel :: PrivilegeLevel
}
deriving (Generic, Show, Eq, NFDataX)
riscvCPUInit :: RISCVCPU
riscvCPUInit =
RISCVCPU
0
gprInit
fprInit
MachineMode

1
hs/Fetch.hs
View file

@ -13,6 +13,7 @@ import Clash.Prelude
Bits(shiftR, (.&.)) )
import Types(Mem, Addr, Insn)
import Util(endianSwapWord)
import Bus(ReadResponse, WriteResponse, read)
data FetchResult = Instruction Insn
| Misaligned Addr

75
hs/Machine.hs
View file

@ -1,75 +0,0 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Machine(
Machine(..),
RISCVCPU(..),
Peripherals(..),
Endian(..),
machineInit) where
import Clash.Prelude
import Types(Pc, Mem)
import RegFiles(GPR, FPR, CSR, gprInit, fprInit, csrInit)
import Peripherals.Ram(Ram)
data Endian = Big | Little
deriving (Generic, Show, Eq, NFDataX)
data PrivilegeLevel
= MachineMode
| SuperVisorMode
| UserMode
deriving (Generic, Show, Eq, NFDataX)
data Peripherals = Peripherals
{
ram :: Ram
}
deriving (Generic, Show, Eq, NFDataX)
data RISCVCPU = RISCVCPU
{ pc :: Pc,
gpr :: GPR,
fpr :: FPR,
privilegeLevel :: PrivilegeLevel
}
deriving (Generic, Show, Eq, NFDataX)
data Machine = Machine
{ cpu :: RISCVCPU,
peripherals :: Peripherals
}
deriving (Generic, Show, Eq, NFDataX)
riscvCPUInit :: RISCVCPU
riscvCPUInit =
RISCVCPU
0
gprInit
fprInit
MachineMode
machineInit :: Peripherals -> Machine
machineInit peripherals =
Machine
riscvCPUInit
peripherals
memInit :: Vec 14 (Unsigned 32)
memInit =
0x0000A03C
:> 0x3000A5E8
:> 0x1A002038
:> 0x18002598
:> 0x10002588
:> 0x01002170
:> 0xF8FF8141
:> 0x08002588
:> 0x01002138
:> 0x00002598
:> 0xE8FFFF4B
:> 0x00000060
:> 0x002000C0
:> 0x00000000
:> Nil

52
hs/Peripherals/Ram.hs
View file

@ -10,7 +10,8 @@ module Peripherals.Ram(
RamLine,
bytesInRam,
read,
write) where
write,
) where
import Clash.Prelude hiding (read)
import qualified Prelude as P
@ -23,8 +24,6 @@ import Types(Addr,
import BusTypes(
TransactionSize(..),
BusVal(..),
ReadResponse(..),
WriteResponse(..)
)
-- vector depth has to be known statically at compile time
@ -85,9 +84,50 @@ readDoubleWordHelper ram addr = bitCoerce $ bitCoerce word0 ++# bitCoerce word1
word0 = readFullWordHelper ram addr
word1 = readFullWordHelper ram (addr + 1)
-- write :: BusVal -> UartAddr -> IO ()
write :: Ram -> RamAddr -> RamLine -> Ram
write ram addr value = replace addr value ram
write :: BusVal -> RamAddr -> Ram -> Ram
write (BusByte byte) addr ram = replace addr updatedWord ram
where
word = ram !! addr
byteOffset :: BitVector 2
byteOffset = slice d1 d0 addr
updatedWord = case byteOffset of
0b00 -> setSlice d31 d24 (pack byte) word
0b01 -> setSlice d23 d16 (pack byte) word
0b10 -> setSlice d15 d8 (pack byte) word
0b11 -> setSlice d7 d0 (pack byte) word
write (BusHalfWord halfWord) addr ram = replace addr updatedWord ram
where
word = ram !! addr
halfWordOffset :: Unsigned 1
halfWordOffset = unpack $ slice d0 d0 addr
updatedWord = case halfWordOffset of
0b0 -> setSlice d31 d16 (pack halfWord) word
0b1 -> setSlice d15 d0 (pack halfWord) word
write (BusFullWord fullWord) addr ram = replace addr fullWord ram
write (BusDoubleWord doubleWord) addr ram = ram''
where
(word0, word1) = bitCoerce doubleWord
ram' = replace addr word0 ram
ram'' = replace (addr + 1) word1 ram'
write (BusQuadWord quadWord) addr ram = ram''''
where
(dword0 :: DoubleWord, dword1 :: DoubleWord) =
bitCoerce quadWord
(word0 :: FullWord, word1 :: FullWord) =
bitCoerce dword0
(word2 :: FullWord, word3 :: FullWord) =
bitCoerce dword1
ram' = replace addr word0 ram
ram'' = replace (addr + 1) word1 ram'
ram''' = replace (addr + 2) word2 ram''
ram'''' = replace (addr + 3) word3 ram'''
initRamFromFile :: FilePath -> IO (Maybe Ram)
initRamFromFile filePath =

2
hs/Peripherals/Uart.hs
View file

@ -17,8 +17,6 @@ import Peripherals.UartCFFI (
import BusTypes (
TransactionSize(..),
BusVal(..),
ReadResponse(..),
WriteResponse(..)
)
import GHC.Generics (URec(UAddr), Generic (from))

19
hs/Simulation.hs
View file

@ -9,11 +9,11 @@ import qualified Prelude as P
import Peripherals.Setup(setupPeripherals, InitializedPeripherals(..))
import Peripherals.Teardown(teardownPeripherals)
import Clash.Prelude
import Machine(
Machine(..),
import Bus(Peripherals(..))
import Cpu(
RISCVCPU(..),
Peripherals(..),
machineInit, RISCVCPU (RISCVCPU))
RISCVCPU (RISCVCPU),
riscvCPUInit)
import Fetch(fetchInstruction, FetchResult (Instruction, Misaligned))
import Isa.Decode(decode)
@ -27,6 +27,11 @@ data Simulation
= Success [Machine]
| Failure String
deriving (Show)
data Machine = Machine
{ cpu :: RISCVCPU,
peripherals :: Peripherals
}
deriving (Generic, Show, Eq, NFDataX)
-- machine :: Machine
-- machine = machineInit
@ -69,7 +74,11 @@ simulation args = do
InitializationError e -> return $ Failure e
InitializedPeripherals ram -> do
let initState = machineInit $ Machine.Peripherals ram
let initState =
Machine {
cpu = riscvCPUInit,
peripherals = Bus.Peripherals ram
}
sim <- simulationLoop 15 initState
teardownPeripherals
return $ Success sim

2
rv_formal.cabal
View file

@ -97,7 +97,7 @@ library
Types,
Bus,
BusTypes,
Machine,
Cpu,
RegFiles,
Fetch,
Util