{-|
Module      : Lion.Rvfi
Description : Lion RISC-V Formal Verification Interface
Copyright   : (c) David Cox, 2021
License     : BSD-3-Clause
Maintainer  : standardsemiconductor@gmail.com

As the pipeline processes instructions, it populates the fields of the Rvfi data. When the instruction reaches the end of the pipeline, the core retires the instruction and writes the Rvfi data to output. This output is inspected and verified by the riscv-formal framework. See [riscv-formal](https://github.com/standardsemiconductor/riscv-formal) for more information about the interface. To verify the Lion core, see [lion-formal](https://github.com/standardsemiconductor/lion/tree/main/lion-formal).
-}

module Lion.Rvfi where

import Clash.Prelude
import Control.Lens
import Data.Maybe
import Data.Monoid

-- | RISC-V Formal Csr Interface
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

-- | RISC-V Formal Interface
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

-- | Unwrap Rvfi from First monoid
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

-- | Construct the RISC-V Formal Interface
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
  }