lion 0.4.0.0 → 0.4.0.1

raw patch · 13 files changed

+1116/−1092 lines, 13 filesdep ~basedep ~clash-preludedep ~ice40-primPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base, clash-prelude, ice40-prim, lens, mtl

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• README.md +3/−3
• lib/Lion/Alu.hs +127/−0
• lib/Lion/Core.hs +93/−0
• lib/Lion/Instruction.hs +194/−0
• lib/Lion/Pipe.hs +510/−0
• lib/Lion/Rvfi.hs +171/−0
• lion.cabal +13/−13
• src/Lion/Alu.hs +0/−121
• src/Lion/Core.hs +0/−93
• src/Lion/Instruction.hs +0/−188
• src/Lion/Pipe.hs +0/−503
• src/Lion/Rvfi.hs +0/−171

@@ -1,6 +1,11 @@ # Revision history for lion +## 0.4.0.1++* GHC and library updates #21+ ## 0.4.0.0+ * Update clash-prelude dependency bounds #4 * Type-level -> data-level configuration #6 

@@ -8,9 +8,9 @@  This repository contains four 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.-  4. [lion-metric](https://github.com/standardsemiconductor/lion/tree/main/lion-metric): Observe Yosys synthesis metrics on the Lion Core.+  2. [lion-formal](lion-formal): formally verify the core using [riscv-formal](https://github.com/standardsemiconductor/riscv-formal/tree/lion).+  3. [lion-soc](lion-soc): a System-on-Chip demonstrating usage of the Lion core on the VELDT.+  4. [lion-metric](lion-metric): Observe Yosys synthesis metrics on the Lion Core.  ## Lion library ### Usage:

@@ -0,0 +1,127 @@+{-# LANGUAGE CPP #-}++{-|+Module      : Lion.Alu+Description : Lion arithmetic logic unit+Copyright   : (c) David Cox, 2021-2024+License     : BSD-3-Clause+Maintainer  : standardsemiconductor@gmail.com++Configurable alu, choose between soft and hard adders/subtractors+-}++module Lion.Alu where++#if __GLASGOW_HASKELL__ > 902+import Clash.Prelude hiding (And(..), Xor(..))+#else+import Clash.Prelude+#endif+import Data.Function ( on )+import Ice40.Mac (+  Input(..),+  Parameter(..),+  defaultInput,+  defaultParameter,+  mac+  )+import Lion.Instruction (Op(..))++-- | ALU configuration+data AluConfig = Hard -- ^ use hard adder and subtractor from iCE40 SB_MAC16+               | Soft -- ^ use generic adder and subtractor: (+) and (-)+  deriving stock (Generic, Show, Eq)++alu+  :: HiddenClockResetEnable dom+  => AluConfig+  -> Signal dom Op+  -> Signal dom (BitVector 32)+  -> Signal dom (BitVector 32)+  -> Signal dom (BitVector 32)+alu = \case+  Hard -> hardAlu+  Soft -> softAlu++softAlu+ :: HiddenClockResetEnable dom+ => Signal dom Op+ -> Signal dom (BitVector 32)+ -> Signal dom (BitVector 32)+ -> Signal dom (BitVector 32)+softAlu op in1 = register 0 . liftA3 aluFunc op in1+    where+      aluFunc = \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+          (...) = (.).(.)++hardAlu+  :: HiddenClockResetEnable dom+  => Signal dom Op+  -> Signal dom (BitVector 32)+  -> Signal dom (BitVector 32)+  -> Signal dom (BitVector 32)+hardAlu op in1 in2 = mux isAddSub adderSubtractor $ register 0 $ baseAlu op in1 in2+    where+      isAdd = (Add == ) <$> op+      isSub = (Sub == ) <$> op+      isAddSub = delay False $ isAdd .||. isSub+      adderSubtractor = hardAddSub (boolToBit <$> isSub) in1 in2++baseAlu+  :: Signal dom Op+  -> Signal dom (BitVector 32)+  -> Signal dom (BitVector 32)+  -> Signal dom (BitVector 32)+baseAlu = liftA3 $ \case+  Add  -> \_ _ -> 0+  Sub  -> \_ _ -> 0+  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+    (...) = (.).(.)++-- | addSub32PipelinedUnsigned+hardAddSub+  :: HiddenClock dom+  => Signal dom Bit -- ^ 0 = Add, 1 = Sub+  -> Signal dom (BitVector 32)+  -> Signal dom (BitVector 32)+  -> Signal dom (BitVector 32)+hardAddSub addSub x y = out+  where+    (out, _, _, _) = mac parameter input+    input = defaultInput{ a = slice d31 d16 <$> y+                        , b = slice d15 d0  <$> y+                        , c = slice d31 d16 <$> x+                        , d = slice d15 d0  <$> x+                        , addsubtop = addSub+                        , addsubbot = addSub+                        }+    parameter = defaultParameter{ topOutputSelect = 1+                                , topAddSubUpperInput = 1+                                , topAddSubCarrySelect = 2+                                , botOutputSelect = 1+                                , botAddSubUpperInput = 1+                                , mode8x8 = 1+                                }

@@ -0,0 +1,93 @@+{-|+Module      : Lion.Core+Description : Lion RISC-V Core+Copyright   : (c) David Cox, 2024+License     : BSD-3-Clause+Maintainer  : standardsemiconductor@gmail.com++The Lion core is a 32-bit [RISC-V](https://riscv.org/about/) 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+  , defaultCoreConfig+  , P.defaultPipeConfig+  , CoreConfig(..)+  , AluConfig(..)+  , P.PipeConfig(..)+  , FromCore(..)+  , P.ToMem(..)+  , P.MemoryAccess(..)+  ) where++import Clash.Prelude+import Data.Maybe+import Data.Monoid+import Lion.Alu+import Lion.Rvfi+import qualified Lion.Pipe as P+import qualified Lion.Instruction as I (Op(Add))++-- | Core configuration+data CoreConfig = CoreConfig+  { aluConfig  :: AluConfig    -- ^ ALU configuration, default: `Soft`+  , pipeConfig :: P.PipeConfig -- ^ pipeline configuration+  }+  deriving stock (Generic, Show, Eq)++-- | Default core configuration+--+-- `aluConfig` = `Soft`+--+-- `pipeConfig` = `P.defaultPipeConfig`+defaultCoreConfig :: CoreConfig+defaultCoreConfig = CoreConfig+  { aluConfig  = Soft+  , pipeConfig = P.defaultPipeConfig+  }++-- | 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+  }++-- | RISC-V Core: RV32I+core+  :: HiddenClockResetEnable dom+  => CoreConfig                 -- ^ core configuration+  -> Signal dom (BitVector 32)  -- ^ core input, from memory/peripherals+  -> FromCore dom               -- ^ core output+core config toCore = FromCore+  { toMem  = getFirst . P._toMem <$> fromPipe+  , toRvfi = fromMaybe mkRvfi . getFirst . P._toRvfi <$> fromPipe+  }+  where+    -- alu connection+    aluOp = fromMaybe I.Add . getFirst . P._toAluOp     <$> fromPipe+    aluInput1 = fromMaybe 0 . getFirst . P._toAluInput1 <$> fromPipe+    aluInput2 = fromMaybe 0 . getFirst . P._toAluInput2 <$> fromPipe+    aluOutput = alu (aluConfig config) aluOp aluInput1 aluInput2++    -- reg bank connection+    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++    -- pipeline connection+    fromPipe = P.pipe (pipeConfig config) $ P.ToPipe <$> rs1Data +                                                     <*> rs2Data +                                                     <*> aluOutput+                                                     <*> toCore++-- | 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

@@ -0,0 +1,194 @@+{-# LANGUAGE CPP #-}++{-|+Module      : Lion.Instruction+Description : RISC-V ISA+Copyright   : (c) David Cox, 2024+License     : BSD-3-Clause+Maintainer  : standardsemiconductor@gmail.com+-}++module Lion.Instruction where++#if __GLASGOW_HASKELL__ > 902+import Clash.Prelude hiding (Xor(Xor), And(And))+#else+import Clash.Prelude+#endif+import Data.Function ( on )++data Exception = IllegalInstruction+  deriving stock (Generic, Show, Eq)+  deriving anyclass NFDataX++-- | Writeback pipeline instruction+data WbInstr = WbRegWr (Unsigned 5) (BitVector 32)+             | WbLoad Load (Unsigned 5) (BitVector 4)+             | WbStore+             | WbNop+  deriving stock (Generic, Show, Eq)+  deriving anyclass NFDataX++-- | Memory pipeline instruction+data MeInstr = MeRegWr      (Unsigned 5)+             | MeJump       (Unsigned 5) (BitVector 32)+             | MeBranch+             | MeStore                   (BitVector 32) (BitVector 4) (BitVector 32)+             | MeLoad  Load (Unsigned 5) (BitVector 32) (BitVector 4)+             | MeNop+  deriving stock (Generic, Show, Eq)+  deriving anyclass NFDataX++-- | Execute pipeline instruction+data ExInstr = Ex       ExOp   (Unsigned 5) (BitVector 32)+             | ExJump   Jump   (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++-- | ALU operation+data Op = Add+        | Sub+        | Sll+        | Slt+        | Sltu+        | Xor+        | Srl+        | Sra+        | Or+        | And+  deriving stock (Generic, Show, Eq)+  deriving anyclass NFDataX++-- | Branch operation+data Branch = Beq+            | Bne+            | Blt+            | Bge+            | Bltu+            | Bgeu+  deriving stock (Generic, Show, Eq)+  deriving anyclass NFDataX++-- | branch calculation+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+  deriving stock (Generic, Show, Eq)+  deriving anyclass NFDataX++data Jump = Jal | Jalr+  deriving stock (Generic, Show, Eq)+  deriving anyclass NFDataX++-- | Store operation+data Store = Sb+           | Sh+           | Sw+  deriving stock (Generic, Show, Eq)+  deriving anyclass NFDataX++-- | Load operation+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 $ ExJump Jal  rd immJ -- jal+  $(bitPattern ".................000.....1100111") -> Right $ ExJump 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+--    npcB = immB + pc+--    npcJ = immJ + pc++    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

@@ -0,0 +1,510 @@+{-# LANGUAGE CPP #-}++{-|+Module      : Lion.Pipe+Description : RISC-V 5-stage pipeline+Copyright   : (c) David Cox, 2024+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++#if __GLASGOW_HASKELL__ > 902+import Data.Monoid (First(..))+import Control.Monad (unless)+#endif++-- | Pipeline configuration+newtype PipeConfig = PipeConfig+  { startPC :: BitVector 32 -- ^ start program counter+  } deriving stock (Generic, Show, Eq)++-- | Default pipeline configuration+--+-- `startPC` = 0+defaultPipeConfig :: PipeConfig+defaultPipeConfig = PipeConfig 0++-- | Pipeline inputs+data ToPipe = ToPipe+  { _fromRs1 :: BitVector 32+  , _fromRs2 :: BitVector 32+  , _fromAlu :: BitVector 32+  , _fromMem :: BitVector 32+  }+  deriving stock (Generic, Show, Eq)+  deriving anyclass NFDataX+makeLenses ''ToPipe++-- | Memory access - Lion has a shared instruction/memory bus+data MemoryAccess = InstrMem -- ^ instruction access+                  | DataMem  -- ^ data access+  deriving stock (Generic, Show, Eq)+  deriving anyclass NFDataX++-- | Memory bus+data ToMem = ToMem+  { memAccess   :: MemoryAccess         -- ^ memory access type+  , memAddress  :: BitVector 32         -- ^ memory address+  , memByteMask :: BitVector 4          -- ^ memory byte mask+  , memWrite    :: Maybe (BitVector 32) -- ^ read=Nothing write=Just wr+  }+  deriving stock (Generic, Show, Eq)+  deriving anyclass NFDataX++-- | Construct instruction memory access+instrMem+  :: BitVector 32 -- ^ instruction address+  -> ToMem+instrMem addr = ToMem+  { memAccess   = InstrMem+  , memAddress  = addr+  , memByteMask = 0xF+  , memWrite    = Nothing+  }++-- | Construct data memory access+dataMem+  :: BitVector 32         -- ^ memory address+  -> BitVector 4          -- ^ byte mask+  -> Maybe (BitVector 32) -- ^ write+  -> ToMem+dataMem addr mask wrM = ToMem+  { memAccess   = DataMem+  , memAddress  = addr+  , memByteMask = mask+  , memWrite    = wrM+  }++-- | Pipeline outputs+data FromPipe = FromPipe+  { _toMem       :: First ToMem+  , _toRs1Addr   :: First (Unsigned 5)+  , _toRs2Addr   :: First (Unsigned 5)+  , _toRd        :: First (Unsigned 5, BitVector 32)+  , _toAluOp     :: First Op+  , _toAluInput1 :: First (BitVector 32)+  , _toAluInput2 :: First (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+  , _exBranching :: Maybe (BitVector 32)             -- ^ execute stage branch/jump+  , _meBranching :: Bool                             -- ^ memory stage branch/jump+  , _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+  , _exBranching = Nothing+  , _meBranching = False+  , _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 :: PipeConfig -> Pipe+mkPipe pipeConfig = Pipe+  { _fetchPC = startPC pipeConfig++  -- 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+  => PipeConfig+  -> Signal dom ToPipe+  -> Signal dom FromPipe+pipe config = mealy pipeMealy (mkPipe config)+  where+    pipeMealy s i = let ((), s', o) = runRWS pipeM i s+                    in (s', o)++-- | Monadic pipeline+pipeM :: RWS ToPipe FromPipe Pipe ()+pipeM = do+  writeback+  memory+  execute+  decode+  fetch+  control .= mkControl{ _firstCycle = False } -- reset control++-- | 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 byte = sliceByte mask mem+          half = sliceHalf mask mem+          wr = case op of+            Lb  -> signExtend byte+            Lh  -> signExtend half+            Lw  -> 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+    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+    MeNop -> wbIR ?= WbNop+    MeRegWr rd -> do+      wr <- view fromAlu+      control.meRegFwd ?= (rd, wr)+      wbIR ?= WbRegWr rd wr+    MeJump rd pc4 -> do+      control.meBranching .= True+      control.meRegFwd ?= (rd, pc4)+      wbIR ?= WbRegWr rd pc4+    MeBranch -> do+      control.meBranching .= True+      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+  pc4 <- 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 -> do+      scribeAlu Add imm $ case op of+        Lui   -> 0+        Auipc -> pc+      meIR ?= MeRegWr rd+    ExJump jump rd imm -> do+      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+          branchPC <- meRvfi.rvfiPcWData <<~ control.exBranching <?= pc + imm+          meRvfi.rvfiTrap ||= isMisaligned branchPC+          meIR ?= MeBranch+        else do+          meRvfi.rvfiTrap ||= isMisaligned pc4+          meIR ?= MeNop+    ExStore op imm -> 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 ||= isMisalignedHalf addr -- trap on half-word boundary+          let wr = concatBitVector# $ replicate d2 $ slice d15 d0 rs2Data+          meIR ?= MeStore addr' (halfMask addr) wr+        Sw -> do+          meRvfi.rvfiTrap ||= isMisaligned addr -- 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 ||= isMisalignedHalf addr -- trap on half-word boundary+             meIR ?= MeLoad op rdAddr addr' (halfMask addr)+         | otherwise -> do -- Lw+             meRvfi.rvfiTrap ||= isMisaligned addr -- trap on word boundary+             meIR ?= MeLoad op rdAddr addr' 0xF+    ExAlu op rd -> do+      scribeAlu op rs1Data rs2Data+      meIR ?= MeRegWr rd+    ExAluImm op rd imm -> do+      scribeAlu op rs1Data imm+      meIR ?= MeRegWr rd+  where+    scribeAlu op in1 in2 = do+      scribe toAluOp     $ First $ Just op+      scribe toAluInput1 $ First $ Just in1+      scribe toAluInput2 $ First $ Just in2++    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+      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 ()+decode = do+  exIR .= Nothing+  exRvfi .= mkRvfi+  exPC <~ use dePC+  mem <- exRvfi.rvfiInsn <<~ view fromMem+  scribe toRs1Addr . First . Just =<< exRvfi.rvfiRs1Addr <<~ exRs1 <.= sliceRs1 mem+  scribe toRs2Addr . First . Just =<< exRvfi.rvfiRs2Addr <<~ exRs2 <.= sliceRs2 mem+  isFirstCycle  <- use $ control.firstCycle -- first memory output undefined+  isMeBranching <- use $ control.meBranching+  isWbMemory    <- use $ control.wbMemory+  isExLoad      <- use $ control.exLoad+  isExBranching <- uses (control.exBranching) isJust+  let bubble = isFirstCycle || isMeBranching || isWbMemory || isExLoad || isExBranching+  case parseInstr mem of+    Right instr -> unless bubble $ do+      exIR ?= instr+      control.deLoad .= case instr of+        ExLoad{} -> True+        _        -> False+    Left IllegalInstruction -> do -- trap and instr=Nop (addi x0 x0 0)+      unless bubble $ exIR ?= ExAlu Add 0+      exRvfi.rvfiTrap .= True++-- | fetch instruction+fetch :: RWS ToPipe FromPipe Pipe ()+fetch = do+  scribe toMem . First . Just . instrMem =<< use fetchPC+  isMeMemory <- use $ control.meMemory+  isDeLoad   <- use $ control.deLoad+  use (control.exBranching) >>= \case+    Just npc -> fetchPC .= npc+    Nothing  -> unless (isMeMemory || isDeLoad) $ dePC <~ 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 "...1") -> slice d7  d0+  $(bitPattern "..1.") -> slice d15 d8+  $(bitPattern ".1..") -> slice d23 d16+  $(bitPattern "1...") -> slice d31 d24+  _ -> const 0++-- | slice address based on mask+sliceHalf :: BitVector 4 -> BitVector 32 -> BitVector 16+sliceHalf = \case+  $(bitPattern "..11") -> slice d15 d0+  $(bitPattern "11..") -> slice d31 d16+  _ -> const 0++-- | check if memory address misaligned on word boundary+isMisaligned :: (Bits a, Num a) => a -> Bool+isMisaligned a = a .&. 0x3 /= 0++-- | check if memory address misaligned on half-word boundary+isMisalignedHalf :: (Bits a, Num a) => a -> Bool+isMisalignedHalf a = a .&. 0x1 /= 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  = JAL+-- JR = JALR+-- O  = Bubble+-- S  = Store+-- *  = Stall+-- B  = Branch+--+-- Jump/Branch+-- +----+------+------+------+----++-- | IF |  DE  |  EX  |  ME  | WB |+-- +====+======+======+======+====++-- | 4  | ---- | ---- | ---- | -- |+-- +----+------+------+------+----++-- | 8  | JR20 | ---- | ---- | -- |+-- +----+------+------+------+----++-- | 12 |  O   | JR20 | ---- | -- |+-- +----+------+------+------+----++-- | 20 |  O   |  O   | JR20 | -- |+-- +----+------+------+------+----++--+-- Store+-- +-------+------+------+------+----++-- |  IF   | DE   |  EX  |  ME  | WB |+-- +=======+======+======+======+====++-- | 4     | ---- | ---- | ---- | -- |+-- +-------+------+------+------+----++-- | 8     |  S   | ---- | ---- | -- |+-- +-------+------+------+------+----++-- | 12    | J100 |  S   | ---- | -- |+-- +-------+------+------+------+----++-- | *16*  |  O   | J100 |  S   | -- |+-- +-------+------+------+------+----++-- |  100  |  O   |  O   | J100 | S  |+-- +-------+------+------+------+----++--+-- Load+-- +------+------+------+------+----++-- | IF   |  DE  |  EX  |  ME  | WB |+-- +======+======+======+======+====++-- | 4    | ---- | ---- | ---- | -- |+-- +------+------+------+------+----++-- | *8*  |  L   | ---- | ---- | -- |+-- +------+------+------+------+----++-- | 8    |  O   |  L   | ---- | -- |+-- +------+------+------+------+----++-- | *12* | B100 |  O   |  L   | -- |+-- +------+------+------+------+----++-- |  12  |  O   | B100 |  O   | L  |+-- +------+------+------+------+----++-- | 100  |  O   |  O   | B100 | O  |+-- +------+------+------+------+----+

@@ -0,0 +1,171 @@+{-|+Module      : Lion.Rvfi+Description : Lion RISC-V Formal Verification Interface+Copyright   : (c) David Cox, 2024+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+  { -- | 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+  , _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+  }

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               lion-version:            0.4.0.0+version:            0.4.0.1 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@@ -19,20 +19,20 @@   location: https://github.com/standardsemiconductor/lion  library-  exposed-modules: Lion.Core-                 , Lion.Rvfi-  other-modules:   Lion.Alu-                 , Lion.Instruction-                 , Lion.Pipe-  hs-source-dirs: src+  exposed-modules:  Lion.Core+                  , Lion.Rvfi+  other-modules:    Lion.Alu+                  , Lion.Instruction+                  , Lion.Pipe+  hs-source-dirs:   lib   default-language: Haskell2010-  build-depends: -    base           >= 4.13  && < 4.17,+  build-depends:+    base           >= 4.13  && < 4.21,     generic-monoid >= 0.1   && < 0.2,-    mtl            >= 2.2   && < 2.3,-    lens           >= 4.19  && < 5.2,-    ice40-prim     >= 0.3   && < 0.3.1.4,-    clash-prelude  >= 1.2.5 && < 1.7,+    mtl            >= 2.2   && < 2.4,+    lens           >= 4.19  && < 5.4,+    ice40-prim     >= 0.3   && < 0.3.1.5,+    clash-prelude  >= 1.2.5 && < 1.9,     ghc-typelits-natnormalise,     ghc-typelits-extra,     ghc-typelits-knownnat

@@ -1,121 +0,0 @@-{-| -Module      : Lion.Alu-Description : Lion arithmetic logic unit-Copyright   : (c) David Cox, 2021-2024-License     : BSD-3-Clause-Maintainer  : standardsemiconductor@gmail.com--Configurable alu, choose between soft and hard adders/subtractors--}--module Lion.Alu where--import Clash.Prelude-import Data.Function ( on )-import Ice40.Mac (-  Input(..),-  Parameter(..),-  defaultInput,-  defaultParameter,-  mac-  )-import Lion.Instruction (Op(..))---- | ALU configuration-data AluConfig = Hard -- ^ use hard adder and subtractor from iCE40 SB_MAC16-               | Soft -- ^ use generic adder and subtractor: (+) and (-)-  deriving stock (Generic, Show, Eq)--alu-  :: HiddenClockResetEnable dom-  => AluConfig-  -> Signal dom Op-  -> Signal dom (BitVector 32)-  -> Signal dom (BitVector 32)-  -> Signal dom (BitVector 32)-alu = \case-  Hard -> hardAlu-  Soft -> softAlu--softAlu- :: HiddenClockResetEnable dom- => Signal dom Op- -> Signal dom (BitVector 32)- -> Signal dom (BitVector 32)- -> Signal dom (BitVector 32)-softAlu op in1 = register 0 . liftA3 aluFunc op in1-    where-      aluFunc = \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-          (...) = (.).(.)--hardAlu-  :: HiddenClockResetEnable dom-  => Signal dom Op-  -> Signal dom (BitVector 32)-  -> Signal dom (BitVector 32)-  -> Signal dom (BitVector 32)-hardAlu op in1 in2 = mux isAddSub adderSubtractor $ register 0 $ baseAlu op in1 in2-    where-      isAdd = (Add == ) <$> op-      isSub = (Sub == ) <$> op-      isAddSub = delay False $ isAdd .||. isSub-      adderSubtractor = hardAddSub (boolToBit <$> isSub) in1 in2-  -baseAlu-  :: Signal dom Op-  -> Signal dom (BitVector 32)-  -> Signal dom (BitVector 32)-  -> Signal dom (BitVector 32)-baseAlu = liftA3 $ \case -  Add  -> \_ _ -> 0-  Sub  -> \_ _ -> 0-  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-    (...) = (.).(.)---- | addSub32PipelinedUnsigned-hardAddSub-  :: HiddenClock dom-  => Signal dom Bit -- ^ 0 = Add, 1 = Sub-  -> Signal dom (BitVector 32)-  -> Signal dom (BitVector 32)-  -> Signal dom (BitVector 32)-hardAddSub addSub x y = out-  where-    (out, _, _, _) = mac parameter input-    input = defaultInput{ a = slice d31 d16 <$> y-                        , b = slice d15 d0  <$> y-                        , c = slice d31 d16 <$> x-                        , d = slice d15 d0  <$> x-                        , addsubtop = addSub-                        , addsubbot = addSub-                        }-    parameter = defaultParameter{ topOutputSelect = 1-                                , topAddSubUpperInput = 1-                                , topAddSubCarrySelect = 2-                                , botOutputSelect = 1-                                , botAddSubUpperInput = 1-                                , mode8x8 = 1-                                }

@@ -1,93 +0,0 @@-{-|-Module      : Lion.Core-Description : Lion RISC-V Core-Copyright   : (c) David Cox, 2024-License     : BSD-3-Clause-Maintainer  : standardsemiconductor@gmail.com--The Lion core is a 32-bit [RISC-V](https://riscv.org/about/) 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-  , defaultCoreConfig-  , P.defaultPipeConfig-  , CoreConfig(..)-  , AluConfig(..)-  , P.PipeConfig(..)-  , FromCore(..)-  , P.ToMem(..)-  , P.MemoryAccess(..)-  ) where--import Clash.Prelude-import Data.Maybe-import Data.Monoid-import Lion.Alu-import Lion.Rvfi-import qualified Lion.Pipe as P-import qualified Lion.Instruction as I (Op(Add))---- | Core configuration-data CoreConfig = CoreConfig-  { aluConfig  :: AluConfig    -- ^ ALU configuration, default: `Soft`-  , pipeConfig :: P.PipeConfig -- ^ pipeline configuration-  }-  deriving stock (Generic, Show, Eq)---- | Default core configuration------ `aluConfig` = `Soft`------ `pipeConfig` = `P.defaultPipeConfig`-defaultCoreConfig :: CoreConfig-defaultCoreConfig = CoreConfig-  { aluConfig  = Soft-  , pipeConfig = P.defaultPipeConfig-  }---- | 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-  }---- | RISC-V Core: RV32I-core-  :: HiddenClockResetEnable dom-  => CoreConfig                 -- ^ core configuration-  -> Signal dom (BitVector 32)  -- ^ core input, from memory/peripherals-  -> FromCore dom               -- ^ core output-core config toCore = FromCore-  { toMem  = getFirst . P._toMem <$> fromPipe-  , toRvfi = fromMaybe mkRvfi . getFirst . P._toRvfi <$> fromPipe-  }-  where-    -- alu connection-    aluOp = fromMaybe I.Add . getFirst . P._toAluOp     <$> fromPipe-    aluInput1 = fromMaybe 0 . getFirst . P._toAluInput1 <$> fromPipe-    aluInput2 = fromMaybe 0 . getFirst . P._toAluInput2 <$> fromPipe-    aluOutput = alu (aluConfig config) aluOp aluInput1 aluInput2--    -- reg bank connection-    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--    -- pipeline connection-    fromPipe = P.pipe (pipeConfig config) $ P.ToPipe <$> rs1Data -                                                     <*> rs2Data -                                                     <*> aluOutput-                                                     <*> toCore---- | 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

@@ -1,188 +0,0 @@-{-|-Module      : Lion.Instruction-Description : RISC-V ISA-Copyright   : (c) David Cox, 2024-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---- | Writeback pipeline instruction-data WbInstr = WbRegWr (Unsigned 5) (BitVector 32)-             | WbLoad Load (Unsigned 5) (BitVector 4)-             | WbStore-             | WbNop-  deriving stock (Generic, Show, Eq)-  deriving anyclass NFDataX---- | Memory pipeline instruction-data MeInstr = MeRegWr      (Unsigned 5)-             | MeJump       (Unsigned 5) (BitVector 32)-             | MeBranch -             | MeStore                   (BitVector 32) (BitVector 4) (BitVector 32)-             | MeLoad  Load (Unsigned 5) (BitVector 32) (BitVector 4)-             | MeNop-  deriving stock (Generic, Show, Eq)-  deriving anyclass NFDataX---- | Execute pipeline instruction-data ExInstr = Ex       ExOp   (Unsigned 5) (BitVector 32)-             | ExJump   Jump   (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---- | ALU operation-data Op = Add-        | Sub-        | Sll-        | Slt-        | Sltu-        | Xor-        | Srl-        | Sra-        | Or-        | And-  deriving stock (Generic, Show, Eq)-  deriving anyclass NFDataX---- | Branch operation-data Branch = Beq-            | Bne-            | Blt-            | Bge-            | Bltu-            | Bgeu-  deriving stock (Generic, Show, Eq)-  deriving anyclass NFDataX---- | branch calculation-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-  deriving stock (Generic, Show, Eq)-  deriving anyclass NFDataX--data Jump = Jal | Jalr-  deriving stock (Generic, Show, Eq)-  deriving anyclass NFDataX---- | Store operation-data Store = Sb-           | Sh-           | Sw-  deriving stock (Generic, Show, Eq)-  deriving anyclass NFDataX---- | Load operation-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 $ ExJump Jal  rd immJ -- jal-  $(bitPattern ".................000.....1100111") -> Right $ ExJump 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---    npcB = immB + pc---    npcJ = immJ + pc--    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

@@ -1,503 +0,0 @@-{-|-Module      : Lion.Pipe-Description : RISC-V 5-stage pipeline-Copyright   : (c) David Cox, 2024-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 configuration-newtype PipeConfig = PipeConfig-  { startPC :: BitVector 32 -- ^ start program counter-  } deriving stock (Generic, Show, Eq)---- | Default pipeline configuration--- --- `startPC` = 0-defaultPipeConfig :: PipeConfig-defaultPipeConfig = PipeConfig 0---- | Pipeline inputs-data ToPipe = ToPipe-  { _fromRs1 :: BitVector 32-  , _fromRs2 :: BitVector 32-  , _fromAlu :: BitVector 32-  , _fromMem :: BitVector 32-  }-  deriving stock (Generic, Show, Eq)-  deriving anyclass NFDataX-makeLenses ''ToPipe---- | Memory access - Lion has a shared instruction/memory bus-data MemoryAccess = InstrMem -- ^ instruction access-                  | DataMem  -- ^ data access-  deriving stock (Generic, Show, Eq)-  deriving anyclass NFDataX---- | Memory bus-data ToMem = ToMem-  { memAccess   :: MemoryAccess         -- ^ memory access type-  , memAddress  :: BitVector 32         -- ^ memory address-  , memByteMask :: BitVector 4          -- ^ memory byte mask-  , memWrite    :: Maybe (BitVector 32) -- ^ read=Nothing write=Just wr-  }-  deriving stock (Generic, Show, Eq)-  deriving anyclass NFDataX---- | Construct instruction memory access-instrMem -  :: BitVector 32 -- ^ instruction address-  -> ToMem-instrMem addr = ToMem-  { memAccess   = InstrMem-  , memAddress  = addr-  , memByteMask = 0xF-  , memWrite    = Nothing-  }---- | Construct data memory access-dataMem -  :: BitVector 32         -- ^ memory address-  -> BitVector 4          -- ^ byte mask-  -> Maybe (BitVector 32) -- ^ write-  -> ToMem-dataMem addr mask wrM = ToMem-  { memAccess   = DataMem-  , memAddress  = addr-  , memByteMask = mask-  , memWrite    = wrM-  }---- | Pipeline outputs-data FromPipe = FromPipe-  { _toMem       :: First ToMem-  , _toRs1Addr   :: First (Unsigned 5)-  , _toRs2Addr   :: First (Unsigned 5)-  , _toRd        :: First (Unsigned 5, BitVector 32)-  , _toAluOp     :: First Op-  , _toAluInput1 :: First (BitVector 32)-  , _toAluInput2 :: First (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-  , _exBranching :: Maybe (BitVector 32)             -- ^ execute stage branch/jump-  , _meBranching :: Bool                             -- ^ memory stage branch/jump-  , _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   -  , _exBranching = Nothing-  , _meBranching = False-  , _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 :: PipeConfig -> Pipe-mkPipe pipeConfig = Pipe-  { _fetchPC = startPC pipeConfig--  -- 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-  => PipeConfig-  -> Signal dom ToPipe-  -> Signal dom FromPipe-pipe config = mealy pipeMealy (mkPipe config)-  where-    pipeMealy s i = let ((), s', o) = runRWS pipeM i s-                    in (s', o) ---- | Monadic pipeline-pipeM :: RWS ToPipe FromPipe Pipe ()-pipeM = do-  writeback-  memory-  execute-  decode-  fetch-  control .= mkControl{ _firstCycle = False } -- reset control---- | 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 byte = sliceByte mask mem-          half = sliceHalf mask mem-          wr = case op of-            Lb  -> signExtend byte-            Lh  -> signExtend half-            Lw  -> 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-    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-    MeNop -> wbIR ?= WbNop-    MeRegWr rd -> do-      wr <- view fromAlu-      control.meRegFwd ?= (rd, wr)-      wbIR ?= WbRegWr rd wr-    MeJump rd pc4 -> do-      control.meBranching .= True-      control.meRegFwd ?= (rd, pc4)-      wbIR ?= WbRegWr rd pc4-    MeBranch -> do-      control.meBranching .= True-      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-  pc4 <- 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 -> do-      scribeAlu Add imm $ case op of-        Lui   -> 0-        Auipc -> pc-      meIR ?= MeRegWr rd-    ExJump jump rd imm -> do-      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-          branchPC <- meRvfi.rvfiPcWData <<~ control.exBranching <?= pc + imm-          meRvfi.rvfiTrap ||= isMisaligned branchPC-          meIR ?= MeBranch-        else do-          meRvfi.rvfiTrap ||= isMisaligned pc4-          meIR ?= MeNop-    ExStore op imm -> 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 ||= isMisalignedHalf addr -- trap on half-word boundary-          let wr = concatBitVector# $ replicate d2 $ slice d15 d0 rs2Data-          meIR ?= MeStore addr' (halfMask addr) wr-        Sw -> do-          meRvfi.rvfiTrap ||= isMisaligned addr -- 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 ||= isMisalignedHalf addr -- trap on half-word boundary-             meIR ?= MeLoad op rdAddr addr' (halfMask addr)-         | otherwise -> do -- Lw-             meRvfi.rvfiTrap ||= isMisaligned addr -- trap on word boundary-             meIR ?= MeLoad op rdAddr addr' 0xF-    ExAlu op rd -> do-      scribeAlu op rs1Data rs2Data-      meIR ?= MeRegWr rd-    ExAluImm op rd imm -> do-      scribeAlu op rs1Data imm-      meIR ?= MeRegWr rd-  where-    scribeAlu op in1 in2 = do-      scribe toAluOp     $ First $ Just op-      scribe toAluInput1 $ First $ Just in1-      scribe toAluInput2 $ First $ Just in2--    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-      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 ()-decode = do-  exIR .= Nothing-  exRvfi .= mkRvfi-  exPC <~ use dePC-  mem <- exRvfi.rvfiInsn <<~ view fromMem-  scribe toRs1Addr . First . Just =<< exRvfi.rvfiRs1Addr <<~ exRs1 <.= sliceRs1 mem-  scribe toRs2Addr . First . Just =<< exRvfi.rvfiRs2Addr <<~ exRs2 <.= sliceRs2 mem-  isFirstCycle  <- use $ control.firstCycle -- first memory output undefined-  isMeBranching <- use $ control.meBranching-  isWbMemory    <- use $ control.wbMemory-  isExLoad      <- use $ control.exLoad-  isExBranching <- uses (control.exBranching) isJust-  let bubble = isFirstCycle || isMeBranching || isWbMemory || isExLoad || isExBranching-  case parseInstr mem of-    Right instr -> unless bubble $ do-      exIR ?= instr-      control.deLoad .= case instr of-        ExLoad{} -> True-        _        -> False-    Left IllegalInstruction -> do -- trap and instr=Nop (addi x0 x0 0)-      unless bubble $ exIR ?= ExAlu Add 0-      exRvfi.rvfiTrap .= True-        --- | fetch instruction-fetch :: RWS ToPipe FromPipe Pipe ()-fetch = do-  scribe toMem . First . Just . instrMem =<< use fetchPC-  isMeMemory <- use $ control.meMemory-  isDeLoad   <- use $ control.deLoad-  use (control.exBranching) >>= \case-    Just npc -> fetchPC .= npc-    Nothing  -> unless (isMeMemory || isDeLoad) $ dePC <~ 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 "...1") -> slice d7  d0-  $(bitPattern "..1.") -> slice d15 d8-  $(bitPattern ".1..") -> slice d23 d16-  $(bitPattern "1...") -> slice d31 d24-  _ -> const 0---- | slice address based on mask-sliceHalf :: BitVector 4 -> BitVector 32 -> BitVector 16-sliceHalf = \case-  $(bitPattern "..11") -> slice d15 d0-  $(bitPattern "11..") -> slice d31 d16-  _ -> const 0---- | check if memory address misaligned on word boundary-isMisaligned :: (Bits a, Num a) => a -> Bool-isMisaligned a = a .&. 0x3 /= 0---- | check if memory address misaligned on half-word boundary-isMisalignedHalf :: (Bits a, Num a) => a -> Bool-isMisalignedHalf a = a .&. 0x1 /= 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  = JAL--- JR = JALR--- O  = Bubble--- S  = Store--- *  = Stall--- B  = Branch------ Jump/Branch--- +----+------+------+------+----+--- | IF |  DE  |  EX  |  ME  | WB |--- +====+======+======+======+====+--- | 4  | ---- | ---- | ---- | -- |--- +----+------+------+------+----+--- | 8  | JR20 | ---- | ---- | -- |--- +----+------+------+------+----+--- | 12 |  O   | JR20 | ---- | -- |--- +----+------+------+------+----+--- | 20 |  O   |  O   | JR20 | -- |--- +----+------+------+------+----+------ Store--- +-------+------+------+------+----+--- |  IF   | DE   |  EX  |  ME  | WB |--- +=======+======+======+======+====+--- | 4     | ---- | ---- | ---- | -- |--- +-------+------+------+------+----+--- | 8     |  S   | ---- | ---- | -- |--- +-------+------+------+------+----+--- | 12    | J100 |  S   | ---- | -- |--- +-------+------+------+------+----+--- | *16*  |  O   | J100 |  S   | -- |--- +-------+------+------+------+----+--- |  100  |  O   |  O   | J100 | S  |--- +-------+------+------+------+----+------ Load--- +------+------+------+------+----+--- | IF   |  DE  |  EX  |  ME  | WB |--- +======+======+======+======+====+--- | 4    | ---- | ---- | ---- | -- |--- +------+------+------+------+----+--- | *8*  |  L   | ---- | ---- | -- |--- +------+------+------+------+----+--- | 8    |  O   |  L   | ---- | -- |--- +------+------+------+------+----+--- | *12* | B100 |  O   |  L   | -- |--- +------+------+------+------+----+--- |  12  |  O   | B100 |  O   | L  |--- +------+------+------+------+----+--- | 100  |  O   |  O   | B100 | O  |--- +------+------+------+------+----+

@@ -1,171 +0,0 @@-{-|-Module      : Lion.Rvfi-Description : Lion RISC-V Formal Verification Interface-Copyright   : (c) David Cox, 2024-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-  { -- | 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-  , _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-  }