Merge branch 'standardsemiconductor:main' into main

cardanonix · Feb 26, 2024 · c3be91b · c3be91b
2 parents df6afac + ae03d4f
commit c3be91b
Show file tree

Hide file tree

Showing 16 changed files with 43 additions and 34 deletions.
diff --git a/.github/workflows/haskell.yml b/.github/workflows/haskell.yml
@@ -29,13 +29,15 @@ jobs:
 
     - name: Free up environment resources
       run: |
+        df -h
         sudo rm -rf /usr/share/dotnet
         sudo rm -rf /opt/ghc
         sudo rm -rf /usr/local/share/boost
         sudo rm -rf "$AGENT_TOOLSDIRECTORY"
+        df -h
 
     - name: Set up GHC ${{ matrix.ghc-version }}
-      uses: haskell/actions/setup@v2
+      uses: haskell-actions/setup@v2
       id: setup
       with:
         ghc-version: ${{ matrix.ghc-version }}
@@ -63,7 +65,7 @@ jobs:
         cabal configure --enable-tests --enable-benchmarks --disable-documentation
         cabal build --dry-run
 
-    - name: Restore cached dependencies
+    - name: Restore Haskell cached dependencies
       uses: actions/cache/restore@v3
       id: cache
       env:
@@ -175,12 +177,12 @@ jobs:
     - name: Install boolector
       working-directory: boolector
       run: |
-        ./contrib/setup-btor2tools.sh
         ./contrib/setup-lingeling.sh
+        ./contrib/setup-btor2tools.sh
         ./configure.sh
         make -C build -j$(nproc)
         sudo cp build/bin/{boolector,btor*} /usr/local/bin
-        sudo cp deps/btor2tools/bin/btorsim /usr/local/bin
+        sudo cp deps/btor2tools/build/bin/btorsim /usr/local/bin
 
     - name: Checkout riscv-gnu-toolchain
       uses: actions/checkout@v3

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,7 +1,8 @@
 # Revision history for lion
 
-## 0.X.X.X
+## 0.4.0.0
 * Update clash-prelude dependency bounds #4
+* Type-level -> data-level configuration #6
 
 ## 0.3.0.0
 

diff --git a/LICENSE b/LICENSE
@@ -1,6 +1,6 @@
 BSD 3-Clause License
 
-Copyright (c) 2021, David Cox
+Copyright (c) 2024, David Cox
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without

diff --git a/lion-formal/README.md b/lion-formal/README.md
@@ -6,7 +6,12 @@ At minimum to run Lion formal verification using [riscv-formal](https://github.c
 > See [here](https://symbiyosys.readthedocs.io/en/latest/install.html)
 > for intall instructions.
 
-If you want to inspect counter example traces or disassemble the code in the counter example traces see the [ricsv-formal prerequisites](https://github.com/standardsemiconductor/riscv-formal/blob/lion/docs/quickstart.md#prerequisites).
+The [nightly pipeline](https://github.com/standardsemiconductor/lion/blob/main/.github/workflows/haskell.yml)
+also has up-to-date steps to install Yosys, SymbiYosys,
+and Boolector.
+
+If you want to inspect counter example traces or disassemble the code in the
+counter example traces see the [ricsv-formal prerequisites](https://github.com/standardsemiconductor/riscv-formal/blob/lion/docs/quickstart.md#prerequisites).
 
 ## Usage
 Build:      `cabal build`

diff --git a/lion-formal/lion-formal.cabal b/lion-formal/lion-formal.cabal
@@ -18,7 +18,7 @@ library
   build-depends:
     base          >= 4.13 && < 4.17,
     clash-prelude >= 1.4  && < 1.7,
-    lion          >= 0.3  && < 0.4,
+    lion          >= 0.4  && < 0.5,
     ghc-typelits-natnormalise,
     ghc-typelits-extra,
     ghc-typelits-knownnat

diff --git a/lion-metric/README.md b/lion-metric/README.md
@@ -10,21 +10,22 @@ generate metrics: `cabal run`
 
 clean: `cabal run metric -- clean`
 
-## Metrics as of Jun 24 2021 for iCE40
+## Metrics as of Jan 17 2024 for iCE40
 ```
 === Metric ===
 
-   Number of wires:               2305
-   Number of wire bits:         632631
-   Number of public wires:        2305
-   Number of public wire bits:  632631
+   Number of wires:               2831
+   Number of wire bits:         380325
+   Number of public wires:        2831
+   Number of public wire bits:  380325
    Number of memories:               0
    Number of memory bits:            0
    Number of processes:              0
-   Number of cells:               2702
-     SB_CARRY                      370
+   Number of cells:               2968
+     SB_CARRY                      368
+     SB_DFF                         72
      SB_DFFER                       64
      SB_DFFR                       266
-     SB_LUT4                      1998
+     SB_LUT4                      2194
      SB_RAM40_4K                     4
 ```
diff --git a/lion-metric/lion-metric.cabal b/lion-metric/lion-metric.cabal
@@ -16,8 +16,8 @@ library
   default-language: Haskell2010
   build-depends:
     base          >= 4.13 && < 4.17,
-    clash-prelude >= 1.4 && < 1.7,
-    lion          >= 0.3 && < 0.4,
+    clash-prelude >= 1.4  && < 1.7,
+    lion          >= 0.4  && < 0.5,
     ghc-typelits-natnormalise,
     ghc-typelits-extra,
     ghc-typelits-knownnat

diff --git a/lion-soc/README.md b/lion-soc/README.md
@@ -16,7 +16,7 @@
     ```
 
 ## Usage
-1. `cabal build`
+1. `cabal build all`
 2. Ensure the VELDT is ON and in the FLASH mode.
 3. `cabal run soc -- prog` 
 4. Cycle power switch, set mode switch to FPGA.
@@ -27,7 +27,7 @@
  / /__/ / _ \/ _ \  _\ \/ _ \/ /__  
 /____/_/\___/_//_/ /___/\___/\___/  
 
-Standard Semiconductor (c) 2021
+Standard Semiconductor (c) 2024
 
 Checking FLASH...SUCCESS
 ```
@@ -36,11 +36,11 @@ To compile, synthesize, and route Lion SoC without programming: `cabal run soc`
 ### Clean
 `cabal run soc -- clean`
 
-## Metrics as of Dec 30 2021 for iCE40
+## Metrics as of Jan 17 2024 for iCE40
 ### Device utilisation
 ```
 Device utilisation:
-   ICESTORM_LC:  2600/ 5280    49%
+   ICESTORM_LC:  2685/ 5280    50%
   ICESTORM_RAM:     8/   30    26%
          SB_IO:     6/   96     6%
          SB_GB:     8/    8   100%
@@ -53,7 +53,7 @@ ICESTORM_SPRAM:     4/    4   100%
 ```
 ### Clock frequency
 ```
-Max frequency for clock: 14.17 MHz (PASS @ 12Mhz)
+Max frequency for clock: 14.93 MHz (PASS @ 12MHz)
 ```
 
 ## Memory Map

diff --git a/lion-soc/bios/bios.S b/lion-soc/bios/bios.S
@@ -335,7 +335,7 @@ name:
     .string "\n\r   __   _             ____     _____\n\r  / /  (_)__  ___    / __/__  / ___/\n\r / /__/ / _ \\/ _ \\  _\\ \\/ _ \\/ /__  \n\r/____/_/\\___/_//_/ /___/\\___/\\___/  \n\r"
 
 copyright:
-    .string "\n\rStandard Semiconductor (c) 2021\n\r\n\r"
+    .string "\n\rStandard Semiconductor (c) 2024\n\r\n\r"
 
 #check_spram_str:
 #    .string "Checking SPRAM..."
@@ -346,4 +346,4 @@ check_flash_str:
 success_str:
     .string "SUCCESS\n\r"
 fail_str:
-    .string "FAIL\n\r"
+    .string "FAIL\n\r"
diff --git a/lion-soc/lion-soc.cabal b/lion-soc/lion-soc.cabal
@@ -25,7 +25,7 @@ library
     generic-monoid >= 0.1 && < 0.2,
     ice40-prim     >= 0.3 && < 0.4,
     lens,
-    lion           >= 0.3 && < 0.4,
+    lion           >= 0.4 && < 0.5,
     mtl            >= 2.2 && < 2.3,
     ghc-typelits-natnormalise,
     ghc-typelits-extra,

diff --git a/lion.cabal b/lion.cabal
@@ -1,14 +1,14 @@
 cabal-version:      2.4
 name:               lion
-version:            0.3.0.0
+version:            0.4.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 <[email protected]>
 maintainer:         dopamane <[email protected]>
-copyright:          (c) 2021-2023 David Cox
+copyright:          (c) 2021-2024 David Cox
 category:           Hardware
 extra-source-files:
     CHANGELOG.md
@@ -31,7 +31,7 @@ library
     generic-monoid >= 0.1   && < 0.2,
     mtl            >= 2.2   && < 2.3,
     lens           >= 4.19  && < 5.2,
-    ice40-prim     >= 0.3   && < 0.4,
+    ice40-prim     >= 0.3   && < 0.3.1.4,
     clash-prelude  >= 1.2.5 && < 1.7,
     ghc-typelits-natnormalise,
     ghc-typelits-extra,

diff --git a/src/Lion/Alu.hs b/src/Lion/Alu.hs
@@ -1,7 +1,7 @@
 {-| 
 Module      : Lion.Alu
 Description : Lion arithmetic logic unit
-Copyright   : (c) David Cox, 2021-2022
+Copyright   : (c) David Cox, 2021-2024
 License     : BSD-3-Clause
 Maintainer  : [email protected]
 

diff --git a/src/Lion/Core.hs b/src/Lion/Core.hs
@@ -1,7 +1,7 @@
 {-|
 Module      : Lion.Core
 Description : Lion RISC-V Core
-Copyright   : (c) David Cox, 2021
+Copyright   : (c) David Cox, 2024
 License     : BSD-3-Clause
 Maintainer  : [email protected]
 

diff --git a/src/Lion/Instruction.hs b/src/Lion/Instruction.hs
@@ -1,7 +1,7 @@
 {-|
 Module      : Lion.Instruction
 Description : RISC-V ISA
-Copyright   : (c) David Cox, 2021
+Copyright   : (c) David Cox, 2024
 License     : BSD-3-Clause
 Maintainer  : [email protected]
 -}

diff --git a/src/Lion/Pipe.hs b/src/Lion/Pipe.hs
@@ -1,7 +1,7 @@
 {-|
 Module      : Lion.Pipe
 Description : RISC-V 5-stage pipeline
-Copyright   : (c) David Cox, 2021
+Copyright   : (c) David Cox, 2024
 License     : BSD-3-Clause
 Maintainer  : [email protected]
 -}

diff --git a/src/Lion/Rvfi.hs b/src/Lion/Rvfi.hs
@@ -1,7 +1,7 @@
 {-|
 Module      : Lion.Rvfi
 Description : Lion RISC-V Formal Verification Interface
-Copyright   : (c) David Cox, 2021
+Copyright   : (c) David Cox, 2024
 License     : BSD-3-Clause
 Maintainer  : [email protected]