Artturin/RiscV-Formal
1
0
Fork 0
forked from Yehowshua/RiscV-Formal
Code Pull requests Activity

added needed context and getting ready to implement execute

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-03-10 22:26:38 -04:00
parent b95b2b962a
commit 69f5cdee6a
7 changed files with 115 additions and 87 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
hs/Bus.hs
View file

@ -15,6 +15,7 @@ import Peripherals.Uart(UartAddr, read, write)
import BusTypes( import BusTypes(
BusError(..), BusError(..),
TransactionSize(..), TransactionSize(..),
WriteRequest(..),
ReadRequest(..), ReadRequest(..),
BusVal(..), BusVal(..),
) )
@ -53,7 +54,7 @@ alignCheck addr SizeQuadWord = addr `mod` 16 == 0
-- reading/writing from/to UART is implemented as reading/writing -- reading/writing from/to UART is implemented as reading/writing
-- from/to stdin/stdout, so we need IO. -- from/to stdin/stdout, so we need IO.
read :: ReadRequest -> Peripherals -> IO ReadResponse read :: ReadRequest -> Peripherals -> IO ReadResponse
read (Request addr size) peripherals read (ReadRequest addr size) peripherals
| not (alignCheck addr size) = return |> Left UnAligned | not (alignCheck addr size) = return |> Left UnAligned
| (addr >= ramStart) && (addr <= ramEnd) = | (addr >= ramStart) && (addr <= ramEnd) =
return |> Right |> Peripherals.Ram.read size ramWordAddr (ram peripherals) return |> Right |> Peripherals.Ram.read size ramWordAddr (ram peripherals)
@ -71,8 +72,8 @@ read (Request addr size) peripherals
uartAddr :: UartAddr uartAddr :: UartAddr
uartAddr = resize uartAddrNoOffset uartAddr = resize uartAddrNoOffset
write :: BusVal -> Addr -> Peripherals -> IO WriteResponse write :: WriteRequest -> Peripherals -> IO WriteResponse
write val addr peripherals write (WriteRequest addr val) peripherals
| not (alignCheck addr |> busValToTransactionSize val) = return |> Left UnAligned | not (alignCheck addr |> busValToTransactionSize val) = return |> Left UnAligned
| (addr >= uartStart) && (addr <= uartEnd) = | (addr >= uartStart) && (addr <= uartEnd) =
do do

8
hs/BusTypes.hs
View file

@ -3,6 +3,7 @@ module BusTypes(
BusError(..), BusError(..),
TransactionSize(..), TransactionSize(..),
ReadRequest(..), ReadRequest(..),
WriteRequest(..),
BusVal(..), BusVal(..),
) where ) where
@ -23,9 +24,14 @@ data TransactionSize
| SizeQuadWord | SizeQuadWord
deriving (Generic, Show, Eq, NFDataX) deriving (Generic, Show, Eq, NFDataX)
data ReadRequest = Request Addr TransactionSize data ReadRequest = ReadRequest Addr TransactionSize
deriving (Generic, Show, Eq, NFDataX) deriving (Generic, Show, Eq, NFDataX)
data WriteRequest = WriteRequest Addr BusVal
deriving (Generic, Show, Eq, NFDataX)
-- data WriteRequest
data BusVal data BusVal
= BusByte Byte = BusByte Byte
| BusHalfWord HalfWord | BusHalfWord HalfWord

18
hs/Decode.hs
View file

@ -11,22 +11,22 @@ import DecodeTypes(
import Clash.Prelude import Clash.Prelude
import Fetch(FetchResult (Instruction, InstructionException)) import Fetch(FetchResult (Instruction, InstructionException))
import Exceptions(Exception(..)) import Exceptions(Exception(..))
import Types(Insn) import Types(Insn, Addr)
import RegFiles(RegVal(..)) import RegFiles(RegVal(..))
import Util((|>)) import Util((|>))
data DecodeResult = Opcode Opcode data DecodeResult = Opcode {opcode :: Opcode, insnAddr :: Addr}
| DecodeException Exception | DecodeException {exception :: Exception, insnAddr :: Addr}
| InstructionException Exception | InstructionException {exception :: Exception, insnAddr :: Addr}
deriving (Generic, Show, Eq, NFDataX) deriving (Generic, Show, Eq, NFDataX)
decode :: FetchResult -> DecodeResult decode :: FetchResult -> DecodeResult
decode (Instruction insn) = decode (Instruction insn addr) =
case insnToOpcode insn of case insnToOpcode insn of
Just opcode -> Opcode opcode Just opcode -> Opcode opcode addr
Nothing -> DecodeException |> IllegalInstruction insn Nothing -> DecodeException (IllegalInstruction insn) addr
decode (Fetch.InstructionException exception) = decode (Fetch.InstructionException exception addr) =
Decode.InstructionException exception Decode.InstructionException exception addr
insnToOpcode :: Insn -> Maybe Opcode insnToOpcode :: Insn -> Maybe Opcode
insnToOpcode insn = insnToOpcode insn =

14
hs/Exceptions.hs
View file

@ -18,9 +18,9 @@ data Exception =
| SupervisorExternalInterrupt | SupervisorExternalInterrupt
| MachineExternalInterrupt | MachineExternalInterrupt
| CounterOverflowInterrupt | CounterOverflowInterrupt
| InstructionAddressMisaligned Addr | InstructionAddressMisaligned
| InstructionAccessFault Addr | InstructionAccessFault
| IllegalInstruction Insn | IllegalInstruction {insn :: Insn}
| Breakpoint | Breakpoint
| LoadAddressMisaligned | LoadAddressMisaligned
| LoadAccessFault | LoadAccessFault
@ -45,8 +45,8 @@ exceptionCode MachineTimerInterrupt = 7
exceptionCode SupervisorExternalInterrupt = 9 exceptionCode SupervisorExternalInterrupt = 9
exceptionCode MachineExternalInterrupt = 11 exceptionCode MachineExternalInterrupt = 11
exceptionCode CounterOverflowInterrupt = 13 exceptionCode CounterOverflowInterrupt = 13
exceptionCode (InstructionAddressMisaligned _) = 0 exceptionCode InstructionAddressMisaligned = 0
exceptionCode (InstructionAccessFault _) = 1 exceptionCode InstructionAccessFault = 1
exceptionCode (IllegalInstruction _) = 2 exceptionCode (IllegalInstruction _) = 2
exceptionCode Breakpoint = 3 exceptionCode Breakpoint = 3
exceptionCode LoadAddressMisaligned = 4 exceptionCode LoadAddressMisaligned = 4
@ -71,8 +71,8 @@ isSynchronousException MachineTimerInterrupt = False
isSynchronousException SupervisorExternalInterrupt = False isSynchronousException SupervisorExternalInterrupt = False
isSynchronousException MachineExternalInterrupt = False isSynchronousException MachineExternalInterrupt = False
isSynchronousException CounterOverflowInterrupt = False isSynchronousException CounterOverflowInterrupt = False
isSynchronousException (InstructionAddressMisaligned _) = True isSynchronousException InstructionAddressMisaligned = True
isSynchronousException (InstructionAccessFault _) = True isSynchronousException InstructionAccessFault = True
isSynchronousException (IllegalInstruction _) = True isSynchronousException (IllegalInstruction _) = True
isSynchronousException Breakpoint = True isSynchronousException Breakpoint = True
isSynchronousException LoadAddressMisaligned = True isSynchronousException LoadAddressMisaligned = True

19
hs/Execute.hs
View file

@ -3,4 +3,21 @@
module Execute(execute) where module Execute(execute) where
execute = 1 import Clash.Prelude
import Decode(DecodeResult(..))
import DecodeTypes(Opcode(..))
import Types(Addr, DoubleWord)
import BusTypes(
WriteRequest(..),
ReadRequest(..),
)
import RegFiles(RegFileIdx)
import Util((|>))
data ExecuteResult = ReadRequest {readRequest :: ReadRequest, insnAddr :: Addr}
| WriteRequest {writeRequest :: WriteRequest, insnAddr :: Addr}
| WriteBackGPR {idx :: RegFileIdx, val :: DoubleWord}
execute :: DecodeResult -> ExecuteResult
execute = undefined

32
hs/Fetch.hs
View file

@ -20,32 +20,32 @@ import BusTypes(
import Exceptions(Exception(..)) import Exceptions(Exception(..))
import Util((|>)) import Util((|>))
data FetchResult = Instruction Insn data FetchResult = Instruction {insn :: Insn, insnAddr :: Addr}
| InstructionException Exception | InstructionException {exception :: Exception, addr :: Addr}
deriving (Generic, Show, Eq, NFDataX) deriving (Generic, Show, Eq, NFDataX)
fetchInstruction :: Peripherals -> Addr -> IO FetchResult fetchInstruction :: Peripherals -> Addr -> IO FetchResult
fetchInstruction peripherals addr = fetchInstruction peripherals addr =
do do
readReasponse <-Bus.read (BusTypes.Request addr BusTypes.SizeFullWord) peripherals readReasponse <-Bus.read (BusTypes.ReadRequest addr BusTypes.SizeFullWord) peripherals
case readReasponse of case readReasponse of
Right (BusFullWord insn) -> Right (BusFullWord insn) ->
pure |> Instruction insn pure |> Instruction insn addr
Left UnAligned -> Left UnAligned ->
pure |> InstructionException (InstructionAddressMisaligned addr) pure |> InstructionException InstructionAddressMisaligned addr
Left UnMapped -> Left UnMapped ->
pure |> InstructionException (InstructionAccessFault addr) pure |> InstructionException InstructionAccessFault addr
Right _ -> Right _ ->
pure |> InstructionException (InstructionAccessFault addr) pure |> InstructionException InstructionAccessFault addr
debugInsn :: FetchResult -> String debugInsn :: FetchResult -> String
debugInsn fetchResult = debugInsn = show
case fetchResult of -- case fetchResult of
Instruction insn -> -- Instruction insn ->
"Instruction raw binary | " -- "Instruction raw binary | "
P.++ binaryInsn -- P.++ binaryInsn
P.++ " (" P.++ show insn P.++ ")" -- P.++ " (" P.++ show insn P.++ ")"
where -- where
binaryInsn = show (bitCoerce insn :: BitVector 32) -- binaryInsn = show (bitCoerce insn :: BitVector 32)
InstructionException e -> show e -- InstructionException e -> show e

104
hs/Read.hs
View file

@ -15,61 +15,65 @@ import Cpu(RISCVCPU(..))
import RegFiles (RegVal(..), GPR) import RegFiles (RegVal(..), GPR)
read :: DecodeResult -> RISCVCPU -> DecodeResult read :: DecodeResult -> RISCVCPU -> DecodeResult
read (Opcode opc) riscvCPU = read (Opcode opcode addr) riscvCPU =
let gprRegFile = gpr riscvCPU let
in case opc of gprRegFile = gpr riscvCPU
-- R-Type opcode' = case opcode of
ADD fields -> Opcode (ADD (readRTypeFields fields gprRegFile)) -- R-Type
SUB fields -> Opcode (SUB (readRTypeFields fields gprRegFile)) ADD fields -> (ADD (readRTypeFields fields gprRegFile))
XOR fields -> Opcode (XOR (readRTypeFields fields gprRegFile)) SUB fields -> (SUB (readRTypeFields fields gprRegFile))
OR fields -> Opcode (OR (readRTypeFields fields gprRegFile)) XOR fields -> (XOR (readRTypeFields fields gprRegFile))
AND fields -> Opcode (AND (readRTypeFields fields gprRegFile)) OR fields -> (OR (readRTypeFields fields gprRegFile))
SLL fields -> Opcode (SLL (readRTypeFields fields gprRegFile)) AND fields -> (AND (readRTypeFields fields gprRegFile))
SRL fields -> Opcode (SRL (readRTypeFields fields gprRegFile)) SLL fields -> (SLL (readRTypeFields fields gprRegFile))
SRA fields -> Opcode (SRA (readRTypeFields fields gprRegFile)) SRL fields -> (SRL (readRTypeFields fields gprRegFile))
SLT fields -> Opcode (SLT (readRTypeFields fields gprRegFile)) SRA fields -> (SRA (readRTypeFields fields gprRegFile))
SLTU fields -> Opcode (SLTU (readRTypeFields fields gprRegFile)) SLT fields -> (SLT (readRTypeFields fields gprRegFile))
SLTU fields -> (SLTU (readRTypeFields fields gprRegFile))
-- I-Type -- I-Type
ADDI fields -> Opcode (ADDI (readITypeFields fields gprRegFile)) ADDI fields -> (ADDI (readITypeFields fields gprRegFile))
XORI fields -> Opcode (XORI (readITypeFields fields gprRegFile)) XORI fields -> (XORI (readITypeFields fields gprRegFile))
ORI fields -> Opcode (ORI (readITypeFields fields gprRegFile)) ORI fields -> (ORI (readITypeFields fields gprRegFile))
ANDI fields -> Opcode (ANDI (readITypeFields fields gprRegFile)) ANDI fields -> (ANDI (readITypeFields fields gprRegFile))
SLLI fields -> Opcode (SLLI (readITypeFields fields gprRegFile)) SLLI fields -> (SLLI (readITypeFields fields gprRegFile))
SRLI fields -> Opcode (SRLI (readITypeFields fields gprRegFile)) SRLI fields -> (SRLI (readITypeFields fields gprRegFile))
SRAI fields -> Opcode (SRAI (readITypeFields fields gprRegFile)) SRAI fields -> (SRAI (readITypeFields fields gprRegFile))
SLTI fields -> Opcode (SLTI (readITypeFields fields gprRegFile)) SLTI fields -> (SLTI (readITypeFields fields gprRegFile))
SLTIU fields -> Opcode (SLTIU (readITypeFields fields gprRegFile)) SLTIU fields -> (SLTIU (readITypeFields fields gprRegFile))
LB fields -> Opcode (LB (readITypeFields fields gprRegFile)) LB fields -> (LB (readITypeFields fields gprRegFile))
LH fields -> Opcode (LH (readITypeFields fields gprRegFile)) LH fields -> (LH (readITypeFields fields gprRegFile))
LW fields -> Opcode (LW (readITypeFields fields gprRegFile)) LW fields -> (LW (readITypeFields fields gprRegFile))
LBU fields -> Opcode (LBU (readITypeFields fields gprRegFile)) LBU fields -> (LBU (readITypeFields fields gprRegFile))
LHU fields -> Opcode (LHU (readITypeFields fields gprRegFile)) LHU fields -> (LHU (readITypeFields fields gprRegFile))
JALR fields -> Opcode (JALR (readITypeFields fields gprRegFile)) JALR fields -> (JALR (readITypeFields fields gprRegFile))
ECALL fields -> Opcode (ECALL (readITypeFields fields gprRegFile)) -- No regs needed, but consistent ECALL fields -> (ECALL (readITypeFields fields gprRegFile)) -- No regs needed, but consistent
EBREAK fields -> Opcode (EBREAK (readITypeFields fields gprRegFile)) -- Ditto EBREAK fields -> (EBREAK (readITypeFields fields gprRegFile)) -- Ditto
-- S-Type -- S-Type
SB fields -> Opcode (SB (readSTypeFields fields gprRegFile)) SB fields -> (SB (readSTypeFields fields gprRegFile))
SH fields -> Opcode (SH (readSTypeFields fields gprRegFile)) SH fields -> (SH (readSTypeFields fields gprRegFile))
SW fields -> Opcode (SW (readSTypeFields fields gprRegFile)) SW fields -> (SW (readSTypeFields fields gprRegFile))
-- B-Type -- B-Type
BEQ fields -> Opcode (BEQ (readBTypeFields fields gprRegFile)) BEQ fields -> (BEQ (readBTypeFields fields gprRegFile))
BNE fields -> Opcode (BNE (readBTypeFields fields gprRegFile)) BNE fields -> (BNE (readBTypeFields fields gprRegFile))
BLT fields -> Opcode (BLT (readBTypeFields fields gprRegFile)) BLT fields -> (BLT (readBTypeFields fields gprRegFile))
BGE fields -> Opcode (BGE (readBTypeFields fields gprRegFile)) BGE fields -> (BGE (readBTypeFields fields gprRegFile))
BLTU fields -> Opcode (BLTU (readBTypeFields fields gprRegFile)) BLTU fields -> (BLTU (readBTypeFields fields gprRegFile))
BGEU fields -> Opcode (BGEU (readBTypeFields fields gprRegFile)) BGEU fields -> (BGEU (readBTypeFields fields gprRegFile))
-- U-Type -- U-Type
LUI fields -> Opcode (LUI (readUTypeFields fields gprRegFile)) LUI fields -> (LUI (readUTypeFields fields gprRegFile))
AUIPC fields -> Opcode (AUIPC (readUTypeFields fields gprRegFile)) AUIPC fields -> (AUIPC (readUTypeFields fields gprRegFile))
-- J-Type -- J-Type
JAL fields -> Opcode (JAL (readJTypeFields fields gprRegFile)) JAL fields -> (JAL (readJTypeFields fields gprRegFile))
read (DecodeException e) _ = DecodeException e in
read (InstructionException e) _ = InstructionException e Opcode opcode' addr
read (DecodeException e addr) _ = DecodeException e addr
read (InstructionException e addr) _ = InstructionException e addr
readRTypeFields :: RTypeFields -> GPR -> RTypeFields readRTypeFields :: RTypeFields -> GPR -> RTypeFields
readRTypeFields (RTypeFields rd funct3 rs1 rs2 funct7) gprRegFile = readRTypeFields (RTypeFields rd funct3 rs1 rs2 funct7) gprRegFile =