Copyright | (c) David Cox 2021 |
---|---|
License | BSD-3-Clause |
Maintainer | standardsemiconductor@gmail.com |
Safe Haskell | None |
Language | Haskell2010 |
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 = RvfiCsr {}
- 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 = 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
- 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
- mkRvfi :: Rvfi
Documentation
RISC-V Formal Csr Interface
Instances
KnownNat n => Eq (RvfiCsr n) Source # | |
KnownNat n => Show (RvfiCsr n) Source # | |
Generic (RvfiCsr n) Source # | |
KnownNat n => NFDataX (RvfiCsr n) Source # | |
type Rep (RvfiCsr n) Source # | |
Defined in Lion.Rvfi type Rep (RvfiCsr n) = D1 ('MetaData "RvfiCsr" "Lion.Rvfi" "lion-0.2.0.0-1lYjfC99CiCH8z7A9CBLqD" '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))))) |
RISC-V Formal Interface