module Lion.Rvfi where
import Clash.Prelude
import Control.Lens
import Data.Maybe
import Data.Monoid
data RvfiCsr n = RvfiCsr
{ RvfiCsr n -> "wdata" ::: BitVector n
_wdataCsr :: "wdata" ::: BitVector n
, RvfiCsr n -> "rdata" ::: BitVector n
_rdataCsr :: "rdata" ::: BitVector n
, RvfiCsr n -> "wmask" ::: BitVector n
_wmaskCsr :: "wmask" ::: BitVector n
, RvfiCsr n -> "rmask" ::: BitVector n
_rmaskCsr :: "rmask" ::: BitVector n
}
deriving stock ((forall x. RvfiCsr n -> Rep (RvfiCsr n) x)
-> (forall x. Rep (RvfiCsr n) x -> RvfiCsr n)
-> Generic (RvfiCsr n)
forall x. Rep (RvfiCsr n) x -> RvfiCsr n
forall x. RvfiCsr n -> Rep (RvfiCsr n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (n :: Nat) x. Rep (RvfiCsr n) x -> RvfiCsr n
forall (n :: Nat) x. RvfiCsr n -> Rep (RvfiCsr n) x
$cto :: forall (n :: Nat) x. Rep (RvfiCsr n) x -> RvfiCsr n
$cfrom :: forall (n :: Nat) x. RvfiCsr n -> Rep (RvfiCsr n) x
Generic, Int -> RvfiCsr n -> ShowS
[RvfiCsr n] -> ShowS
RvfiCsr n -> String
(Int -> RvfiCsr n -> ShowS)
-> (RvfiCsr n -> String)
-> ([RvfiCsr n] -> ShowS)
-> Show (RvfiCsr n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat). KnownNat n => Int -> RvfiCsr n -> ShowS
forall (n :: Nat). KnownNat n => [RvfiCsr n] -> ShowS
forall (n :: Nat). KnownNat n => RvfiCsr n -> String
showList :: [RvfiCsr n] -> ShowS
$cshowList :: forall (n :: Nat). KnownNat n => [RvfiCsr n] -> ShowS
show :: RvfiCsr n -> String
$cshow :: forall (n :: Nat). KnownNat n => RvfiCsr n -> String
showsPrec :: Int -> RvfiCsr n -> ShowS
$cshowsPrec :: forall (n :: Nat). KnownNat n => Int -> RvfiCsr n -> ShowS
Show, RvfiCsr n -> RvfiCsr n -> Bool
(RvfiCsr n -> RvfiCsr n -> Bool)
-> (RvfiCsr n -> RvfiCsr n -> Bool) -> Eq (RvfiCsr n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: Nat). KnownNat n => RvfiCsr n -> RvfiCsr n -> Bool
/= :: RvfiCsr n -> RvfiCsr n -> Bool
$c/= :: forall (n :: Nat). KnownNat n => RvfiCsr n -> RvfiCsr n -> Bool
== :: RvfiCsr n -> RvfiCsr n -> Bool
$c== :: forall (n :: Nat). KnownNat n => RvfiCsr n -> RvfiCsr n -> Bool
Eq)
deriving anyclass HasCallStack => String -> RvfiCsr n
RvfiCsr n -> Bool
RvfiCsr n -> ()
RvfiCsr n -> RvfiCsr n
(HasCallStack => String -> RvfiCsr n)
-> (RvfiCsr n -> Bool)
-> (RvfiCsr n -> RvfiCsr n)
-> (RvfiCsr n -> ())
-> NFDataX (RvfiCsr n)
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
forall (n :: Nat).
(KnownNat n, HasCallStack) =>
String -> RvfiCsr n
forall (n :: Nat). KnownNat n => RvfiCsr n -> Bool
forall (n :: Nat). KnownNat n => RvfiCsr n -> ()
forall (n :: Nat). KnownNat n => RvfiCsr n -> RvfiCsr n
rnfX :: RvfiCsr n -> ()
$crnfX :: forall (n :: Nat). KnownNat n => RvfiCsr n -> ()
ensureSpine :: RvfiCsr n -> RvfiCsr n
$censureSpine :: forall (n :: Nat). KnownNat n => RvfiCsr n -> RvfiCsr n
hasUndefined :: RvfiCsr n -> Bool
$chasUndefined :: forall (n :: Nat). KnownNat n => RvfiCsr n -> Bool
deepErrorX :: String -> RvfiCsr n
$cdeepErrorX :: forall (n :: Nat).
(KnownNat n, HasCallStack) =>
String -> RvfiCsr n
NFDataX
makeLenses ''RvfiCsr
data Rvfi = Rvfi
{
Rvfi -> Bool
_rvfiValid :: "valid" ::: Bool
, Rvfi -> "order" ::: BitVector 64
_rvfiOrder :: "order" ::: BitVector 64
, Rvfi -> "insn" ::: BitVector 32
_rvfiInsn :: "insn" ::: BitVector 32
, Rvfi -> Bool
_rvfiTrap :: "trap" ::: Bool
, Rvfi -> Bool
_rvfiHalt :: "halt" ::: Bool
, Rvfi -> Bool
_rvfiIntr :: "intr" ::: Bool
, Rvfi -> "mode" ::: BitVector 2
_rvfiMode :: "mode" ::: BitVector 2
, Rvfi -> "mode" ::: BitVector 2
_rvfiIxl :: "ixl" ::: BitVector 2
, Rvfi -> "rs1_addr" ::: Unsigned 5
_rvfiRs1Addr :: "rs1_addr" ::: Unsigned 5
, Rvfi -> "rs1_addr" ::: Unsigned 5
_rvfiRs2Addr :: "rs2_addr" ::: Unsigned 5
, Rvfi -> "insn" ::: BitVector 32
_rvfiRs1Data :: "rs1_rdata" ::: BitVector 32
, Rvfi -> "insn" ::: BitVector 32
_rvfiRs2Data :: "rs2_rdata" ::: BitVector 32
, Rvfi -> "rs1_addr" ::: Unsigned 5
_rvfiRdAddr :: "rd_addr" ::: Unsigned 5
, Rvfi -> "insn" ::: BitVector 32
_rvfiRdWData :: "rd_wdata" ::: BitVector 32
, Rvfi -> "insn" ::: BitVector 32
_rvfiPcRData :: "pc_rdata" ::: BitVector 32
, Rvfi -> "insn" ::: BitVector 32
_rvfiPcWData :: "pc_wdata" ::: BitVector 32
, Rvfi -> "insn" ::: BitVector 32
_rvfiMemAddr :: "mem_addr" ::: BitVector 32
, Rvfi -> "mem_rmask" ::: BitVector 4
_rvfiMemRMask :: "mem_rmask" ::: BitVector 4
, Rvfi -> "mem_rmask" ::: BitVector 4
_rvfiMemWMask :: "mem_wmask" ::: BitVector 4
, Rvfi -> "insn" ::: BitVector 32
_rvfiMemRData :: "mem_rdata" ::: BitVector 32
, Rvfi -> "insn" ::: BitVector 32
_rvfiMemWData :: "mem_wdata" ::: BitVector 32
, Rvfi -> "csr_minstret" ::: RvfiCsr 64
_rvfiCsrMinstret :: "csr_minstret" ::: RvfiCsr 64
, Rvfi -> "csr_minstret" ::: RvfiCsr 64
_rvfiCsrMcycle :: "csr_mcycle" ::: RvfiCsr 64
, Rvfi -> "csr_mscratch" ::: RvfiCsr 32
_rvfiCsrMscratch :: "csr_mscratch" ::: RvfiCsr 32
, Rvfi -> "csr_mscratch" ::: RvfiCsr 32
_rvfiCsrMstatus :: "csr_mstatus" ::: RvfiCsr 32
, Rvfi -> "csr_mscratch" ::: RvfiCsr 32
_rvfiCsrMisa :: "csr_misa" ::: RvfiCsr 32
}
deriving stock ((forall x. Rvfi -> Rep Rvfi x)
-> (forall x. Rep Rvfi x -> Rvfi) -> Generic Rvfi
forall x. Rep Rvfi x -> Rvfi
forall x. Rvfi -> Rep Rvfi x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Rvfi x -> Rvfi
$cfrom :: forall x. Rvfi -> Rep Rvfi x
Generic, Int -> Rvfi -> ShowS
[Rvfi] -> ShowS
Rvfi -> String
(Int -> Rvfi -> ShowS)
-> (Rvfi -> String) -> ([Rvfi] -> ShowS) -> Show Rvfi
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rvfi] -> ShowS
$cshowList :: [Rvfi] -> ShowS
show :: Rvfi -> String
$cshow :: Rvfi -> String
showsPrec :: Int -> Rvfi -> ShowS
$cshowsPrec :: Int -> Rvfi -> ShowS
Show, Rvfi -> Rvfi -> Bool
(Rvfi -> Rvfi -> Bool) -> (Rvfi -> Rvfi -> Bool) -> Eq Rvfi
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rvfi -> Rvfi -> Bool
$c/= :: Rvfi -> Rvfi -> Bool
== :: Rvfi -> Rvfi -> Bool
$c== :: Rvfi -> Rvfi -> Bool
Eq)
deriving anyclass HasCallStack => String -> Rvfi
Rvfi -> Bool
Rvfi -> ()
Rvfi -> Rvfi
(HasCallStack => String -> Rvfi)
-> (Rvfi -> Bool) -> (Rvfi -> Rvfi) -> (Rvfi -> ()) -> NFDataX Rvfi
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
rnfX :: Rvfi -> ()
$crnfX :: Rvfi -> ()
ensureSpine :: Rvfi -> Rvfi
$censureSpine :: Rvfi -> Rvfi
hasUndefined :: Rvfi -> Bool
$chasUndefined :: Rvfi -> Bool
deepErrorX :: String -> Rvfi
$cdeepErrorX :: HasCallStack => String -> Rvfi
NFDataX
makeLenses ''Rvfi
fromRvfi :: First Rvfi -> Rvfi
fromRvfi :: First Rvfi -> Rvfi
fromRvfi = Rvfi -> Maybe Rvfi -> Rvfi
forall a. a -> Maybe a -> a
fromMaybe Rvfi
mkRvfi (Maybe Rvfi -> Rvfi)
-> (First Rvfi -> Maybe Rvfi) -> First Rvfi -> Rvfi
forall b c a. (b -> c) -> (a -> b) -> a -> c
. First Rvfi -> Maybe Rvfi
forall a. First a -> Maybe a
getFirst
mkRvfi :: Rvfi
mkRvfi :: Rvfi
mkRvfi = Rvfi :: Bool
-> ("order" ::: BitVector 64)
-> ("insn" ::: BitVector 32)
-> Bool
-> Bool
-> Bool
-> ("mode" ::: BitVector 2)
-> ("mode" ::: BitVector 2)
-> ("rs1_addr" ::: Unsigned 5)
-> ("rs1_addr" ::: Unsigned 5)
-> ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> ("rs1_addr" ::: Unsigned 5)
-> ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> ("mem_rmask" ::: BitVector 4)
-> ("mem_rmask" ::: BitVector 4)
-> ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> ("csr_minstret" ::: RvfiCsr 64)
-> ("csr_minstret" ::: RvfiCsr 64)
-> ("csr_mscratch" ::: RvfiCsr 32)
-> ("csr_mscratch" ::: RvfiCsr 32)
-> ("csr_mscratch" ::: RvfiCsr 32)
-> Rvfi
Rvfi
{ _rvfiValid :: Bool
_rvfiValid = Bool
False
, _rvfiOrder :: "order" ::: BitVector 64
_rvfiOrder = "order" ::: BitVector 64
0
, _rvfiInsn :: "insn" ::: BitVector 32
_rvfiInsn = "insn" ::: BitVector 32
0
, _rvfiTrap :: Bool
_rvfiTrap = Bool
False
, _rvfiHalt :: Bool
_rvfiHalt = Bool
False
, _rvfiIntr :: Bool
_rvfiIntr = Bool
False
, _rvfiMode :: "mode" ::: BitVector 2
_rvfiMode = "mode" ::: BitVector 2
3
, _rvfiIxl :: "mode" ::: BitVector 2
_rvfiIxl = "mode" ::: BitVector 2
1
, _rvfiRs1Addr :: "rs1_addr" ::: Unsigned 5
_rvfiRs1Addr = "rs1_addr" ::: Unsigned 5
0
, _rvfiRs2Addr :: "rs1_addr" ::: Unsigned 5
_rvfiRs2Addr = "rs1_addr" ::: Unsigned 5
0
, _rvfiRs1Data :: "insn" ::: BitVector 32
_rvfiRs1Data = "insn" ::: BitVector 32
0
, _rvfiRs2Data :: "insn" ::: BitVector 32
_rvfiRs2Data = "insn" ::: BitVector 32
0
, _rvfiRdAddr :: "rs1_addr" ::: Unsigned 5
_rvfiRdAddr = "rs1_addr" ::: Unsigned 5
0
, _rvfiRdWData :: "insn" ::: BitVector 32
_rvfiRdWData = "insn" ::: BitVector 32
0
, _rvfiPcRData :: "insn" ::: BitVector 32
_rvfiPcRData = "insn" ::: BitVector 32
0
, _rvfiPcWData :: "insn" ::: BitVector 32
_rvfiPcWData = "insn" ::: BitVector 32
0
, _rvfiMemAddr :: "insn" ::: BitVector 32
_rvfiMemAddr = "insn" ::: BitVector 32
0
, _rvfiMemRMask :: "mem_rmask" ::: BitVector 4
_rvfiMemRMask = "mem_rmask" ::: BitVector 4
0
, _rvfiMemWMask :: "mem_rmask" ::: BitVector 4
_rvfiMemWMask = "mem_rmask" ::: BitVector 4
0
, _rvfiMemRData :: "insn" ::: BitVector 32
_rvfiMemRData = "insn" ::: BitVector 32
0
, _rvfiMemWData :: "insn" ::: BitVector 32
_rvfiMemWData = "insn" ::: BitVector 32
0
, _rvfiCsrMinstret :: "csr_minstret" ::: RvfiCsr 64
_rvfiCsrMinstret = ("order" ::: BitVector 64)
-> ("order" ::: BitVector 64)
-> ("order" ::: BitVector 64)
-> ("order" ::: BitVector 64)
-> "csr_minstret" ::: RvfiCsr 64
forall (n :: Nat).
("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> RvfiCsr n
RvfiCsr "order" ::: BitVector 64
0 "order" ::: BitVector 64
0 "order" ::: BitVector 64
0 "order" ::: BitVector 64
0
, _rvfiCsrMcycle :: "csr_minstret" ::: RvfiCsr 64
_rvfiCsrMcycle = ("order" ::: BitVector 64)
-> ("order" ::: BitVector 64)
-> ("order" ::: BitVector 64)
-> ("order" ::: BitVector 64)
-> "csr_minstret" ::: RvfiCsr 64
forall (n :: Nat).
("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> RvfiCsr n
RvfiCsr "order" ::: BitVector 64
0 "order" ::: BitVector 64
0 "order" ::: BitVector 64
0 "order" ::: BitVector 64
0
, _rvfiCsrMscratch :: "csr_mscratch" ::: RvfiCsr 32
_rvfiCsrMscratch = ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> "csr_mscratch" ::: RvfiCsr 32
forall (n :: Nat).
("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> RvfiCsr n
RvfiCsr "insn" ::: BitVector 32
0 "insn" ::: BitVector 32
0 "insn" ::: BitVector 32
0 "insn" ::: BitVector 32
0
, _rvfiCsrMstatus :: "csr_mscratch" ::: RvfiCsr 32
_rvfiCsrMstatus = ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> "csr_mscratch" ::: RvfiCsr 32
forall (n :: Nat).
("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> RvfiCsr n
RvfiCsr "insn" ::: BitVector 32
0 "insn" ::: BitVector 32
0 "insn" ::: BitVector 32
0 "insn" ::: BitVector 32
0
, _rvfiCsrMisa :: "csr_mscratch" ::: RvfiCsr 32
_rvfiCsrMisa = ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> ("insn" ::: BitVector 32)
-> "csr_mscratch" ::: RvfiCsr 32
forall (n :: Nat).
("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> RvfiCsr n
RvfiCsr "insn" ::: BitVector 32
0 "insn" ::: BitVector 32
0 "insn" ::: BitVector 32
0 "insn" ::: BitVector 32
0
}