Merge branch 'standardsemiconductor:main' into main

.github/dependabot.yml

@@ -0,0 +1,11 @@
+# To get started with Dependabot version updates, you'll need to specify which
+# package ecosystems to update and where the package manifests are located.
+# Please see the documentation for all configuration options:
+# https://docs.github.com/code-security/dependabot/dependabot-version-updates/configuration-options-for-the-dependabot.yml-file
+
+version: 2
+updates:
+  - package-ecosystem: "github-actions" # See documentation for possible values
+    directory: "/" # Location of package manifests
+    schedule:
+      interval: "weekly"

.github/workflows/haskell.yml

@@ -23,7 +23,7 @@ jobs:
         os: [ubuntu-20.04]
 
     steps:
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
       with:
         submodules: true
 
@@ -66,7 +66,7 @@ jobs:
         cabal build --dry-run
 
     - name: Restore Haskell cached dependencies
-      uses: actions/cache/restore@v3
+      uses: actions/cache/restore@v4
       id: cache
       env:
         key: ${{ runner.os }}-ghc-${{ steps.setup.outputs.ghc-version }}-cabal-${{ steps.setup.outputs.cabal-version }}
@@ -91,7 +91,7 @@ jobs:
       run: cabal build all --only-dependencies
 
     - name: Save cached dependencies
-      uses: actions/cache/save@v3
+      uses: actions/cache/save@v4
       if: ${{ steps.cache.outputs.cache-primary-key != steps.cache.outputs.cache-matched-key }}
       with:
         path: ${{ steps.setup.outputs.cabal-store }}
@@ -115,7 +115,7 @@ jobs:
         sudo apt-get install build-essential clang bison flex libreadline-dev gawk tcl-dev libffi-dev git graphviz xdot pkg-config python python3 libftdi-dev qt5-default python3-dev libboost-all-dev cmake libeigen3-dev
 
     - name: Checkout icestorm
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         repository: YosysHQ/icestorm
         path: icestorm
@@ -127,7 +127,7 @@ jobs:
         sudo make install
 
     - name: Checkout nextpnr
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         repository: YosysHQ/nextpnr
         ref: master
@@ -142,33 +142,34 @@ jobs:
         sudo make install
 
     - name: Checkout yosys
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         repository: YosysHQ/yosys
-        ref: master
+        ref: main
         path: yosys
+        submodules: true
 
     - name: Install yosys
       working-directory: yosys
       run: |
         make -j$(nproc)
         sudo make install
 
-    - name: Checkout SymbiYosys
-      uses: actions/checkout@v3
+    - name: Checkout SymbiYosys (sby)
+      uses: actions/checkout@v4
       with:
-        repository: YosysHQ/SymbiYosys
-        ref: master
-        path: SymbiYosys
+        repository: YosysHQ/sby
+        ref: main
+        path: sby
 
     - name: Install SymbiYosys
-      working-directory: SymbiYosys
+      working-directory: sby
       run: |
         sudo apt-get install libboost-program-options-dev autoconf libgmp-dev cmake
         sudo make install
 
     - name: Checkout Boolector
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         repository: boolector/boolector
         ref: master
@@ -185,7 +186,7 @@ jobs:
         sudo cp deps/btor2tools/build/bin/btorsim /usr/local/bin
 
     - name: Checkout riscv-gnu-toolchain
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         repository: riscv/riscv-gnu-toolchain
         ref: master

CHANGELOG.md

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

README.md

@@ -8,9 +8,9 @@ Lion is a formally verified, 5-stage pipeline [RISC-V](https://riscv.org) core.
 
 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:

src/Lion/Alu.hs → lib/Lion/Alu.hs

@@ -1,4 +1,6 @@
-{-| 
+{-# LANGUAGE CPP #-}
+
+{-|
 Module      : Lion.Alu
 Description : Lion arithmetic logic unit
 Copyright   : (c) David Cox, 2021-2024
@@ -10,7 +12,11 @@ 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(..),
@@ -45,7 +51,7 @@ softAlu
  -> Signal dom (BitVector 32)
 softAlu op in1 = register 0 . liftA3 aluFunc op in1
     where
-      aluFunc = \case 
+      aluFunc = \case
         Add  -> (+)
         Sub  -> (-)
         Sll  -> \x y -> x `shiftL` shamt y
@@ -73,13 +79,13 @@ hardAlu op in1 in2 = mux isAddSub adderSubtractor $ register 0 $ baseAlu op in1
       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 
+baseAlu = liftA3 $ \case
   Add  -> \_ _ -> 0
   Sub  -> \_ _ -> 0
   Sll  -> \x y -> x `shiftL` shamt y

src/Lion/Instruction.hs → lib/Lion/Instruction.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
 {-|
 Module      : Lion.Instruction
 Description : RISC-V ISA
@@ -8,7 +10,11 @@ Maintainer  : [email protected]
 
 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
@@ -26,7 +32,7 @@ data WbInstr = WbRegWr (Unsigned 5) (BitVector 32)
 -- | Memory pipeline instruction
 data MeInstr = MeRegWr      (Unsigned 5)
              | MeJump       (Unsigned 5) (BitVector 32)
-             | MeBranch 
+             | MeBranch
              | MeStore                   (BitVector 32) (BitVector 4) (BitVector 32)
              | MeLoad  Load (Unsigned 5) (BitVector 32) (BitVector 4)
              | MeNop
@@ -155,7 +161,7 @@ parseInstr i = case i of
 
     immI :: BitVector 32
     immI = signExtend $ slice d31 d20 i
-    
+
     immS :: BitVector 32
     immS = signExtend $ slice d31 d25 i ++# slice d11 d7 i
 
@@ -164,7 +170,7 @@ parseInstr i = case i of
 
     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
 

src/Lion/Pipe.hs → lib/Lion/Pipe.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
 {-|
 Module      : Lion.Pipe
 Description : RISC-V 5-stage pipeline
@@ -16,13 +18,18 @@ 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
@@ -55,7 +62,7 @@ data ToMem = ToMem
   deriving anyclass NFDataX
 
 -- | Construct instruction memory access
-instrMem 
+instrMem
   :: BitVector 32 -- ^ instruction address
   -> ToMem
 instrMem addr = ToMem
@@ -66,7 +73,7 @@ instrMem addr = ToMem
   }
 
 -- | Construct data memory access
-dataMem 
+dataMem
   :: BitVector 32         -- ^ memory address
   -> BitVector 4          -- ^ byte mask
   -> Maybe (BitVector 32) -- ^ write
@@ -111,8 +118,8 @@ data Control = Control
 makeLenses ''Control
 
 mkControl :: Control
-mkControl = Control 
-  { _firstCycle  = True   
+mkControl = Control
+  { _firstCycle  = True
   , _exBranching = Nothing
   , _meBranching = False
   , _deLoad      = False
@@ -156,9 +163,9 @@ mkPipe :: PipeConfig -> Pipe
 mkPipe pipeConfig = Pipe
   { _fetchPC = startPC pipeConfig
 
-  -- decode stage 
+  -- decode stage
   , _dePC    = 0
-  
+
   -- execute stage
   , _exIR    = Nothing
   , _exPC    = 0
@@ -169,26 +176,26 @@ mkPipe pipeConfig = Pipe
   -- memory stage
   , _meIR    = Nothing
   , _meRvfi  = mkRvfi
- 
+
   -- writeback stage
   , _wbIR    = Nothing
   , _wbNRet  = 0
   , _wbRvfi  = mkRvfi
-  
+
   -- pipeline control
   , _control = mkControl
   }
 
 -- | 5-Stage RISC-V pipeline
-pipe 
+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) 
+                    in (s', o)
 
 -- | Monadic pipeline
 pipeM :: RWS ToPipe FromPipe Pipe ()
@@ -329,21 +336,21 @@ execute = do
       scribe toAluInput1 $ First $ Just in1
       scribe toAluInput2 $ First $ Just in2
 
-    regFwd 
-      :: MonadState s m 
+    regFwd
+      :: MonadState s m
       => MonadReader r m
-      => Lens' s (Unsigned 5) 
+      => 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 = 
+    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 
+          :: MonadState s m
+          => Lens' s (Unsigned 5)
+          -> BitVector 32
           -> m (BitVector 32)
         guardZero addr value = do
           isZero <- uses addr (== 0)
@@ -375,7 +382,7 @@ decode = do
     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
@@ -391,9 +398,9 @@ fetch = do
 -------------
 
 -- | forward register writes
-fwd 
-  :: Unsigned 5 
-  -> BitVector 32 
+fwd
+  :: Unsigned 5
+  -> BitVector 32
   -> Maybe (Unsigned 5, BitVector 32) -- ^ meRegFwd
   -> Maybe (Unsigned 5, BitVector 32) -- ^ wbRegFwd
   -> BitVector 32

lion-formal/lion-formal.cabal

@@ -16,8 +16,8 @@ library
   hs-source-dirs: src
   default-language: Haskell2010
   build-depends:
-    base          >= 4.13 && < 4.17,
-    clash-prelude >= 1.4  && < 1.7,
+    base          >= 4.13 && < 4.21,
+    clash-prelude >= 1.4  && < 1.9,
     lion          >= 0.4  && < 0.5,
     ghc-typelits-natnormalise,
     ghc-typelits-extra,

lion-metric/cabal.project

@@ -1,5 +1,6 @@
 packages: lion-metric.cabal
         , ../lion.cabal
+        , https://hackage.haskell.org/package/ice40-prim-0.3.1.3/ice40-prim-0.3.1.3.tar.gz
 
 write-ghc-environment-files: always