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

still compiling after refactoring field types

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-03-07 20:31:41 -05:00
parent 73d5e1204c
commit 3f50fe32f8
5 changed files with 95 additions and 74 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

89
hs/Decode.hs
View file

@ -1,7 +1,7 @@
{-# LANGUAGE DataKinds #-} {-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE NumericUnderscores #-}
module Decode(decode) where module Decode(decode, DecodeResult) where
import DecodeTypes( import DecodeTypes(
RTypeFields(..), ITypeFields(..), STypeFields(..), RTypeFields(..), ITypeFields(..), STypeFields(..),
@ -12,6 +12,7 @@ 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)
import RegFiles(RegVal(..))
import Util((|>)) import Util((|>))
data DecodeResult = Opcode Opcode data DecodeResult = Opcode Opcode
@ -47,19 +48,19 @@ decodeRType insn =
0b0110011 -> 0b0110011 ->
case funct3 of case funct3 of
0x00 -> case funct7 of 0x00 -> case funct7 of
0x00 -> Just |> ADD (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x00 -> Just |> ADD (RTypeFields rd funct3 rs1 rs2 funct7)
0x20 -> Just |> SUB (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x20 -> Just |> SUB (RTypeFields rd funct3 rs1 rs2 funct7)
_ -> Nothing _ -> Nothing
0x04 -> Just |> XOR (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x04 -> Just |> XOR (RTypeFields rd funct3 rs1 rs2 funct7)
0x06 -> Just |> OR (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x06 -> Just |> OR (RTypeFields rd funct3 rs1 rs2 funct7)
0x07 -> Just |> AND (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x07 -> Just |> AND (RTypeFields rd funct3 rs1 rs2 funct7)
0x01 -> Just |> SLL (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x01 -> Just |> SLL (RTypeFields rd funct3 rs1 rs2 funct7)
0x05 -> case funct7 of 0x05 -> case funct7 of
0x00 -> Just |> SRL (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x00 -> Just |> SRL (RTypeFields rd funct3 rs1 rs2 funct7)
0x20 -> Just |> SRA (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x20 -> Just |> SRA (RTypeFields rd funct3 rs1 rs2 funct7)
_ -> Nothing _ -> Nothing
0x02 -> Just |> SLT (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x02 -> Just |> SLT (RTypeFields rd funct3 rs1 rs2 funct7)
0x03 -> Just |> SLTU (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x03 -> Just |> SLTU (RTypeFields rd funct3 rs1 rs2 funct7)
_ -> Nothing _ -> Nothing
_ -> Nothing _ -> Nothing
where where
@ -73,36 +74,36 @@ decodeRType insn =
decodeIType :: Insn -> Maybe Opcode decodeIType :: Insn -> Maybe Opcode
decodeIType insn = case opcode of decodeIType insn = case opcode of
0b0010011 -> case funct3 of 0b0010011 -> case funct3 of
0x0 -> Just |> ADDI (ITypeFields opcode rd funct3 rs1 imm) 0x0 -> Just |> ADDI (ITypeFields rd funct3 rs1 imm)
0x4 -> Just |> XORI (ITypeFields opcode rd funct3 rs1 imm) 0x4 -> Just |> XORI (ITypeFields rd funct3 rs1 imm)
0x6 -> Just |> ORI (ITypeFields opcode rd funct3 rs1 imm) 0x6 -> Just |> ORI (ITypeFields rd funct3 rs1 imm)
0x7 -> Just |> ANDI (ITypeFields opcode rd funct3 rs1 imm) 0x7 -> Just |> ANDI (ITypeFields rd funct3 rs1 imm)
0x1 -> if slice d31 d25 (pack insn) == 0 0x1 -> if slice d31 d25 (pack insn) == 0
then Just |> SLLI (ITypeFields opcode rd funct3 rs1 imm) then Just |> SLLI (ITypeFields rd funct3 rs1 imm)
else Nothing else Nothing
0x5 -> case slice d31 d25 (pack insn) of -- Distinguish SRLI and SRAI 0x5 -> case slice d31 d25 (pack insn) of -- Distinguish SRLI and SRAI
0x00 -> Just |> SRLI (ITypeFields opcode rd funct3 rs1 imm) 0x00 -> Just |> SRLI (ITypeFields rd funct3 rs1 imm)
0x20 -> Just |> SRAI (ITypeFields opcode rd funct3 rs1 imm) 0x20 -> Just |> SRAI (ITypeFields rd funct3 rs1 imm)
_ -> Nothing _ -> Nothing
0x2 -> Just |> SLTI (ITypeFields opcode rd funct3 rs1 imm) 0x2 -> Just |> SLTI (ITypeFields rd funct3 rs1 imm)
0x3 -> Just |> SLTIU (ITypeFields opcode rd funct3 rs1 imm) 0x3 -> Just |> SLTIU (ITypeFields rd funct3 rs1 imm)
_ -> Nothing _ -> Nothing
0b0000011 -> case funct3 of 0b0000011 -> case funct3 of
0x0 -> Just |> LB (ITypeFields opcode rd funct3 rs1 imm) 0x0 -> Just |> LB (ITypeFields rd funct3 rs1 imm)
0x1 -> Just |> LH (ITypeFields opcode rd funct3 rs1 imm) 0x1 -> Just |> LH (ITypeFields rd funct3 rs1 imm)
0x2 -> Just |> LW (ITypeFields opcode rd funct3 rs1 imm) 0x2 -> Just |> LW (ITypeFields rd funct3 rs1 imm)
0x4 -> Just |> LBU (ITypeFields opcode rd funct3 rs1 imm) 0x4 -> Just |> LBU (ITypeFields rd funct3 rs1 imm)
0x5 -> Just |> LHU (ITypeFields opcode rd funct3 rs1 imm) 0x5 -> Just |> LHU (ITypeFields rd funct3 rs1 imm)
_ -> Nothing _ -> Nothing
0b1100111 -> case funct3 of 0b1100111 -> case funct3 of
0x0 -> Just |> JALR (ITypeFields opcode rd funct3 rs1 imm) 0x0 -> Just |> JALR (ITypeFields rd funct3 rs1 imm)
_ -> Nothing _ -> Nothing
0b1110011 -> case imm of 0b1110011 -> case imm of
0x000 -> Just |> ECALL (ITypeFields opcode rd funct3 rs1 imm) 0x000 -> Just |> ECALL (ITypeFields rd funct3 rs1 imm)
0x001 -> Just |> EBREAK (ITypeFields opcode rd funct3 rs1 imm) 0x001 -> Just |> EBREAK (ITypeFields rd funct3 rs1 imm)
_ -> Nothing _ -> Nothing
_ -> Nothing _ -> Nothing
@ -117,9 +118,9 @@ decodeSType :: Insn -> Maybe Opcode
decodeSType insn = decodeSType insn =
case opcode of case opcode of
0b0100011 -> case funct3 of 0b0100011 -> case funct3 of
0x0 -> Just |> SB (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Byte 0x0 -> Just |> SB (STypeFields funct3 rs1 rs2 imm12) -- Store Byte
0x1 -> Just |> SH (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Halfword 0x1 -> Just |> SH (STypeFields funct3 rs1 rs2 imm12) -- Store Halfword
0x2 -> Just |> SW (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Word 0x2 -> Just |> SW (STypeFields funct3 rs1 rs2 imm12) -- Store Word
_ -> Nothing _ -> Nothing
_ -> Nothing _ -> Nothing
where where
@ -133,12 +134,12 @@ decodeBType :: Insn -> Maybe Opcode
decodeBType insn = decodeBType insn =
case opcode of case opcode of
0b1100011 -> case funct3 of 0b1100011 -> case funct3 of
0x0 -> Just |> BEQ (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if equal 0x0 -> Just |> BEQ (BTypeFields funct3 rs1 rs2 imm13) -- Branch if equal
0x1 -> Just |> BNE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if not equal 0x1 -> Just |> BNE (BTypeFields funct3 rs1 rs2 imm13) -- Branch if not equal
0x4 -> Just |> BLT (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than 0x4 -> Just |> BLT (BTypeFields funct3 rs1 rs2 imm13) -- Branch if less than
0x5 -> Just |> BGE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal 0x5 -> Just |> BGE (BTypeFields funct3 rs1 rs2 imm13) -- Branch if greater or equal
0x6 -> Just |> BLTU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than (unsigned) 0x6 -> Just |> BLTU (BTypeFields funct3 rs1 rs2 imm13) -- Branch if less than (unsigned)
0x7 -> Just |> BGEU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal (unsigned) 0x7 -> Just |> BGEU (BTypeFields funct3 rs1 rs2 imm13) -- Branch if greater or equal (unsigned)
_ -> Nothing _ -> Nothing
_ -> Nothing _ -> Nothing
where where
@ -150,8 +151,8 @@ decodeBType insn =
decodeUType :: Insn -> Maybe Opcode decodeUType :: Insn -> Maybe Opcode
decodeUType insn = case opcode of decodeUType insn = case opcode of
0b0110111 -> Just |> LUI (UTypeFields opcode rd imm20) -- LUI 0b0110111 -> Just |> LUI (UTypeFields rd imm20) -- LUI
0b0010111 -> Just |> AUIPC (UTypeFields opcode rd imm20) -- AUIPC 0b0010111 -> Just |> AUIPC (UTypeFields rd imm20) -- AUIPC
_ -> Nothing _ -> Nothing
where where
opcode = getOpcode insn opcode = getOpcode insn
@ -161,7 +162,7 @@ decodeUType insn = case opcode of
decodeJType :: Insn -> Maybe Opcode decodeJType :: Insn -> Maybe Opcode
decodeJType insn = decodeJType insn =
case opcode of case opcode of
0b1101111 -> Just |> JAL (JTypeFields opcode rd imm21) -- JAL 0b1101111 -> Just |> JAL (JTypeFields rd imm21) -- JAL
_ -> Nothing _ -> Nothing
where where
opcode = getOpcode insn opcode = getOpcode insn
@ -210,8 +211,8 @@ getFunct7 instr = bitCoerce |> slice d31 d25 (pack instr)
getRd :: Insn -> Unsigned 5 getRd :: Insn -> Unsigned 5
getRd instr = bitCoerce |> slice d11 d7 (pack instr) getRd instr = bitCoerce |> slice d11 d7 (pack instr)
getRs2 :: Insn -> Unsigned 5 getRs2 :: Insn -> RegVal
getRs2 instr = bitCoerce |> slice d24 d20 (pack instr) getRs2 instr = Unpopulated |> bitCoerce |> slice d24 d20 (pack instr)
getRs1 :: Insn -> Unsigned 5 getRs1 :: Insn -> RegVal
getRs1 instr = bitCoerce |> slice d19 d15 (pack instr) getRs1 instr = Unpopulated |> bitCoerce |> slice d19 d15 (pack instr)

19
hs/DecodeTypes.hs
View file

@ -11,12 +11,13 @@ module DecodeTypes(
Opcode(..) Opcode(..)
) where ) where
import Clash.Prelude import Clash.Prelude
import RegFiles(RegFileIdx, RegVal)
type FUNCT7 = Unsigned 7 type FUNCT7 = Unsigned 7
type RS2 = Unsigned 5 type RS2 = RegVal
type RS1 = Unsigned 5 type RS1 = RegVal
type RD = RegFileIdx
type FUNCT3 = Unsigned 3 type FUNCT3 = Unsigned 3
type RD = Unsigned 5
type OPCODE = Unsigned 7 type OPCODE = Unsigned 7
type IMM12 = Unsigned 12 type IMM12 = Unsigned 12
@ -24,12 +25,12 @@ type IMM13 = Unsigned 13
type IMM20 = Unsigned 20 type IMM20 = Unsigned 20
type IMM21 = Unsigned 21 type IMM21 = Unsigned 21
data RTypeFields = RTypeFields OPCODE RD FUNCT3 RS1 RS2 FUNCT7 deriving (Generic, Show, Eq, NFDataX) data RTypeFields = RTypeFields RD FUNCT3 RS1 RS2 FUNCT7 deriving (Generic, Show, Eq, NFDataX)
data ITypeFields = ITypeFields OPCODE RD FUNCT3 RS1 IMM12 deriving (Generic, Show, Eq, NFDataX) data ITypeFields = ITypeFields RD FUNCT3 RS1 IMM12 deriving (Generic, Show, Eq, NFDataX)
data STypeFields = STypeFields OPCODE FUNCT3 RS1 RS2 IMM12 deriving (Generic, Show, Eq, NFDataX) data STypeFields = STypeFields FUNCT3 RS1 RS2 IMM12 deriving (Generic, Show, Eq, NFDataX)
data BTypeFields = BTypeFields OPCODE FUNCT3 RS1 RS2 IMM13 deriving (Generic, Show, Eq, NFDataX) data BTypeFields = BTypeFields FUNCT3 RS1 RS2 IMM13 deriving (Generic, Show, Eq, NFDataX)
data UTypeFields = UTypeFields OPCODE RD IMM20 deriving (Generic, Show, Eq, NFDataX) data UTypeFields = UTypeFields RD IMM20 deriving (Generic, Show, Eq, NFDataX)
data JTypeFields = JTypeFields OPCODE RD IMM21 deriving (Generic, Show, Eq, NFDataX) data JTypeFields = JTypeFields RD IMM21 deriving (Generic, Show, Eq, NFDataX)
data Opcode data Opcode
= =

39
hs/Read.hs
View file

@ -2,24 +2,33 @@
{-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE NumericUnderscores #-}
module Read(Read.read) where module Read(Read.read) where
import DecodeTypes(
Opcode(..),
RTypeFields(..), ITypeFields(..), STypeFields(..),
BTypeFields(..), UTypeFields(..), JTypeFields(..),
)
import Clash.Prelude import Clash.Prelude
import Types(DoubleWord, Addr) import Decode(DecodeResult)
-- import Types(DoubleWord, RegFileIdx, Addr)
data RegVal = Value DoubleWord
| Borrowed
deriving (Generic, Show, Eq, NFDataX)
data SRC = GPR RegVal -- data SRC = GPR RegVal
| FPR RegVal -- | FPR RegVal
| CSR RegVal -- | CSR RegVal
| PC Addr -- | PC Addr
deriving (Generic, Show, Eq, NFDataX) -- deriving (Generic, Show, Eq, NFDataX)
data ReadResult = ReadResult -- data ReadResult = ReadResult
{ src1 :: SRC, -- { src1 :: SRC,
src2 :: SRC, -- src2 :: SRC,
src3 :: SRC -- src3 :: SRC
} -- }
deriving (Generic, Show, Eq, NFDataX) -- deriving (Generic, Show, Eq, NFDataX)
read = 2 read = 2
-- opcodeToReadResult :: Opcode -> ReadResult
-- opcodeToReadResult (ADD (RTypeFields _ rd funct3 rs1 rs2 funct7)) = undefined
-- opcodeToReadResult _ = undefined

8
hs/RegFiles.hs
View file

@ -13,6 +13,8 @@
-- * Counter/Timer Registers for time/cycle counting. -- * Counter/Timer Registers for time/cycle counting.
-- * Hypervisor Registers (HPR) for guest virtualization. -- * Hypervisor Registers (HPR) for guest virtualization.
module RegFiles( module RegFiles(
RegFileIdx,
RegVal(..),
GPR, GPR,
FPR, FPR,
CSR, CSR,
@ -23,6 +25,12 @@ module RegFiles(
import Clash.Prelude import Clash.Prelude
import Util((|>)) import Util((|>))
import Types(DoubleWord)
type RegFileIdx = Unsigned 5
data RegVal = Value RegFileIdx DoubleWord
| Unpopulated RegFileIdx
deriving (Generic, Show, Eq, NFDataX)
type GPR = Vec 32 (Unsigned 64) -- General Purpose Registers type GPR = Vec 32 (Unsigned 64) -- General Purpose Registers
type FPR = Vec 32 (Unsigned 64) -- Floating Point Registers type FPR = Vec 32 (Unsigned 64) -- Floating Point Registers

6
hs/Types.hs
View file

@ -1,8 +1,10 @@
{-# LANGUAGE DataKinds #-} {-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE NumericUnderscores #-}
module Types(Pc, Mem, Insn, Addr, module Types(
Byte, HalfWord, FullWord, DoubleWord, QuadWord) Pc, Mem, Insn, Addr,
Byte, HalfWord, FullWord, DoubleWord, QuadWord
)
where where
import Clash.Prelude import Clash.Prelude