RiscV-Formal/hs/Simulation.hs
2025-03-04 23:37:33 -05:00

107 lines
3 KiB
Haskell

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
module Simulation(
Args(..),
simulation,
RISCVCPU(..),
Machine(..),
Simulation(..)
) where
import qualified Prelude as P
import Peripherals.Setup(setupPeripherals, InitializedPeripherals(..))
import Peripherals.Teardown(teardownPeripherals)
import Clash.Prelude
import Bus(Peripherals(..))
import Cpu(
RISCVCPU(..),
riscvCPUInit)
import Fetch(fetchInstruction, FetchResult (Instruction, Misaligned), fetchInstruction1, FetchResult1(..))
import Isa.Decode(decode)
import Debug.Trace
import Types (Insn)
import Control.Monad.RWS (MonadState(put))
data Args = Args {
firmware :: FilePath
} deriving (Show)
data Simulation
= Success [Machine]
| Failure String
deriving (Show)
data Machine = Machine
{ cpu :: RISCVCPU,
peripherals :: Peripherals
}
deriving (Generic, Show, Eq, NFDataX)
machine' :: Machine -> Machine
machine' machine =
let
machinePeripherals = peripherals machine
machineMem = ram $ machinePeripherals
machineCPU = cpu machine
machinePC = pc machineCPU
cpu' = machineCPU { pc = machinePC + 4 }
in
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' }
where
opcode = decode insn
Misaligned addr -> undefined
debugInsn :: FetchResult1 -> String
debugInsn fetchResult =
case fetchResult of
Instruction1 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 0 machine = return [machine]
simulationLoop n machine = do
-- let newState = machine' machine
let machinePeripherals = peripherals machine
currPc = pc $ cpu machine
fetchResult <- fetchInstruction1 machinePeripherals currPc
putStrLn $ debugInsn fetchResult
let pc' = currPc + 4
cpu' = (cpu machine) { pc = pc' }
machine' = machine { cpu = cpu' }
-- let machine' = machine { cpu = cpu $ machine { pc = pc $ cpu machine + 4 } }
rest <- simulationLoop (n - 1) machine'
return (machine : rest)
simulation :: Args -> IO Simulation
simulation args = do
initializedPeripherals <- setupPeripherals (firmware args)
case initializedPeripherals of
InitializationError e -> return $ Failure e
InitializedPeripherals ram -> do
let initState =
Machine {
cpu = riscvCPUInit,
peripherals = Bus.Peripherals ram
}
sim <- simulationLoop 15 initState
teardownPeripherals
return $ Success sim