forked from Yehowshua/RiscV-Formal
getting closer...
This commit is contained in:
parent
32932f4816
commit
f9248057f9
|
@ -12,18 +12,23 @@ import Data.Maybe (listToMaybe)
|
||||||
import Data.List (isPrefixOf)
|
import Data.List (isPrefixOf)
|
||||||
import Text.Show.Pretty (ppShow)
|
import Text.Show.Pretty (ppShow)
|
||||||
|
|
||||||
import Simulation (simulation, Args(..))
|
import Simulation (simulation, Args(..), Simulation(..))
|
||||||
|
|
||||||
main :: IO ()
|
main :: IO ()
|
||||||
main = do
|
main = do
|
||||||
rawArgs <- getArgs
|
rawArgs <- getArgs
|
||||||
args <- parseArgs rawArgs
|
args <- parseArgs rawArgs
|
||||||
states <- simulation args
|
simResult <- simulation args
|
||||||
putStrLn "Simulating Machine"
|
putStrLn "Simulating Machine"
|
||||||
|
case simResult of
|
||||||
|
Success states -> do
|
||||||
-- mapM_ (putStrLn . ppShow) states -- Uncomment to print each state, if needed.
|
-- mapM_ (putStrLn . ppShow) states -- Uncomment to print each state, if needed.
|
||||||
putStrLn $ "Last state: " ++ show (last states)
|
putStrLn $ "Last state: " ++ show (last states)
|
||||||
putStrLn $ "Executed for " ++ show (length states) ++ " cycles"
|
putStrLn $ "Executed for " ++ show (length states) ++ " cycles"
|
||||||
putStrLn "Simulation complete"
|
putStrLn "Simulation complete"
|
||||||
|
Failure err -> do
|
||||||
|
putStrLn $ "Simulation failed: " ++ err
|
||||||
|
exitFailure
|
||||||
|
|
||||||
-- Function to parse command line arguments into the Args data type
|
-- Function to parse command line arguments into the Args data type
|
||||||
parseArgs :: [String] -> IO Args
|
parseArgs :: [String] -> IO Args
|
||||||
|
|
|
@ -1,7 +1,9 @@
|
||||||
{-# LANGUAGE DataKinds #-}
|
{-# LANGUAGE DataKinds #-}
|
||||||
{-# LANGUAGE NumericUnderscores #-}
|
{-# LANGUAGE NumericUnderscores #-}
|
||||||
|
|
||||||
module Fetch(fetchInstruction) where
|
module Fetch(
|
||||||
|
fetchInstruction,
|
||||||
|
FetchResult(..)) where
|
||||||
|
|
||||||
import Clash.Prelude
|
import Clash.Prelude
|
||||||
import Types(Mem, Addr, Insn)
|
import Types(Mem, Addr, Insn)
|
||||||
|
|
|
@ -4,12 +4,14 @@
|
||||||
module Machine(
|
module Machine(
|
||||||
Machine(..),
|
Machine(..),
|
||||||
RISCVCPU(..),
|
RISCVCPU(..),
|
||||||
|
Peripherals(..),
|
||||||
Endian(..),
|
Endian(..),
|
||||||
machineInit) where
|
machineInit) where
|
||||||
|
|
||||||
import Clash.Prelude
|
import Clash.Prelude
|
||||||
import Types(Pc, Mem)
|
import Types(Pc, Mem)
|
||||||
import RegFiles(GPR, FPR, CSR, gprInit, fprInit, csrInit)
|
import RegFiles(GPR, FPR, CSR, gprInit, fprInit, csrInit)
|
||||||
|
import Peripherals.Ram(Ram)
|
||||||
|
|
||||||
data Endian = Big | Little
|
data Endian = Big | Little
|
||||||
deriving (Generic, Show, Eq, NFDataX)
|
deriving (Generic, Show, Eq, NFDataX)
|
||||||
|
@ -20,6 +22,12 @@ data PrivilegeLevel
|
||||||
| UserMode
|
| UserMode
|
||||||
deriving (Generic, Show, Eq, NFDataX)
|
deriving (Generic, Show, Eq, NFDataX)
|
||||||
|
|
||||||
|
data Peripherals = Peripherals
|
||||||
|
{
|
||||||
|
ram :: Ram
|
||||||
|
}
|
||||||
|
deriving (Generic, Show, Eq, NFDataX)
|
||||||
|
|
||||||
data RISCVCPU = RISCVCPU
|
data RISCVCPU = RISCVCPU
|
||||||
{ pc :: Pc,
|
{ pc :: Pc,
|
||||||
gpr :: GPR,
|
gpr :: GPR,
|
||||||
|
@ -30,7 +38,7 @@ data RISCVCPU = RISCVCPU
|
||||||
|
|
||||||
data Machine = Machine
|
data Machine = Machine
|
||||||
{ cpu :: RISCVCPU,
|
{ cpu :: RISCVCPU,
|
||||||
mem :: Mem 14
|
peripherals :: Peripherals
|
||||||
}
|
}
|
||||||
deriving (Generic, Show, Eq, NFDataX)
|
deriving (Generic, Show, Eq, NFDataX)
|
||||||
|
|
||||||
|
@ -42,11 +50,11 @@ riscvCPUInit =
|
||||||
fprInit
|
fprInit
|
||||||
MachineMode
|
MachineMode
|
||||||
|
|
||||||
machineInit :: Machine
|
machineInit :: Peripherals -> Machine
|
||||||
machineInit =
|
machineInit peripherals =
|
||||||
Machine
|
Machine
|
||||||
riscvCPUInit
|
riscvCPUInit
|
||||||
memInit
|
peripherals
|
||||||
|
|
||||||
memInit :: Vec 14 (Unsigned 32)
|
memInit :: Vec 14 (Unsigned 32)
|
||||||
memInit =
|
memInit =
|
||||||
|
|
|
@ -3,7 +3,7 @@
|
||||||
{-# LANGUAGE OverloadedStrings #-}
|
{-# LANGUAGE OverloadedStrings #-}
|
||||||
{-# LANGUAGE TemplateHaskell #-}
|
{-# LANGUAGE TemplateHaskell #-}
|
||||||
|
|
||||||
module Peripherals.Ram() where
|
module Peripherals.Ram(initRamFromFile, Ram) where
|
||||||
|
|
||||||
import Clash.Prelude
|
import Clash.Prelude
|
||||||
import qualified Prelude as P
|
import qualified Prelude as P
|
||||||
|
|
|
@ -1,8 +1,29 @@
|
||||||
module Peripherals.Setup (setupPeripherals) where
|
module Peripherals.Setup (
|
||||||
|
setupPeripherals, InitializedPeripherals(..)
|
||||||
|
) where
|
||||||
|
|
||||||
import Prelude
|
import Prelude
|
||||||
import Peripherals.UartCFFI(initTerminal)
|
import Peripherals.UartCFFI(initTerminal)
|
||||||
|
import Peripherals.Ram (initRamFromFile, Ram)
|
||||||
|
import Control.Exception (try)
|
||||||
|
import System.IO.Error (ioeGetErrorString)
|
||||||
|
|
||||||
setupPeripherals :: IO ()
|
type FirmwareFilePath = FilePath
|
||||||
setupPeripherals = do
|
|
||||||
|
data InitializedPeripherals
|
||||||
|
= InitializedPeripherals Ram
|
||||||
|
| InitializationError String
|
||||||
|
deriving (Show)
|
||||||
|
|
||||||
|
setupPeripherals :: FirmwareFilePath -> IO InitializedPeripherals
|
||||||
|
setupPeripherals firmwareFilePath = do
|
||||||
initTerminal
|
initTerminal
|
||||||
|
result <- try (initRamFromFile firmwareFilePath)
|
||||||
|
|
||||||
|
return $ case result of
|
||||||
|
Right (Just ram) -> InitializedPeripherals ram
|
||||||
|
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?"
|
||||||
|
|
|
@ -3,49 +3,66 @@
|
||||||
{-# LANGUAGE TypeOperators #-}
|
{-# LANGUAGE TypeOperators #-}
|
||||||
{-# LANGUAGE ConstraintKinds #-}
|
{-# LANGUAGE ConstraintKinds #-}
|
||||||
|
|
||||||
module Simulation(Args(..), simulation) where
|
module Simulation(Args(..), simulation, Simulation(..)) where
|
||||||
|
|
||||||
import Peripherals.Setup(setupPeripherals)
|
import qualified Prelude as P
|
||||||
|
import Peripherals.Setup(setupPeripherals, InitializedPeripherals(..))
|
||||||
import Peripherals.Teardown(teardownPeripherals)
|
import Peripherals.Teardown(teardownPeripherals)
|
||||||
import Text.Printf (printf)
|
import Text.Printf (printf)
|
||||||
import Clash.Prelude
|
import Clash.Prelude
|
||||||
import Machine(
|
import Machine(
|
||||||
Machine(..),
|
Machine(..),
|
||||||
RISCVCPU(..),
|
RISCVCPU(..),
|
||||||
|
Peripherals(..),
|
||||||
machineInit, RISCVCPU (RISCVCPU))
|
machineInit, RISCVCPU (RISCVCPU))
|
||||||
import Fetch(fetchInstruction)
|
import Fetch(fetchInstruction, FetchResult (Instruction, Misaligned))
|
||||||
|
import Isa.Decode(decode)
|
||||||
|
import Isa.Forms(Opcode(..))
|
||||||
import Peripherals.UartCFFI(writeCharToTerminal)
|
import Peripherals.UartCFFI(writeCharToTerminal)
|
||||||
import Control.Concurrent (threadDelay)
|
import Control.Concurrent (threadDelay)
|
||||||
|
|
||||||
import Debug.Trace
|
import Debug.Trace
|
||||||
|
import Types (Mem, Addr)
|
||||||
|
|
||||||
data Args = Args {
|
data Args = Args {
|
||||||
firmware :: FilePath
|
firmware :: FilePath
|
||||||
} deriving (Show)
|
} deriving (Show)
|
||||||
|
|
||||||
machine :: Machine
|
data Simulation
|
||||||
machine = machineInit
|
= Success [Machine]
|
||||||
|
| Failure String
|
||||||
|
deriving (Show)
|
||||||
|
|
||||||
|
-- machine :: Machine
|
||||||
|
-- machine = machineInit
|
||||||
|
|
||||||
machine' :: Machine -> Machine
|
machine' :: Machine -> Machine
|
||||||
machine' machine =
|
machine' machine =
|
||||||
let
|
let
|
||||||
-- instruction =
|
machinePeripherals = peripherals machine
|
||||||
-- traceShow
|
machineMem = ram $ machinePeripherals
|
||||||
-- (printf "0x%X" (toInteger v) :: String)
|
|
||||||
-- v
|
|
||||||
-- where v = fetchInstruction mem msr pc
|
|
||||||
-- instruction = traceShow (bitpatToOpcode v) v
|
|
||||||
-- where v = fetchInstruction machineMem machinePC
|
|
||||||
machineMem = mem machine
|
|
||||||
machineCPU = cpu machine
|
machineCPU = cpu machine
|
||||||
machinePC = pc machineCPU
|
machinePC = pc machineCPU
|
||||||
instruction = fetchInstruction machineMem machinePC
|
|
||||||
addr = 0 :: Integer
|
addr = 0 :: Integer
|
||||||
-- execute would go here, but right now, we simply
|
|
||||||
mem' = replace addr (3) machineMem
|
mem' = replace addr (3) machineMem
|
||||||
|
peripherals' = machinePeripherals { ram = mem' }
|
||||||
cpu' = machineCPU { pc = machinePC + 4 }
|
cpu' = machineCPU { pc = machinePC + 4 }
|
||||||
|
|
||||||
|
instruction =
|
||||||
|
case (fetchInstruction machineMem machinePC) of
|
||||||
|
Instruction i -> i
|
||||||
|
_ -> undefined
|
||||||
in
|
in
|
||||||
machine { cpu = cpu', mem = mem' }
|
case (fetchInstruction machineMem machinePC) of
|
||||||
|
Instruction insn ->
|
||||||
|
let binaryInsn = show (bitCoerce insn :: BitVector 32)
|
||||||
|
in trace ("Decoded instruction: " P.++ show opcode
|
||||||
|
P.++ " | Binary: " P.++ binaryInsn
|
||||||
|
P.++ " (" P.++ show insn P.++ ")") $
|
||||||
|
machine { cpu = cpu', peripherals = peripherals' }
|
||||||
|
where
|
||||||
|
opcode = decode insn
|
||||||
|
Misaligned addr -> undefined
|
||||||
|
|
||||||
simulationLoop :: Int -> Machine -> IO [Machine]
|
simulationLoop :: Int -> Machine -> IO [Machine]
|
||||||
simulationLoop 0 state = return [state]
|
simulationLoop 0 state = return [state]
|
||||||
|
@ -54,15 +71,14 @@ simulationLoop n state = do
|
||||||
rest <- simulationLoop (n - 1) newState
|
rest <- simulationLoop (n - 1) newState
|
||||||
return (state : rest)
|
return (state : rest)
|
||||||
|
|
||||||
simulation :: Args -> IO [Machine]
|
simulation :: Args -> IO Simulation
|
||||||
simulation args = do
|
simulation args = do
|
||||||
setupPeripherals
|
initializedPeripherals <- setupPeripherals (firmware args)
|
||||||
|
case initializedPeripherals of
|
||||||
|
InitializationError e -> return $ Failure e
|
||||||
|
InitializedPeripherals ram -> do
|
||||||
|
|
||||||
-- quick smoketest that UART works - remove later
|
let initState = machineInit $ Machine.Peripherals ram
|
||||||
writeCharToTerminal 'a'
|
|
||||||
threadDelay 1000000 -- Delay for 1 second (1,000,000 microseconds)
|
|
||||||
|
|
||||||
let initState = machine
|
|
||||||
sim <- simulationLoop 5 initState
|
sim <- simulationLoop 5 initState
|
||||||
teardownPeripherals
|
teardownPeripherals
|
||||||
return sim
|
return $ Success sim
|
||||||
|
|
|
@ -23,9 +23,13 @@ $(ELF): $(SRC) $(LDSCRIPT)
|
||||||
$(AS) $(ARCH_FLAGS) -o $(OBJ) $(SRC)
|
$(AS) $(ARCH_FLAGS) -o $(OBJ) $(SRC)
|
||||||
$(LD) -T $(LDSCRIPT) -o $(ELF) $(OBJ)
|
$(LD) -T $(LDSCRIPT) -o $(ELF) $(OBJ)
|
||||||
|
|
||||||
# Convert ELF to raw binary
|
# Convert ELF to raw binary and pad to the next multiple of 4 bytes
|
||||||
$(BIN): $(ELF)
|
$(BIN): $(ELF)
|
||||||
$(OBJCOPY) -O binary $(ELF) $(BIN)
|
$(OBJCOPY) -O binary $(ELF) $(BIN)
|
||||||
|
# Pad the binary to a multiple of 4 bytes
|
||||||
|
size=$$(stat -f%z $(BIN)); \
|
||||||
|
padding=$$(( (4 - (size % 4)) % 4 )); \
|
||||||
|
[ $$padding -ne 0 ] && dd if=/dev/zero bs=1 count=$$padding >> $(BIN) || true
|
||||||
|
|
||||||
# Run in QEMU
|
# Run in QEMU
|
||||||
run: $(BIN)
|
run: $(BIN)
|
||||||
|
|
Loading…
Reference in a new issue