Lion.Rvfi

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.

Documentation

data RvfiCsr n

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

KnownNat n => Eq (RvfiCsr n)

Defined in Lion.Rvfi

Methods

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

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

KnownNat n => Show (RvfiCsr n)

Defined in Lion.Rvfi

Methods

showsPrec :: Int -> RvfiCsr n -> ShowS

show :: RvfiCsr n -> String

showList :: [RvfiCsr n] -> ShowS

Generic (RvfiCsr n)

Defined in Lion.Rvfi

Associated Types

type Rep (RvfiCsr n) :: Type -> Type

Methods

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

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

KnownNat n => NFDataX (RvfiCsr n)

Defined in Lion.Rvfi

Methods

deepErrorX :: String -> RvfiCsr n

hasUndefined :: RvfiCsr n -> Bool

ensureSpine :: RvfiCsr n -> RvfiCsr n

rnfX :: RvfiCsr n -> ()

type Rep (RvfiCsr n)

Defined in Lion.Rvfi

type Rep (RvfiCsr n) = D1 ('MetaData "RvfiCsr" "Lion.Rvfi" "lion-0.3.0.0-5TeZzf2f4nX8XqM2dA3bRI" '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)))))

wmaskCsr :: forall n. Lens' (RvfiCsr n) ((:::) "wmask" (BitVector n))

wdataCsr :: forall n. Lens' (RvfiCsr n) ((:::) "wdata" (BitVector n))

rmaskCsr :: forall n. Lens' (RvfiCsr n) ((:::) "rmask" (BitVector n))

rdataCsr :: forall n. Lens' (RvfiCsr n) ((:::) "rdata" (BitVector n))

data Rvfi

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

Instances

Eq Rvfi

Defined in Lion.Rvfi

Methods

(==) :: Rvfi -> Rvfi -> Bool

(/=) :: Rvfi -> Rvfi -> Bool

Show Rvfi

Defined in Lion.Rvfi

Methods

showsPrec :: Int -> Rvfi -> ShowS

show :: Rvfi -> String

showList :: [Rvfi] -> ShowS

Generic Rvfi

Defined in Lion.Rvfi

Associated Types

type Rep Rvfi :: Type -> Type

Methods

from :: Rvfi -> Rep Rvfi x

to :: Rep Rvfi x -> Rvfi

NFDataX Rvfi

Defined in Lion.Rvfi

Methods

deepErrorX :: String -> Rvfi

hasUndefined :: Rvfi -> Bool

ensureSpine :: Rvfi -> Rvfi

rnfX :: Rvfi -> ()

type Rep Rvfi

Defined in Lion.Rvfi

type Rep Rvfi = D1 ('MetaData "Rvfi" "Lion.Rvfi" "lion-0.3.0.0-5TeZzf2f4nX8XqM2dA3bRI" 'False) (C1 ('MetaCons "Rvfi" 'PrefixI 'True) ((((S1 ('MetaSel ('Just "_rvfiValid") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("valid" ::: Bool)) :*: (S1 ('MetaSel ('Just "_rvfiOrder") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("order" ::: BitVector 64)) :*: S1 ('MetaSel ('Just "_rvfiInsn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("insn" ::: BitVector 32)))) :*: (S1 ('MetaSel ('Just "_rvfiTrap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("trap" ::: Bool)) :*: (S1 ('MetaSel ('Just "_rvfiHalt") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("halt" ::: Bool)) :*: S1 ('MetaSel ('Just "_rvfiIntr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("intr" ::: Bool))))) :*: ((S1 ('MetaSel ('Just "_rvfiMode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("mode" ::: BitVector 2)) :*: (S1 ('MetaSel ('Just "_rvfiIxl") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("ixl" ::: BitVector 2)) :*: S1 ('MetaSel ('Just "_rvfiRs1Addr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("rs1_addr" ::: Unsigned 5)))) :*: ((S1 ('MetaSel ('Just "_rvfiRs2Addr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("rs2_addr" ::: Unsigned 5)) :*: S1 ('MetaSel ('Just "_rvfiRs1Data") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("rs1_rdata" ::: BitVector 32))) :*: (S1 ('MetaSel ('Just "_rvfiRs2Data") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("rs2_rdata" ::: BitVector 32)) :*: S1 ('MetaSel ('Just "_rvfiRdAddr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("rd_addr" ::: Unsigned 5)))))) :*: (((S1 ('MetaSel ('Just "_rvfiRdWData") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("rd_wdata" ::: BitVector 32)) :*: (S1 ('MetaSel ('Just "_rvfiPcRData") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("pc_rdata" ::: BitVector 32)) :*: S1 ('MetaSel ('Just "_rvfiPcWData") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("pc_wdata" ::: BitVector 32)))) :*: (S1 ('MetaSel ('Just "_rvfiMemAddr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("mem_addr" ::: BitVector 32)) :*: (S1 ('MetaSel ('Just "_rvfiMemRMask") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("mem_rmask" ::: BitVector 4)) :*: S1 ('MetaSel ('Just "_rvfiMemWMask") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("mem_wmask" ::: BitVector 4))))) :*: ((S1 ('MetaSel ('Just "_rvfiMemRData") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("mem_rdata" ::: BitVector 32)) :*: (S1 ('MetaSel ('Just "_rvfiMemWData") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("mem_wdata" ::: BitVector 32)) :*: S1 ('MetaSel ('Just "_rvfiCsrMinstret") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("csr_minstret" ::: RvfiCsr 64)))) :*: ((S1 ('MetaSel ('Just "_rvfiCsrMcycle") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("csr_mcycle" ::: RvfiCsr 64)) :*: S1 ('MetaSel ('Just "_rvfiCsrMscratch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("csr_mscratch" ::: RvfiCsr 32))) :*: (S1 ('MetaSel ('Just "_rvfiCsrMstatus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("csr_mstatus" ::: RvfiCsr 32)) :*: S1 ('MetaSel ('Just "_rvfiCsrMisa") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ("csr_misa" ::: RvfiCsr 32))))))))

rvfiValid :: Lens' Rvfi ((:::) "valid" Bool)

rvfiTrap :: Lens' Rvfi ((:::) "trap" Bool)

rvfiRs2Data :: Lens' Rvfi ((:::) "rs2_rdata" (BitVector 32))

rvfiRs2Addr :: Lens' Rvfi ((:::) "rs2_addr" (Unsigned 5))

rvfiRs1Data :: Lens' Rvfi ((:::) "rs1_rdata" (BitVector 32))

rvfiRs1Addr :: Lens' Rvfi ((:::) "rs1_addr" (Unsigned 5))

rvfiRdWData :: Lens' Rvfi ((:::) "rd_wdata" (BitVector 32))

rvfiRdAddr :: Lens' Rvfi ((:::) "rd_addr" (Unsigned 5))

rvfiPcWData :: Lens' Rvfi ((:::) "pc_wdata" (BitVector 32))

rvfiPcRData :: Lens' Rvfi ((:::) "pc_rdata" (BitVector 32))

rvfiOrder :: Lens' Rvfi ((:::) "order" (BitVector 64))

rvfiMode :: Lens' Rvfi ((:::) "mode" (BitVector 2))

rvfiMemWMask :: Lens' Rvfi ((:::) "mem_wmask" (BitVector 4))

rvfiMemWData :: Lens' Rvfi ((:::) "mem_wdata" (BitVector 32))

rvfiMemRMask :: Lens' Rvfi ((:::) "mem_rmask" (BitVector 4))

rvfiMemRData :: Lens' Rvfi ((:::) "mem_rdata" (BitVector 32))

rvfiMemAddr :: Lens' Rvfi ((:::) "mem_addr" (BitVector 32))

rvfiIxl :: Lens' Rvfi ((:::) "ixl" (BitVector 2))

rvfiIntr :: Lens' Rvfi ((:::) "intr" Bool)

rvfiInsn :: Lens' Rvfi ((:::) "insn" (BitVector 32))

rvfiHalt :: Lens' Rvfi ((:::) "halt" Bool)

rvfiCsrMstatus :: Lens' Rvfi ((:::) "csr_mstatus" (RvfiCsr 32))

rvfiCsrMscratch :: Lens' Rvfi ((:::) "csr_mscratch" (RvfiCsr 32))

rvfiCsrMisa :: Lens' Rvfi ((:::) "csr_misa" (RvfiCsr 32))

rvfiCsrMinstret :: Lens' Rvfi ((:::) "csr_minstret" (RvfiCsr 64))

rvfiCsrMcycle :: Lens' Rvfi ((:::) "csr_mcycle" (RvfiCsr 64))

fromRvfi :: First Rvfi -> Rvfi

Unwrap Rvfi from First monoid

mkRvfi :: Rvfi

Construct the RISC-V Formal Interface