lion 0.2.0.0 → 0.3.0.0

raw patch · 5 files changed

+135/−50 lines, 5 filesdep −Cabaldep ~basePVP ok

version bump matches the API change (PVP)

Dependencies removed: Cabal

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−0
• lion.cabal +4/−4
• src/Lion/Core.hs +6/−5
• src/Lion/Pipe.hs +40/−40
• src/Lion/Rvfi.hs +77/−1

@@ -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

@@ -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

@@ -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

@@ -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 <?= pc + imm-          meRvfi.rvfiTrap ||= isMisaligned npc-          meIR ?= MeJump rd pc4-        Jalr -> do-          npc <- meRvfi.rvfiPcWData <<~ control.exBranching <?= clearBit (rs1Data + imm) 0-          meRvfi.rvfiTrap ||= isMisaligned npc-          meIR ?= MeJump rd pc4+      npc <- meRvfi.rvfiPcWData <<~ control.exBranching <?= case jump of+        Jal  -> 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 ()

@@ -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