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

read seemingly complete

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-03-10 17:46:06 -04:00
parent ad751a5039
commit b95b2b962a
4 changed files with 82 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
hs/Decode.hs
View file

@ -30,17 +30,17 @@ decode (Fetch.InstructionException exception) =
insnToOpcode :: Insn -> Maybe Opcode insnToOpcode :: Insn -> Maybe Opcode
insnToOpcode insn = insnToOpcode insn =
decodeRType insn `orElse` decodeRType insn `chainAndTry`
decodeIType insn `orElse` decodeIType insn `chainAndTry`
decodeSType insn `orElse` decodeSType insn `chainAndTry`
decodeBType insn `orElse` decodeBType insn `chainAndTry`
decodeUType insn `orElse` decodeUType insn `chainAndTry`
decodeJType insn decodeJType insn
where where
orElse :: Maybe Opcode -> Maybe Opcode -> Maybe Opcode chainAndTry :: Maybe Opcode -> Maybe Opcode -> Maybe Opcode
orElse (Just left) _ = Just left chainAndTry (Just left) _ = Just left
orElse Nothing (Just right) = Just right chainAndTry Nothing (Just right) = Just right
orElse _ _ = Nothing chainAndTry _ _ = Nothing
decodeRType :: Insn -> Maybe Opcode decodeRType :: Insn -> Maybe Opcode
decodeRType insn = decodeRType insn =

91
hs/Read.hs
View file

@ -16,42 +16,82 @@ import RegFiles (RegVal(..), GPR)
read :: DecodeResult -> RISCVCPU -> DecodeResult read :: DecodeResult -> RISCVCPU -> DecodeResult
read (Opcode opc) riscvCPU = read (Opcode opc) riscvCPU =
case opc of let gprRegFile = gpr riscvCPU
ADD fields -> Opcode (ADD (readRTypeFields fields (gpr riscvCPU))) in case opc of
SUB fields -> Opcode (SUB (readRTypeFields fields (gpr riscvCPU))) -- R-Type
XOR fields -> Opcode (XOR (readRTypeFields fields (gpr riscvCPU))) ADD fields -> Opcode (ADD (readRTypeFields fields gprRegFile))
OR fields -> Opcode (OR (readRTypeFields fields (gpr riscvCPU))) SUB fields -> Opcode (SUB (readRTypeFields fields gprRegFile))
AND fields -> Opcode (AND (readRTypeFields fields (gpr riscvCPU))) XOR fields -> Opcode (XOR (readRTypeFields fields gprRegFile))
SLL fields -> Opcode (SLL (readRTypeFields fields (gpr riscvCPU))) OR fields -> Opcode (OR (readRTypeFields fields gprRegFile))
SRL fields -> Opcode (SRL (readRTypeFields fields (gpr riscvCPU))) AND fields -> Opcode (AND (readRTypeFields fields gprRegFile))
SRA fields -> Opcode (SRA (readRTypeFields fields (gpr riscvCPU))) SLL fields -> Opcode (SLL (readRTypeFields fields gprRegFile))
SLT fields -> Opcode (SLT (readRTypeFields fields (gpr riscvCPU))) SRL fields -> Opcode (SRL (readRTypeFields fields gprRegFile))
SLTU fields -> Opcode (SLTU (readRTypeFields fields (gpr riscvCPU))) SRA fields -> Opcode (SRA (readRTypeFields fields gprRegFile))
_ -> undefined SLT fields -> Opcode (SLT (readRTypeFields fields gprRegFile))
SLTU fields -> Opcode (SLTU (readRTypeFields fields gprRegFile))
-- I-Type
ADDI fields -> Opcode (ADDI (readITypeFields fields gprRegFile))
XORI fields -> Opcode (XORI (readITypeFields fields gprRegFile))
ORI fields -> Opcode (ORI (readITypeFields fields gprRegFile))
ANDI fields -> Opcode (ANDI (readITypeFields fields gprRegFile))
SLLI fields -> Opcode (SLLI (readITypeFields fields gprRegFile))
SRLI fields -> Opcode (SRLI (readITypeFields fields gprRegFile))
SRAI fields -> Opcode (SRAI (readITypeFields fields gprRegFile))
SLTI fields -> Opcode (SLTI (readITypeFields fields gprRegFile))
SLTIU fields -> Opcode (SLTIU (readITypeFields fields gprRegFile))
LB fields -> Opcode (LB (readITypeFields fields gprRegFile))
LH fields -> Opcode (LH (readITypeFields fields gprRegFile))
LW fields -> Opcode (LW (readITypeFields fields gprRegFile))
LBU fields -> Opcode (LBU (readITypeFields fields gprRegFile))
LHU fields -> Opcode (LHU (readITypeFields fields gprRegFile))
JALR fields -> Opcode (JALR (readITypeFields fields gprRegFile))
ECALL fields -> Opcode (ECALL (readITypeFields fields gprRegFile)) -- No regs needed, but consistent
EBREAK fields -> Opcode (EBREAK (readITypeFields fields gprRegFile)) -- Ditto
-- S-Type
SB fields -> Opcode (SB (readSTypeFields fields gprRegFile))
SH fields -> Opcode (SH (readSTypeFields fields gprRegFile))
SW fields -> Opcode (SW (readSTypeFields fields gprRegFile))
-- B-Type
BEQ fields -> Opcode (BEQ (readBTypeFields fields gprRegFile))
BNE fields -> Opcode (BNE (readBTypeFields fields gprRegFile))
BLT fields -> Opcode (BLT (readBTypeFields fields gprRegFile))
BGE fields -> Opcode (BGE (readBTypeFields fields gprRegFile))
BLTU fields -> Opcode (BLTU (readBTypeFields fields gprRegFile))
BGEU fields -> Opcode (BGEU (readBTypeFields fields gprRegFile))
-- U-Type
LUI fields -> Opcode (LUI (readUTypeFields fields gprRegFile))
AUIPC fields -> Opcode (AUIPC (readUTypeFields fields gprRegFile))
-- J-Type
JAL fields -> Opcode (JAL (readJTypeFields fields gprRegFile))
read (DecodeException e) _ = DecodeException e read (DecodeException e) _ = DecodeException e
read (InstructionException e) _ = InstructionException e read (InstructionException e) _ = InstructionException e
readRTypeFields :: RTypeFields -> GPR -> RTypeFields readRTypeFields :: RTypeFields -> GPR -> RTypeFields
readRTypeFields (RTypeFields rd funct3 rs1 rs2 funct7) gprRegFile = readRTypeFields (RTypeFields rd funct3 rs1 rs2 funct7) gprRegFile =
let rs1_val = fetchRegVal rs1 gprRegFile let rs1_val = fetchGPRRegVal rs1 gprRegFile
rs2_val = fetchRegVal rs2 gprRegFile rs2_val = fetchGPRRegVal rs2 gprRegFile
in RTypeFields rd funct3 rs1_val rs2_val funct7 in RTypeFields rd funct3 rs1_val rs2_val funct7
readITypeFields :: ITypeFields -> GPR -> ITypeFields readITypeFields :: ITypeFields -> GPR -> ITypeFields
readITypeFields (ITypeFields rd funct3 rs1 imm) gpr = readITypeFields (ITypeFields rd funct3 rs1 imm) gprRegFile =
let rs1_val = fetchRegVal rs1 gpr let rs1_val = fetchGPRRegVal rs1 gprRegFile
in ITypeFields rd funct3 rs1_val imm in ITypeFields rd funct3 rs1_val imm
readSTypeFields :: STypeFields -> GPR -> STypeFields readSTypeFields :: STypeFields -> GPR -> STypeFields
readSTypeFields (STypeFields funct3 rs1 rs2 imm12) gpr = readSTypeFields (STypeFields funct3 rs1 rs2 imm12) gprRegFile =
let rs1_val = fetchRegVal rs1 gpr let rs1_val = fetchGPRRegVal rs1 gprRegFile
rs2_val = fetchRegVal rs2 gpr rs2_val = fetchGPRRegVal rs2 gprRegFile
in STypeFields funct3 rs1_val rs2_val imm12 in STypeFields funct3 rs1_val rs2_val imm12
readBTypeFields :: BTypeFields -> GPR -> BTypeFields readBTypeFields :: BTypeFields -> GPR -> BTypeFields
readBTypeFields (BTypeFields funct3 rs1 rs2 imm13) gpr = readBTypeFields (BTypeFields funct3 rs1 rs2 imm13) gprRegFile =
let rs1_val = fetchRegVal rs1 gpr let rs1_val = fetchGPRRegVal rs1 gprRegFile
rs2_val = fetchRegVal rs2 gpr rs2_val = fetchGPRRegVal rs2 gprRegFile
in BTypeFields funct3 rs1_val rs2_val imm13 in BTypeFields funct3 rs1_val rs2_val imm13
readUTypeFields :: UTypeFields -> GPR -> UTypeFields readUTypeFields :: UTypeFields -> GPR -> UTypeFields
@ -60,7 +100,6 @@ readUTypeFields fields@(UTypeFields rd imm20) _ = fields
readJTypeFields :: JTypeFields -> GPR -> JTypeFields readJTypeFields :: JTypeFields -> GPR -> JTypeFields
readJTypeFields fields@(JTypeFields rd imm21) _ = fields readJTypeFields fields@(JTypeFields rd imm21) _ = fields
-- Helper function to fetch register value fetchGPRRegVal :: RegVal -> GPR -> RegVal
fetchRegVal :: RegVal -> GPR -> RegVal fetchGPRRegVal (Unpopulated idx) gprVal = Value idx (gprVal !! idx)
fetchRegVal (Unpopulated idx) gprVal = Value idx (gprVal !! idx) fetchGPRRegVal val@(Value _ _) _ = val -- Already populated, no change
fetchRegVal val@(Value _ _) _ = val -- Already populated, no change

7
hs/RegFiles.hs
View file

@ -28,8 +28,11 @@ import Util((|>))
import Types(DoubleWord) import Types(DoubleWord)
type RegFileIdx = Unsigned 5 type RegFileIdx = Unsigned 5
data RegVal = Value RegFileIdx DoubleWord data RegVal = Value {
| Unpopulated RegFileIdx regFileIdx :: RegFileIdx,
regVal :: DoubleWord
}
| Unpopulated {regFileIdx :: RegFileIdx}
deriving (Generic, Show, Eq, NFDataX) deriving (Generic, Show, Eq, NFDataX)
type GPR = Vec 32 (Unsigned 64) -- General Purpose Registers type GPR = Vec 32 (Unsigned 64) -- General Purpose Registers

5
hs/Simulation.hs
View file

@ -15,6 +15,7 @@ import Peripherals.Setup(setupPeripherals, InitializedPeripherals(..))
import Peripherals.Teardown(teardownPeripherals) import Peripherals.Teardown(teardownPeripherals)
import Clash.Prelude import Clash.Prelude
import Bus(Peripherals(..)) import Bus(Peripherals(..))
import Read(read)
import Cpu( import Cpu(
RISCVCPU(..), RISCVCPU(..),
riscvCPUInit) riscvCPUInit)
@ -44,8 +45,8 @@ simulationLoop n machine = do
let machinePeripherals = peripherals machine let machinePeripherals = peripherals machine
currPc = pc |> cpu machine currPc = pc |> cpu machine
fetchResult <- fetchInstruction machinePeripherals currPc fetchResult <- fetchInstruction machinePeripherals currPc
let decodeResult = decode fetchResult let decodeResult = Read.read (decode fetchResult) (cpu machine)
putStrLn |> show decodeResult P.++ debugInsn fetchResult putStrLn |> show decodeResult -- P.++ debugInsn fetchResult
let pc' = currPc + 4 let pc' = currPc + 4
cpu' = (cpu machine) { pc = pc' } cpu' = (cpu machine) { pc = pc' }
machine' = machine { cpu = cpu' } machine' = machine { cpu = cpu' }