Copyright	(c) David Cox 2024
License	BSD-3-Clause
Maintainer	standardsemiconductor@gmail.com
Safe Haskell	None
Language	Haskell2010

Lion.Rvfi

Description

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 for more information about the interface. To verify the Lion core, see lion-formal.

Synopsis

data RvfiCsr (n :: Nat) = RvfiCsr {
- _wdataCsr :: "wdata" ::: BitVector n
- _rdataCsr :: "rdata" ::: BitVector n
- _wmaskCsr :: "wmask" ::: BitVector n
- _rmaskCsr :: "rmask" ::: BitVector n
}
rdataCsr :: forall (n :: Nat) f. Functor f => (("rdata" ::: BitVector n) -> f ("rdata" ::: BitVector n)) -> RvfiCsr n -> f (RvfiCsr n)
rmaskCsr :: forall (n :: Nat) f. Functor f => (("rmask" ::: BitVector n) -> f ("rmask" ::: BitVector n)) -> RvfiCsr n -> f (RvfiCsr n)
wdataCsr :: forall (n :: Nat) f. Functor f => (("wdata" ::: BitVector n) -> f ("wdata" ::: BitVector n)) -> RvfiCsr n -> f (RvfiCsr n)
wmaskCsr :: forall (n :: Nat) f. Functor f => (("wmask" ::: BitVector n) -> f ("wmask" ::: BitVector n)) -> RvfiCsr n -> f (RvfiCsr n)
data Rvfi = Rvfi {
- _rvfiValid :: "valid" ::: Bool
- _rvfiOrder :: "order" ::: BitVector 64
- _rvfiInsn :: "insn" ::: BitVector 32
- _rvfiTrap :: "trap" ::: Bool
- _rvfiHalt :: "halt" ::: Bool
- _rvfiIntr :: "intr" ::: Bool
- _rvfiMode :: "mode" ::: BitVector 2
- _rvfiIxl :: "ixl" ::: BitVector 2
- _rvfiRs1Addr :: "rs1_addr" ::: Unsigned 5
- _rvfiRs2Addr :: "rs2_addr" ::: Unsigned 5
- _rvfiRs1Data :: "rs1_rdata" ::: BitVector 32
- _rvfiRs2Data :: "rs2_rdata" ::: BitVector 32
- _rvfiRdAddr :: "rd_addr" ::: Unsigned 5
- _rvfiRdWData :: "rd_wdata" ::: BitVector 32
- _rvfiPcRData :: "pc_rdata" ::: BitVector 32
- _rvfiPcWData :: "pc_wdata" ::: BitVector 32
- _rvfiMemAddr :: "mem_addr" ::: BitVector 32
- _rvfiMemRMask :: "mem_rmask" ::: BitVector 4
- _rvfiMemWMask :: "mem_wmask" ::: BitVector 4
- _rvfiMemRData :: "mem_rdata" ::: BitVector 32
- _rvfiMemWData :: "mem_wdata" ::: BitVector 32
- _rvfiCsrMinstret :: "csr_minstret" ::: RvfiCsr 64
- _rvfiCsrMcycle :: "csr_mcycle" ::: RvfiCsr 64
- _rvfiCsrMscratch :: "csr_mscratch" ::: RvfiCsr 32
- _rvfiCsrMstatus :: "csr_mstatus" ::: RvfiCsr 32
- _rvfiCsrMisa :: "csr_misa" ::: RvfiCsr 32
}
rvfiCsrMcycle :: Lens' Rvfi ("csr_mcycle" ::: RvfiCsr 64)
rvfiCsrMinstret :: Lens' Rvfi ("csr_minstret" ::: RvfiCsr 64)
rvfiCsrMisa :: Lens' Rvfi ("csr_misa" ::: RvfiCsr 32)
rvfiCsrMscratch :: Lens' Rvfi ("csr_mscratch" ::: RvfiCsr 32)
rvfiCsrMstatus :: Lens' Rvfi ("csr_mstatus" ::: RvfiCsr 32)
rvfiHalt :: Lens' Rvfi ("halt" ::: Bool)
rvfiInsn :: Lens' Rvfi ("insn" ::: BitVector 32)
rvfiIntr :: Lens' Rvfi ("intr" ::: Bool)
rvfiIxl :: Lens' Rvfi ("ixl" ::: BitVector 2)
rvfiMemAddr :: Lens' Rvfi ("mem_addr" ::: BitVector 32)
rvfiMemRData :: Lens' Rvfi ("mem_rdata" ::: BitVector 32)
rvfiMemRMask :: Lens' Rvfi ("mem_rmask" ::: BitVector 4)
rvfiMemWData :: Lens' Rvfi ("mem_wdata" ::: BitVector 32)
rvfiMemWMask :: Lens' Rvfi ("mem_wmask" ::: BitVector 4)
rvfiMode :: Lens' Rvfi ("mode" ::: BitVector 2)
rvfiOrder :: Lens' Rvfi ("order" ::: BitVector 64)
rvfiPcRData :: Lens' Rvfi ("pc_rdata" ::: BitVector 32)
rvfiPcWData :: Lens' Rvfi ("pc_wdata" ::: BitVector 32)
rvfiRdAddr :: Lens' Rvfi ("rd_addr" ::: Unsigned 5)
rvfiRdWData :: Lens' Rvfi ("rd_wdata" ::: BitVector 32)
rvfiRs1Addr :: Lens' Rvfi ("rs1_addr" ::: Unsigned 5)
rvfiRs1Data :: Lens' Rvfi ("rs1_rdata" ::: BitVector 32)
rvfiRs2Addr :: Lens' Rvfi ("rs2_addr" ::: Unsigned 5)
rvfiRs2Data :: Lens' Rvfi ("rs2_rdata" ::: BitVector 32)
rvfiTrap :: Lens' Rvfi ("trap" ::: Bool)
rvfiValid :: Lens' Rvfi ("valid" ::: Bool)
fromRvfi :: First Rvfi -> Rvfi
mkRvfi :: Rvfi

Documentation

data RvfiCsr (n :: Nat) Source #

RISC-V Formal Csr Interface

Constructors

RvfiCsr
Fields _wdataCsr :: "wdata" ::: BitVector n _rdataCsr :: "rdata" ::: BitVector n _wmaskCsr :: "wmask" ::: BitVector n _rmaskCsr :: "rmask" ::: BitVector n

Instances

Instances details

Generic (RvfiCsr n) Source #

Instance details

Defined in Lion.Rvfi

Associated Types

type Rep (RvfiCsr n)

Instance details

Defined in Lion.Rvfi

type Rep (RvfiCsr n) = D1 ('MetaData "RvfiCsr" "Lion.Rvfi" "lion-0.4.0.1-inplace" 'False) (C1 ('MetaCons "RvfiCsr" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_wdataCsr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("wdata" ::: BitVector n)) :*: S1 ('MetaSel ('Just "_rdataCsr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("rdata" ::: BitVector n))) :*: (S1 ('MetaSel ('Just "_wmaskCsr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("wmask" ::: BitVector n)) :*: S1 ('MetaSel ('Just "_rmaskCsr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("rmask" ::: BitVector n)))))

Methods

from :: RvfiCsr n -> Rep (RvfiCsr n) x #

to :: Rep (RvfiCsr n) x -> RvfiCsr n #

KnownNat n => Show (RvfiCsr n) Source #

Instance details

Defined in Lion.Rvfi

Methods

showsPrec :: Int -> RvfiCsr n -> ShowS #

show :: RvfiCsr n -> String #

showList :: [RvfiCsr n] -> ShowS #

KnownNat n => NFDataX (RvfiCsr n) Source #

Instance details

Defined in Lion.Rvfi

Methods

deepErrorX :: String -> RvfiCsr n #

hasUndefined :: RvfiCsr n -> Bool #

ensureSpine :: RvfiCsr n -> RvfiCsr n #

rnfX :: RvfiCsr n -> () #

KnownNat n => Eq (RvfiCsr n) Source #

Instance details

Defined in Lion.Rvfi

Methods

(==) :: RvfiCsr n -> RvfiCsr n -> Bool #

(/=) :: RvfiCsr n -> RvfiCsr n -> Bool #

type Rep (RvfiCsr n) Source #

Instance details

Defined in Lion.Rvfi

type Rep (RvfiCsr n) = D1 ('MetaData "RvfiCsr" "Lion.Rvfi" "lion-0.4.0.1-inplace" 'False) (C1 ('MetaCons "RvfiCsr" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_wdataCsr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("wdata" ::: BitVector n)) :*: S1 ('MetaSel ('Just "_rdataCsr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("rdata" ::: BitVector n))) :*: (S1 ('MetaSel ('Just "_wmaskCsr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("wmask" ::: BitVector n)) :*: S1 ('MetaSel ('Just "_rmaskCsr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("rmask" ::: BitVector n)))))

rdataCsr :: forall (n :: Nat) f. Functor f => (("rdata" ::: BitVector n) -> f ("rdata" ::: BitVector n)) -> RvfiCsr n -> f (RvfiCsr n) Source #

rmaskCsr :: forall (n :: Nat) f. Functor f => (("rmask" ::: BitVector n) -> f ("rmask" ::: BitVector n)) -> RvfiCsr n -> f (RvfiCsr n) Source #

wdataCsr :: forall (n :: Nat) f. Functor f => (("wdata" ::: BitVector n) -> f ("wdata" ::: BitVector n)) -> RvfiCsr n -> f (RvfiCsr n) Source #

wmaskCsr :: forall (n :: Nat) f. Functor f => (("wmask" ::: BitVector n) -> f ("wmask" ::: BitVector n)) -> RvfiCsr n -> f (RvfiCsr n) Source #

data Rvfi Source #

RISC-V Formal Interface

Constructors

Rvfi

Fields

_rvfiValid :: "valid" ::: Bool
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.
_rvfiOrder :: "order" ::: BitVector 64
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).
_rvfiInsn :: "insn" ::: BitVector 32
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
_rvfiTrap :: "trap" ::: Bool
rvfiTrap must be set for an instruction that cannot be decoded as a legal instruction, such as 0x00000000.
_rvfiHalt :: "halt" ::: 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.
_rvfiIntr :: "intr" ::: 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.
_rvfiMode :: "mode" ::: BitVector 2
rvfiMode must be set to the current privilege level, using the following encoding: 0=U-Mode, 1=S-Mode, 2=Reserved, 3=M-Mode
_rvfiIxl :: "ixl" ::: BitVector 2
rvfiIxl must be set to the value of MXLSXLUXL in the current privilege level, using the following encoding: 1=32, 2=64
_rvfiRs1Addr :: "rs1_addr" ::: Unsigned 5
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.
_rvfiRs2Addr :: "rs2_addr" ::: Unsigned 5
_rvfiRs1Data :: "rs1_rdata" ::: BitVector 32
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.
_rvfiRs2Data :: "rs2_rdata" ::: BitVector 32
_rvfiRdAddr :: "rd_addr" ::: Unsigned 5
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.
_rvfiRdWData :: "rd_wdata" ::: BitVector 32
rvfiRdWData is the value of the register addressed by rd after execution of this instruction. This output must be zero when rd is zero.
_rvfiPcRData :: "pc_rdata" ::: 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.
_rvfiPcWData :: "pc_wdata" ::: BitVector 32
_rvfiMemAddr :: "mem_addr" ::: BitVector 32
For memory operations (rvfiMemRMask and/or rvfiMemWMask are non-zero), rvfiMemAddr holds the accessed memory location.
_rvfiMemRMask :: "mem_rmask" ::: BitVector 4
rvfiMemRMask is a bitmask that specifies which bytes in rvfiMemRData contain valid read data from rvfiMemAddr.
_rvfiMemWMask :: "mem_wmask" ::: BitVector 4
rvfiMemWMask is a bitmask that specifies which bytes in rvfiMemWData contain valid data this is written to rvfiMemAddr.
_rvfiMemRData :: "mem_rdata" ::: BitVector 32
rvfiMemRData is the pre-state data read from rvfiMemAddr. rvfiMemRMask specifies which bytes are valid.
_rvfiMemWData :: "mem_wdata" ::: BitVector 32
rvfiMemWData is the post-state data written to rvfiMemAddr. rvfiMemWMask specifies which bytes are valid.
_rvfiCsrMinstret :: "csr_minstret" ::: RvfiCsr 64
_rvfiCsrMcycle :: "csr_mcycle" ::: RvfiCsr 64
_rvfiCsrMscratch :: "csr_mscratch" ::: RvfiCsr 32
_rvfiCsrMstatus :: "csr_mstatus" ::: RvfiCsr 32
_rvfiCsrMisa :: "csr_misa" ::: RvfiCsr 32