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

Replacing $ operator with more readable |> operator

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-03-06 08:41:00 -05:00
parent 2b1c486c17
commit 0792bf3c7d
12 changed files with 122 additions and 101 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
hs/Bus.hs
View file

@ -20,6 +20,8 @@ import BusTypes(
)
import Types(Addr)
import Peripherals.Ram(write, bytesInRam)
import Util((|>))
data Peripherals = Peripherals
{
@ -52,12 +54,12 @@ alignCheck addr SizeQuadWord = addr `mod` 16 == 0
-- from/to stdin/stdout, so we need IO.
read :: ReadRequest -> Peripherals -> IO ReadResponse
read (Request addr size) peripherals
| not (alignCheck addr size) = return $ Left UnAligned
| not (alignCheck addr size) = return |> Left UnAligned
| (addr >= ramStart) && (addr <= ramEnd) =
return $ Right $ Peripherals.Ram.read size ramAddr (ram peripherals)
return |> Right |> Peripherals.Ram.read size ramAddr (ram peripherals)
| (addr >= uartStart) && (addr <= uartEnd) =
Right <$> Peripherals.Uart.read size uartAddr
| otherwise = return $ Left UnMapped
fmap Right (Peripherals.Uart.read size uartAddr)
| otherwise = return |> Left UnMapped
where
ramAddrNoOffset = addr - ramStart
ramAddr :: RamAddr
@ -69,17 +71,17 @@ read (Request addr size) peripherals
write :: BusVal -> Addr -> Peripherals -> IO WriteResponse
write val addr peripherals
| not (alignCheck addr $ busValToTransactionSize val) = return $ Left UnAligned
| not (alignCheck addr |> busValToTransactionSize val) = return |> Left UnAligned
| (addr >= uartStart) && (addr <= uartEnd) =
do
Peripherals.Uart.write val uartAddr
return $ Right peripherals
return |> Right peripherals
| (addr >= ramStart) && (addr <= ramEnd) =
return $ Right $
return |> Right |>
peripherals {
ram = Peripherals.Ram.write val ramAddr (ram peripherals)
}
| otherwise = return $ Left UnMapped
| otherwise = return |> Left UnMapped
where
ramAddrNoOffset = addr - ramStart
ramAddr :: RamAddr

3
hs/BusTypes.hs
View file

@ -7,10 +7,9 @@ module BusTypes(
) where
import Clash.Prelude
import Types(Addr,
Byte, HalfWord, FullWord, DoubleWord, QuadWord)
import Util((|>))
data BusError
= UnMapped
| UnAligned

103
hs/Decode.hs
View file

@ -12,6 +12,7 @@ import Clash.Prelude
import Fetch(FetchResult (Instruction, InstructionException))
import Exceptions(Exception(..))
import Types(Insn)
import Util((|>))
data DecodeResult = Opcode Opcode
| DecodeException Exception
@ -22,7 +23,7 @@ decode :: FetchResult -> DecodeResult
decode (Instruction insn) =
case insnToOpcode insn of
Just opcode -> Opcode opcode
Nothing -> DecodeException $ IllegalInstruction insn
Nothing -> DecodeException |> IllegalInstruction insn
decode (Fetch.InstructionException exception) =
Decode.InstructionException exception
@ -46,19 +47,19 @@ decodeRType insn =
0b0110011 ->
case funct3 of
0x00 -> case funct7 of
0x00 -> Just $ ADD (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x20 -> Just $ SUB (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x00 -> Just |> ADD (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x20 -> Just |> SUB (RTypeFields opcode rd funct3 rs1 rs2 funct7)
_ -> Nothing
0x04 -> Just $ XOR (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x06 -> Just $ OR (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x07 -> Just $ AND (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x01 -> Just $ SLL (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x04 -> Just |> XOR (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x06 -> Just |> OR (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x07 -> Just |> AND (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x01 -> Just |> SLL (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x05 -> case funct7 of
0x00 -> Just $ SRL (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x20 -> Just $ SRA (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x00 -> Just |> SRL (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x20 -> Just |> SRA (RTypeFields opcode rd funct3 rs1 rs2 funct7)
_ -> Nothing
0x02 -> Just $ SLT (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x03 -> Just $ SLTU (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x02 -> Just |> SLT (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x03 -> Just |> SLTU (RTypeFields opcode rd funct3 rs1 rs2 funct7)
_ -> Nothing
_ -> Nothing
where
@ -72,36 +73,36 @@ decodeRType insn =
decodeIType :: Insn -> Maybe Opcode
decodeIType insn = case opcode of
0b0010011 -> case funct3 of
0x0 -> Just $ ADDI (ITypeFields opcode rd funct3 rs1 imm)
0x4 -> Just $ XORI (ITypeFields opcode rd funct3 rs1 imm)
0x6 -> Just $ ORI (ITypeFields opcode rd funct3 rs1 imm)
0x7 -> Just $ ANDI (ITypeFields opcode rd funct3 rs1 imm)
0x0 -> Just |> ADDI (ITypeFields opcode rd funct3 rs1 imm)
0x4 -> Just |> XORI (ITypeFields opcode rd funct3 rs1 imm)
0x6 -> Just |> ORI (ITypeFields opcode rd funct3 rs1 imm)
0x7 -> Just |> ANDI (ITypeFields opcode rd funct3 rs1 imm)
0x1 -> if slice d31 d25 (pack insn) == 0
then Just $ SLLI (ITypeFields opcode rd funct3 rs1 imm)
then Just |> SLLI (ITypeFields opcode rd funct3 rs1 imm)
else Nothing
0x5 -> case slice d31 d25 (pack insn) of -- Distinguish SRLI and SRAI
0x00 -> Just $ SRLI (ITypeFields opcode rd funct3 rs1 imm)
0x20 -> Just $ SRAI (ITypeFields opcode rd funct3 rs1 imm)
0x00 -> Just |> SRLI (ITypeFields opcode rd funct3 rs1 imm)
0x20 -> Just |> SRAI (ITypeFields opcode rd funct3 rs1 imm)
_ -> Nothing
0x2 -> Just $ SLTI (ITypeFields opcode rd funct3 rs1 imm)
0x3 -> Just $ SLTIU (ITypeFields opcode rd funct3 rs1 imm)
0x2 -> Just |> SLTI (ITypeFields opcode rd funct3 rs1 imm)
0x3 -> Just |> SLTIU (ITypeFields opcode rd funct3 rs1 imm)
_ -> Nothing
0b0000011 -> case funct3 of
0x0 -> Just $ LB (ITypeFields opcode rd funct3 rs1 imm)
0x1 -> Just $ LH (ITypeFields opcode rd funct3 rs1 imm)
0x2 -> Just $ LW (ITypeFields opcode rd funct3 rs1 imm)
0x4 -> Just $ LBU (ITypeFields opcode rd funct3 rs1 imm)
0x5 -> Just $ LHU (ITypeFields opcode rd funct3 rs1 imm)
0x0 -> Just |> LB (ITypeFields opcode rd funct3 rs1 imm)
0x1 -> Just |> LH (ITypeFields opcode rd funct3 rs1 imm)
0x2 -> Just |> LW (ITypeFields opcode rd funct3 rs1 imm)
0x4 -> Just |> LBU (ITypeFields opcode rd funct3 rs1 imm)
0x5 -> Just |> LHU (ITypeFields opcode rd funct3 rs1 imm)
_ -> Nothing
0b1100111 -> case funct3 of
0x0 -> Just $ JALR (ITypeFields opcode rd funct3 rs1 imm)
0x0 -> Just |> JALR (ITypeFields opcode rd funct3 rs1 imm)
_ -> Nothing
0b1110011 -> case imm of
0x000 -> Just $ ECALL (ITypeFields opcode rd funct3 rs1 imm)
0x001 -> Just $ EBREAK (ITypeFields opcode rd funct3 rs1 imm)
0x000 -> Just |> ECALL (ITypeFields opcode rd funct3 rs1 imm)
0x001 -> Just |> EBREAK (ITypeFields opcode rd funct3 rs1 imm)
_ -> Nothing
_ -> Nothing
@ -116,9 +117,9 @@ decodeSType :: Insn -> Maybe Opcode
decodeSType insn =
case opcode of
0b0100011 -> case funct3 of
0x0 -> Just $ SB (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Byte
0x1 -> Just $ SH (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Halfword
0x2 -> Just $ SW (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Word
0x0 -> Just |> SB (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Byte
0x1 -> Just |> SH (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Halfword
0x2 -> Just |> SW (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Word
_ -> Nothing
_ -> Nothing
where
@ -132,12 +133,12 @@ decodeBType :: Insn -> Maybe Opcode
decodeBType insn =
case opcode of
0b1100011 -> case funct3 of
0x0 -> Just $ BEQ (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if equal
0x1 -> Just $ BNE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if not equal
0x4 -> Just $ BLT (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than
0x5 -> Just $ BGE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal
0x6 -> Just $ BLTU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than (unsigned)
0x7 -> Just $ BGEU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal (unsigned)
0x0 -> Just |> BEQ (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if equal
0x1 -> Just |> BNE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if not equal
0x4 -> Just |> BLT (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than
0x5 -> Just |> BGE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal
0x6 -> Just |> BLTU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than (unsigned)
0x7 -> Just |> BGEU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal (unsigned)
_ -> Nothing
_ -> Nothing
where
@ -149,8 +150,8 @@ decodeBType insn =
decodeUType :: Insn -> Maybe Opcode
decodeUType insn = case opcode of
0b0110111 -> Just $ LUI (UTypeFields opcode rd imm20) -- LUI
0b0010111 -> Just $ AUIPC (UTypeFields opcode rd imm20) -- AUIPC
0b0110111 -> Just |> LUI (UTypeFields opcode rd imm20) -- LUI
0b0010111 -> Just |> AUIPC (UTypeFields opcode rd imm20) -- AUIPC
_ -> Nothing
where
opcode = getOpcode insn
@ -158,7 +159,7 @@ decodeUType insn = case opcode of
imm20 = getImm20UType insn
getImm21JType :: Insn -> Unsigned 21
getImm21JType instr = bitCoerce $ imm20 ++# imm10_1 ++# imm11 ++# imm19_12 ++# zero
getImm21JType instr = bitCoerce |> imm20 ++# imm10_1 ++# imm11 ++# imm19_12 ++# zero
where
imm20 = slice d31 d31 (pack instr) -- imm[20]
imm10_1 = slice d30 d21 (pack instr) -- imm[10:1]
@ -169,7 +170,7 @@ getImm21JType instr = bitCoerce $ imm20 ++# imm10_1 ++# imm11 ++# imm19_12 ++# z
decodeJType :: Insn -> Maybe Opcode
decodeJType insn =
case opcode of
0b1101111 -> Just $ JAL (JTypeFields opcode rd imm21) -- JAL
0b1101111 -> Just |> JAL (JTypeFields opcode rd imm21) -- JAL
_ -> Nothing
where
opcode = getOpcode insn
@ -177,22 +178,22 @@ decodeJType insn =
imm21 = getImm21JType insn
getOpcode :: Insn -> Unsigned 7
getOpcode instr = bitCoerce $ slice d6 d0 (pack instr)
getOpcode instr = bitCoerce |> slice d6 d0 (pack instr)
getImm12 :: Insn -> Unsigned 12
getImm12 instr = bitCoerce $ slice d31 d20 (pack instr)
getImm12 instr = bitCoerce |> slice d31 d20 (pack instr)
getImm12SType :: Insn -> Unsigned 12
getImm12SType instr = bitCoerce $ immediateUpper ++# immediateLower
getImm12SType instr = bitCoerce |> immediateUpper ++# immediateLower
where
immediateUpper = (slice d31 d25 (pack instr))
immediateLower = (slice d11 d7 (pack instr))
getImm20UType :: Insn -> Unsigned 20
getImm20UType instr = bitCoerce $ slice d31 d12 (pack instr)
getImm20UType instr = bitCoerce |> slice d31 d12 (pack instr)
getImm13BType :: Insn -> Unsigned 13
getImm13BType instr = bitCoerce $ imm12 ++# imm10_5 ++# imm4_1 ++# imm11 ++# zero
getImm13BType instr = bitCoerce |> imm12 ++# imm10_5 ++# imm4_1 ++# imm11 ++# zero
where
imm12 = slice d31 d31 (pack instr) -- imm[12]
imm10_5 = slice d30 d25 (pack instr) -- imm[10:5]
@ -201,16 +202,16 @@ getImm13BType instr = bitCoerce $ imm12 ++# imm10_5 ++# imm4_1 ++# imm11 ++# zer
zero = 0 :: BitVector 1 -- LSB always zero for B-type
getFunct3 :: Insn -> Unsigned 3
getFunct3 instr = bitCoerce $ slice d14 d12 (pack instr)
getFunct3 instr = bitCoerce |> slice d14 d12 (pack instr)
getFunct7 :: Insn -> Unsigned 7
getFunct7 instr = bitCoerce $ slice d31 d25 (pack instr)
getFunct7 instr = bitCoerce |> slice d31 d25 (pack instr)
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 instr = bitCoerce $ slice d24 d20 (pack instr)
getRs2 instr = bitCoerce |> slice d24 d20 (pack instr)
getRs1 :: Insn -> Unsigned 5
getRs1 instr = bitCoerce $ slice d19 d15 (pack instr)
getRs1 instr = bitCoerce |> slice d19 d15 (pack instr)

10
hs/Fetch.hs
View file

@ -18,24 +18,26 @@ import BusTypes(
BusVal(..),
BusError(..))
import Exceptions(Exception(..))
import Util((|>))
data FetchResult = Instruction Insn
| InstructionException Exception
deriving (Generic, Show, Eq, NFDataX)
fetchInstruction :: Peripherals -> Addr -> IO FetchResult
fetchInstruction peripherals addr =
do
readReasponse <-Bus.read (BusTypes.Request addr BusTypes.SizeFullWord) peripherals
case readReasponse of
Right (BusFullWord insn) ->
pure $ Instruction insn
pure |> Instruction insn
Left UnAligned ->
pure $ InstructionException (InstructionAddressMisaligned addr)
pure |> InstructionException (InstructionAddressMisaligned addr)
Left UnMapped ->
pure $ InstructionException (InstructionAccessFault addr)
pure |> InstructionException (InstructionAccessFault addr)
Right _ ->
pure $ InstructionException (InstructionAccessFault addr)
pure |> InstructionException (InstructionAccessFault addr)
debugInsn :: FetchResult -> String
debugInsn fetchResult =

19
hs/Peripherals/Ram.hs
View file

@ -24,6 +24,7 @@ import BusTypes(
TransactionSize(..),
BusVal(..),
)
import Util((|>))
-- vector depth has to be known statically at compile time
#ifndef _RAM_DEPTH
@ -38,7 +39,7 @@ bytesInRam :: Addr
bytesInRam = _RAM_DEPTH * 4
read :: TransactionSize -> RamAddr -> Ram -> BusVal
read SizeByte addr ram = BusByte $ unpack byte
read SizeByte addr ram = BusByte |> unpack byte
where
word = ram !! addr
byteOffset :: BitVector 2
@ -49,11 +50,11 @@ read SizeByte addr ram = BusByte $ unpack byte
0b10 -> slice d15 d8 word
0b11 -> slice d7 d0 word
read SizeHalfWord addr ram = BusHalfWord $ unpack halfWord
read SizeHalfWord addr ram = BusHalfWord |> unpack halfWord
where
word = ram !! addr
halfWordOffset :: Unsigned 1
halfWordOffset = unpack $ slice d0 d0 addr
halfWordOffset = unpack |> slice d0 d0 addr
halfWord = case halfWordOffset of
0b0 -> slice d31 d16 word
0b1 -> slice d15 d0 word
@ -64,13 +65,13 @@ read SizeFullWord addr ram = BusFullWord fullWord
read SizeDoubleWord addr ram = BusDoubleWord doubleWord
where
doubleWord = bitCoerce $ bitCoerce word0 ++# bitCoerce word1
doubleWord = bitCoerce |> bitCoerce word0 ++# bitCoerce word1
word0 = readFullWordHelper ram addr
word1 = readFullWordHelper ram (addr + 1)
read SizeQuadWord addr ram = BusQuadWord quadWord
where
quadWord = bitCoerce $ bitCoerce dword0 ++# bitCoerce dword1
quadWord = bitCoerce |> bitCoerce dword0 ++# bitCoerce dword1
dword0 = readDoubleWordHelper ram addr
dword1 = readDoubleWordHelper ram (addr + 2)
@ -78,7 +79,7 @@ readFullWordHelper :: Ram -> RamAddr -> FullWord
readFullWordHelper ram addr = ram !! addr
readDoubleWordHelper :: Ram -> RamAddr -> DoubleWord
readDoubleWordHelper ram addr = bitCoerce $ bitCoerce word0 ++# bitCoerce word1
readDoubleWordHelper ram addr = bitCoerce |> bitCoerce word0 ++# bitCoerce word1
where
word0 = readFullWordHelper ram addr
word1 = readFullWordHelper ram (addr + 1)
@ -99,7 +100,7 @@ write (BusHalfWord halfWord) addr ram = replace addr updatedWord ram
where
word = ram !! addr
halfWordOffset :: Unsigned 1
halfWordOffset = unpack $ slice d0 d0 addr
halfWordOffset = unpack |> slice d0 d0 addr
updatedWord = case halfWordOffset of
0b0 -> setSlice d31 d16 (pack halfWord) word
0b1 -> setSlice d15 d0 (pack halfWord) word
@ -136,7 +137,7 @@ initRamFromFile filePath =
do
bs <- readFileIntoByteString filePath
let ints = getInts bs
pure $ populateVectorFromInt32 ints initRam
pure |> populateVectorFromInt32 ints initRam
readFileIntoByteString :: FilePath -> IO BL.ByteString
readFileIntoByteString filePath = BL.readFile filePath
@ -163,6 +164,6 @@ populateVectorFromInt32 ::
populateVectorFromInt32 ls v = Vec.fromList adjustedLs
where
vecLen = length v
adjustedLs = fromIntegral <$> adjustLength vecLen ls
adjustedLs = fmap fromIntegral (adjustLength vecLen ls)
adjustLength :: Int -> [Int32] -> [Int32]
adjustLength n xs = P.take n (xs P.++ P.repeat 0)

7
hs/Peripherals/Setup.hs
View file

@ -7,6 +7,7 @@ import Peripherals.UartCFFI(initTerminal)
import Peripherals.Ram (initRamFromFile, Ram)
import Control.Exception (try)
import System.IO.Error (ioeGetErrorString)
import Util((|>))
type FirmwareFilePath = FilePath
@ -20,10 +21,10 @@ setupPeripherals firmwareFilePath = do
initTerminal
result <- try (initRamFromFile firmwareFilePath)
return $ case result of
return |> case result of
Right (Just ram) -> InitializedPeripherals ram
Right Nothing -> InitializationError $ firmwareFilePath ++ failure ++ suggestion
Left e -> InitializationError $ firmwareFilePath ++ failure ++ suggestion ++ " Error: " ++ ioeGetErrorString e
Right Nothing -> InitializationError |> firmwareFilePath ++ failure ++ suggestion
Left e -> InitializationError |> firmwareFilePath ++ failure ++ suggestion ++ " Error: " ++ ioeGetErrorString e
where
failure = ": Failed to initialize RAM from file!"
suggestion = " Is the file 4-byte aligned?"

7
hs/Peripherals/Uart.hs
View file

@ -14,6 +14,7 @@ import BusTypes (
TransactionSize(..),
BusVal(..),
)
import Util((|>))
-- based on a 16550 UART which has an address space of 8 bytes
type UartAddr = Unsigned 3
@ -47,7 +48,7 @@ buildRBR = do
-- Reads the Line Status Register (LSR) to check character availability
buildLSR :: IO Byte
buildLSR = do
(char_available :: Byte) <- fromIntegral <$> isCharAvailable
(char_available :: Byte) <- fmap fromIntegral isCharAvailable
-- highly unlikely that we overflow stdout buffer, so we set
-- transmit to always ready
let (transmit_ready :: Byte) = 0b0010_0000
@ -56,8 +57,8 @@ buildLSR = do
-- Updated 'read' function to handle RBR and LSR reads
read :: TransactionSize -> UartAddr -> IO BusVal
read size addr
| addr == rbrAddr = busValFromByte size <$> buildRBR
| addr == lsrAddr = busValFromByte size <$> buildLSR
| addr == rbrAddr = fmap (busValFromByte size) buildRBR
| addr == lsrAddr = fmap (busValFromByte size) buildLSR
| otherwise = return $ busValFromByte size 0x00
extractLowestByte :: BusVal -> Byte

3
hs/Peripherals/UartCFFI.hs
View file

@ -11,6 +11,7 @@ module Peripherals.UartCFFI (
) where
import Prelude
import Util((|>))
import Foreign.C.Types
import Data.Char (chr, ord)
@ -34,7 +35,7 @@ getCharFromTerminal :: IO Char
getCharFromTerminal = fmap (chr . fromEnum) c_getCharFromTerminal
writeCharToTerminal :: Char -> IO ()
writeCharToTerminal char = c_writeCharToTerminal (toEnum $ ord char)
writeCharToTerminal char = c_writeCharToTerminal (toEnum |> ord char)
isCharAvailable :: IO Int
isCharAvailable = fmap fromEnum c_isCharAvailable

21
hs/RegFiles.hs
View file

@ -22,6 +22,7 @@ module RegFiles(
) where
import Clash.Prelude
import Util((|>))
type GPR = Vec 32 (Unsigned 64) -- General Purpose Registers
type FPR = Vec 32 (Unsigned 64) -- Floating Point Registers
@ -64,16 +65,16 @@ csrNameToAddr MIMPID = 0xF13
-- are placeholders to be revisited for proper initialization later.
csrInit :: CSR
csrInit =
replace (csrNameToAddr STVEC) stvec_init
$ replace (csrNameToAddr SEPC) sepc_init
$ replace (csrNameToAddr MSTATUS) mstatus_init
$ replace (csrNameToAddr MISA) misa_init
$ replace (csrNameToAddr MTVEC) mtvec_init
$ replace (csrNameToAddr MEPC) mepc_init
$ replace (csrNameToAddr MVENDORID) mvendorid_init
$ replace (csrNameToAddr MARCHID) marchid_init
$ replace (csrNameToAddr MIMPID) mimpid_init
$ repeat 0
replace (csrNameToAddr STVEC) stvec_init |>
replace (csrNameToAddr SEPC) sepc_init |>
replace (csrNameToAddr MSTATUS) mstatus_init |>
replace (csrNameToAddr MISA) misa_init |>
replace (csrNameToAddr MTVEC) mtvec_init |>
replace (csrNameToAddr MEPC) mepc_init |>
replace (csrNameToAddr MVENDORID) mvendorid_init |>
replace (csrNameToAddr MARCHID) marchid_init |>
replace (csrNameToAddr MIMPID) mimpid_init |>
repeat 0
where
stvec_init = 0x0000000000002000 -- Supervisor mode trap vector base address.
sepc_init = 0x0000000000000000 -- Supervisor Exception PC initial value.

9
hs/Simulation.hs
View file

@ -21,6 +21,7 @@ import Cpu(
import Fetch(fetchInstruction, debugInsn)
import Decode(decode)
import qualified Prelude as P
import Util((|>))
data Args = Args {
firmware :: FilePath
@ -41,10 +42,10 @@ simulationLoop :: Int -> Machine -> IO [Machine]
simulationLoop 0 machine = return [machine]
simulationLoop n machine = do
let machinePeripherals = peripherals machine
currPc = pc $ cpu machine
currPc = pc |> cpu machine
fetchResult <- fetchInstruction machinePeripherals currPc
let decodeResult = decode fetchResult
putStrLn $ show decodeResult P.++ debugInsn fetchResult
putStrLn |> show decodeResult P.++ debugInsn fetchResult
let pc' = currPc + 4
cpu' = (cpu machine) { pc = pc' }
machine' = machine { cpu = cpu' }
@ -56,7 +57,7 @@ simulation :: Args -> IO Simulation
simulation args = do
initializedPeripherals <- setupPeripherals (firmware args)
case initializedPeripherals of
InitializationError e -> return $ Failure e
InitializationError e -> return |> Failure e
InitializedPeripherals ramDevice -> do
let initState =
@ -66,4 +67,4 @@ simulation args = do
}
sim <- simulationLoop 15 initState
teardownPeripherals
return $ Success sim
return |> Success sim

10
hs/Util.hs Normal file
View file

@ -0,0 +1,10 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Util(
(|>),
) where
(|>) :: (a -> b) -> a -> b
f |> x = f x
infixr 0 |>

3
rv_formal.cabal
View file

@ -100,7 +100,8 @@ library
Cpu,
RegFiles,
Fetch,
Exceptions
Exceptions,
Util
c-sources: c/uart_sim_device.c
include-dirs: c
default-language: Haskell2010