Update installation instructions

.gitignore

@@ -8,3 +8,9 @@ docs/*
 *.bin
 .cache/
 .venv*/
+
+# artifacts from compiling the examples
+examples/project
+.metals
+.scala-build
+.bsp

source/SpinalHDL/Getting Started/Install and setup.rst

@@ -3,44 +3,91 @@
 Install and setup
 =================
 
-Spinal is a Scala library so it requires setting up a Scala environment; there
-are many ways to do so. Also, it generates VHDL, Verilog or SystemVerilog, which
-can be used by many different tools. This section describes the supported way to
-install a *SpinalHDL description to Simulation* flow, but there can be many
-variations.
+Spinal is a Scala library (a programming language using the Java VM) so it
+requires setting up a Scala environment; there are many ways to do so.
+Also, it generates VHDL, Verilog or SystemVerilog, which can be used by many
+different tools. This section describes the supported way to install a
+*SpinalHDL description to Simulation* flow, but there can be many variations.
 
-
-Mandatory requirements
-----------------------
+Required/Recommended tools
+--------------------------
 
 Before you download the SpinalHDL tools, you need to install a Scala environment:
 
 * `Java JDK <https://www.oracle.com/java/technologies/downloads/>`_, a Java
   environment
+* `Scala 2 <https://www.scala-lang.org/>`_, compiler and library
 * `SBT <https://www.scala-sbt.org/download.html>`_, a Scala build tool
 
 These tools enable to use Spinal; but without any other tools, it is limited to
-code generation.
+HDL code generation.
+
+To enable more features we recommend:
+
+* An IDE (for instance the currently recommended `IntelliJ <https://www.jetbrains.com/idea/>`_
+  with its Scala plugin or `VSCodium <https://vscodium.com/>`_ with Metals extension) to
+  get features such as:
+
+    * Code suggestions / completion
+    * Automatic build with syntax errors right in the code
+    * Generate code with a single click
+    * Run simulation / tests with a single click (if a supported simulator is
+      set up)
+
+* A supported simulator like `Verilator <https://www.veripool.org/verilator/>`_
+  to test the design right from SpinalHDL.
+* `Gtkwave <https://gtkwave.sourceforge.net/>`_ to view the waves generated by
+  Verilator during simulation.
+* `Git <https://git-scm.com/>`_ for version control system
+* A C++ toolchain, needed for simulating with Verilator
+* A linux shell, needed for simulating with Verilator
 
 Linux Installation
-----------------------
+------------------
 
-For instance, to install them on the Debian distribution:
+At time of writing the recommended way of installing Scala and SBT is via `Coursier <https://get-coursier.io/docs/cli-installation>`_.
+Coursier is able to in addition to the scala tools install a Java JDK to use, in the
+example below we install Java from the package manager. We recommend to install JDK 17 (LTS)
+because of compatibility with the used Scala version.
+
+For Debian or Ubuntu we run:
 
 .. code-block:: sh
 
-   sudo apt-get install openjdk-8-jdk
-   sudo apt-get install scala
-   echo "deb https://repo.scala-sbt.org/scalasbt/debian all main" | sudo tee /etc/apt/sources.list.d/sbt.list
-   echo "deb https://repo.scala-sbt.org/scalasbt/debian /" | sudo tee /etc/apt/sources.list.d/sbt_old.list
-   curl -sL "https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x2EE0EA64E40A89B84B2DF73499E82A75642AC823" | sudo apt-key add
    sudo apt-get update
-   sudo apt-get install sbt
+   sudo apt-get install openjdk-17-jdk-headless curl git
+   curl -fL "https://github.com/coursier/launchers/raw/master/cs-x86_64-pc-linux.gz" | gzip -d > cs
+   chmod +x cs
+   # should find the just installed jdk, agree to cs' questions for adding to your PATH
+   ./cs setup
+   source ~/.profile
+
+If you want to install the tools for simulation and/or formal proofs, we recommend `oss-cad-suite <https://github.com/YosysHQ/oss-cad-suite-build>`_.
+It contains a waveform viewer (gtkWave), verilog simulators (verilator and iverilog), VHDL simulator (GHDL) and other tools.
+In case you want to build the tools yourself have a look at the legacy simulation tool :ref:`installation instructions <sim backend install>`.
+
+We first install the needed C++ toolchain and download oss-cad-suite. To use it we must load the oss-cad-suite
+environment for each shell we want to use it in. Note that oss-cad-suite contains a Python 3 interpreter that
+may interfere with the system Python installation if loaded permanently.
+
+Go to the oss-cad-suite `release page <https://github.com/YosysHQ/oss-cad-suite-build/releases/latest>`_ to get the
+download link for the latest version. You can download/extract oss-cad-suite to a folder of your choice.
+(last tested version of oss-cad-suite is `2023-10-22`, but more recent ones will most likely also work)
+
+.. code-block:: sh
+
+   sudo apt-get install make gcc g++ zlib1g-dev
+   curl -fLO <download link>
+   tar xzf <file that you downloaded>
+
+To use oss-cad-suite in a shell you need to load it's environment, e.g. via ``souce <path to oss-cad-suite>/environment``.
+
 
 Mac OS X Installation
 ----------------------
 You can use homebrew to install on Mac OS X.  By default homebrew installs Java 21, but the  SpinalHDL tutorial 
-SpinalTemplateSbt uses Scala version 2.12.16, which is not supported by Java 21 (17 is still the recommended LTS version, https://whichjdk.com/). So to install Java version 1.7 do:
+SpinalTemplateSbt uses Scala version 2.12.16, which is not supported by Java 21 (17 is still the recommended LTS version,
+https://whichjdk.com/). So to install Java version 1.7 do:
 
 .. code-block:: sh
 
@@ -52,7 +99,7 @@ And then add this to your path.
 
    export PATH="/opt/homebrew/opt/openjdk@17/bin:$PATH"
 
-To manage multiple versions of Java, it is also essential to have jenv installed.
+To manage multiple versions of Java it is also essential to have jenv installed.
 
 .. code-block:: sh
 
@@ -73,64 +120,126 @@ Next you have to install scala's interactive build tool sbt.
 
 If this works for you, please let us know.  If this does not work for you, you can read the github issue about Mac o SX installation here. 
 https://github.com/SpinalHDL/SpinalHDL/issues/1216
-
-Installing SBT in an internet-free environment
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+If you want to install the tools for simulation and/or formal proofs, we recommend `oss-cad-suite <https://github.com/YosysHQ/oss-cad-suite-build>`_.
+
+Windows installation
+--------------------
 
 .. note::
-   If you do not need this, you can skip to the next section:
-   :ref:`recommended`.
+   While a native installation is possible the simpler and currently recommended way is to use WSL on Windows.
+   If you want to use WSL, install `it <https://learn.microsoft.com/en-us/windows/wsl/install>`_, a distribution of your choice and
+   follow the Linux installation instructions. Data in your WSL instance can be accessed from windows under ``\\wsl$``.
+   In case you want to use IntelliJ you'll have to download the Linux version to WSL, if you want to use VSCode then the Windows
+   version can be used to remotely edit in WSL.
 
-Normally, SBT uses online repositories to download and cache your projects
-dependencies. This cache is located in several folders:
+At time of writing the recommended way of installing Scala and SBT is via `Coursier <https://get-coursier.io/docs/cli-installation>`_.
+Coursier is able to in addition to the scala tools install a Java JDK to use, in the
+example below we install Java manually. We recommend to install JDK 17 (LTS) because of
+compatibility with Scala.
 
-* ``~/.sbt``
-* ``~/.cache/JNA``
-* ``~/.cache/coursier``
+First download and install `Adoptium JDK 17 <https://adoptium.net/temurin/releases/?os=windows&version=17>`_.
+Download, unzip and run the `Coursier installer <https://github.com/coursier/launchers/raw/master/cs-x86_64-pc-win32.zip>`_,
+when asked agree to an update of your ``PATH`` variable. Reboot to force an update of ``PATH``.
 
-To set up an internet-free environment, you can:
+This is sufficient for generating hardware. For simulation continue with either choice below.
+In case you want to build the tools yourself have a look at the legacy simulation tool :ref:`installation instructions <sim backend install>`.
 
-#. Set up an environment with internet
-#. Launch a Spinal command (see :ref:`Using SBT`) to fetch dependencies (for
-   instance using the `getting started
-   <https://github.com/SpinalHDL/SpinalTemplateSbt>`_ repository)
-#. Copy the caches to the internet-free environment.
+MSYS2 verilator for simulation
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-.. note::
-   You can get a portable SBT setup here: https://www.scala-sbt.org/download.html
+We recommend to install compiler/verilator through `MSYS2 <https://www.msys2.org>`.
+Other methods of installing gcc/make/shell (e.g. chocolatey, scoop, etc.) may also work but are untested.
 
-.. note::
-   You might be interested in `SpinalNomad <https://github.com/SpinalHDL/SpinalNomad/tree/main/sbt>`_.
+SpinalHDL maintainer `Readon <https://github.com/Readon>` is maintaining a MSYS2 fork that default
+installs all needed officially available and custom built packages (also maintained by Readon `here <https://github.com/Readon/MINGW-SpinalHDL>`) 
+for simulation and formal verification. It can be found `here <https://github.com/Readon/msys2-installer>`.
+If used then the packages installed below via ``pacman`` are already installed and those
+installation steps can be skipped.
 
+Currently verilator 4.228 is latest available version known to work.
 
-.. _recommended:
+Download the latest installer and install MSYS2 with default settings. You should get a MSYS2 terminal at
+the end of the installation, there run:
 
-Recommended requirements
-------------------------
+.. code-block:: sh
 
-To enable more features:
+   pacman -Syuu
+   # will (request) close down terminal
+   # open 'MSYS2 MINGW64' from start menu
+   pacman -Syuu
+   pacman -S --needed base-devel mingw-w64-x86_64-toolchain mingw-w64-x86_64-iverilog mingw-w64-x86_64-ghdl-llvm git 
+   curl -O https://repo.msys2.org/mingw/mingw64/mingw-w64-x86_64-verilator-4.228-1-any.pkg.tar.zst
+   pacman -U mingw-w64-x86_64-verilator-4.228-1-any.pkg.tar.zst   
 
-* An IDE (for instance `IntelliJ <https://www.jetbrains.com/idea/>`_ with its
-  Scala plugin or `VSCodium <https://vscodium.com/>`_ with Metals extension) to
-  get features such as:
+In a MSYS2 MINGW64 terminal we need to set some environment variables to make Java/sbt available (you can make these
+settings persistent by adding them to ``~/.bashrc`` in MSYS2):
 
-    * Code suggestions / completion
-    * Automatic build with syntax errors right in the code
-    * Generate code with a single click
-    * Run simulation / tests with a single click (if a supported simulator is
-      set up)
+.. code-block:: sh
 
-* A supported simulator like `Verilator <https://www.veripool.org/verilator/>`_
-  to test the design right from SpinalHDL.
-* `Gtkwave <https://gtkwave.sourceforge.net/>`_ to view the waves generated by
-  Verilator during simulation.
-* `Git <https://git-scm.com/>`_ for version control system
+   export VERILATOR_ROOT=/mingw64/share/verilator/
+   export PATH=/c/Program\ Files/Eclipse\ Adoptium/jdk-17.0.8.101-hotspot/bin:$PATH
+   export PATH=/c/Users/User/AppData/Local/Coursier/data/bin:$PATH
+
+With this you should be able to run sbt/verilator simulations from MSYS2 terminals (sbt via calling ``sbt.bat``).
+
+MSYS2 for formal verification
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+In addition to the steps above we also need to install yosys, sby, z3 and yices. Both yosys and sby are
+not available as official MSYS2 packages, but packages are provided by `Readon <https://github.com/Readon>`.
+If you used their installer then these steps are not needed (you should check if there are newer packages available).
+
+.. code-block:: sh
+
+   pacman -S mingw-w64-x86_64-z3 mingw-w64-x86_64-yices mingw-w64-x86_64-autotools mingw-w64-x86_64-python3-pip
+   python3 -m pip install click
+   curl -OL https://github.com/Readon/MINGW-SpinalHDL/releases/download/v0.4.9/mingw-w64-x86_64-yosys-0.31-1-any.pkg.tar.zst
+   curl -OL https://github.com/Readon/MINGW-SpinalHDL/releases/download/v0.4.9/mingw-w64-x86_64-python-sby-0.31-1-any.pkg.tar.zst
+   pacman -U *-yosys-*.pkg.tar.*
+   pacman -U *-python-sby-*.pkg.tar*
+
+OCI Container
+-------------
 
+A container for SpinalHDL development is available as well.
+The container is hosted at ``ghcr.io/spinalhdl/docker:master`` and can be used with Docker/Podman/Github Codespaces.
+It is used for the SpinalHDL CI regression and can therefore be an easy way to run the CI commands locally.
+
+To run the container run e.g. ``podman run -v .:/workspace -it ghcr.io/spinalhdl/docker:master`` in a SpinalHDL project
+root directory, making the project directory available in ``/workspace``.
+
+Please consult the documentation of you Distribution (Linux, WSL) or Docker (Windows) on how to install the container
+runtime you want to use. Multiple editors/IDEs (e.g. VSCode, IntelliJ, Neovide) allow for remote development in a container.
+Please consult the documentation of the editor on how to do remote development.
+
+Installing SBT in an internet-free Linux environment
+----------------------------------------------------
+
+.. note::
+   If you are not using an air-gapped environment we recommend to
+   go with the normal linux installation. (which is a subset of the
+   installation for an air-gapped environment)
+
+Normally, SBT uses online repositories to download and cache your projects
+dependencies. This cache is located in several folders:
+
+* ``~/.sbt``
+* ``~/.cache/JNA``
+* ``~/.cache/coursier``
+
+To set up an internet-free environment, you can:
+
+#. Set up an environment with internet (see above)
+#. Launch a Spinal command (see :ref:`Using SBT`) to fetch dependencies (for
+   instance using the `getting started
+   <https://github.com/SpinalHDL/SpinalTemplateSbt>`_ repository)
+#. Copy the caches to the internet-free environment.
 
 .. _template:
 
-Create a SpinalHDL project
---------------------------
+Create a first SpinalHDL project
+================================
 
 We have prepared a ready-to-go project for you the: `getting started <https://github.com/SpinalHDL/SpinalTemplateSbt>`_ repository.
 

source/SpinalHDL/Simulation/index.rst

@@ -2,7 +2,11 @@
 Simulation
 ==========
 
-As always, you can use your standard simulation tools to simulate the VHDL/Verilog generated by SpinalHDL. However, since SpinalHDL 1.0.0, the language integrates an API to write testbenches and test your hardware directly in Scala. This API provides the capabilities to read and write the DUT signals, fork and join simulation processes, sleep and wait until a given condition is reached. Therefore, using SpinalHDL's simulation API, it is easy to integrate testbenches with the most common Scala unit-test frameworks.
+As always, you can use your standard simulation tools to simulate the VHDL/Verilog generated by SpinalHDL.
+However, since SpinalHDL 1.0.0, the language integrates an API to write testbenches and test your hardware
+directly in Scala. This API provides the capabilities to read and write the DUT signals, fork and join
+simulation processes, sleep and wait until a given condition is reached. Therefore, using SpinalHDL's
+simulation API, it is easy to integrate testbenches with the most common Scala unit-test frameworks.
 
 To be able to simulate user-defined components, SpinalHDL uses external HDL simulators as backend. Currently, four simulators are supported:
 
@@ -12,7 +16,7 @@ To be able to simulate user-defined components, SpinalHDL uses external HDL simu
 - `VCS <https://www.synopsys.com/verification/simulation/vcs.html>`_ **(experimental, since SpinalHDL 1.7.0)**
 - `XSim <https://www.google.com/search?q=site%3Axilinx.com+xsim>`_ **(experimental, since SpinalHDL 1.7.0)**
 
-With external HDL simulators it is possible to directly test the generated HDL sources without increasing the SpinalHDL codebase complexity. 
+With external HDL simulators it is possible to directly test the generated HDL sources without increasing the SpinalHDL codebase complexity.
 
 .. toctree::
    :hidden:

source/SpinalHDL/Simulation/install/GHDL.rst

@@ -2,6 +2,10 @@
 Setup and installation of GHDL
 ==============================
 
+.. note::
+   If you installed the recommended oss-cad-suite during SpinalHDL :ref:`setup <Install>` you
+   can skip the instructions below - but you need to activate the oss-cad-suite environment.
+
 Even though GHDL is generally available in linux distributions package system, SpinalHDL depends on bugfixes of GHDL codebase that were added after the release of GHDL v0.37. Therefore it is reccomended to install GHDL from source.
 The C++ library boost-interprocess, which is contained in the libboost-dev package in debian-like distributions, has to be installed too. boost-interprocess is required to generate the shared memory communication interface. 
 

source/SpinalHDL/Simulation/install/Icarus Verilog.rst

@@ -2,6 +2,10 @@
 Setup and installation of Icarus Verilog
 ========================================
 
+.. note::
+   If you installed the recommended oss-cad-suite during SpinalHDL :ref:`setup <Install>` you
+   can skip the instructions below - but you need to activate the oss-cad-suite environment.
+
 In most recent linux distributions, a recent version of Icarus Verilog is generally available through the package system.
 The C++ library boost-interprocess, which is contained in the libboost-dev package in debian-like distributions, has to be installed too. boost-interprocess is required to generate the shared memory communication interface. 
 

source/SpinalHDL/Simulation/install/Verilator.rst

@@ -2,6 +2,9 @@
 Setup and installation of Verilator
 ===================================
 
+.. note::
+   If you installed the recommended oss-cad-suite during SpinalHDL :ref:`setup <Install>` you
+   can skip the instructions below - but you need to activate the oss-cad-suite environment.
 
 SpinalSim + Verilator is supported on both Linux and Windows platforms.
 
@@ -57,7 +60,7 @@ In order to get SpinalSim + Verilator working on Windows, you have to do the fol
 * Install `MSYS2 <https://www.msys2.org/>`_
 * Via MSYS2 get gcc/g++/verilator (for Verilator you can compile it from the sources)
 * Add ``bin`` and ``usr\bin`` of MSYS2 into your windows ``PATH`` (ie : ``C:\msys64\usr\bin;C:\msys64\mingw64\bin``)
-* Check that the JAVA_HOME environnement variable point to the JDK installation folder (ie : ``C:\Program Files\Java\jdk-13.0.2``)
+* Check that the JAVA_HOME environment variable points to the JDK installation folder (i.e.: ``C:\Program Files\Java\jdk-13.0.2``)
 
 Then you should be able to run SpinalSim + Verilator from your Scala project without having to use MSYS2 anymore.
 

source/SpinalHDL/Simulation/install/index.rst

@@ -1,8 +1,5 @@
-Installation instructions
-=========================
-
-Scala
-^^^^^
+SBT setup for simulation
+========================
 
 To enable SpinalSim, the following lines have to be added in your build.sbt file :
 
@@ -17,6 +14,8 @@ Also the following imports have to be added in testbenches sources :
    import spinal.core._
    import spinal.core.sim._
 
+.. _sim backend install:
+
 Backend-dependent installation instructions
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^