{-|
Module      : Lion.Rvfi
Description : Lion RISC-V Formal Verification Interface
Copyright   : (c) David Cox, 2024
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
  { forall (n :: Nat). RvfiCsr n -> "wdata" ::: BitVector n
_wdataCsr :: "wdata" ::: BitVector n
  , forall (n :: Nat). RvfiCsr n -> "wdata" ::: BitVector n
_rdataCsr :: "rdata" ::: BitVector n
  , forall (n :: Nat). RvfiCsr n -> "wdata" ::: BitVector n
_wmaskCsr :: "wmask" ::: BitVector n
  , forall (n :: Nat). RvfiCsr n -> "wdata" ::: 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 (n :: Nat) x. Rep (RvfiCsr n) x -> RvfiCsr n
forall (n :: Nat) x. RvfiCsr n -> Rep (RvfiCsr n) x
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
$cfrom :: forall (n :: Nat) x. RvfiCsr n -> Rep (RvfiCsr n) x
from :: forall x. RvfiCsr n -> Rep (RvfiCsr n) x
$cto :: forall (n :: Nat) x. Rep (RvfiCsr n) x -> RvfiCsr n
to :: forall x. Rep (RvfiCsr n) x -> RvfiCsr n
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 (n :: Nat). KnownNat n => Int -> RvfiCsr n -> ShowS
forall (n :: Nat). KnownNat n => [RvfiCsr n] -> ShowS
forall (n :: Nat). KnownNat n => RvfiCsr n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: Nat). KnownNat n => Int -> RvfiCsr n -> ShowS
showsPrec :: Int -> RvfiCsr n -> ShowS
$cshow :: forall (n :: Nat). KnownNat n => RvfiCsr n -> String
show :: RvfiCsr n -> String
$cshowList :: forall (n :: Nat). KnownNat n => [RvfiCsr n] -> ShowS
showList :: [RvfiCsr n] -> ShowS
Show, RvfiCsr n -> RvfiCsr n -> Bool
(RvfiCsr n -> RvfiCsr n -> Bool)
-> (RvfiCsr n -> RvfiCsr n -> Bool) -> Eq (RvfiCsr n)
forall (n :: Nat). KnownNat n => RvfiCsr n -> RvfiCsr n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: 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 (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
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
$cdeepErrorX :: forall (n :: Nat).
(KnownNat n, HasCallStack) =>
String -> RvfiCsr n
deepErrorX :: HasCallStack => String -> RvfiCsr n
$chasUndefined :: forall (n :: Nat). KnownNat n => RvfiCsr n -> Bool
hasUndefined :: RvfiCsr n -> Bool
$censureSpine :: forall (n :: Nat). KnownNat n => RvfiCsr n -> RvfiCsr n
ensureSpine :: RvfiCsr n -> RvfiCsr n
$crnfX :: forall (n :: Nat). KnownNat n => RvfiCsr n -> ()
rnfX :: RvfiCsr n -> ()
NFDataX
makeLenses ''RvfiCsr

-- | RISC-V Formal Interface
data Rvfi = Rvfi
  { -- | When the core retires an instruction, it asserts the `rvfiValid` signal
    -- and uses the signals described in Rvfi to output the details of the
    -- retired instruction. The signals below are only valid during such a
    -- cycle and can be driven to arbitrary values in a cycle in which `_rvfiValid
    -- is not asserted.
    Rvfi -> Bool
_rvfiValid       :: "valid"        ::: Bool

    -- | The `rvfiOrder` field must be set to the instruction index. No indices
    -- must be used twice and there must be no gaps. Instructions may be retired
    -- in a reordered fashion, as long as causality is preserved
    -- (register nad memory write operations must be retired before the read
    -- operations that depend on them).
  , Rvfi -> BitVector 64
_rvfiOrder       :: "order"        ::: BitVector 64

    -- | `rvfiInsn` is the instruction word for the retired instruction.
    -- In case of an instruction with fewer than ILEN bits, the upper bits
    -- of this output must all be zero. For compressed instructions the
    -- compressed instruction word must be output on this port.
    -- For fused instructions the complete fused instruciton sequence must
    -- be output
  , Rvfi -> BitVector 32
_rvfiInsn        :: "insn"         ::: BitVector 32

    -- | `rvfiTrap` must be set for an instruction that cannot be decoded
    -- as a legal instruction, such as 0x00000000.
  , Rvfi -> Bool
_rvfiTrap        :: "trap"         ::: Bool

    -- | The signal `rvfiHalt` must be set when the instruction is
    -- the last instruction that the core retires before halting execution.
    -- It should not be set for an instruction that triggers a trap condition
    -- if the CPU reacts to the trap by executing a trap handler. This signal
    -- enable verification of liveness properties.
  , Rvfi -> Bool
_rvfiHalt        :: "halt"         ::: Bool

    -- | `rvfiIntr` must be set for the first instruction that is part of a
    -- trap handler, i.e. an instruction that has a `rvfiPcRData` that
    -- does not match the `rvfiPcWData` of the previous instruction.
  , Rvfi -> Bool
_rvfiIntr        :: "intr"         ::: Bool

    -- | `rvfiMode` must be set to the current privilege level, using the
    -- following encoding: 0=U-Mode, 1=S-Mode, 2=Reserved, 3=M-Mode
  , Rvfi -> BitVector 2
_rvfiMode        :: "mode"         ::: BitVector 2

    -- | `rvfiIxl` must be set to the value of MXL/SXL/UXL in the current
    -- privilege level, using the following encoding: 1=32, 2=64
  , Rvfi -> BitVector 2
_rvfiIxl         :: "ixl"          ::: BitVector 2

    -- | `rvfiRs1Addr` and `rvfiRs2Addr` are the decoded rs1 and rs2
    -- register addresses for the retired instruction. For an instruction
    -- that reads no rs1/rs2 register, this output can have an arbitrary value.
    -- However if this output is nonzero then `rvfiRs1Data` or `rvfiRs2Data` must
    -- carry the value stored in that register in the pre-state.
  , Rvfi -> Unsigned 5
_rvfiRs1Addr     :: "rs1_addr"     ::: Unsigned 5
  , Rvfi -> Unsigned 5
_rvfiRs2Addr     :: "rs2_addr"     ::: Unsigned 5

    -- | `rvfiRs1Data` and `rvfiRs2Data` are the values of the register
    -- addressed by rs1 and rs2 before execute of this instruction.
    -- This output must be zero when rs1/rs2 is zero.
  , Rvfi -> BitVector 32
_rvfiRs1Data     :: "rs1_rdata"    ::: BitVector 32
  , Rvfi -> BitVector 32
_rvfiRs2Data     :: "rs2_rdata"    ::: BitVector 32

    -- | `rvfiRdAddr` is the decoded rd register address for the retired
    -- instruction. For an instruction that writes no rd register, this output
    -- must always be zero.
  , Rvfi -> Unsigned 5
_rvfiRdAddr      :: "rd_addr"      ::: Unsigned 5

    -- | `rvfiRdWData` is the value of the register addressed by rd after
    -- execution of this instruction. This output must be zero when rd
    -- is zero.
  , Rvfi -> BitVector 32
_rvfiRdWData     :: "rd_wdata"     ::: BitVector 32

    -- | This is the program counter (pc) before (`rvfiPcRData`) and after
    -- (`rvfiPcWData`) execution of this instruciton. I.e. this is the
    -- address of the retired instruction and the address of the next
    -- instruction.
  , Rvfi -> BitVector 32
_rvfiPcRData     :: "pc_rdata"     ::: BitVector 32
  , Rvfi -> BitVector 32
_rvfiPcWData     :: "pc_wdata"     ::: BitVector 32

    -- | For memory operations (`rvfiMemRMask` and/or `rvfiMemWMask` are non-zero),
    -- `rvfiMemAddr` holds the accessed memory location.
  , Rvfi -> BitVector 32
_rvfiMemAddr     :: "mem_addr"     ::: BitVector 32

    -- | `rvfiMemRMask` is a bitmask that specifies which bytes in `rvfiMemRData`
    -- contain valid read data from `rvfiMemAddr`.
  , Rvfi -> BitVector 4
_rvfiMemRMask    :: "mem_rmask"    ::: BitVector 4

    -- | `rvfiMemWMask` is a bitmask that specifies which bytes in `rvfiMemWData` 
    -- contain valid data this is written to `rvfiMemAddr`.
  , Rvfi -> BitVector 4
_rvfiMemWMask    :: "mem_wmask"    ::: BitVector 4

    -- | `rvfiMemRData` is the pre-state data read from `rvfiMemAddr`.
    -- `rvfiMemRMask` specifies which bytes are valid.
  , Rvfi -> BitVector 32
_rvfiMemRData    :: "mem_rdata"    ::: BitVector 32

    -- | `rvfiMemWData` is the post-state data written to `rvfiMemAddr`.
    -- `rvfiMemWMask` specifies which bytes are valid.
  , Rvfi -> 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
$cfrom :: forall x. Rvfi -> Rep Rvfi x
from :: forall x. Rvfi -> Rep Rvfi x
$cto :: forall x. Rep Rvfi x -> Rvfi
to :: forall x. Rep Rvfi x -> Rvfi
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
$cshowsPrec :: Int -> Rvfi -> ShowS
showsPrec :: Int -> Rvfi -> ShowS
$cshow :: Rvfi -> String
show :: Rvfi -> String
$cshowList :: [Rvfi] -> ShowS
showList :: [Rvfi] -> ShowS
Show, Rvfi -> Rvfi -> Bool
(Rvfi -> Rvfi -> Bool) -> (Rvfi -> Rvfi -> Bool) -> Eq Rvfi
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Rvfi -> Rvfi -> Bool
== :: Rvfi -> Rvfi -> Bool
$c/= :: Rvfi -> Rvfi -> Bool
/= :: 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
$cdeepErrorX :: HasCallStack => String -> Rvfi
deepErrorX :: HasCallStack => String -> Rvfi
$chasUndefined :: Rvfi -> Bool
hasUndefined :: Rvfi -> Bool
$censureSpine :: Rvfi -> Rvfi
ensureSpine :: Rvfi -> Rvfi
$crnfX :: Rvfi -> ()
rnfX :: 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
  { _rvfiValid :: Bool
_rvfiValid       = Bool
False
  , _rvfiOrder :: BitVector 64
_rvfiOrder       = BitVector 64
0    
  , _rvfiInsn :: BitVector 32
_rvfiInsn        = BitVector 32
0    
  , _rvfiTrap :: Bool
_rvfiTrap        = Bool
False
  , _rvfiHalt :: Bool
_rvfiHalt        = Bool
False
  , _rvfiIntr :: Bool
_rvfiIntr        = Bool
False
  , _rvfiMode :: BitVector 2
_rvfiMode        = BitVector 2
3    
  , _rvfiIxl :: BitVector 2
_rvfiIxl         = BitVector 2
1    
  , _rvfiRs1Addr :: Unsigned 5
_rvfiRs1Addr     = Unsigned 5
0    
  , _rvfiRs2Addr :: Unsigned 5
_rvfiRs2Addr     = Unsigned 5
0    
  , _rvfiRs1Data :: BitVector 32
_rvfiRs1Data     = BitVector 32
0    
  , _rvfiRs2Data :: BitVector 32
_rvfiRs2Data     = BitVector 32
0    
  , _rvfiRdAddr :: Unsigned 5
_rvfiRdAddr      = Unsigned 5
0    
  , _rvfiRdWData :: BitVector 32
_rvfiRdWData     = BitVector 32
0    
  , _rvfiPcRData :: BitVector 32
_rvfiPcRData     = BitVector 32
0    
  , _rvfiPcWData :: BitVector 32
_rvfiPcWData     = BitVector 32
0    
  , _rvfiMemAddr :: BitVector 32
_rvfiMemAddr     = BitVector 32
0    
  , _rvfiMemRMask :: BitVector 4
_rvfiMemRMask    = BitVector 4
0    
  , _rvfiMemWMask :: BitVector 4
_rvfiMemWMask    = BitVector 4
0    
  , _rvfiMemRData :: BitVector 32
_rvfiMemRData    = BitVector 32
0    
  , _rvfiMemWData :: BitVector 32
_rvfiMemWData    = BitVector 32
0    
  , _rvfiCsrMinstret :: "csr_minstret" ::: RvfiCsr 64
_rvfiCsrMinstret = BitVector 64
-> BitVector 64
-> BitVector 64
-> BitVector 64
-> "csr_minstret" ::: RvfiCsr 64
forall (n :: Nat).
("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> RvfiCsr n
RvfiCsr BitVector 64
0 BitVector 64
0 BitVector 64
0 BitVector 64
0
  , _rvfiCsrMcycle :: "csr_minstret" ::: RvfiCsr 64
_rvfiCsrMcycle   = BitVector 64
-> BitVector 64
-> BitVector 64
-> BitVector 64
-> "csr_minstret" ::: RvfiCsr 64
forall (n :: Nat).
("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> RvfiCsr n
RvfiCsr BitVector 64
0 BitVector 64
0 BitVector 64
0 BitVector 64
0
  , _rvfiCsrMscratch :: "csr_mscratch" ::: RvfiCsr 32
_rvfiCsrMscratch = BitVector 32
-> BitVector 32
-> BitVector 32
-> BitVector 32
-> "csr_mscratch" ::: RvfiCsr 32
forall (n :: Nat).
("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> RvfiCsr n
RvfiCsr BitVector 32
0 BitVector 32
0 BitVector 32
0 BitVector 32
0 
  , _rvfiCsrMstatus :: "csr_mscratch" ::: RvfiCsr 32
_rvfiCsrMstatus  = BitVector 32
-> BitVector 32
-> BitVector 32
-> BitVector 32
-> "csr_mscratch" ::: RvfiCsr 32
forall (n :: Nat).
("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> RvfiCsr n
RvfiCsr BitVector 32
0 BitVector 32
0 BitVector 32
0 BitVector 32
0
  , _rvfiCsrMisa :: "csr_mscratch" ::: RvfiCsr 32
_rvfiCsrMisa     = BitVector 32
-> BitVector 32
-> BitVector 32
-> BitVector 32
-> "csr_mscratch" ::: RvfiCsr 32
forall (n :: Nat).
("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> ("wdata" ::: BitVector n)
-> RvfiCsr n
RvfiCsr BitVector 32
0 BitVector 32
0 BitVector 32
0 BitVector 32
0
  }