CSRGetSet.hs

module Spec.CSRGetSet where
import Spec.CSR
import Spec.Machine
import Utility.Utility
import qualified Spec.CSRField as Field
import Data.Bits
import Control.Monad
import Prelude
import Debug.Trace
-- Permission checks are handled in ExecuteCSR.

-- helper function to make it very clear to Coq that getCSR terminates
getCSR_SStatus :: (RiscvMachine p t) => p MachineInt
getCSR_SStatus = do
  mxr <- getCSRField Field.MXR
  sum <- getCSRField Field.SUM
  spp <- getCSRField Field.SPP
  spie <- getCSRField Field.SPIE
  sie <- getCSRField Field.SIE
  let base = (shift mxr 19 .|. shift sum 18 .|. shift spp 8 .|.
              shift spie 5 .|. shift sie 1)
  xlen <- getXLEN
  if xlen > 32
    then do
    -- SXL and UXL are currently hardwired to MXL.
    mxl <- getCSRField Field.MXL
    -- return (shift mxl 32 .|. shift mxl 34 .|. base)
    vpc <- getPC
    --return $ (\x-> trace ((show $ (fromIntegral vpc)) ++ " " ++ show x) x)(shift mxl 32 .|. base)
    return $ (shift mxl 32 .|. base)
    else return base

-- helper function to make it very clear to Coq that setCSR terminates
setCSR_SStatus :: (RiscvMachine p t) => MachineInt -> p ()
setCSR_SStatus val = do
  setCSRField Field.MXR (bitSlice val 19 20)
  setCSRField Field.SUM (bitSlice val 18 19)
  setCSRField Field.SPP (bitSlice val 8 9)
  setCSRField Field.SPIE (bitSlice val 5 6)
  setCSRField Field.SIE (bitSlice val 1 2)
  getCSR_SStatus
  return ()


getCSR :: (RiscvMachine p t) => CSR -> p MachineInt

-- Currently ignores writes.
getCSR MISA = do
  xlen <- getXLEN
  mxl <- getCSRField Field.MXL
  ext <- getCSRField Field.Extensions
  return (shift mxl (xlen - 2) .|. ext)

getCSR MHartID = do
  return 0
getCSR MStatus = do
  tsr <- getCSRField Field.TSR
  tw <- getCSRField Field.TW
  tvm <- getCSRField Field.TVM
  mprv <- getCSRField Field.MPRV
  mpp <- getCSRField Field.MPP
  mpie <- getCSRField Field.MPIE
  mie <- getCSRField Field.MIE
  -- mxl = sxl = uxl for now
  mxl <- getCSRField Field.MXL
  sstatus <- getCSR_SStatus
  return (shift tsr 22 .|. shift tw 21 .|. shift tvm 20 .|. shift mprv 17 .|.
          shift mpp 11 .|. shift mpie 7 .|. shift mie 3 .|. sstatus .|. shift mxl 34)

getCSR MEDeleg = getCSRField Field.MEDeleg

getCSR MIDeleg = getCSRField Field.MIDeleg

getCSR SIP = do
 seip <- getCSRField Field.SEIP
 ueip <- getCSRField Field.UEIP
 stip <- getCSRField Field.STIP
 utip <- getCSRField Field.UTIP
 ssip <- getCSRField Field.SSIP
 usip <- getCSRField Field.USIP
 return (usip .|. shift ssip 1 .|. --shift msie 3 .|.
         shift utip 4 .|. shift stip 5 .|. -- shift mtie 7 .|.
         shift ueip 8 .|. shift seip 9 ) -- .|.  shift meie 11 )


-- For now we don't support user level interrupts in this spec.
getCSR SIE = do
-- meie <- getCSRField Field.MEIE
 seie <- getCSRField Field.SEIE
 ueie <- return 0 -- getCSRField Field.UEIE
-- mtie <- getCSRField Field.MTIE
 stie <- getCSRField Field.STIE
 utie <- return 0 -- getCSRField Field.UTIE
--  msie <- getCSRField Field.MSIE
 ssie <- getCSRField Field.SSIE
 usie <- return 0 -- getCSRField Field.USIE
 return (usie .|. shift ssie 1 .|. --shift msie 3 .|.
         shift utie 4 .|. shift stie 5 .|. -- shift mtie 7 .|.
         shift ueie 8 .|. shift seie 9 ) -- .|.  shift meie 11 )


getCSR MTVec = do
  base <- getCSRField Field.MTVecBase
  mode <- getCSRField Field.MTVecMode
  return (shift base 2 .|. mode)

-- Read-only
getCSR MCycle = getCSRField Field.MCycle

-- Read-only
getCSR MInstRet = getCSRField Field.MInstRet

getCSR MEPC = getCSRField Field.MEPC

getCSR MScratch = getCSRField Field.MScratch

getCSR InstRet = getCSR_InstRet

getCSR Time = getCSR_Time

getCSR Cycle = getCSR_Cycle

getCSR MHPMCounter3 = undefined
getCSR MHPMCounter4 = undefined
getCSR MHPMCounter5 = undefined
getCSR MHPMCounter6 = undefined
getCSR MHPMCounter7 = undefined
getCSR MHPMCounter8 = undefined
getCSR MHPMCounter9 = undefined
getCSR MHPMCounter10 = undefined
getCSR MHPMCounter11 = undefined
getCSR MHPMCounter12 = undefined
getCSR MHPMCounter13 = undefined
getCSR MHPMCounter14 = undefined
getCSR MHPMCounter15 = undefined
getCSR MHPMCounter16 = undefined
getCSR MHPMCounter17 = undefined
getCSR MHPMCounter18 = undefined
getCSR MHPMCounter19 = undefined
getCSR MHPMCounter20 = undefined
getCSR MHPMCounter21 = undefined
getCSR MHPMCounter22 = undefined
getCSR MHPMCounter23 = undefined
getCSR MHPMCounter24 = undefined
getCSR MHPMCounter25 = undefined
getCSR MHPMCounter26 = undefined
getCSR MHPMCounter27 = undefined
getCSR MHPMCounter28 = undefined
getCSR MHPMCounter29 = undefined
getCSR MHPMCounter30 = undefined
getCSR MHPMCounter31 = undefined

                --MHPM | MIR | MTM | MCY | -- mcounteren

getCSR MCounterEn = do
  mhpm <- getCSRField Field.MHPM
  mir <- getCSRField Field.MIR
  mtm <- getCSRField Field.MTM
  mcy <- getCSRField Field.MCY
  return (mcy .|. shift mtm 1 .|. shift mir 2 .|. shift mhpm 3)

getCSR MCause = do
  xlen <- getXLEN
  code <- getCSRField Field.MCauseCode
  interrupt <- getCSRField Field.MCauseInterrupt
  return (shift interrupt (xlen - 1) .|. code)

getCSR MTVal = getCSRField Field.MTVal

-- Supervisor-level CSRs:

getCSR SStatus = getCSR_SStatus

getCSR STVec = do
  base <- getCSRField Field.STVecBase
  mode <- getCSRField Field.STVecMode
  return (shift base 2 .|. mode)

getCSR SEPC = getCSRField Field.SEPC

getCSR SCounterEn = do
  shpm <- getCSRField Field.SHPM
  sir <- getCSRField Field.SIR
  stm <- getCSRField Field.STM
  scy <- getCSRField Field.SCY
  return (scy .|. shift stm 1 .|. shift sir 2 .|. shift shpm 3)


getCSR SScratch = getCSRField Field.SScratch

getCSR SCause = do
  xlen <- getXLEN
  code <- getCSRField Field.SCauseCode
  interrupt <- getCSRField Field.SCauseInterrupt
  return (shift interrupt (xlen - 1) .|. code)

getCSR STVal = getCSRField Field.STVal

getCSR SATP = do
  tvm <- getCSRField Field.TVM
  when (tvm == 1) (raiseException 0 2)
  xlen <- getXLEN
  mode <- getCSRField Field.MODE
  asid <- getCSRField Field.ASID
  ppn <- getCSRField Field.PPN
  if xlen == 32 then do
    return (shift mode 31 .|. shift asid 22 .|. ppn)
    else do
    return (shift mode 60 .|. shift asid 44 .|. ppn)

-- User-level CSRs:

getCSR FFlags = getCSRField Field.FFlags

getCSR FRM = getCSRField Field.FRM

getCSR MIP = do
 meip <- getCSRField Field.MEIP
 seip <- getCSRField Field.SEIP
 ueip <- getCSRField Field.UEIP
 mtip <- getCSRField Field.MTIP
 stip <- getCSRField Field.STIP
 utip <- getCSRField Field.UTIP
 msip <- getCSRField Field.MSIP
 ssip <- getCSRField Field.SSIP
 usip <- getCSRField Field.USIP
 return (usip .|. shift ssip 1 .|. shift msip 3 .|.
         shift utip 4 .|. shift stip 5 .|. shift mtip 7 .|.
         shift ueip 8 .|. shift seip 9 .|. shift meip 11 )


getCSR MIE = do
 meie <- getCSRField Field.MEIE
 seie <- getCSRField Field.SEIE
 ueie <- return 0 -- getCSRField Field.UEIE
 mtie <- getCSRField Field.MTIE
 stie <- getCSRField Field.STIE
 utie <- return 0 -- getCSRField Field.UTIE
 msie <- getCSRField Field.MSIE
 ssie <- getCSRField Field.SSIE
 usie <- return 0 -- getCSRField Field.USIE
 return (usie .|. shift ssie 1 .|. shift msie 3 .|.
         shift utie 4 .|. shift stie 5 .|. shift mtie 7 .|.
         shift ueie 8 .|. shift seie 9 .|. shift meie 11 )

getCSR FCSR = do
  fflags <- getCSRField Field.FFlags
  frm <- getCSRField Field.FRM
  return (shift frm 5 .|. fflags)


getCSR _ = return (-1) -- Hmmm, why did I hardwire that to -1?

setCSR :: (RiscvMachine p t) => CSR -> MachineInt -> p ()

setCSR MStatus val = do
  setCSR_SStatus val
  setCSRField Field.TSR (bitSlice val 22 23)
  setCSRField Field.TW (bitSlice val 21 22)
  setCSRField Field.TVM (bitSlice val 20 21)
  setCSRField Field.MPRV (bitSlice val 17 18)
  setCSRField Field.MPP (bitSlice val 11 13)
  setCSRField Field.MPIE (bitSlice val 7 8)
  setCSRField Field.MIE (bitSlice val 3 4)

setCSR MEDeleg val = setCSRField Field.MEDeleg (val .&. complement (shift 1 11))

setCSR MIDeleg val = setCSRField Field.MIDeleg val


setCSR SIP val = do
   let usip = bitSlice val 0 1
   let ssip = bitSlice val 1 2
   let utip = bitSlice val 4 5
   let stip = bitSlice val 5 6
   let ueip = bitSlice val 8 9
   let seip = bitSlice val 9 10
   setCSRField Field.USIP usip
   setCSRField Field.SSIP ssip
   setCSRField Field.UTIP utip
   setCSRField Field.STIP stip
   setCSRField Field.UEIP ueip
   setCSRField Field.SEIP seip


setCSR SIE val = do
   let usie = bitSlice val 0 1
   let ssie = bitSlice val 1 2
   let utie = bitSlice val 4 5
   let stie = bitSlice val 5 6
   let ueie = bitSlice val 8 9
   let seie = bitSlice val 9 10
   --setCSRField Field.USIE usie
   setCSRField Field.SSIE ssie
   --setCSRField Field.UTIE utie
   setCSRField Field.STIE stie
   --setCSRField Field.UEIE ueie
   setCSRField Field.SEIE seie

setCSR MTVec val = do
  setCSRField Field.MTVecMode (bitSlice val 0 2)
  setCSRField Field.MTVecBase (shift val (-2))

setCSR MEPC val = setCSRField Field.MEPC val

setCSR MCounterEn val = do
  let mhpm = shift val (-3)
  let mir = bitSlice val 2 3
  let mtm = bitSlice val 1 2
  let mcy = bitSlice val 0 1
  setCSRField Field.MHPM mhpm
  setCSRField Field.MIR mir
  setCSRField Field.MTM mtm
  setCSRField Field.MCY mcy

setCSR MScratch val = setCSRField Field.MScratch val

setCSR MCause val = do
  xlen <- getXLEN
  setCSRField Field.MCauseCode (bitSlice val 0 (xlen - 1))
  setCSRField Field.MCauseInterrupt (bitSlice val (xlen - 1) xlen)

setCSR MTVal val = setCSRField Field.MTVal val

-- Supervisor-level CSRs:

setCSR SStatus val = setCSR_SStatus val

setCSR STVec val = do
  setCSRField Field.STVecMode (bitSlice val 0 2)
  setCSRField Field.STVecBase (shift val (-2))

setCSR SEPC val = setCSRField Field.SEPC val

setCSR SScratch val = setCSRField Field.SScratch val

setCSR SCounterEn val = do
  let shpm = shift val (-3)
  let sir = bitSlice val 2 3
  let stm = bitSlice val 1 2
  let scy = bitSlice val 0 1
  setCSRField Field.SHPM shpm
  setCSRField Field.SIR sir
  setCSRField Field.STM stm
  setCSRField Field.SCY scy

setCSR SCause val = do
  xlen <- getXLEN
  setCSRField Field.SCauseCode (bitSlice val 0 (xlen - 1))
  setCSRField Field.SCauseInterrupt (bitSlice val (xlen - 1) xlen)

setCSR STVal val = setCSRField Field.STVal val


setCSR MIP val = do
   let usip = bitSlice val 0 1
   let ssip = bitSlice val 1 2
   let msip = bitSlice val 3 4
   let utip = bitSlice val 4 5
   let stip = bitSlice val 5 6
   let mtip = bitSlice val 7 8
   let ueip = bitSlice val 8 9
   let seip = bitSlice val 9 10
   let meip = bitSlice val 11 12
   setCSRField Field.USIP usip
   setCSRField Field.SSIP ssip
   setCSRField Field.MSIP msip
   setCSRField Field.UTIP utip
   setCSRField Field.STIP stip
   setCSRField Field.MTIP mtip
   setCSRField Field.UEIP ueip
   setCSRField Field.SEIP seip
   setCSRField Field.MEIP meip



setCSR MIE val = do
   let usie = bitSlice val 0 1
   let ssie = bitSlice val 1 2
   let msie = bitSlice val 3 4
   let utie = bitSlice val 4 5
   let stie = bitSlice val 5 6
   let mtie = bitSlice val 7 8
   let ueie = bitSlice val 8 9
   let seie = bitSlice val 9 10
   let meie = bitSlice val 11 12
  -- setCSRField Field.USIE usie
   setCSRField Field.SSIE ssie
   setCSRField Field.MSIE msie
  --setCSRField Field.UTIE utie
   setCSRField Field.STIE stie
   setCSRField Field.MTIE mtie
  -- setCSRField Field.UEIE ueie
   setCSRField Field.SEIE seie
   setCSRField Field.MEIE meie

setCSR SATP val = do
  priv <- getPrivMode
  tvm <- getCSRField Field.TVM
  when (priv == Supervisor && tvm == 1) (raiseException 0 2)
  xlen <- getXLEN
  let mode = if xlen == 32 then bitSlice val 31 32 else bitSlice val 60 64
  -- If the mode is unsupported, the write has no effect.
  when (mode == 1 || mode == 8 || mode == 9) $ do
    if xlen == 32
      then do
      setCSRField Field.MODE mode
      setCSRField Field.ASID (bitSlice val 22 31)
      setCSRField Field.PPN (bitSlice val 0 22)
      else do
      setCSRField Field.MODE mode
      setCSRField Field.ASID (bitSlice val 44 60)
      setCSRField Field.PPN (bitSlice val 0 44)

-- User-level CSRs:

setCSR FFlags val = setCSRField Field.FFlags (bitSlice val 0 5)

setCSR FRM val = setCSRField Field.FRM (bitSlice val 0 3)

setCSR FCSR val = do
  setCSRField Field.FFlags (bitSlice val 0 5)
  setCSRField Field.FRM (bitSlice val 5 8)

setCSR _ _ = return () -- raiseException 0 2