RiscV-Formal/hs/Simulation.hs

85 lines
2.4 KiB
Haskell
Raw Normal View History

2025-02-13 04:54:15 +00:00
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
2025-02-19 14:06:40 +00:00
module Simulation(Args(..), simulation, Simulation(..)) where
2025-02-13 04:54:15 +00:00
2025-02-19 14:06:40 +00:00
import qualified Prelude as P
import Peripherals.Setup(setupPeripherals, InitializedPeripherals(..))
2025-02-13 04:54:15 +00:00
import Peripherals.Teardown(teardownPeripherals)
import Text.Printf (printf)
import Clash.Prelude
import Machine(
Machine(..),
RISCVCPU(..),
2025-02-19 14:06:40 +00:00
Peripherals(..),
2025-02-13 04:54:15 +00:00
machineInit, RISCVCPU (RISCVCPU))
2025-02-19 14:06:40 +00:00
import Fetch(fetchInstruction, FetchResult (Instruction, Misaligned))
import Isa.Decode(decode)
import Isa.Forms(Opcode(..))
2025-02-13 04:54:15 +00:00
import Peripherals.UartCFFI(writeCharToTerminal)
import Control.Concurrent (threadDelay)
import Debug.Trace
2025-02-19 14:06:40 +00:00
import Types (Mem, Addr)
2025-02-13 04:54:15 +00:00
data Args = Args {
firmware :: FilePath
} deriving (Show)
2025-02-19 14:06:40 +00:00
data Simulation
= Success [Machine]
| Failure String
deriving (Show)
-- machine :: Machine
-- machine = machineInit
2025-02-13 04:54:15 +00:00
machine' :: Machine -> Machine
machine' machine =
let
2025-02-19 14:06:40 +00:00
machinePeripherals = peripherals machine
machineMem = ram $ machinePeripherals
2025-02-13 04:54:15 +00:00
machineCPU = cpu machine
machinePC = pc machineCPU
addr = 0 :: Integer
mem' = replace addr (3) machineMem
2025-02-19 14:06:40 +00:00
peripherals' = machinePeripherals { ram = mem' }
2025-02-13 04:54:15 +00:00
cpu' = machineCPU { pc = machinePC + 4 }
2025-02-19 14:06:40 +00:00
instruction =
case (fetchInstruction machineMem machinePC) of
Instruction i -> i
_ -> undefined
2025-02-13 04:54:15 +00:00
in
2025-02-19 14:06:40 +00:00
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
2025-02-13 04:54:15 +00:00
simulationLoop :: Int -> Machine -> IO [Machine]
simulationLoop 0 state = return [state]
simulationLoop n state = do
let newState = machine' state
rest <- simulationLoop (n - 1) newState
return (state : rest)
2025-02-19 14:06:40 +00:00
simulation :: Args -> IO Simulation
2025-02-13 04:54:15 +00:00
simulation args = do
2025-02-19 14:06:40 +00:00
initializedPeripherals <- setupPeripherals (firmware args)
case initializedPeripherals of
InitializationError e -> return $ Failure e
InitializedPeripherals ram -> do
2025-02-13 04:54:15 +00:00
2025-02-19 14:06:40 +00:00
let initState = machineInit $ Machine.Peripherals ram
2025-02-19 23:28:08 +00:00
sim <- simulationLoop 15 initState
2025-02-19 14:06:40 +00:00
teardownPeripherals
return $ Success sim