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

read is getting there...

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-03-10 17:22:51 -04:00
parent 171fcece98
commit ad751a5039
2 changed files with 50 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hs/Decode.hs
View file

@ -1,7 +1,7 @@
{-# LANGUAGE DataKinds #-} {-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE NumericUnderscores #-}
module Decode(decode, DecodeResult) where module Decode(decode, DecodeResult(..)) where
import DecodeTypes( import DecodeTypes(
RTypeFields(..), ITypeFields(..), STypeFields(..), RTypeFields(..), ITypeFields(..), STypeFields(..),

66
hs/Read.hs
View file

@ -10,25 +10,57 @@ import DecodeTypes(
) )
import Clash.Prelude import Clash.Prelude
import Decode(DecodeResult) import Decode(DecodeResult(..))
-- import Types(DoubleWord, RegFileIdx, Addr) import Cpu(RISCVCPU(..))
import RegFiles (RegVal(..), GPR)
read :: DecodeResult -> RISCVCPU -> DecodeResult
read (Opcode opc) riscvCPU =
case opc of
ADD fields -> Opcode (ADD (readRTypeFields fields (gpr riscvCPU)))
SUB fields -> Opcode (SUB (readRTypeFields fields (gpr riscvCPU)))
XOR fields -> Opcode (XOR (readRTypeFields fields (gpr riscvCPU)))
OR fields -> Opcode (OR (readRTypeFields fields (gpr riscvCPU)))
AND fields -> Opcode (AND (readRTypeFields fields (gpr riscvCPU)))
SLL fields -> Opcode (SLL (readRTypeFields fields (gpr riscvCPU)))
SRL fields -> Opcode (SRL (readRTypeFields fields (gpr riscvCPU)))
SRA fields -> Opcode (SRA (readRTypeFields fields (gpr riscvCPU)))
SLT fields -> Opcode (SLT (readRTypeFields fields (gpr riscvCPU)))
SLTU fields -> Opcode (SLTU (readRTypeFields fields (gpr riscvCPU)))
_ -> undefined
read (DecodeException e) _ = DecodeException e
read (InstructionException e) _ = InstructionException e
-- data SRC = GPR RegVal readRTypeFields :: RTypeFields -> GPR -> RTypeFields
-- | FPR RegVal readRTypeFields (RTypeFields rd funct3 rs1 rs2 funct7) gprRegFile =
-- | CSR RegVal let rs1_val = fetchRegVal rs1 gprRegFile
-- | PC Addr rs2_val = fetchRegVal rs2 gprRegFile
-- deriving (Generic, Show, Eq, NFDataX) in RTypeFields rd funct3 rs1_val rs2_val funct7
-- data ReadResult = ReadResult readITypeFields :: ITypeFields -> GPR -> ITypeFields
-- { src1 :: SRC, readITypeFields (ITypeFields rd funct3 rs1 imm) gpr =
-- src2 :: SRC, let rs1_val = fetchRegVal rs1 gpr
-- src3 :: SRC in ITypeFields rd funct3 rs1_val imm
-- }
-- deriving (Generic, Show, Eq, NFDataX)
read = 2 readSTypeFields :: STypeFields -> GPR -> STypeFields
readSTypeFields (STypeFields funct3 rs1 rs2 imm12) gpr =
let rs1_val = fetchRegVal rs1 gpr
rs2_val = fetchRegVal rs2 gpr
in STypeFields funct3 rs1_val rs2_val imm12
-- opcodeToReadResult :: Opcode -> ReadResult readBTypeFields :: BTypeFields -> GPR -> BTypeFields
-- opcodeToReadResult (ADD (RTypeFields _ rd funct3 rs1 rs2 funct7)) = undefined readBTypeFields (BTypeFields funct3 rs1 rs2 imm13) gpr =
-- opcodeToReadResult _ = undefined let rs1_val = fetchRegVal rs1 gpr
rs2_val = fetchRegVal rs2 gpr
in BTypeFields funct3 rs1_val rs2_val imm13
readUTypeFields :: UTypeFields -> GPR -> UTypeFields
readUTypeFields fields@(UTypeFields rd imm20) _ = fields
readJTypeFields :: JTypeFields -> GPR -> JTypeFields
readJTypeFields fields@(JTypeFields rd imm21) _ = fields
-- Helper function to fetch register value
fetchRegVal :: RegVal -> GPR -> RegVal
fetchRegVal (Unpopulated idx) gprVal = Value idx (gprVal !! idx)
fetchRegVal val@(Value _ _) _ = val -- Already populated, no change