{-|
Module      : Lion.Instruction
Description : RISC-V ISA
Copyright   : (c) David Cox, 2021
License     : BSD-3-Clause
Maintainer  : standardsemiconductor@gmail.com
-}

module Lion.Instruction where

import Clash.Prelude
import Data.Function ( on )

data Exception = IllegalInstruction
  deriving stock ((forall x. Exception -> Rep Exception x)
-> (forall x. Rep Exception x -> Exception) -> Generic Exception
forall x. Rep Exception x -> Exception
forall x. Exception -> Rep Exception x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Exception x -> Exception
$cfrom :: forall x. Exception -> Rep Exception x
Generic, Int -> Exception -> ShowS
[Exception] -> ShowS
Exception -> String
(Int -> Exception -> ShowS)
-> (Exception -> String)
-> ([Exception] -> ShowS)
-> Show Exception
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Exception] -> ShowS
$cshowList :: [Exception] -> ShowS
show :: Exception -> String
$cshow :: Exception -> String
showsPrec :: Int -> Exception -> ShowS
$cshowsPrec :: Int -> Exception -> ShowS
Show, Exception -> Exception -> Bool
(Exception -> Exception -> Bool)
-> (Exception -> Exception -> Bool) -> Eq Exception
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Exception -> Exception -> Bool
$c/= :: Exception -> Exception -> Bool
== :: Exception -> Exception -> Bool
$c== :: Exception -> Exception -> Bool
Eq)
  deriving anyclass HasCallStack => String -> Exception
Exception -> Bool
Exception -> ()
Exception -> Exception
(HasCallStack => String -> Exception)
-> (Exception -> Bool)
-> (Exception -> Exception)
-> (Exception -> ())
-> NFDataX Exception
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: Exception -> ()
$crnfX :: Exception -> ()
ensureSpine :: Exception -> Exception
$censureSpine :: Exception -> Exception
hasUndefined :: Exception -> Bool
$chasUndefined :: Exception -> Bool
deepErrorX :: String -> Exception
$cdeepErrorX :: HasCallStack => String -> Exception
NFDataX

-- | Writeback pipeline instruction
data WbInstr = WbRegWr (Unsigned 5) (BitVector 32)
             | WbLoad Load (Unsigned 5) (BitVector 4)
             | WbStore
             | WbNop
  deriving stock ((forall x. WbInstr -> Rep WbInstr x)
-> (forall x. Rep WbInstr x -> WbInstr) -> Generic WbInstr
forall x. Rep WbInstr x -> WbInstr
forall x. WbInstr -> Rep WbInstr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep WbInstr x -> WbInstr
$cfrom :: forall x. WbInstr -> Rep WbInstr x
Generic, Int -> WbInstr -> ShowS
[WbInstr] -> ShowS
WbInstr -> String
(Int -> WbInstr -> ShowS)
-> (WbInstr -> String) -> ([WbInstr] -> ShowS) -> Show WbInstr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WbInstr] -> ShowS
$cshowList :: [WbInstr] -> ShowS
show :: WbInstr -> String
$cshow :: WbInstr -> String
showsPrec :: Int -> WbInstr -> ShowS
$cshowsPrec :: Int -> WbInstr -> ShowS
Show, WbInstr -> WbInstr -> Bool
(WbInstr -> WbInstr -> Bool)
-> (WbInstr -> WbInstr -> Bool) -> Eq WbInstr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WbInstr -> WbInstr -> Bool
$c/= :: WbInstr -> WbInstr -> Bool
== :: WbInstr -> WbInstr -> Bool
$c== :: WbInstr -> WbInstr -> Bool
Eq)
  deriving anyclass HasCallStack => String -> WbInstr
WbInstr -> Bool
WbInstr -> ()
WbInstr -> WbInstr
(HasCallStack => String -> WbInstr)
-> (WbInstr -> Bool)
-> (WbInstr -> WbInstr)
-> (WbInstr -> ())
-> NFDataX WbInstr
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: WbInstr -> ()
$crnfX :: WbInstr -> ()
ensureSpine :: WbInstr -> WbInstr
$censureSpine :: WbInstr -> WbInstr
hasUndefined :: WbInstr -> Bool
$chasUndefined :: WbInstr -> Bool
deepErrorX :: String -> WbInstr
$cdeepErrorX :: HasCallStack => String -> WbInstr
NFDataX

-- | Memory pipeline instruction
data MeInstr = MeRegWr      (Unsigned 5)
             | MeJump       (Unsigned 5) (BitVector 32)
             | MeBranch 
             | MeStore                   (BitVector 32) (BitVector 4) (BitVector 32)
             | MeLoad  Load (Unsigned 5) (BitVector 32) (BitVector 4)
             | MeNop
  deriving stock ((forall x. MeInstr -> Rep MeInstr x)
-> (forall x. Rep MeInstr x -> MeInstr) -> Generic MeInstr
forall x. Rep MeInstr x -> MeInstr
forall x. MeInstr -> Rep MeInstr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MeInstr x -> MeInstr
$cfrom :: forall x. MeInstr -> Rep MeInstr x
Generic, Int -> MeInstr -> ShowS
[MeInstr] -> ShowS
MeInstr -> String
(Int -> MeInstr -> ShowS)
-> (MeInstr -> String) -> ([MeInstr] -> ShowS) -> Show MeInstr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MeInstr] -> ShowS
$cshowList :: [MeInstr] -> ShowS
show :: MeInstr -> String
$cshow :: MeInstr -> String
showsPrec :: Int -> MeInstr -> ShowS
$cshowsPrec :: Int -> MeInstr -> ShowS
Show, MeInstr -> MeInstr -> Bool
(MeInstr -> MeInstr -> Bool)
-> (MeInstr -> MeInstr -> Bool) -> Eq MeInstr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MeInstr -> MeInstr -> Bool
$c/= :: MeInstr -> MeInstr -> Bool
== :: MeInstr -> MeInstr -> Bool
$c== :: MeInstr -> MeInstr -> Bool
Eq)
  deriving anyclass HasCallStack => String -> MeInstr
MeInstr -> Bool
MeInstr -> ()
MeInstr -> MeInstr
(HasCallStack => String -> MeInstr)
-> (MeInstr -> Bool)
-> (MeInstr -> MeInstr)
-> (MeInstr -> ())
-> NFDataX MeInstr
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: MeInstr -> ()
$crnfX :: MeInstr -> ()
ensureSpine :: MeInstr -> MeInstr
$censureSpine :: MeInstr -> MeInstr
hasUndefined :: MeInstr -> Bool
$chasUndefined :: MeInstr -> Bool
deepErrorX :: String -> MeInstr
$cdeepErrorX :: HasCallStack => String -> MeInstr
NFDataX

-- | Execute pipeline instruction
data ExInstr = Ex       ExOp   (Unsigned 5) (BitVector 32)
             | ExJump   Jump   (Unsigned 5) (BitVector 32)
             | ExBranch Branch              (BitVector 32)
             | ExStore  Store               (BitVector 32)
             | ExLoad   Load   (Unsigned 5) (BitVector 32)
             | ExAlu    Op     (Unsigned 5)
             | ExAluImm Op     (Unsigned 5) (BitVector 32)
  deriving stock ((forall x. ExInstr -> Rep ExInstr x)
-> (forall x. Rep ExInstr x -> ExInstr) -> Generic ExInstr
forall x. Rep ExInstr x -> ExInstr
forall x. ExInstr -> Rep ExInstr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ExInstr x -> ExInstr
$cfrom :: forall x. ExInstr -> Rep ExInstr x
Generic, Int -> ExInstr -> ShowS
[ExInstr] -> ShowS
ExInstr -> String
(Int -> ExInstr -> ShowS)
-> (ExInstr -> String) -> ([ExInstr] -> ShowS) -> Show ExInstr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExInstr] -> ShowS
$cshowList :: [ExInstr] -> ShowS
show :: ExInstr -> String
$cshow :: ExInstr -> String
showsPrec :: Int -> ExInstr -> ShowS
$cshowsPrec :: Int -> ExInstr -> ShowS
Show, ExInstr -> ExInstr -> Bool
(ExInstr -> ExInstr -> Bool)
-> (ExInstr -> ExInstr -> Bool) -> Eq ExInstr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExInstr -> ExInstr -> Bool
$c/= :: ExInstr -> ExInstr -> Bool
== :: ExInstr -> ExInstr -> Bool
$c== :: ExInstr -> ExInstr -> Bool
Eq)
  deriving anyclass HasCallStack => String -> ExInstr
ExInstr -> Bool
ExInstr -> ()
ExInstr -> ExInstr
(HasCallStack => String -> ExInstr)
-> (ExInstr -> Bool)
-> (ExInstr -> ExInstr)
-> (ExInstr -> ())
-> NFDataX ExInstr
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: ExInstr -> ()
$crnfX :: ExInstr -> ()
ensureSpine :: ExInstr -> ExInstr
$censureSpine :: ExInstr -> ExInstr
hasUndefined :: ExInstr -> Bool
$chasUndefined :: ExInstr -> Bool
deepErrorX :: String -> ExInstr
$cdeepErrorX :: HasCallStack => String -> ExInstr
NFDataX

-- | ALU operation
data Op = Add
        | Sub
        | Sll
        | Slt
        | Sltu
        | Xor
        | Srl
        | Sra
        | Or
        | And
  deriving stock ((forall x. Op -> Rep Op x)
-> (forall x. Rep Op x -> Op) -> Generic Op
forall x. Rep Op x -> Op
forall x. Op -> Rep Op x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Op x -> Op
$cfrom :: forall x. Op -> Rep Op x
Generic, Int -> Op -> ShowS
[Op] -> ShowS
Op -> String
(Int -> Op -> ShowS)
-> (Op -> String) -> ([Op] -> ShowS) -> Show Op
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Op] -> ShowS
$cshowList :: [Op] -> ShowS
show :: Op -> String
$cshow :: Op -> String
showsPrec :: Int -> Op -> ShowS
$cshowsPrec :: Int -> Op -> ShowS
Show, Op -> Op -> Bool
(Op -> Op -> Bool) -> (Op -> Op -> Bool) -> Eq Op
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Op -> Op -> Bool
$c/= :: Op -> Op -> Bool
== :: Op -> Op -> Bool
$c== :: Op -> Op -> Bool
Eq)
  deriving anyclass HasCallStack => String -> Op
Op -> Bool
Op -> ()
Op -> Op
(HasCallStack => String -> Op)
-> (Op -> Bool) -> (Op -> Op) -> (Op -> ()) -> NFDataX Op
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: Op -> ()
$crnfX :: Op -> ()
ensureSpine :: Op -> Op
$censureSpine :: Op -> Op
hasUndefined :: Op -> Bool
$chasUndefined :: Op -> Bool
deepErrorX :: String -> Op
$cdeepErrorX :: HasCallStack => String -> Op
NFDataX

-- | Branch operation
data Branch = Beq
            | Bne
            | Blt
            | Bge
            | Bltu
            | Bgeu
  deriving stock ((forall x. Branch -> Rep Branch x)
-> (forall x. Rep Branch x -> Branch) -> Generic Branch
forall x. Rep Branch x -> Branch
forall x. Branch -> Rep Branch x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Branch x -> Branch
$cfrom :: forall x. Branch -> Rep Branch x
Generic, Int -> Branch -> ShowS
[Branch] -> ShowS
Branch -> String
(Int -> Branch -> ShowS)
-> (Branch -> String) -> ([Branch] -> ShowS) -> Show Branch
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Branch] -> ShowS
$cshowList :: [Branch] -> ShowS
show :: Branch -> String
$cshow :: Branch -> String
showsPrec :: Int -> Branch -> ShowS
$cshowsPrec :: Int -> Branch -> ShowS
Show, Branch -> Branch -> Bool
(Branch -> Branch -> Bool)
-> (Branch -> Branch -> Bool) -> Eq Branch
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Branch -> Branch -> Bool
$c/= :: Branch -> Branch -> Bool
== :: Branch -> Branch -> Bool
$c== :: Branch -> Branch -> Bool
Eq)
  deriving anyclass HasCallStack => String -> Branch
Branch -> Bool
Branch -> ()
Branch -> Branch
(HasCallStack => String -> Branch)
-> (Branch -> Bool)
-> (Branch -> Branch)
-> (Branch -> ())
-> NFDataX Branch
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: Branch -> ()
$crnfX :: Branch -> ()
ensureSpine :: Branch -> Branch
$censureSpine :: Branch -> Branch
hasUndefined :: Branch -> Bool
$chasUndefined :: Branch -> Bool
deepErrorX :: String -> Branch
$cdeepErrorX :: HasCallStack => String -> Branch
NFDataX

-- | branch calculation
branch :: Branch -> BitVector 32 -> BitVector 32 -> Bool
branch :: Branch -> BitVector 32 -> BitVector 32 -> Bool
branch = \case
  Branch
Beq  -> Bool -> Bool
not (Bool -> Bool)
-> (BitVector 32 -> BitVector 32 -> Bool)
-> BitVector 32
-> BitVector 32
-> Bool
forall b c a a. (b -> c) -> (a -> a -> b) -> a -> a -> c
... BitVector 32 -> BitVector 32 -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
  Branch
Bne  -> BitVector 32 -> BitVector 32 -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
  Branch
Bge  -> Bool -> Bool
not (Bool -> Bool)
-> (Signed 32 -> Signed 32 -> Bool)
-> Signed 32
-> Signed 32
-> Bool
forall b c a a. (b -> c) -> (a -> a -> b) -> a -> a -> c
... Signed 32 -> Signed 32 -> Bool
forall a. Ord a => a -> a -> Bool
(<) (Signed 32 -> Signed 32 -> Bool)
-> (BitVector 32 -> Signed 32)
-> BitVector 32
-> BitVector 32
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` BitVector 32 -> Signed 32
sign
  Branch
Bgeu -> Bool -> Bool
not (Bool -> Bool)
-> (BitVector 32 -> BitVector 32 -> Bool)
-> BitVector 32
-> BitVector 32
-> Bool
forall b c a a. (b -> c) -> (a -> a -> b) -> a -> a -> c
... BitVector 32 -> BitVector 32 -> Bool
forall a. Ord a => a -> a -> Bool
(<)
  Branch
Blt  -> Signed 32 -> Signed 32 -> Bool
forall a. Ord a => a -> a -> Bool
(<) (Signed 32 -> Signed 32 -> Bool)
-> (BitVector 32 -> Signed 32)
-> BitVector 32
-> BitVector 32
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` BitVector 32 -> Signed 32
sign
  Branch
Bltu -> BitVector 32 -> BitVector 32 -> Bool
forall a. Ord a => a -> a -> Bool
(<)
  where
    ... :: (b -> c) -> (a -> a -> b) -> a -> a -> c
(...) = ((a -> b) -> a -> c) -> (a -> a -> b) -> a -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)(((a -> b) -> a -> c) -> (a -> a -> b) -> a -> a -> c)
-> ((b -> c) -> (a -> b) -> a -> c)
-> (b -> c)
-> (a -> a -> b)
-> a
-> a
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)
    sign :: BitVector 32 -> Signed 32
    sign :: BitVector 32 -> Signed 32
sign = BitVector 32 -> Signed 32
forall a. BitPack a => BitVector (BitSize a) -> a
unpack

data ExOp = Lui
          | Auipc
  deriving stock ((forall x. ExOp -> Rep ExOp x)
-> (forall x. Rep ExOp x -> ExOp) -> Generic ExOp
forall x. Rep ExOp x -> ExOp
forall x. ExOp -> Rep ExOp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ExOp x -> ExOp
$cfrom :: forall x. ExOp -> Rep ExOp x
Generic, Int -> ExOp -> ShowS
[ExOp] -> ShowS
ExOp -> String
(Int -> ExOp -> ShowS)
-> (ExOp -> String) -> ([ExOp] -> ShowS) -> Show ExOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExOp] -> ShowS
$cshowList :: [ExOp] -> ShowS
show :: ExOp -> String
$cshow :: ExOp -> String
showsPrec :: Int -> ExOp -> ShowS
$cshowsPrec :: Int -> ExOp -> ShowS
Show, ExOp -> ExOp -> Bool
(ExOp -> ExOp -> Bool) -> (ExOp -> ExOp -> Bool) -> Eq ExOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExOp -> ExOp -> Bool
$c/= :: ExOp -> ExOp -> Bool
== :: ExOp -> ExOp -> Bool
$c== :: ExOp -> ExOp -> Bool
Eq)
  deriving anyclass HasCallStack => String -> ExOp
ExOp -> Bool
ExOp -> ()
ExOp -> ExOp
(HasCallStack => String -> ExOp)
-> (ExOp -> Bool) -> (ExOp -> ExOp) -> (ExOp -> ()) -> NFDataX ExOp
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: ExOp -> ()
$crnfX :: ExOp -> ()
ensureSpine :: ExOp -> ExOp
$censureSpine :: ExOp -> ExOp
hasUndefined :: ExOp -> Bool
$chasUndefined :: ExOp -> Bool
deepErrorX :: String -> ExOp
$cdeepErrorX :: HasCallStack => String -> ExOp
NFDataX

data Jump = Jal | Jalr
  deriving stock ((forall x. Jump -> Rep Jump x)
-> (forall x. Rep Jump x -> Jump) -> Generic Jump
forall x. Rep Jump x -> Jump
forall x. Jump -> Rep Jump x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Jump x -> Jump
$cfrom :: forall x. Jump -> Rep Jump x
Generic, Int -> Jump -> ShowS
[Jump] -> ShowS
Jump -> String
(Int -> Jump -> ShowS)
-> (Jump -> String) -> ([Jump] -> ShowS) -> Show Jump
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Jump] -> ShowS
$cshowList :: [Jump] -> ShowS
show :: Jump -> String
$cshow :: Jump -> String
showsPrec :: Int -> Jump -> ShowS
$cshowsPrec :: Int -> Jump -> ShowS
Show, Jump -> Jump -> Bool
(Jump -> Jump -> Bool) -> (Jump -> Jump -> Bool) -> Eq Jump
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Jump -> Jump -> Bool
$c/= :: Jump -> Jump -> Bool
== :: Jump -> Jump -> Bool
$c== :: Jump -> Jump -> Bool
Eq)
  deriving anyclass HasCallStack => String -> Jump
Jump -> Bool
Jump -> ()
Jump -> Jump
(HasCallStack => String -> Jump)
-> (Jump -> Bool) -> (Jump -> Jump) -> (Jump -> ()) -> NFDataX Jump
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: Jump -> ()
$crnfX :: Jump -> ()
ensureSpine :: Jump -> Jump
$censureSpine :: Jump -> Jump
hasUndefined :: Jump -> Bool
$chasUndefined :: Jump -> Bool
deepErrorX :: String -> Jump
$cdeepErrorX :: HasCallStack => String -> Jump
NFDataX

-- | Store operation
data Store = Sb
           | Sh
           | Sw
  deriving stock ((forall x. Store -> Rep Store x)
-> (forall x. Rep Store x -> Store) -> Generic Store
forall x. Rep Store x -> Store
forall x. Store -> Rep Store x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Store x -> Store
$cfrom :: forall x. Store -> Rep Store x
Generic, Int -> Store -> ShowS
[Store] -> ShowS
Store -> String
(Int -> Store -> ShowS)
-> (Store -> String) -> ([Store] -> ShowS) -> Show Store
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Store] -> ShowS
$cshowList :: [Store] -> ShowS
show :: Store -> String
$cshow :: Store -> String
showsPrec :: Int -> Store -> ShowS
$cshowsPrec :: Int -> Store -> ShowS
Show, Store -> Store -> Bool
(Store -> Store -> Bool) -> (Store -> Store -> Bool) -> Eq Store
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Store -> Store -> Bool
$c/= :: Store -> Store -> Bool
== :: Store -> Store -> Bool
$c== :: Store -> Store -> Bool
Eq)
  deriving anyclass HasCallStack => String -> Store
Store -> Bool
Store -> ()
Store -> Store
(HasCallStack => String -> Store)
-> (Store -> Bool)
-> (Store -> Store)
-> (Store -> ())
-> NFDataX Store
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: Store -> ()
$crnfX :: Store -> ()
ensureSpine :: Store -> Store
$censureSpine :: Store -> Store
hasUndefined :: Store -> Bool
$chasUndefined :: Store -> Bool
deepErrorX :: String -> Store
$cdeepErrorX :: HasCallStack => String -> Store
NFDataX

-- | Load operation
data Load = Lb
          | Lh
          | Lw
          | Lbu
          | Lhu
  deriving stock ((forall x. Load -> Rep Load x)
-> (forall x. Rep Load x -> Load) -> Generic Load
forall x. Rep Load x -> Load
forall x. Load -> Rep Load x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Load x -> Load
$cfrom :: forall x. Load -> Rep Load x
Generic, Int -> Load -> ShowS
[Load] -> ShowS
Load -> String
(Int -> Load -> ShowS)
-> (Load -> String) -> ([Load] -> ShowS) -> Show Load
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Load] -> ShowS
$cshowList :: [Load] -> ShowS
show :: Load -> String
$cshow :: Load -> String
showsPrec :: Int -> Load -> ShowS
$cshowsPrec :: Int -> Load -> ShowS
Show, Load -> Load -> Bool
(Load -> Load -> Bool) -> (Load -> Load -> Bool) -> Eq Load
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Load -> Load -> Bool
$c/= :: Load -> Load -> Bool
== :: Load -> Load -> Bool
$c== :: Load -> Load -> Bool
Eq)
  deriving anyclass HasCallStack => String -> Load
Load -> Bool
Load -> ()
Load -> Load
(HasCallStack => String -> Load)
-> (Load -> Bool) -> (Load -> Load) -> (Load -> ()) -> NFDataX Load
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: Load -> ()
$crnfX :: Load -> ()
ensureSpine :: Load -> Load
$censureSpine :: Load -> Load
hasUndefined :: Load -> Bool
$chasUndefined :: Load -> Bool
deepErrorX :: String -> Load
$cdeepErrorX :: HasCallStack => String -> Load
NFDataX

parseInstr :: BitVector 32 -> Either Exception ExInstr
parseInstr :: BitVector 32 -> Either Exception ExInstr
parseInstr BitVector 32
i = case BitVector 32
i of
  $(bitPattern ".........................0110111") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ ExOp -> Unsigned 5 -> BitVector 32 -> ExInstr
Ex ExOp
Lui   Unsigned 5
rd BitVector 32
immU -- lui
  $(bitPattern ".........................0010111") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ ExOp -> Unsigned 5 -> BitVector 32 -> ExInstr
Ex ExOp
Auipc Unsigned 5
rd BitVector 32
immU -- auipc
  $(bitPattern ".........................1101111") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Jump -> Unsigned 5 -> BitVector 32 -> ExInstr
ExJump Jump
Jal  Unsigned 5
rd BitVector 32
immJ -- jal
  $(bitPattern ".................000.....1100111") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Jump -> Unsigned 5 -> BitVector 32 -> ExInstr
ExJump Jump
Jalr Unsigned 5
rd BitVector 32
immI -- jalr
  $(bitPattern ".................000.....1100011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Branch -> BitVector 32 -> ExInstr
ExBranch Branch
Beq  BitVector 32
immB -- beq
  $(bitPattern ".................001.....1100011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Branch -> BitVector 32 -> ExInstr
ExBranch Branch
Bne  BitVector 32
immB -- bne
  $(bitPattern ".................100.....1100011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Branch -> BitVector 32 -> ExInstr
ExBranch Branch
Blt  BitVector 32
immB -- blt
  $(bitPattern ".................101.....1100011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Branch -> BitVector 32 -> ExInstr
ExBranch Branch
Bge  BitVector 32
immB -- bge
  $(bitPattern ".................110.....1100011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Branch -> BitVector 32 -> ExInstr
ExBranch Branch
Bltu BitVector 32
immB -- bltu
  $(bitPattern ".................111.....1100011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Branch -> BitVector 32 -> ExInstr
ExBranch Branch
Bgeu BitVector 32
immB -- bgeu
  $(bitPattern ".................000.....0000011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Load -> Unsigned 5 -> BitVector 32 -> ExInstr
ExLoad Load
Lb  Unsigned 5
rd BitVector 32
immI -- lb
  $(bitPattern ".................001.....0000011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Load -> Unsigned 5 -> BitVector 32 -> ExInstr
ExLoad Load
Lh  Unsigned 5
rd BitVector 32
immI -- lh
  $(bitPattern ".................010.....0000011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Load -> Unsigned 5 -> BitVector 32 -> ExInstr
ExLoad Load
Lw  Unsigned 5
rd BitVector 32
immI -- lw
  $(bitPattern ".................100.....0000011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Load -> Unsigned 5 -> BitVector 32 -> ExInstr
ExLoad Load
Lbu Unsigned 5
rd BitVector 32
immI -- lbu
  $(bitPattern ".................101.....0000011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Load -> Unsigned 5 -> BitVector 32 -> ExInstr
ExLoad Load
Lhu Unsigned 5
rd BitVector 32
immI -- lhu
  $(bitPattern ".................000.....0100011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Store -> BitVector 32 -> ExInstr
ExStore Store
Sb BitVector 32
immS -- sb
  $(bitPattern ".................001.....0100011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Store -> BitVector 32 -> ExInstr
ExStore Store
Sh BitVector 32
immS -- sh
  $(bitPattern ".................010.....0100011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Store -> BitVector 32 -> ExInstr
ExStore Store
Sw BitVector 32
immS -- sw
  $(bitPattern ".................000.....0010011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> BitVector 32 -> ExInstr
ExAluImm Op
Add  Unsigned 5
rd BitVector 32
immI -- addi
  $(bitPattern ".................010.....0010011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> BitVector 32 -> ExInstr
ExAluImm Op
Slt  Unsigned 5
rd BitVector 32
immI -- slti
  $(bitPattern ".................011.....0010011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> BitVector 32 -> ExInstr
ExAluImm Op
Sltu Unsigned 5
rd BitVector 32
immI -- sltiu
  $(bitPattern ".................100.....0010011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> BitVector 32 -> ExInstr
ExAluImm Op
Xor  Unsigned 5
rd BitVector 32
immI -- xori
  $(bitPattern ".................110.....0010011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> BitVector 32 -> ExInstr
ExAluImm Op
Or   Unsigned 5
rd BitVector 32
immI -- ori
  $(bitPattern ".................111.....0010011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> BitVector 32 -> ExInstr
ExAluImm Op
And  Unsigned 5
rd BitVector 32
immI -- andi
  $(bitPattern "0000000..........001.....0010011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> BitVector 32 -> ExInstr
ExAluImm Op
Sll  Unsigned 5
rd BitVector 32
immI -- slli
  $(bitPattern "0000000..........101.....0010011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> BitVector 32 -> ExInstr
ExAluImm Op
Srl  Unsigned 5
rd BitVector 32
immI -- srli
  $(bitPattern "0100000..........101.....0010011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> BitVector 32 -> ExInstr
ExAluImm Op
Sra  Unsigned 5
rd BitVector 32
immI -- srai
  $(bitPattern "0000000..........000.....0110011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> ExInstr
ExAlu Op
Add  Unsigned 5
rd -- add
  $(bitPattern "0100000..........000.....0110011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> ExInstr
ExAlu Op
Sub  Unsigned 5
rd -- sub
  $(bitPattern "0000000..........001.....0110011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> ExInstr
ExAlu Op
Sll  Unsigned 5
rd -- sll
  $(bitPattern "0000000..........010.....0110011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> ExInstr
ExAlu Op
Slt  Unsigned 5
rd -- slt
  $(bitPattern "0000000..........011.....0110011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> ExInstr
ExAlu Op
Sltu Unsigned 5
rd -- sltu
  $(bitPattern "0000000..........100.....0110011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> ExInstr
ExAlu Op
Xor  Unsigned 5
rd -- xor
  $(bitPattern "0000000..........101.....0110011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> ExInstr
ExAlu Op
Srl  Unsigned 5
rd -- srl
  $(bitPattern "0100000..........101.....0110011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> ExInstr
ExAlu Op
Sra  Unsigned 5
rd -- sra
  $(bitPattern "0000000..........110.....0110011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> ExInstr
ExAlu Op
Or   Unsigned 5
rd -- or
  $(bitPattern "0000000..........111.....0110011") -> ExInstr -> Either Exception ExInstr
forall a b. b -> Either a b
Right (ExInstr -> Either Exception ExInstr)
-> ExInstr -> Either Exception ExInstr
forall a b. (a -> b) -> a -> b
$ Op -> Unsigned 5 -> ExInstr
ExAlu Op
And  Unsigned 5
rd -- and
  BitVector 32
_ -> Exception -> Either Exception ExInstr
forall a b. a -> Either a b
Left Exception
IllegalInstruction
  where
--    npcB = immB + pc
--    npcJ = immJ + pc

    rd :: Unsigned 5
rd = BitVector 32 -> Unsigned 5
sliceRd BitVector 32
i

    immI :: BitVector 32
    immI :: BitVector 32
immI = BitVector 12 -> BitVector (20 + 12)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
signExtend (BitVector 12 -> BitVector (20 + 12))
-> BitVector 12 -> BitVector (20 + 12)
forall a b. (a -> b) -> a -> b
$ SNat 31 -> SNat 20 -> BitVector 32 -> BitVector ((31 + 1) - 20)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 31
d31 SNat 20
d20 BitVector 32
i
    
    immS :: BitVector 32
    immS :: BitVector 32
immS = BitVector 12 -> BitVector (20 + 12)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
signExtend (BitVector 12 -> BitVector (20 + 12))
-> BitVector 12 -> BitVector (20 + 12)
forall a b. (a -> b) -> a -> b
$ SNat 31 -> SNat 25 -> BitVector 32 -> BitVector ((31 + 1) - 25)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 31
d31 SNat 25
d25 BitVector 32
i BitVector 7 -> BitVector 5 -> BitVector (7 + 5)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# SNat 11 -> SNat 7 -> BitVector 32 -> BitVector ((11 + 1) - 7)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 11
d11 SNat 7
d7 BitVector 32
i

    immB :: BitVector 32
    immB :: BitVector 32
immB = BitVector 12 -> BitVector (20 + 12)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
signExtend (SNat 31 -> SNat 31 -> BitVector 32 -> BitVector ((31 + 1) - 31)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 31
d31 SNat 31
d31 BitVector 32
i BitVector 1 -> BitVector 1 -> BitVector (1 + 1)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# SNat 7 -> SNat 7 -> BitVector 32 -> BitVector ((7 + 1) - 7)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 7
d7 SNat 7
d7 BitVector 32
i BitVector 2 -> BitVector 6 -> BitVector (2 + 6)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# SNat 30 -> SNat 25 -> BitVector 32 -> BitVector ((30 + 1) - 25)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 30
d30 SNat 25
d25 BitVector 32
i BitVector 8 -> BitVector 4 -> BitVector (8 + 4)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# SNat 11 -> SNat 8 -> BitVector 32 -> BitVector ((11 + 1) - 8)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 11
d11 SNat 8
d8 BitVector 32
i) BitVector 32 -> Int -> BitVector 32
forall a. Bits a => a -> Int -> a
`shiftL` Int
1

    immU :: BitVector 32
    immU :: BitVector 32
immU = SNat 31 -> SNat 12 -> BitVector 32 -> BitVector ((31 + 1) - 12)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 31
d31 SNat 12
d12 BitVector 32
i BitVector 20 -> BitVector 12 -> BitVector (20 + 12)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# BitVector 12
0
    
    immJ :: BitVector 32
    immJ :: BitVector 32
immJ = BitVector 20 -> BitVector (12 + 20)
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
signExtend (SNat 31 -> SNat 31 -> BitVector 32 -> BitVector ((31 + 1) - 31)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 31
d31 SNat 31
d31 BitVector 32
i BitVector 1 -> BitVector 8 -> BitVector (1 + 8)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# SNat 19 -> SNat 12 -> BitVector 32 -> BitVector ((19 + 1) - 12)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 19
d19 SNat 12
d12 BitVector 32
i BitVector 9 -> BitVector 1 -> BitVector (9 + 1)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# SNat 20 -> SNat 20 -> BitVector 32 -> BitVector ((20 + 1) - 20)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 20
d20 SNat 20
d20 BitVector 32
i BitVector 10 -> BitVector 6 -> BitVector (10 + 6)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# SNat 30 -> SNat 25 -> BitVector 32 -> BitVector ((30 + 1) - 25)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 30
d30 SNat 25
d25 BitVector 32
i BitVector 16 -> BitVector 4 -> BitVector (16 + 4)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# SNat 24 -> SNat 21 -> BitVector 32 -> BitVector ((24 + 1) - 21)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 24
d24 SNat 21
d21 BitVector 32
i) BitVector 32 -> Int -> BitVector 32
forall a. Bits a => a -> Int -> a
`shiftL` Int
1


sliceRd :: BitVector 32 -> Unsigned 5
sliceRd :: BitVector 32 -> Unsigned 5
sliceRd = BitVector 5 -> Unsigned 5
forall a. BitPack a => BitVector (BitSize a) -> a
unpack (BitVector 5 -> Unsigned 5)
-> (BitVector 32 -> BitVector 5) -> BitVector 32 -> Unsigned 5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat 11 -> SNat 7 -> BitVector 32 -> BitVector ((11 + 1) - 7)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 11
d11 SNat 7
d7

sliceRs1 :: BitVector 32 -> Unsigned 5
sliceRs1 :: BitVector 32 -> Unsigned 5
sliceRs1 = BitVector 5 -> Unsigned 5
forall a. BitPack a => BitVector (BitSize a) -> a
unpack (BitVector 5 -> Unsigned 5)
-> (BitVector 32 -> BitVector 5) -> BitVector 32 -> Unsigned 5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat 19 -> SNat 15 -> BitVector 32 -> BitVector ((19 + 1) - 15)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 19
d19 SNat 15
d15

sliceRs2 :: BitVector 32 -> Unsigned 5
sliceRs2 :: BitVector 32 -> Unsigned 5
sliceRs2 = BitVector 5 -> Unsigned 5
forall a. BitPack a => BitVector (BitSize a) -> a
unpack (BitVector 5 -> Unsigned 5)
-> (BitVector 32 -> BitVector 5) -> BitVector 32 -> Unsigned 5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat 24 -> SNat 20 -> BitVector 32 -> BitVector ((24 + 1) - 20)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 24
d24 SNat 20
d20

sliceOpcode :: BitVector 32 -> BitVector 7
sliceOpcode :: BitVector 32 -> BitVector 7
sliceOpcode = SNat 6 -> SNat 0 -> BitVector 32 -> BitVector ((6 + 1) - 0)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 6
d6 SNat 0
d0

sliceFunct3 :: BitVector 32 -> BitVector 3
sliceFunct3 :: BitVector 32 -> BitVector 3
sliceFunct3 = SNat 14 -> SNat 12 -> BitVector 32 -> BitVector ((14 + 1) - 12)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 14
d14 SNat 12
d12

sliceFunct7 :: BitVector 32 -> BitVector 7
sliceFunct7 :: BitVector 32 -> BitVector 7
sliceFunct7 = SNat 31 -> SNat 25 -> BitVector 32 -> BitVector ((31 + 1) - 25)
forall a (m :: Nat) (i :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ ((m + 1) + i)) =>
SNat m -> SNat n -> a -> BitVector ((m + 1) - n)
slice SNat 31
d31 SNat 25
d25