diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,13 @@ # Revision history for lion +## 0.3.0.0 + +* Update base dependency version bounds +* Minor internal pipeline updates +* Remove Cabal dependency +* Move start PC configuration variable to type-level +* Update documentation + ## 0.2.0.0 -- 2021-03-27 * Update core/memory/peripheral interface diff --git a/lion.cabal b/lion.cabal --- a/lion.cabal +++ b/lion.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: lion -version: 0.2.0.0 +version: 0.3.0.0 synopsis: RISC-V Core description: Lion is a formally verified, 5-stage pipeline [RISC-V](https://riscv.org) core. Lion targets the [VELDT FPGA development board](https://standardsemiconductor.com) and is written in Haskell using [Clash](https://clash-lang.org). bug-reports: https://github.com/standardsemiconductor/lion/issues @@ -16,7 +16,7 @@ source-repository head type: git - location: git://github.com/standardsemiconductor/lion.git + location: https://github.com/standardsemiconductor/lion library exposed-modules: Lion.Core @@ -27,8 +27,7 @@ hs-source-dirs: src default-language: Haskell2010 build-depends: - base >= 4.13 && < 4.15, - Cabal, + base >= 4.13 && < 4.16, generic-monoid >= 0.1 && < 0.2, mtl >= 2.2 && < 2.3, lens >= 4.19 && < 5.1, @@ -67,6 +66,7 @@ ScopedTypeVariables TemplateHaskell TupleSections + TypeApplications TypeFamilies TypeOperators ViewPatterns diff --git a/src/Lion/Core.hs b/src/Lion/Core.hs --- a/src/Lion/Core.hs +++ b/src/Lion/Core.hs @@ -33,8 +33,8 @@ -- | Core configuration -- -- ALU configuration default: `Soft` -newtype CoreConfig (a :: AluConfig) = CoreConfig - { pipeConfig :: P.PipeConfig -- ^ pipeline configuration +newtype CoreConfig (startPC :: Nat) (a :: AluConfig) = CoreConfig + { pipeConfig :: P.PipeConfig (startPC :: Nat) -- ^ pipeline configuration } deriving stock (Generic, Show, Eq) @@ -43,7 +43,7 @@ -- ALU configuration = `Soft` -- -- `pipeConfig` = `defaultPipeConfig` -defaultCoreConfig :: CoreConfig 'Soft +defaultCoreConfig :: CoreConfig 0 'Soft defaultCoreConfig = CoreConfig { pipeConfig = P.defaultPipeConfig } @@ -56,10 +56,11 @@ -- | RISC-V Core: RV32I core - :: forall a dom + :: forall a startPC dom . HiddenClockResetEnable dom => Alu a - => CoreConfig (a :: AluConfig) -- ^ core configuration + => (KnownNat startPC, startPC <= 0xFFFFFFFF) + => CoreConfig (startPC :: Nat) (a :: AluConfig) -- ^ core configuration -> Signal dom (BitVector 32) -- ^ core input, from memory/peripherals -> FromCore dom -- ^ core output core config toCore = FromCore diff --git a/src/Lion/Pipe.hs b/src/Lion/Pipe.hs --- a/src/Lion/Pipe.hs +++ b/src/Lion/Pipe.hs @@ -17,16 +17,14 @@ import Lion.Rvfi -- | Pipeline configuration -newtype PipeConfig = PipeConfig - { startPC :: BitVector 32 -- ^ initial Program Counter address, default = 0 - } +data PipeConfig (startPC :: Nat) = PipeConfig deriving stock (Generic, Show, Eq) -- | Default pipeline configuration -- -- `startPC` = 0 -defaultPipeConfig :: PipeConfig -defaultPipeConfig = PipeConfig 0 +defaultPipeConfig :: PipeConfig 0 +defaultPipeConfig = PipeConfig -- | Pipeline inputs data ToPipe = ToPipe @@ -153,9 +151,13 @@ deriving anyclass NFDataX makeLenses ''Pipe -mkPipe :: PipeConfig -> Pipe -mkPipe config = Pipe - { _fetchPC = startPC config +mkPipe + :: forall startPC + . (KnownNat startPC, startPC <= 0xFFFFFFFF) + => PipeConfig (startPC :: Nat) + -> Pipe +mkPipe _ = Pipe + { _fetchPC = natToNum @startPC -- decode stage , _dePC = 0 @@ -183,7 +185,8 @@ -- | 5-Stage RISC-V pipeline pipe :: HiddenClockResetEnable dom - => PipeConfig + => (KnownNat startPC, startPC <= 0xFFFFFFFF) + => PipeConfig (startPC :: Nat) -> Signal dom ToPipe -> Signal dom FromPipe pipe config = mealy pipeMealy (mkPipe config) @@ -215,12 +218,14 @@ control.wbMemory .= True wbRvfi.rvfiRdAddr .= rdAddr mem <- wbRvfi.rvfiMemRData <<~ view fromMem - let wr = case op of - Lb -> signExtend $ sliceByte mask mem - Lh -> signExtend $ sliceHalf mask mem + let byte = sliceByte mask mem + half = sliceHalf mask mem + wr = case op of + Lb -> signExtend byte + Lh -> signExtend half Lw -> mem - Lbu -> zeroExtend $ sliceByte mask mem - Lhu -> zeroExtend $ sliceHalf mask mem + Lbu -> zeroExtend byte + Lhu -> zeroExtend half rdData <- wbRvfi.rvfiRdWData <.= guardZero rdAddr wr scribe toRd . First =<< control.wbRegFwd <.= Just (rdAddr, rdData) WbStore -> control.wbMemory .= True @@ -272,23 +277,17 @@ rs1Data <- meRvfi.rvfiRs1Data <<~ regFwd exRs1 fromRs1 (control.meRegFwd) (control.wbRegFwd) rs2Data <- meRvfi.rvfiRs2Data <<~ regFwd exRs2 fromRs2 (control.meRegFwd) (control.wbRegFwd) withInstr exIR $ \case - Ex op rd imm -> case op of - Lui -> do - scribeAlu Add 0 imm - meIR ?= MeRegWr rd - Auipc -> do - scribeAlu Add pc imm - meIR ?= MeRegWr rd + Ex op rd imm -> do + scribeAlu Add imm $ case op of + Lui -> 0 + Auipc -> pc + meIR ?= MeRegWr rd ExJump jump rd imm -> do - case jump of - Jal -> do - npc <- meRvfi.rvfiPcWData <<~ control.exBranching do - npc <- meRvfi.rvfiPcWData <<~ control.exBranching pc + imm + Jalr -> clearBit (rs1Data + imm) 0 + meRvfi.rvfiTrap ||= isMisaligned npc + meIR ?= MeJump rd pc4 ExBranch op imm -> if branch op rs1Data rs2Data then do @@ -334,16 +333,6 @@ scribe toAluInput1 $ First $ Just in1 scribe toAluInput2 $ First $ Just in2 - guardZero -- register x0 always has value 0. - :: MonadState s m - => Lens' s (Unsigned 5) - -> BitVector 32 - -> m (BitVector 32) - guardZero rsAddr rsValue = do - isZero <- uses rsAddr (== 0) - return $ if isZero - then 0 - else rsValue regFwd :: MonadState s m => MonadReader r m @@ -354,6 +343,17 @@ -> m (BitVector 32) regFwd rsAddr rsData meFwd wbFwd = guardZero rsAddr =<< fwd <$> use rsAddr <*> view rsData <*> use meFwd <*> use wbFwd + where + guardZero -- register x0 always has value 0. + :: MonadState s m + => Lens' s (Unsigned 5) + -> BitVector 32 + -> m (BitVector 32) + guardZero addr value = do + isZero <- uses addr (== 0) + return $ if isZero + then 0 + else value -- | Decode stage decode :: RWS ToPipe FromPipe Pipe () diff --git a/src/Lion/Rvfi.hs b/src/Lion/Rvfi.hs --- a/src/Lion/Rvfi.hs +++ b/src/Lion/Rvfi.hs @@ -28,27 +28,103 @@ -- | RISC-V Formal Interface data Rvfi = Rvfi - { _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. + _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). , _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 , _rvfiInsn :: "insn" ::: BitVector 32 + + -- | `rvfiTrap` must be set for an instruction that cannot be decoded + -- as a legal instruction, such as 0x00000000. , _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. , _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. , _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 , _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 , _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. , _rvfiRs1Addr :: "rs1_addr" ::: 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. , _rvfiRs1Data :: "rs1_rdata" ::: 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. , _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. , _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. , _rvfiPcRData :: "pc_rdata" ::: BitVector 32 , _rvfiPcWData :: "pc_wdata" ::: BitVector 32 + + -- | For memory operations (`rvfiMemRMask` and/or `rvfiMemWMask` are non-zero), + -- `rvfiMemAddr` holds the accessed memory location. , _rvfiMemAddr :: "mem_addr" ::: BitVector 32 + + -- | `rvfiMemRMask` is a bitmask that specifies which bytes in `rvfiMemRData` + -- contain valid read data from `rvfiMemAddr`. , _rvfiMemRMask :: "mem_rmask" ::: BitVector 4 + + -- | `rvfiMemWMask` is a bitmask that specifies which bytes in `rvfiMemWData` + -- contain valid data this is written to `rvfiMemAddr`. , _rvfiMemWMask :: "mem_wmask" ::: BitVector 4 + + -- | `rvfiMemRData` is the pre-state data read from `rvfiMemAddr`. + -- `rvfiMemRMask` specifies which bytes are valid. , _rvfiMemRData :: "mem_rdata" ::: BitVector 32 + + -- | `rvfiMemWData` is the post-state data written to `rvfiMemAddr`. + -- `rvfiMemWMask` specifies which bytes are valid. , _rvfiMemWData :: "mem_wdata" ::: BitVector 32 + , _rvfiCsrMinstret :: "csr_minstret" ::: RvfiCsr 64 , _rvfiCsrMcycle :: "csr_mcycle" ::: RvfiCsr 64 , _rvfiCsrMscratch :: "csr_mscratch" ::: RvfiCsr 32