Updated to use Amaranth HDL

Author: RobertBaruch

00_intro.md

@@ -1,10 +1,10 @@
 # What's this?
 
-This is a series of graded exercises in using nMigen, the Python-based Hardware Design Language, to design and verify digital circuits!
+This is a series of graded exercises in using [Amaranth HDL](https://amaranth-lang.org/docs/amaranth/latest/intro.html), the Python-based Hardware Design Language, to design and verify digital circuits!
 
 It's also a work in progress.
 
-Please note, the goal is not to be pedantically correct in every explanation. As you progress through the exercises, you'll learn for yourself the breadth of nMigen and what you can do with it!
+Please note, the goal is not to be pedantically correct in every explanation. As you progress through the exercises, you'll learn for yourself the breadth of Amaranth and what you can do with it!
 
 ## Prerequisite knowledge
 
@@ -16,66 +16,26 @@ You will need knowledge of:
 
 ## Software prerequisites
 
-If you're using Windows, I hope you're using Windows Subsystem for Linux. If not, you're on your own.
+YosysHQ has put together a [comprehensive installer](https://github.com/YosysHQ/oss-cad-suite-build#installation) containing everything you need, and then some. Simply follow the instructions.
 
-### Option 1: Docker (recommended)
+### Tip for Windows users
 
-Victor Muñoz has put together a [docker container](https://github.com/vmunoz82/eda_tools) that has everything you need: Python 3, nMigen, yosys, SymbiYosys, and the Z3, boolector, and yices solvers.
+If you just downloaded the exe file, it will be in your Downloads folder. Run the executable, and it extracts everything to Downloads/oss-cad-suite. You can simply move the oss-cad-suite directory to somewhere more convient.
 
-You'll need to get [Docker Desktop](https://www.docker.com/get-started). If you're on Windows, follow the instructions for [Docker/WSL](https://docs.docker.com/docker-for-windows/wsl/) instead.
+*Do not use PowerShell*. Use Command Prompt instead. Always be sure to run `<your-directory>\oss-cad-suite\environment.bat` in Command Prompt before doing any work. You'll know if the environment was set properly if you see `[OSS CAD Suite]` before your prompt:
 
-Also, if you're on Windows, you will want to download and run an [X server](https://medium.com/@japheth.yates/the-complete-wsl2-gui-setup-2582828f4577) so that you can use gtkwave from the command line on WSL.
+```txt
+F:\amaranth-exercises>..\oss-cad-suite\environment.bat
 
-Once you've done that, you can open up WSL (if you're on Windows) and then run [`eda_tools.sh`](https://raw.githubusercontent.com/vmunoz82/eda_tools/main/eda_tools.sh). This will conveniently start up the docker container with all the right options. 
-
-You may want to replace `-v $HOME:/$HOME` in `eda_tools.sh` with `-v /your/host/working/directory:/some/nice/directory/on/docker`, and then you can access your files in `/some/nice/directory/on/docker` in the docker container. For example, I do my work in WSL in `/mnt/f` so I simply use `-v /mnt/f:/mnt/f`.
-
-Remember that the docker container will not save local files (e.g. files in `/workspace`), so make sure you have your working directory mapped!
-
-### Option 2: Build it all yourself
-
-You will need:
-
-* Python 3.6 or above: See below for Python 3.6 on WSL.
-
-* Install yosys, Symbiyosys, yices2, and z3.
-  * `sudo apt install curl`
-  * Now follow the [instructions to install these](https://symbiyosys.readthedocs.io/en/latest/install.html). It is highly recommended to follow those instructions, especially for yosys since the git repo has many more fixes than the official release.
-  * Note that when you see `-j$(nproc)`, it means to specify the number of processors your CPU has. You can't really go wrong by using `-j4`. You can go higher if you know you have more.
-  * z3 takes a long time to compile. Go watch a YouTube video in the meantime.
-
-* Install nMigen
-  * `pip3 install wheel`
-  * `pip3 install git+https://github.com/nmigen/nmigen`
-
-* Signal viewer for simulation and formal verification
-  * [gtkwave](https://sourceforge.net/projects/gtkwave/)
-    * For WSL, get the Windows version unless you want to run an [X server](https://medium.com/@japheth.yates/the-complete-wsl2-gui-setup-2582828f4577).
-    * The package for gtkwave for Windows gives you no clue how to install for Windows. Unzip the zip file into, say, C:, and then add C:\gtkwave\bin to your Windows path.
-
-## Python and WSL
-
-Python 2 and Python 3 are not compatible. This is why this happens:
-
-* `python`, `pip` -> Python 2
-* `python3`, `pip3` -> Python 3
-
-On my freshly-installed WSL, the only version present is Python 3.8. If it is not on your version, you may want to upgrade to 3.8. Upgrading is beyond the scope of this document.
-
-Now install some bare minimum tools:
-
-```sh
-sudo apt install python3-pip build-essential libssl-dev libffi-dev
+[OSS CAD Suite] F:\amaranth-exercises>
 ```
 
-In installing the yosys prerequisites, Python 2 will be installed. So be aware that when you want to run anything under Python 3, you must use `python3` (or `pip3` for installing), not `python` (or `pip`).
-
-# Tip for vscode users:
+## Tip for vscode users
 
 Open File > Preferences > Settings, look for pylint args, and add:
 
-```
---contextmanager-decorators=contextlib.contextmanager,nmigen.hdl.dsl._guardedcontextmanager
+```txt
+--contextmanager-decorators=contextlib.contextmanager,amaranth.hdl.dsl._guardedcontextmanager
 ```
 
-This is because pylint doesn't recognize that `nmigen.hdl.dsl._guardedcontextmanager` is a valid context manager. Otherwise pylint will complain for every `with m.If` statement.
+This is because pylint doesn't recognize that `amaranth.hdl.dsl._guardedcontextmanager` is a valid context manager. Otherwise pylint will complain for every `with m.If` statement.

01_input.md

@@ -1,11 +1,12 @@
 # Exercise 1: Counting coin
 
 <p align="right">
-Khajiit has knowledge... if you have coin.
+<i>Khajiit has knowledge... if you have coin.</i>
 </p>
 
 ---
-## What you'll do:
+
+## What you'll do
 
 Create a module that takes as inputs:
 
@@ -29,25 +30,25 @@ Use formal verification to:
 
 ## Step 1: Create a module
 
-An nMigen *module* is a Python class that has inputs and outputs, and code that generates the logic for the desired functionality. Note that I didn't say code that *implements* the function. A key concept is that nMigen is a Python library for writing logic. When the module is *elaborated*, your code runs and nMigen outputs the corresponding logic.
+An Amaranth *module* is a Python class that has inputs and outputs, and code that generates the logic for the desired functionality. Note that I didn't say code that *implements* the function. A key concept is that Amaranth is a Python library for writing logic. When the module is *elaborated*, your code runs and Amaranth outputs the corresponding logic.
 
-You can think of the logic that nMigen writes as an integrated circuit, and the code that you write as the instructions for how to create a copy of that integrated circuit.
+You can think of the logic that Amaranth writes as an integrated circuit, and the code that you write as the instructions for how to create a copy of that integrated circuit.
 
-Modules can use other modules (*submodules*), and you can have as many copies of the module as you want. Your design has one top-level module that contains all of your other modules. When you elaborate the top-level module, nMigen outputs its logic into a file. That file can then be given to other software for synthesis on an FPGA, or for formal verification (i.e. bug hunting).
+Modules can use other modules (*submodules*), and you can have as many copies of the module as you want. Your design has one top-level module that contains all of your other modules. When you elaborate the top-level module, Amaranth outputs its logic into a file. That file can then be given to other software for synthesis on an FPGA, or for formal verification (i.e. bug hunting).
 
-![Toolchain flow](diagrams/nmigen_blocks.png)
+![Toolchain flow](diagrams/amaranth_blocks.png)
 
 You can use the [`skeleton.py`](skeleton.py) file to start. Some key features here are:
 
 * Your class is derived from `Elaboratable`
 * Your public (or visible) inputs and outputs are attributes of the class.
-* The class has an `elaborate` function that gets called by nMigen to generate the logic.
+* The class has an `elaborate` function that gets called by Amaranth to generate the logic.
 * The class has a class-level `formal` method for verifying your logic.
 * You can run your class to generate the output. This requires the `main` function in [`util.py`](util.py).
 
 ## Step 2: Create input and output signals
 
-A `Signal` in nMigen is a wire or register with some number of bits. For example:
+A `Signal` in Amaranth is a wire or register with some number of bits. For example:
 
 ```python
 x = Signal(5)      # creates a 5-bit signal named "x".
@@ -64,7 +65,7 @@ For this exercise, the logic is completely *combinatorial*: the outputs depend d
 m.d.comb += y.eq(x)
 ```
 
-This is just like writing `y = x`, except using the nMigen library, which requires using the `eq` function. That function returns a statement which can then be added to one of the domains in the module. Here, `m.d.comb` is the module's combinatorial domain.
+This is just like writing `y = x`, except using the Amaranth library, which requires using the `eq` function. That function returns a statement which can then be added to one of the domains in the module. Here, `m.d.comb` is the module's combinatorial domain.
 
 You can use constants, and arithmetic functions, too:
 
@@ -95,7 +96,7 @@ if x == 7:
     y = z
 ```
 
-The equivalent in nMigen is:
+The equivalent in Amaranth is:
 
 ```python
 m.d.comb += y.eq(0)
@@ -116,12 +117,12 @@ This does the same thing.
 
 ![An if-else-statement](diagrams/if.png)
 
-## Step 4: Make sure it compiles!
+## Step 4: Make sure it compiles
 
 You can quickly check that there aren't any syntax errors by just generating the code:
 
-```
-python3 your_file.py gen
+```sh
+python your_file.py gen
 ```
 
 ## Step 5: Write some formal verification code
@@ -180,22 +181,22 @@ If the engine cannot satisfy a cover, it will complain. This usually means that
 
 Write the asserts and covers according to the requirements of the exercise. Compile again to make sure you haven't introduced any syntax errors.
 
-```
-python3 your_file.py gen
+```sh
+python your_file.py gen
 ```
 
 ## Step 6: Run the formal verification engine for covers
 
 Running your code with `gen` will have it output a file `toplevel.il`. This can be run through the SymbiYosys formal verification tool. It requires a `.sby` configuration file, which I've included in `answers/e01_to_pennies.sby`.
 
-```
-python3 your_class.py gen
+```sh
+python your_class.py gen
 sby -f answers/e01_to_pennies.sby cover
 ```
 
 First, look for the cover conditions to be satisfied. These are the `Reached cover statement at...` lines below. And, if all your cover statements were satisfied, you'll get a `DONE (PASS, rc=0)` line.
 
-```
+```txt
 SBY 15:17:27 [answers/e01_to_pennies_cover] Removing directory 'answers/e01_to_pennies_cover'.
 SBY 15:17:27 [answers/e01_to_pennies_cover] Copy 'toplevel.il' to 'answers/e01_to_pennies_cover/src/toplevel.il'.
 SBY 15:17:27 [answers/e01_to_pennies_cover] engine_0: smtbmc z3
@@ -236,17 +237,22 @@ The cover statements aren't found in the order you put them in your code!
 
 Each cover statement found generates a trace where you can see the inputs and outputs, as well as some intermediate signals if they are there, using `gtkwave`:
 
-```
+```sh
 gtkwave -f answers/e01_to_pennies_cover/engine_0/trace0.vcd
 ```
 
-In this case, the first trace came from the first cover statement in the exercise. The output shows `1DD`, or 477.
+In this case, the first trace came from the first cover statement in the exercise. The output shows `1DD`, or 477. You can tell which cover statement the trace corresponds to by looking at the output from `sby`:
+
+```txt
+SBY 15:17:27 [answers/e01_to_pennies_cover] engine_0: ##   0:00:00  Reached cover statement at answers/to_pennies.py:45 in step 0.
+SBY 15:17:27 [answers/e01_to_pennies_cover] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace0.vcd
+```
 
 ![gtkwave output](diagrams/ex1_tr0.JPG)
 
 ## Step 7: Run the formal verification engine for bounded model checking
 
-```
+```sh
 sby -f answers/e01_to_pennies.sby bmc
 ```
 

02_switch.md

@@ -1,11 +1,12 @@
 # Exercise 2: The day after
 
 <p align="right">
-The 14th of January is World Logic Day.
+<i>The 14th of January is World Logic Day.</i>
 </p>
 
 ----
-## What you'll do:
+
+## What you'll do
 
 Create a module that takes as inputs a date, consisting of:
 
@@ -108,7 +109,7 @@ As before, you will need to:
 * Define your inputs and outputs.
 * Write the logic for the module in `elaborate`.
 * Write your asserts in `formal`.
-* Make sure it compiles with `python3 your_file.py gen`.
+* Make sure it compiles with `python your_file.py gen`.
 * Run formal verification in cover mode using `sby -f answers/e02_next_day.sby cover`.
 * Run formal verification in BMC mode using `sby -f answers/e02_next_day.sby bmc`.
 

03_parts.md

@@ -1,6 +1,6 @@
 # Exercise 3: Life finds a way
 
-## What you'll do, part 1:
+## What you'll do, part 1
 
 Create a module that determines the state of a cell in the Game of Life. It takes as input:
 

04_signs.md

@@ -4,8 +4,8 @@
 
 Write a module that takes a 64-bit signed number, and negates it in three ways:
 
-* Invert and add 1.
-* Directly negate it.
+* Bitwise complement (invert) it and add 1.
+* Arithmetically negate it.
 * Starting from the least significant bit, copy up to and including the first 1, then invert the remaining bits.
 
 That last one seems a bit strange, but it works like this (using 8-bit numbers):
@@ -29,8 +29,8 @@ However, in 2's complement, `1000` is -8 while `0111` is 7, which means that if
 x = Signal(signed(4))
 y = Signal(signed(4))
 m.d.comb += [
-    x.eq(0b1000),
-    y.eq(0b0111),
+    x.eq(0b1000),  # -8
+    y.eq(0b0111),  # +7
     Assert(x < y),
 ]
 ```
@@ -41,8 +41,8 @@ To treat an unsigned (or signed) signal as signed:
 x = Signal(4)
 y = Signal(4)
 m.d.comb += [
-    x.eq(0b1000),
-    y.eq(0b0111),
+    x.eq(0b1000),  # 8 (or -8 if signed)
+    y.eq(0b0111),  # 7
     Assert(x.as_signed() < y.as_signed()),
 ]
 ```
@@ -55,10 +55,10 @@ Negating a signal always results in a signed signal, regardless of whether the i
 x = Signal(4)
 y = Signal(4)
 m.d.comb += [
-    x.eq(0b0011),
-    y.eq(0b1101),
+    x.eq(0b0011),  # 3
+    y.eq(0b1101),  # 13
     Assert(y > x),
-    Assert(-x < x),
+    Assert(-x < x),  # -x is signed, so this is a signed comparison
 ]
 ```
 
@@ -68,8 +68,8 @@ Equality, on the other hand, does not take into account signedness. It is bit-fo
 x = Signal(4)
 y = Signal(4)
 m.d.comb += [
-    x.eq(0b0011),
-    y.eq(0b1101),
+    x.eq(0b0011),  # 3
+    y.eq(0b1101),  # 13 (or -3 if signed)
     Assert(y > x),
     Assert(-x == y),
 ]
@@ -90,10 +90,12 @@ m.d.comb += [
 
 ### Library: priority encoder
 
-A *priority encoder* is a circuit that takes an N-bit input and outputs the position of the first set bit, where "first" could mean most significant or least significant. nMigen has a coding library with a PriorityEncoder module built in, which outputs the position of the first least significant bit set.
+A *priority encoder* is a circuit that takes an N-bit input and outputs the position of the first set bit, where "first" could mean first *most* significant or first *least* significant. Amaranth has a coding library with a `PriorityEncoder` module built in, which outputs the position of the first *least* significant bit set.
+
+The encoder has three ports (attributes): `i`, the input, `o`, the output, which is the lowest bit number that is set in the input, and `n`, set if and only if the input is zero. The encoder also has a parameter, `width`, which tells it how many bits are in the input.
 
 ```python
-from nmigen.lib.coding import PriorityEncoder
+from amaranth.lib.coding import PriorityEncoder
 
 enc = PriorityEncoder(width=8)
 input = Signal(8)
@@ -107,7 +109,7 @@ m.d.comb += [
 ]
 ```
 
-For example, the input `0101000` will result in the output being 3 and bit_set being high.
+For example, setting `input` to `0101000` will result in `output` being 3 and `bit_set` being high.
 
 ### Limitations on slices
 
@@ -123,13 +125,11 @@ You can achieve the same effect using bit tricks. For example, `1 << y` gives yo
 
 What does `(-1 << y) & x` give you?
 
------
-
-Interested in more bit-manipulation tricks? Check out Knuth's The Art of Computer Programming, Volume 4A, chapter 7.1.3 (Bitwise Tricks and Techniques). Hacker's Delight also contains copious bit manipulation fun.
+> Interested in more bit-manipulation tricks? Check out Knuth's [The Art of Computer Programming](https://en.wikipedia.org/wiki/The_Art_of_Computer_Programming), Volume 4A, chapter 7.1.3 (Bitwise Tricks and Techniques). [Hacker's Delight](https://en.wikipedia.org/wiki/Hacker%27s_Delight) also contains copious bit manipulation fun.
 
 -----
 
-## What you'll do, part 2:
+## What you'll do, part 2
 
 Suppose you have a chip that can compare two 16-bit numbers, but only as unsigned numbers. It outputs whether the first is less than the second. Write such a module.