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

created Decode result

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-03-05 09:04:54 -05:00
parent a6c435791a
commit 2b1c486c17
5 changed files with 156 additions and 137 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

150
hs/Decode.hs
View file

@ -9,10 +9,25 @@ import DecodeTypes(
Opcode(..) Opcode(..)
) )
import Clash.Prelude import Clash.Prelude
import Fetch(FetchResult (Instruction, InstructionException))
import Exceptions(Exception(..))
import Types(Insn) import Types(Insn)
decode :: Insn -> Opcode data DecodeResult = Opcode Opcode
decode insn = | DecodeException Exception
| InstructionException Exception
deriving (Generic, Show, Eq, NFDataX)
decode :: FetchResult -> DecodeResult
decode (Instruction insn) =
case insnToOpcode insn of
Just opcode -> Opcode opcode
Nothing -> DecodeException $ IllegalInstruction insn
decode (Fetch.InstructionException exception) =
Decode.InstructionException exception
insnToOpcode :: Insn -> Maybe Opcode
insnToOpcode insn =
decodeRType insn `orElse` decodeRType insn `orElse`
decodeIType insn `orElse` decodeIType insn `orElse`
decodeSType insn `orElse` decodeSType insn `orElse`
@ -20,31 +35,32 @@ decode insn =
decodeUType insn `orElse` decodeUType insn `orElse`
decodeJType insn decodeJType insn
where where
orElse :: Opcode -> Opcode -> Opcode orElse :: Maybe Opcode -> Maybe Opcode -> Maybe Opcode
orElse Unimplemented y = y orElse (Just left) _ = Just left
orElse x _ = x orElse Nothing (Just right) = Just right
orElse _ _ = Nothing
decodeRType :: Insn -> Opcode decodeRType :: Insn -> Maybe Opcode
decodeRType insn = decodeRType insn =
case opcode of case opcode of
0b0110011 -> 0b0110011 ->
case funct3 of case funct3 of
0x00 -> case funct7 of 0x00 -> case funct7 of
0x00 -> ADD (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x00 -> Just $ ADD (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x20 -> SUB (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x20 -> Just $ SUB (RTypeFields opcode rd funct3 rs1 rs2 funct7)
_ -> Unimplemented _ -> Nothing
0x04 -> XOR (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x04 -> Just $ XOR (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x06 -> OR (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x06 -> Just $ OR (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x07 -> AND (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x07 -> Just $ AND (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x01 -> SLL (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x01 -> Just $ SLL (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x05 -> case funct7 of 0x05 -> case funct7 of
0x00 -> SRL (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x00 -> Just $ SRL (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x20 -> SRA (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x20 -> Just $ SRA (RTypeFields opcode rd funct3 rs1 rs2 funct7)
_ -> Unimplemented _ -> Nothing
0x02 -> SLT (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x02 -> Just $ SLT (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x03 -> SLTU (RTypeFields opcode rd funct3 rs1 rs2 funct7) 0x03 -> Just $ SLTU (RTypeFields opcode rd funct3 rs1 rs2 funct7)
_ -> Unimplemented _ -> Nothing
_ -> Unimplemented _ -> Nothing
where where
opcode = getOpcode insn opcode = getOpcode insn
rd = getRd insn rd = getRd insn
@ -53,42 +69,42 @@ decodeRType insn =
rs2 = getRs2 insn rs2 = getRs2 insn
funct7 = getFunct7 insn funct7 = getFunct7 insn
decodeIType :: Insn -> Opcode decodeIType :: Insn -> Maybe Opcode
decodeIType insn = case opcode of decodeIType insn = case opcode of
0b0010011 -> case funct3 of 0b0010011 -> case funct3 of
0x0 -> ADDI (ITypeFields opcode rd funct3 rs1 imm) 0x0 -> Just $ ADDI (ITypeFields opcode rd funct3 rs1 imm)
0x4 -> XORI (ITypeFields opcode rd funct3 rs1 imm) 0x4 -> Just $ XORI (ITypeFields opcode rd funct3 rs1 imm)
0x6 -> ORI (ITypeFields opcode rd funct3 rs1 imm) 0x6 -> Just $ ORI (ITypeFields opcode rd funct3 rs1 imm)
0x7 -> ANDI (ITypeFields opcode rd funct3 rs1 imm) 0x7 -> Just $ ANDI (ITypeFields opcode rd funct3 rs1 imm)
0x1 -> if slice d31 d25 (pack insn) == 0 0x1 -> if slice d31 d25 (pack insn) == 0
then SLLI (ITypeFields opcode rd funct3 rs1 imm) then Just $ SLLI (ITypeFields opcode rd funct3 rs1 imm)
else Unimplemented 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 -> SRLI (ITypeFields opcode rd funct3 rs1 imm) 0x00 -> Just $ SRLI (ITypeFields opcode rd funct3 rs1 imm)
0x20 -> SRAI (ITypeFields opcode rd funct3 rs1 imm) 0x20 -> Just $ SRAI (ITypeFields opcode rd funct3 rs1 imm)
_ -> Unimplemented _ -> Nothing
0x2 -> SLTI (ITypeFields opcode rd funct3 rs1 imm) 0x2 -> Just $ SLTI (ITypeFields opcode rd funct3 rs1 imm)
0x3 -> SLTIU (ITypeFields opcode rd funct3 rs1 imm) 0x3 -> Just $ SLTIU (ITypeFields opcode rd funct3 rs1 imm)
_ -> Unimplemented _ -> Nothing
0b0000011 -> case funct3 of 0b0000011 -> case funct3 of
0x0 -> LB (ITypeFields opcode rd funct3 rs1 imm) 0x0 -> Just $ LB (ITypeFields opcode rd funct3 rs1 imm)
0x1 -> LH (ITypeFields opcode rd funct3 rs1 imm) 0x1 -> Just $ LH (ITypeFields opcode rd funct3 rs1 imm)
0x2 -> LW (ITypeFields opcode rd funct3 rs1 imm) 0x2 -> Just $ LW (ITypeFields opcode rd funct3 rs1 imm)
0x4 -> LBU (ITypeFields opcode rd funct3 rs1 imm) 0x4 -> Just $ LBU (ITypeFields opcode rd funct3 rs1 imm)
0x5 -> LHU (ITypeFields opcode rd funct3 rs1 imm) 0x5 -> Just $ LHU (ITypeFields opcode rd funct3 rs1 imm)
_ -> Unimplemented _ -> Nothing
0b1100111 -> case funct3 of 0b1100111 -> case funct3 of
0x0 -> JALR (ITypeFields opcode rd funct3 rs1 imm) 0x0 -> Just $ JALR (ITypeFields opcode rd funct3 rs1 imm)
_ -> Unimplemented _ -> Nothing
0b1110011 -> case imm of 0b1110011 -> case imm of
0x000 -> ECALL (ITypeFields opcode rd funct3 rs1 imm) 0x000 -> Just $ ECALL (ITypeFields opcode rd funct3 rs1 imm)
0x001 -> EBREAK (ITypeFields opcode rd funct3 rs1 imm) 0x001 -> Just $ EBREAK (ITypeFields opcode rd funct3 rs1 imm)
_ -> Unimplemented _ -> Nothing
_ -> Unimplemented _ -> Nothing
where where
opcode = getOpcode insn opcode = getOpcode insn
rd = getRd insn rd = getRd insn
@ -96,15 +112,15 @@ decodeIType insn = case opcode of
rs1 = getRs1 insn rs1 = getRs1 insn
imm = getImm12 insn imm = getImm12 insn
decodeSType :: Insn -> Opcode decodeSType :: Insn -> Maybe Opcode
decodeSType insn = decodeSType insn =
case opcode of case opcode of
0b0100011 -> case funct3 of 0b0100011 -> case funct3 of
0x0 -> SB (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Byte 0x0 -> Just $ SB (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Byte
0x1 -> SH (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Halfword 0x1 -> Just $ SH (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Halfword
0x2 -> SW (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Word 0x2 -> Just $ SW (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Word
_ -> Unimplemented _ -> Nothing
_ -> Unimplemented _ -> Nothing
where where
opcode = getOpcode insn opcode = getOpcode insn
funct3 = getFunct3 insn funct3 = getFunct3 insn
@ -112,18 +128,18 @@ decodeSType insn =
rs2 = getRs2 insn rs2 = getRs2 insn
imm12 = getImm12SType insn imm12 = getImm12SType insn
decodeBType :: Insn -> Opcode decodeBType :: Insn -> Maybe Opcode
decodeBType insn = decodeBType insn =
case opcode of case opcode of
0b1100011 -> case funct3 of 0b1100011 -> case funct3 of
0x0 -> BEQ (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if equal 0x0 -> Just $ BEQ (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if equal
0x1 -> BNE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if not equal 0x1 -> Just $ BNE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if not equal
0x4 -> BLT (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than 0x4 -> Just $ BLT (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than
0x5 -> BGE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal 0x5 -> Just $ BGE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal
0x6 -> BLTU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than (unsigned) 0x6 -> Just $ BLTU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than (unsigned)
0x7 -> BGEU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal (unsigned) 0x7 -> Just $ BGEU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal (unsigned)
_ -> Unimplemented _ -> Nothing
_ -> Unimplemented _ -> Nothing
where where
opcode = getOpcode insn opcode = getOpcode insn
funct3 = getFunct3 insn funct3 = getFunct3 insn
@ -131,11 +147,11 @@ decodeBType insn =
rs2 = getRs2 insn rs2 = getRs2 insn
imm13 = getImm13BType insn imm13 = getImm13BType insn
decodeUType :: Insn -> Opcode decodeUType :: Insn -> Maybe Opcode
decodeUType insn = case opcode of decodeUType insn = case opcode of
0b0110111 -> LUI (UTypeFields opcode rd imm20) -- LUI 0b0110111 -> Just $ LUI (UTypeFields opcode rd imm20) -- LUI
0b0010111 -> AUIPC (UTypeFields opcode rd imm20) -- AUIPC 0b0010111 -> Just $ AUIPC (UTypeFields opcode rd imm20) -- AUIPC
_ -> Unimplemented _ -> Nothing
where where
opcode = getOpcode insn opcode = getOpcode insn
rd = getRd insn rd = getRd insn
@ -150,11 +166,11 @@ getImm21JType instr = bitCoerce $ imm20 ++# imm10_1 ++# imm11 ++# imm19_12 ++# z
imm19_12 = slice d19 d12 (pack instr) -- imm[19:12] imm19_12 = slice d19 d12 (pack instr) -- imm[19:12]
zero = 0 :: BitVector 1 -- LSB always zero for J-type zero = 0 :: BitVector 1 -- LSB always zero for J-type
decodeJType :: Insn -> Opcode decodeJType :: Insn -> Maybe Opcode
decodeJType insn = decodeJType insn =
case opcode of case opcode of
0b1101111 -> JAL (JTypeFields opcode rd imm21) -- JAL 0b1101111 -> Just $ JAL (JTypeFields opcode rd imm21) -- JAL
_ -> Unimplemented _ -> Nothing
where where
opcode = getOpcode insn opcode = getOpcode insn
rd = getRd insn rd = getRd insn

2
hs/DecodeTypes.hs
View file

@ -83,6 +83,4 @@ data Opcode
-- U-Type -- U-Type
| LUI UTypeFields | LUI UTypeFields
| AUIPC UTypeFields | AUIPC UTypeFields
| Unimplemented
deriving (Generic, Show, Eq, NFDataX) deriving (Generic, Show, Eq, NFDataX)

103
hs/Exceptions.hs
View file

@ -8,6 +8,7 @@ module Exceptions(
) where ) where
import Clash.Prelude import Clash.Prelude
import Types(Addr, Insn)
data Exception = data Exception =
SupervisorSoftwareInterrupt SupervisorSoftwareInterrupt
@ -17,9 +18,9 @@ data Exception =
| SupervisorExternalInterrupt | SupervisorExternalInterrupt
| MachineExternalInterrupt | MachineExternalInterrupt
| CounterOverflowInterrupt | CounterOverflowInterrupt
| InstructionAddressMisaligned | InstructionAddressMisaligned Addr
| InstructionAccessFault | InstructionAccessFault Addr
| IllegalInstruction | IllegalInstruction Insn
| Breakpoint | Breakpoint
| LoadAddressMisaligned | LoadAddressMisaligned
| LoadAccessFault | LoadAccessFault
@ -37,53 +38,53 @@ data Exception =
deriving (Generic, Show, Eq, NFDataX) deriving (Generic, Show, Eq, NFDataX)
exceptionCode :: Exception -> Unsigned 6 exceptionCode :: Exception -> Unsigned 6
exceptionCode SupervisorSoftwareInterrupt = 1 exceptionCode SupervisorSoftwareInterrupt = 1
exceptionCode MachineSoftwareInterrupt = 3 exceptionCode MachineSoftwareInterrupt = 3
exceptionCode SupervisorTimerInterrupt = 5 exceptionCode SupervisorTimerInterrupt = 5
exceptionCode MachineTimerInterrupt = 7 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
exceptionCode LoadAccessFault = 5 exceptionCode LoadAccessFault = 5
exceptionCode StoreAMOAddressMisaligned = 6 exceptionCode StoreAMOAddressMisaligned = 6
exceptionCode StoreAMOAccessFault = 7 exceptionCode StoreAMOAccessFault = 7
exceptionCode EnvironmentCallFromUMode = 8 exceptionCode EnvironmentCallFromUMode = 8
exceptionCode EnvironmentCallFromSMode = 9 exceptionCode EnvironmentCallFromSMode = 9
exceptionCode EnvironmentCallFromMMode = 11 exceptionCode EnvironmentCallFromMMode = 11
exceptionCode InstructionPageFault = 12 exceptionCode InstructionPageFault = 12
exceptionCode LoadPageFault = 13 exceptionCode LoadPageFault = 13
exceptionCode StoreAMOPageFault = 15 exceptionCode StoreAMOPageFault = 15
exceptionCode DoubleTrap = 16 exceptionCode DoubleTrap = 16
exceptionCode SoftwareCheck = 18 exceptionCode SoftwareCheck = 18
exceptionCode HardwareError = 19 exceptionCode HardwareError = 19
isSynchronousException :: Exception -> Bool isSynchronousException :: Exception -> Bool
isSynchronousException SupervisorSoftwareInterrupt = False isSynchronousException SupervisorSoftwareInterrupt = False
isSynchronousException MachineSoftwareInterrupt = False isSynchronousException MachineSoftwareInterrupt = False
isSynchronousException SupervisorTimerInterrupt = False isSynchronousException SupervisorTimerInterrupt = False
isSynchronousException MachineTimerInterrupt = False 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
isSynchronousException LoadAccessFault = True isSynchronousException LoadAccessFault = True
isSynchronousException StoreAMOAddressMisaligned = True isSynchronousException StoreAMOAddressMisaligned = True
isSynchronousException StoreAMOAccessFault = True isSynchronousException StoreAMOAccessFault = True
isSynchronousException EnvironmentCallFromUMode = True isSynchronousException EnvironmentCallFromUMode = True
isSynchronousException EnvironmentCallFromSMode = True isSynchronousException EnvironmentCallFromSMode = True
isSynchronousException EnvironmentCallFromMMode = True isSynchronousException EnvironmentCallFromMMode = True
isSynchronousException InstructionPageFault = True isSynchronousException InstructionPageFault = True
isSynchronousException LoadPageFault = True isSynchronousException LoadPageFault = True
isSynchronousException StoreAMOPageFault = True isSynchronousException StoreAMOPageFault = True
isSynchronousException DoubleTrap = True isSynchronousException DoubleTrap = True
isSynchronousException SoftwareCheck = True isSynchronousException SoftwareCheck = True
isSynchronousException HardwareError = True isSynchronousException HardwareError = True

20
hs/Fetch.hs
View file

@ -3,10 +3,12 @@
module Fetch( module Fetch(
fetchInstruction, fetchInstruction,
debugInsn,
FetchResult(..), FetchResult(..),
) where ) where
import Clash.Prelude import Clash.Prelude
import qualified Prelude as P
import Types(Addr, Insn) import Types(Addr, Insn)
import Bus(read) import Bus(read)
import Bus(Peripherals(..)) import Bus(Peripherals(..))
@ -19,6 +21,7 @@ import Exceptions(Exception(..))
data FetchResult = Instruction Insn data FetchResult = Instruction Insn
| InstructionException Exception | InstructionException Exception
deriving (Generic, Show, Eq, NFDataX)
fetchInstruction :: Peripherals -> Addr -> IO FetchResult fetchInstruction :: Peripherals -> Addr -> IO FetchResult
fetchInstruction peripherals addr = fetchInstruction peripherals addr =
@ -28,8 +31,19 @@ fetchInstruction peripherals addr =
Right (BusFullWord insn) -> Right (BusFullWord insn) ->
pure $ Instruction insn pure $ Instruction insn
Left UnAligned -> Left UnAligned ->
pure $ InstructionException InstructionAddressMisaligned pure $ InstructionException (InstructionAddressMisaligned addr)
Left UnMapped -> Left UnMapped ->
pure $ InstructionException InstructionAccessFault pure $ InstructionException (InstructionAccessFault addr)
Right _ -> Right _ ->
pure $ InstructionException InstructionAccessFault pure $ InstructionException (InstructionAccessFault addr)
debugInsn :: FetchResult -> String
debugInsn fetchResult =
case fetchResult of
Instruction insn ->
"Instruction raw binary | "
P.++ binaryInsn
P.++ " (" P.++ show insn P.++ ")"
where
binaryInsn = show (bitCoerce insn :: BitVector 32)
InstructionException e -> show e

18
hs/Simulation.hs
View file

@ -11,7 +11,6 @@ module Simulation(
Simulation(..) Simulation(..)
) where ) where
import qualified Prelude as P
import Peripherals.Setup(setupPeripherals, InitializedPeripherals(..)) import Peripherals.Setup(setupPeripherals, InitializedPeripherals(..))
import Peripherals.Teardown(teardownPeripherals) import Peripherals.Teardown(teardownPeripherals)
import Clash.Prelude import Clash.Prelude
@ -19,8 +18,9 @@ import Bus(Peripherals(..))
import Cpu( import Cpu(
RISCVCPU(..), RISCVCPU(..),
riscvCPUInit) riscvCPUInit)
import Fetch(fetchInstruction, FetchResult (..)) import Fetch(fetchInstruction, debugInsn)
import Decode(decode) import Decode(decode)
import qualified Prelude as P
data Args = Args { data Args = Args {
firmware :: FilePath firmware :: FilePath
@ -36,17 +36,6 @@ data Machine = Machine
} }
deriving (Generic, Show, Eq, NFDataX) deriving (Generic, Show, Eq, NFDataX)
debugInsn :: FetchResult -> String
debugInsn fetchResult =
case fetchResult of
Instruction insn ->
"Decoded instruction: " P.++ show opcode
P.++ " | Binary: " P.++ binaryInsn
P.++ " (" P.++ show insn P.++ ")"
where
binaryInsn = show (bitCoerce insn :: BitVector 32)
opcode = decode insn
InstructionException e -> show e
simulationLoop :: Int -> Machine -> IO [Machine] simulationLoop :: Int -> Machine -> IO [Machine]
simulationLoop 0 machine = return [machine] simulationLoop 0 machine = return [machine]
@ -54,7 +43,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
putStrLn $ debugInsn fetchResult let decodeResult = decode 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' }