diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,6 @@ +# Revision history for lion + +## 0.1.0.0 -- 2021-02-28 + +* First version. +* RV32I (no FENCE, ECALL, EBREAK) diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,29 @@ +BSD 3-Clause License + +Copyright (c) 2021, David Cox +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +3. Neither the name of the copyright holder nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,35 @@ +# Where Lions Roam: RISC-V on the VELDT + +[![Haskell CI](https://github.com/standardsemiconductor/lion/actions/workflows/haskell.yml/badge.svg?branch=main)](https://github.com/standardsemiconductor/lion/actions/workflows/haskell.yml) +[![Hackage][hackage-badge]][hackage] +[![Hackage Dependencies][hackage-deps-badge]][hackage-deps] + +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). + +This repository contains three parts: + 1. The Lion library: a pipelined RISC-V core. + 2. [lion-formal](https://github.com/standardsemiconductor/lion/tree/main/lion-formal): formally verify the core using [riscv-formal](https://github.com/standardsemiconductor/riscv-formal/tree/lion). + 3. [lion-soc](https://github.com/standardsemiconductor/lion/tree/main/lion-soc): a System-on-Chip demonstrating usage of the Lion core on the VELDT. + +## Lion library +### Usage: +1. Add `lion` to build depends section of Cabal file +2. import module in source files `import Lion.Core` + +When connecting the `core` to memory and peripherals, ensure single cycle latency. + +## Features +### Current Support +Architecture: RV32I (no FENCE, ECALL, EBREAK) -- Default configuration + +### Future Support +**All features will be added in a configurable manner extending the default configuration noted above** +* Zicsr, Control and Status Register (CSR) Instructions +* CSR registers +* RV32IM +* Hard IP ALU + +[hackage]: +[hackage-badge]: +[hackage-deps-badge]: +[hackage-deps]: diff --git a/lion.cabal b/lion.cabal new file mode 100644 --- /dev/null +++ b/lion.cabal @@ -0,0 +1,69 @@ +cabal-version: 2.4 +name: lion +version: 0.1.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 +license: BSD-3-Clause +license-file: LICENSE +author: dopamane +maintainer: dopamane +copyright: (c) 2021 David Cox +category: Hardware +extra-source-files: + CHANGELOG.md + README.md + +source-repository head + type: git + location: git://github.com/standardsemiconductor/lion.git + +library + exposed-modules: Lion.Core + , Lion.Rvfi + other-modules: Lion.Instruction + , Lion.Pipe + hs-source-dirs: src + default-language: Haskell2010 + build-depends: + base >= 4.13 && < 4.15, + Cabal, + generic-monoid >= 0.1 && < 0.2, + mtl, + lens, + ice40-prim >= 0.1 && < 0.2, + clash-prelude >= 1.2.5 && < 1.4, + ghc-typelits-natnormalise, + ghc-typelits-extra, + ghc-typelits-knownnat + ghc-options: + -Wall -Wcompat + -haddock + -fplugin GHC.TypeLits.Extra.Solver + -fplugin GHC.TypeLits.Normalise + -fplugin GHC.TypeLits.KnownNat.Solver + -fexpose-all-unfoldings + -fno-worker-wrapper + default-extensions: + BinaryLiterals + DataKinds + DeriveAnyClass + DeriveGeneric + DerivingStrategies + DerivingVia + FlexibleContexts + FlexibleInstances + GADTs + GeneralizedNewtypeDeriving + LambdaCase + MagicHash + MultiWayIf + NoImplicitPrelude + NoStarIsType + PolyKinds + RankNTypes + TemplateHaskell + TupleSections + TypeFamilies + TypeOperators + ViewPatterns diff --git a/src/Lion/Core.hs b/src/Lion/Core.hs new file mode 100644 --- /dev/null +++ b/src/Lion/Core.hs @@ -0,0 +1,59 @@ +{-| +Module : Lion.Core +Description : Lion RISC-V Core +Copyright : (c) David Cox, 2021 +License : BSD-3-Clause +Maintainer : standardsemiconductor@gmail.com + +The Lion core is a 32-bit RISC-V processor written in Haskell using [Clash](https://clash-lang.org). Note, all peripherals and memory must have single cycle latency. See [lion-soc](https://github.com/standardsemiconductor/lion/tree/main/lion-soc) for an example of using the Lion core in a system. +-} + +module Lion.Core + ( core + , FromCore(..) + , toMem + , toRvfi + , P.ToMem(..) + ) where + +import Clash.Prelude +import Control.Lens +import Data.Maybe +import Data.Monoid +import Lion.Rvfi +import qualified Lion.Pipe as P + +-- | Core outputs +data FromCore dom = FromCore + { _toMem :: Signal dom (Maybe P.ToMem) -- ^ shared memory and instruction bus, output from core to memory and peripherals + , _toRvfi :: Signal dom Rvfi -- ^ formal verification interface output, see [lion-formal](https://github.com/standardsemiconductor/lion/tree/main/lion-formal) for usage + } +makeLenses ''FromCore + +-- | RISC-V Core +core + :: HiddenClockResetEnable dom + => BitVector 32 -- ^ start address + -> Signal dom (BitVector 32) -- ^ core input, from memory/peripherals + -> FromCore dom -- ^ core output +core start toCore = FromCore + { _toMem = getFirst . P._toMem <$> fromPipe + , _toRvfi = fromMaybe mkRvfi . getFirst . P._toRvfi <$> fromPipe + } + where + fromPipe = P.pipe start $ P.ToPipe <$> rs1Data <*> rs2Data <*> toCore + rs1Addr = fromMaybe 0 . getFirst . P._toRs1Addr <$> fromPipe + rs2Addr = fromMaybe 0 . getFirst . P._toRs2Addr <$> fromPipe + rdWrM = getFirst . P._toRd <$> fromPipe + (rs1Data, rs2Data) = regBank rs1Addr rs2Addr rdWrM + +-- | Register bank +regBank + :: HiddenClockResetEnable dom + => Signal dom (Unsigned 5) -- ^ Rs1 Addr + -> Signal dom (Unsigned 5) -- ^ Rs2 Addr + -> Signal dom (Maybe (Unsigned 5, BitVector 32)) -- ^ Rd Write + -> Unbundled dom (BitVector 32, BitVector 32) -- ^ (Rs1Data, Rs2Data) +regBank rs1Addr rs2Addr rdWrM = (regFile rs1Addr, regFile rs2Addr) + where + regFile = flip (readNew (blockRamPow2 (repeat 0))) rdWrM diff --git a/src/Lion/Instruction.hs b/src/Lion/Instruction.hs new file mode 100644 --- /dev/null +++ b/src/Lion/Instruction.hs @@ -0,0 +1,189 @@ +{-| +Module : Lion.Instruction +Description : RISC-V ISA +Copyright : (c) David Cox, 2021 +License : BSD-3-Clause +Maintainer : standardsemiconductor@gmail.com +-} + +module Lion.Instruction where + +import Clash.Prelude +import Data.Function ( on ) + +data Exception = IllegalInstruction + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX + +data WbInstr = WbRegWr (Unsigned 5) (BitVector 32) + | WbLoad Load (Unsigned 5) (BitVector 4) + | WbStore + | WbNop + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX + +data MeInstr = MeRegWr (Unsigned 5) (BitVector 32) + | MeStore (BitVector 32) (BitVector 4) (BitVector 32) + | MeLoad Load (Unsigned 5) (BitVector 32) (BitVector 4) + | MeNop + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX + +data ExInstr = Ex ExOp (Unsigned 5) (BitVector 32) + | ExBranch Branch (BitVector 32) + | ExStore Store (BitVector 32) + | ExLoad Load (Unsigned 5) (BitVector 32) + | ExAlu Op (Unsigned 5) + | ExAluImm Op (Unsigned 5) (BitVector 32) + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX + +data Op = Add + | Sub + | Sll + | Slt + | Sltu + | Xor + | Srl + | Sra + | Or + | And + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX + +alu :: Op -> BitVector 32 -> BitVector 32 -> BitVector 32 +alu = \case + Add -> (+) + Sub -> (-) + Sll -> \x y -> x `shiftL` shamt y + Slt -> boolToBV ... (<) `on` sign + Sltu -> boolToBV ... (<) + Xor -> xor + Srl -> \x y -> x `shiftR` shamt y + Sra -> \x y -> pack $ sign x `shiftR` shamt y + Or -> (.|.) + And -> (.&.) + where + shamt = unpack . resize . slice d4 d0 + sign = unpack :: BitVector 32 -> Signed 32 + (...) = (.).(.) + +data Branch = Beq + | Bne + | Blt + | Bge + | Bltu + | Bgeu + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX + +branch :: Branch -> BitVector 32 -> BitVector 32 -> Bool +branch = \case + Beq -> not ... (/=) + Bne -> (/=) + Bge -> not ... (<) `on` sign + Bgeu -> not ... (<) + Blt -> (<) `on` sign + Bltu -> (<) + where + (...) = (.).(.) + sign :: BitVector 32 -> Signed 32 + sign = unpack + +data ExOp = Lui + | Auipc + | Jal + | Jalr + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX + +data Store = Sb + | Sh + | Sw + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX + +data Load = Lb + | Lh + | Lw + | Lbu + | Lhu + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX + +parseInstr :: BitVector 32 -> Either Exception ExInstr +parseInstr i = case i of + $(bitPattern ".........................0110111") -> Right $ Ex Lui rd immU -- lui + $(bitPattern ".........................0010111") -> Right $ Ex Auipc rd immU -- auipc + $(bitPattern ".........................1101111") -> Right $ Ex Jal rd immJ -- jal + $(bitPattern ".................000.....1100111") -> Right $ Ex Jalr rd immI -- jalr + $(bitPattern ".................000.....1100011") -> Right $ ExBranch Beq immB -- beq + $(bitPattern ".................001.....1100011") -> Right $ ExBranch Bne immB -- bne + $(bitPattern ".................100.....1100011") -> Right $ ExBranch Blt immB -- blt + $(bitPattern ".................101.....1100011") -> Right $ ExBranch Bge immB -- bge + $(bitPattern ".................110.....1100011") -> Right $ ExBranch Bltu immB -- bltu + $(bitPattern ".................111.....1100011") -> Right $ ExBranch Bgeu immB -- bgeu + $(bitPattern ".................000.....0000011") -> Right $ ExLoad Lb rd immI -- lb + $(bitPattern ".................001.....0000011") -> Right $ ExLoad Lh rd immI -- lh + $(bitPattern ".................010.....0000011") -> Right $ ExLoad Lw rd immI -- lw + $(bitPattern ".................100.....0000011") -> Right $ ExLoad Lbu rd immI -- lbu + $(bitPattern ".................101.....0000011") -> Right $ ExLoad Lhu rd immI -- lhu + $(bitPattern ".................000.....0100011") -> Right $ ExStore Sb immS -- sb + $(bitPattern ".................001.....0100011") -> Right $ ExStore Sh immS -- sh + $(bitPattern ".................010.....0100011") -> Right $ ExStore Sw immS -- sw + $(bitPattern ".................000.....0010011") -> Right $ ExAluImm Add rd immI -- addi + $(bitPattern ".................010.....0010011") -> Right $ ExAluImm Slt rd immI -- slti + $(bitPattern ".................011.....0010011") -> Right $ ExAluImm Sltu rd immI -- sltiu + $(bitPattern ".................100.....0010011") -> Right $ ExAluImm Xor rd immI -- xori + $(bitPattern ".................110.....0010011") -> Right $ ExAluImm Or rd immI -- ori + $(bitPattern ".................111.....0010011") -> Right $ ExAluImm And rd immI -- andi + $(bitPattern "0000000..........001.....0010011") -> Right $ ExAluImm Sll rd immI -- slli + $(bitPattern "0000000..........101.....0010011") -> Right $ ExAluImm Srl rd immI -- srli + $(bitPattern "0100000..........101.....0010011") -> Right $ ExAluImm Sra rd immI -- srai + $(bitPattern "0000000..........000.....0110011") -> Right $ ExAlu Add rd -- add + $(bitPattern "0100000..........000.....0110011") -> Right $ ExAlu Sub rd -- sub + $(bitPattern "0000000..........001.....0110011") -> Right $ ExAlu Sll rd -- sll + $(bitPattern "0000000..........010.....0110011") -> Right $ ExAlu Slt rd -- slt + $(bitPattern "0000000..........011.....0110011") -> Right $ ExAlu Sltu rd -- sltu + $(bitPattern "0000000..........100.....0110011") -> Right $ ExAlu Xor rd -- xor + $(bitPattern "0000000..........101.....0110011") -> Right $ ExAlu Srl rd -- srl + $(bitPattern "0100000..........101.....0110011") -> Right $ ExAlu Sra rd -- sra + $(bitPattern "0000000..........110.....0110011") -> Right $ ExAlu Or rd -- or + $(bitPattern "0000000..........111.....0110011") -> Right $ ExAlu And rd -- and + _ -> Left IllegalInstruction + where + rd = sliceRd i + + immI :: BitVector 32 + immI = signExtend $ slice d31 d20 i + + immS :: BitVector 32 + immS = signExtend $ slice d31 d25 i ++# slice d11 d7 i + + immB :: BitVector 32 + immB = signExtend (slice d31 d31 i ++# slice d7 d7 i ++# slice d30 d25 i ++# slice d11 d8 i) `shiftL` 1 + + immU :: BitVector 32 + immU = (slice d31 d12 i) ++# 0 + + immJ :: BitVector 32 + immJ = signExtend (slice d31 d31 i ++# slice d19 d12 i ++# slice d20 d20 i ++# slice d30 d25 i ++# slice d24 d21 i) `shiftL` 1 + + +sliceRd :: BitVector 32 -> Unsigned 5 +sliceRd = unpack . slice d11 d7 + +sliceRs1 :: BitVector 32 -> Unsigned 5 +sliceRs1 = unpack . slice d19 d15 + +sliceRs2 :: BitVector 32 -> Unsigned 5 +sliceRs2 = unpack . slice d24 d20 + +sliceOpcode :: BitVector 32 -> BitVector 7 +sliceOpcode = slice d6 d0 + +sliceFunct3 :: BitVector 32 -> BitVector 3 +sliceFunct3 = slice d14 d12 + +sliceFunct7 :: BitVector 32 -> BitVector 7 +sliceFunct7 = slice d31 d25 diff --git a/src/Lion/Pipe.hs b/src/Lion/Pipe.hs new file mode 100644 --- /dev/null +++ b/src/Lion/Pipe.hs @@ -0,0 +1,430 @@ +{-| +Module : Lion.Pipe +Description : RISC-V 5-stage pipeline +Copyright : (c) David Cox, 2021 +License : BSD-3-Clause +Maintainer : standardsemiconductor@gmail.com +-} + +module Lion.Pipe where + +import Clash.Prelude +import Control.Lens hiding ( op ) +import Control.Monad.RWS +import Data.Maybe ( isJust ) +import Data.Monoid.Generic +import Lion.Instruction +import Lion.Rvfi + +-- | Pipeline inputs +data ToPipe = ToPipe + { _fromRs1 :: BitVector 32 + , _fromRs2 :: BitVector 32 + , _fromMem :: BitVector 32 + } + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX +makeLenses ''ToPipe + +-- | Memory bus +-- +-- Lion has a shared instruction/memory bus +data ToMem = InstrMem -- ^ instruction read + (BitVector 32) -- ^ instruction address + | DataMem -- ^ data access + (BitVector 32) -- ^ data address + (BitVector 4) -- ^ data byte mask + (Maybe (BitVector 32)) -- ^ read=Nothing write=(Just wr) + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX + +-- | Pipeline outputs +data FromPipe = FromPipe + { _toMem :: First ToMem + , _toRs1Addr :: First (Unsigned 5) + , _toRs2Addr :: First (Unsigned 5) + , _toRd :: First (Unsigned 5, BitVector 32) + , _toRvfi :: First Rvfi + } + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX + deriving Semigroup via GenericSemigroup FromPipe + deriving Monoid via GenericMonoid FromPipe +makeLenses ''FromPipe + +data Control = Control + { _firstCycle :: Bool -- ^ First cycle True, then always False + , _branching :: Maybe (BitVector 32) -- ^ execute stage branch + , _deLoad :: Bool -- ^ decode stage load + , _exLoad :: Bool -- ^ execute stage load + , _meMemory :: Bool -- ^ memory stage load/store + , _wbMemory :: Bool -- ^ writeback stage load/store + , _meRegFwd :: Maybe (Unsigned 5, BitVector 32) -- ^ memory stage register forwarding + , _wbRegFwd :: Maybe (Unsigned 5, BitVector 32) -- ^ writeback stage register forwading + } + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX +makeLenses ''Control + +mkControl :: Control +mkControl = Control + { _firstCycle = True + , _branching = Nothing + , _deLoad = False + , _exLoad = False + , _meMemory = False + , _wbMemory = False + , _meRegFwd = Nothing + , _wbRegFwd = Nothing + } + +data Pipe = Pipe + { _fetchPC :: BitVector 32 + + -- decode stage + , _dePC :: BitVector 32 + + -- execute stage + , _exIR :: Maybe ExInstr + , _exPC :: BitVector 32 + , _exRs1 :: Unsigned 5 + , _exRs2 :: Unsigned 5 + , _exRvfi :: Rvfi + + -- memory stage + , _meIR :: Maybe MeInstr + , _meRvfi :: Rvfi + + -- writeback stage + , _wbIR :: Maybe WbInstr + , _wbNRet :: BitVector 64 + , _wbRvfi :: Rvfi + + -- pipeline control + , _control :: Control + } + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX +makeLenses ''Pipe + +mkPipe :: BitVector 32 -> Pipe +mkPipe start = Pipe + { _fetchPC = start + + -- decode stage + , _dePC = 0 + + -- execute stage + , _exIR = Nothing + , _exPC = 0 + , _exRs1 = 0 + , _exRs2 = 0 + , _exRvfi = mkRvfi + + -- memory stage + , _meIR = Nothing + , _meRvfi = mkRvfi + + -- writeback stage + , _wbIR = Nothing + , _wbNRet = 0 + , _wbRvfi = mkRvfi + + -- pipeline control + , _control = mkControl + } + +-- | 5-Stage RISC-V pipeline +pipe + :: HiddenClockResetEnable dom + => BitVector 32 + -> Signal dom ToPipe + -> Signal dom FromPipe +pipe start = mealy pipeMealy (mkPipe start) + where + pipeMealy s i = let ((), s', o) = runRWS pipeM i s + in (s', o) + +-- | reset control signals (except first cycle) +resetControl :: MonadState Pipe m => m () +resetControl = do + control.branching .= Nothing + control.deLoad .= False + control.exLoad .= False + control.meMemory .= False + control.wbMemory .= False + control.meRegFwd .= Nothing + control.wbRegFwd .= Nothing + +-- | Monadic pipeline +pipeM :: RWS ToPipe FromPipe Pipe () +pipeM = do + resetControl + writeback + memory + execute + decode + fetch + +-- | Writeback stage +writeback :: RWS ToPipe FromPipe Pipe () +writeback = withInstr wbIR $ \instr -> do + wbRvfi.rvfiValid .= True + wbRvfi.rvfiOrder <~ wbNRet <<+= 1 + case instr of + WbRegWr rdAddr wr -> do + wbRvfi.rvfiRdAddr .= rdAddr + rdData <- wbRvfi.rvfiRdWData <.= guardZero rdAddr wr + scribe toRd . First =<< control.wbRegFwd <.= Just (rdAddr, rdData) + WbLoad op rdAddr mask -> do + 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 + Lw -> mem + Lbu -> zeroExtend $ sliceByte mask mem + Lhu -> zeroExtend $ sliceHalf mask mem + rdData <- wbRvfi.rvfiRdWData <.= guardZero rdAddr wr + scribe toRd . First =<< control.wbRegFwd <.= Just (rdAddr, rdData) + WbStore -> control.wbMemory .= True + WbNop -> return () + scribe toRvfi . First . Just =<< use wbRvfi + where + guardZero 0 = const 0 + guardZero _ = id + +-- | Memory stage +memory :: RWS ToPipe FromPipe Pipe () +memory = do + wbIR .= Nothing + wbRvfi <~ use meRvfi + withInstr meIR $ \case + MeRegWr rd wr -> do + control.meRegFwd ?= (rd, wr) + wbIR ?= WbRegWr rd wr + MeNop -> wbIR ?= WbNop + MeStore addr mask value -> do + control.meMemory .= True + scribe toMem $ First $ Just $ DataMem addr mask $ Just value + wbRvfi.rvfiMemAddr .= addr + wbRvfi.rvfiMemWMask .= mask + wbRvfi.rvfiMemWData .= value + wbIR ?= WbStore + MeLoad op rdAddr addr mask -> do + control.meMemory .= True + scribe toMem $ First $ Just $ DataMem addr mask Nothing + wbRvfi.rvfiMemAddr .= addr + wbRvfi.rvfiMemRMask .= mask + wbIR ?= WbLoad op rdAddr mask + +-- | Execute stage +execute :: RWS ToPipe FromPipe Pipe () +execute = do + meIR .= Nothing + meRvfi <~ use exRvfi + pc <- meRvfi.rvfiPcRData <<~ use exPC + meRvfi.rvfiPcWData .= pc + 4 + 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 -> meIR ?= MeRegWr rd imm + Auipc -> meIR ?= MeRegWr rd (pc + imm) + Jal -> do + npc <- meRvfi.rvfiPcWData <.= pc + imm + meRvfi.rvfiTrap ||= (npc .&. 0x3 /= 0) + control.branching ?= npc + meIR ?= MeRegWr rd (pc + 4) + Jalr -> do + npc <- meRvfi.rvfiPcWData <.= clearBit (rs1Data + imm) 0 + meRvfi.rvfiTrap ||= (npc .&. 0x3 /= 0) + control.branching ?= npc + meIR ?= MeRegWr rd (pc + 4) + ExBranch op imm -> do + npc <- meRvfi.rvfiPcWData <<~ if branch op rs1Data rs2Data + then control.branching do + let addr = rs1Data + imm -- unaligned + addr' = addr .&. complement 0x3 -- aligned + case op of + Sb -> let wr = concatBitVector# $ replicate d4 $ slice d7 d0 rs2Data + in meIR ?= MeStore addr' (byteMask addr) wr + Sh -> do + meRvfi.rvfiTrap ||= (addr .&. 0x1 /= 0) -- trap on half-word boundary + let wr = concatBitVector# $ replicate d2 $ slice d15 d0 rs2Data + meIR ?= MeStore addr' (halfMask addr) wr + Sw -> do + meRvfi.rvfiTrap ||= (addr .&. 0x3 /= 0) -- trap on word boundary + meIR ?= MeStore addr' 0xF rs2Data + ExLoad op rdAddr imm -> do + control.exLoad .= True + let addr = rs1Data + imm -- unaligned + addr' = addr .&. complement 0x3 -- aligned + if | op == Lb || op == Lbu -> meIR ?= MeLoad op rdAddr addr' (byteMask addr) + | op == Lh || op == Lhu -> do + meRvfi.rvfiTrap ||= (addr .&. 0x1 /= 0) -- trap on half-word boundary + meIR ?= MeLoad op rdAddr addr' (halfMask addr) + | otherwise -> do -- Lw + meRvfi.rvfiTrap ||= (addr .&. 0x3 /= 0) -- trap on word boundary + meIR ?= MeLoad op rdAddr addr' 0xF + ExAlu op rd -> meIR ?= MeRegWr rd (alu op rs1Data rs2Data) + ExAluImm op rd imm -> meIR ?= MeRegWr rd (alu op rs1Data imm) + where + guardZero :: 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 + => Lens' s (Unsigned 5) + -> Lens' r (BitVector 32) + -> Lens' s (Maybe (Unsigned 5, BitVector 32)) + -> Lens' s (Maybe (Unsigned 5, BitVector 32)) + -> m (BitVector 32) + regFwd rsAddr rsData meFwd wbFwd = + guardZero rsAddr =<< fwd <$> use rsAddr <*> view rsData <*> use meFwd <*> use wbFwd + +-- | Decode stage +decode :: RWS ToPipe FromPipe Pipe () +decode = do + exIR .= Nothing + exRvfi .= mkRvfi + isFirstCycle <- control.firstCycle <<.= False -- first memory output undefined + isBranching <- uses (control.branching) isJust + isWbMemory <- use $ control.wbMemory + isExLoad <- use $ control.exLoad + unless (isFirstCycle || isBranching || isWbMemory || isExLoad) $ do + mem <- view fromMem + case parseInstr mem of + Right instr -> do + exIR ?= instr + exPC <~ use dePC + exRvfi.rvfiInsn .= mem + control.deLoad .= case instr of + ExLoad _ _ _ -> True + _ -> False + scribe toRs1Addr . First . Just =<< exRvfi.rvfiRs1Addr <<~ exRs1 <.= sliceRs1 mem + scribe toRs2Addr . First . Just =<< exRvfi.rvfiRs2Addr <<~ exRs2 <.= sliceRs2 mem + Left IllegalInstruction -> fetchPC <~ use dePC -- roll-back PC, should handle trap + + +-- | fetch instruction +-- stalled when instruction in memory stage needs bus +fetch :: RWS ToPipe FromPipe Pipe () +fetch = do + use (control.branching) >>= mapM_ (assign fetchPC) + scribe toMem . First . Just . InstrMem =<< dePC <<~ use fetchPC + isMeMemory <- use $ control.meMemory + isDeLoad <- use $ control.deLoad + unless (isMeMemory || isDeLoad) $ fetchPC += 4 + +------------- +-- Utility -- +------------- + +-- | forward register writes +fwd + :: Unsigned 5 + -> BitVector 32 + -> Maybe (Unsigned 5, BitVector 32) -- ^ meRegFwd + -> Maybe (Unsigned 5, BitVector 32) -- ^ wbRegFwd + -> BitVector 32 +fwd _ wr Nothing Nothing = wr +fwd addr wr Nothing (Just (wbAddr, wbWr)) + | addr == wbAddr = wbWr + | otherwise = wr +fwd addr wr (Just (meAddr, meWr)) Nothing + | addr == meAddr = meWr + | otherwise = wr +fwd addr wr (Just (meAddr, meWr)) (Just (wbAddr, wbWr)) + | addr == meAddr = meWr + | addr == wbAddr = wbWr + | otherwise = wr + +-- | calcluate byte mask based on address +byteMask :: BitVector 32 -> BitVector 4 +byteMask = (1 `shiftL`) . unpack . resize . slice d1 d0 + +-- | calculate half word mask based on address +halfMask :: BitVector 32 -> BitVector 4 +halfMask addr = if addr .&. 0x2 == 0 + then 0x3 + else 0xC + +-- | slice address based on mask +sliceByte :: BitVector 4 -> BitVector 32 -> BitVector 8 +sliceByte = \case + $(bitPattern "0001") -> slice d7 d0 + $(bitPattern "0010") -> slice d15 d8 + $(bitPattern "0100") -> slice d23 d16 + $(bitPattern "1000") -> slice d31 d24 + _ -> const 0 + +-- | slice address based on mask +sliceHalf :: BitVector 4 -> BitVector 32 -> BitVector 16 +sliceHalf = \case + $(bitPattern "0011") -> slice d15 d0 + $(bitPattern "1100") -> slice d31 d16 + _ -> const 0 + +-- | run monadic action when instruction is Just +withInstr :: MonadState s m => Lens' s (Maybe a) -> (a -> m ()) -> m () +withInstr l k = use l >>= mapM_ k + +-- | Hazards Note +-- +-- Key: +-- J = Jump +-- O = Bubble +-- S = Store +-- * = Stall +-- B = Branch +-- +-- Jump/Branch +-- +----+-----+-----+----+----+ +-- | IF | DE | EX | ME | WB | +-- +====+=====+=====+====+====+ +-- | 4 | --- | --- | -- | -- | +-- +----+-----+-----+----+----+ +-- | 8 | J15 | --- | -- | -- | +-- +----+-----+-----+----+----+ +-- | 15 | O | J15 | -- | -- | +-- +----+-----+-----+----+----+ +-- +-- Store +-- +-------+------+------+------+----+ +-- | IF | DE | EX | ME | WB | +-- +=======+======+======+======+====+ +-- | 4 | ---- | ---- | ---- | -- | +-- +-------+------+------+------+----+ +-- | 8 | S | ---- | ---- | -- | +-- +-------+------+------+------+----+ +-- | 12 | J100 | S | ---- | -- | +-- +-------+------+------+------+----+ +-- | *100* | O | J100 | S | -- | +-- +-------+------+------+------+----+ +-- | 100 | O | O | J100 | S | +-- +-------+------+------+------+----+ +-- +-- Load +-- +------+------+------+----+----+ +-- | IF | DE | EX | ME | WB | +-- +======+======+======+====+====+ +-- | 4 | ---- | ---- | -- | -- | +-- +------+------+------+----+----+ +-- | *8* | L | ---- | -- | -- | +-- +------+------+------+----+----+ +-- | 8 | O | L | -- | -- | +-- +------+------+------+----+----+ +-- | *12* | B100 | O | L | -- | +-- +------+------+------+----+----+ +-- | 100 | O | B100 | O | L | +-- +------+------+------+----+----+ diff --git a/src/Lion/Rvfi.hs b/src/Lion/Rvfi.hs new file mode 100644 --- /dev/null +++ b/src/Lion/Rvfi.hs @@ -0,0 +1,95 @@ +{-| +Module : Lion.Rvfi +Description : Lion RISC-V Formal Verification Interface +Copyright : (c) David Cox, 2021 +License : BSD-3-Clause +Maintainer : standardsemiconductor@gmail.com + +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](https://github.com/standardsemiconductor/riscv-formal) for more information about the interface. To verify the Lion core, see [lion-formal](https://github.com/standardsemiconductor/lion/tree/main/lion-formal). +-} + +module Lion.Rvfi where + +import Clash.Prelude +import Control.Lens +import Data.Maybe +import Data.Monoid + +-- | RISC-V Formal Csr Interface +data RvfiCsr n = RvfiCsr + { _wdataCsr :: "wdata" ::: BitVector n + , _rdataCsr :: "rdata" ::: BitVector n + , _wmaskCsr :: "wmask" ::: BitVector n + , _rmaskCsr :: "rmask" ::: BitVector n + } + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX +makeLenses ''RvfiCsr + +-- | RISC-V Formal Interface +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 + } + deriving stock (Generic, Show, Eq) + deriving anyclass NFDataX +makeLenses ''Rvfi + +-- | Unwrap Rvfi from First monoid +fromRvfi :: First Rvfi -> Rvfi +fromRvfi = fromMaybe mkRvfi . getFirst + +-- | Construct the RISC-V Formal Interface +mkRvfi :: Rvfi +mkRvfi = Rvfi + { _rvfiValid = False + , _rvfiOrder = 0 + , _rvfiInsn = 0 + , _rvfiTrap = False + , _rvfiHalt = False + , _rvfiIntr = False + , _rvfiMode = 3 + , _rvfiIxl = 1 + , _rvfiRs1Addr = 0 + , _rvfiRs2Addr = 0 + , _rvfiRs1Data = 0 + , _rvfiRs2Data = 0 + , _rvfiRdAddr = 0 + , _rvfiRdWData = 0 + , _rvfiPcRData = 0 + , _rvfiPcWData = 0 + , _rvfiMemAddr = 0 + , _rvfiMemRMask = 0 + , _rvfiMemWMask = 0 + , _rvfiMemRData = 0 + , _rvfiMemWData = 0 + , _rvfiCsrMinstret = RvfiCsr 0 0 0 0 + , _rvfiCsrMcycle = RvfiCsr 0 0 0 0 + , _rvfiCsrMscratch = RvfiCsr 0 0 0 0 + , _rvfiCsrMstatus = RvfiCsr 0 0 0 0 + , _rvfiCsrMisa = RvfiCsr 0 0 0 0 + }