[documentation] Cookbook : a project of library written with amaranth hdl

[sporniket]

I thought this would be usefull.

Abstract

You have written some hardware design using amaranth-hdl, that you wish to promote into a library in order to reuse it in another project ?
You also have written some tests that use SymbiYosys(sby) to validate this library in part or in full ?

This cookbook will describe the minimal settings to run those test in a github action in order to validate a commit. Before that, as a reminder or quick start, it will also describe what to install locally and a way to write tests. It is based on this commit from a project of mine to gather some reusable stuff for my own projects.

Target audience

This cookbook will be easier to understand provided :

• The reader already has set up github actions preferably for a python project.
• The reader already has set up a python package to publish to the Python Package Index

However, the reference project is small enough to be studied at a leisurely pace and be used as an informative template

Overview

This cookbook will describe the following item, in that order

• Local setup : what you need to install to be able to use sby ; I am working on Ubuntu 20 LTS
• Python package definition : how to fill you package descriptor ; I will use setuptools and follows PEP 621
• Github actions : how to run the test on the github repository to validate commits and pull request.

Local Setup

The key point is to install SymbiYosys from source, meaning following the installation manual.

I installed the required parts ("Yosys, Yosys-SMTBMC and ABC", and "sby") and the recommanded part ("boolector").

Python package definition

See the reference file in full.

The key point is the list of dependencies. In order to use up to dates versions of amaranth, I instruct the setup tools to use a recent commit on the main branch. The targeted commit hashes will have to be updated with time.

dependencies = [
    "amaranth @ git+https://github.com/amaranth-lang/amaranth@3a51b612844a23b08e744c4b3372ecb44bf9fe5d",
    "amaranth-boards @ git+https://github.com/amaranth-lang/amaranth-boards@2d0a23b75ebb769874719297dec65ff07ca9e79f",
    'importlib-metadata; python_version>"3.8"',
]

Implementing tests that call sby

See the reference file in full

First thing first, I instructed git to ignore any file named tmp or like tmp.*. Then, my tests generate RTLIL files and their companion SBY files with names starting with tmp. This is to make sure that those artefacts will not end up in the repository.

This part will show :

• The instanciation of a simple test bench
• The generation of the RTLIL from the test bench
• The generation of the SBY configuration file for the test bench
• The invocation of sby

Instanciate a simple test bench

1. Embed an instance of you Elaboratable module as a submodule of your test bench. For my project, I wrote a little helper to avoid repeating myself

class Test:
    @staticmethod
    def _buildTestBench(dut: Elaboratable, test) -> Module:
        """
        dut : 'Device Under Test'
        test : a function that will add assertions to the test bench
        """
        m = Module()
        cd = Test._clockDomain("sync")
        m.domains.sync = cd
        m.submodules.dut = dut
        test(m, cd)
        return m

2. Add assertions to your test bench ; For my project, I devised for a function provided with the test bench and the clock domain, in order to add those assertions ; then, this function is given to the helper presented at step 1

def shouldAssertTheCorrectBitWhenInputIsInRange(m: Module, cd: ClockDomain):
    rst = cd.rst
    demux = m.submodules.dut
    channelCount = demux.channelCount
    for i in range(0, channelCount):
        with m.If(~Past(rst) & (Past(demux.input) == i)):
            m.d.sync += [
                Assert(demux.output == (1 << i)),
                Assert(~(demux.outOfRange)),
            ]

Generate the RTLIL file

Given a base name, I will instruct amaranth.back.rtill to generate the specified RTLIL file with :

        ilName = f"tmp.{baseName}.il"

        m = Test._buildTestBench(dut, test)
        fragment = Fragment.get(m, platform)
        output = rtlil.convert(
            fragment,
            ports=dut.ports(),
        )
        print(f"Generating {ilName}...")
        with open(ilName, "wt") as f:
            f.write(output)

Generate the SBY configuration file

Each test will require a SBY configuration file in order to target the generated RTLIL. For my project, I wrote a little helper that generate the file from the target RTLIL file and the required depth ; then I use this helper

class Test:
    @staticmethod
    def _generateSbyConfig(sbyName: str, ilName: str, depth: int):
        print(f"Generating {sbyName}...")
        with open(sbyName, "wt") as f:
            f.write(
                "\n".join(
                    [
                        "[tasks]",
                        "bmc",
                        "cover",
                        "",
                        "[options]",
                        "bmc: mode bmc",
                        "cover: mode cover",
                        f"depth {depth}",
                        "multiclock off",
                        "",
                        "[engines]",
                        "smtbmc boolector",
                        "",
                        "[script]",
                        f"read_ilang {ilName}",
                        "prep -top top",
                        "",
                        "[files]",
                        f"{ilName}",
                    ]
                )
            )

        ilName = f"tmp.{baseName}.il"
        sbyName = f"tmp.{baseName}.sby"

        Test._generateSbyConfig(sbyName, ilName, depth)

Invoke sby

For now I rely on amaranth._toolchain.require_tool to mimic what is done for the amaranth project, it will be necessary for the github action.

In a subprocess, we launch a simple invocation like sby -f <the-sby-configuration-file>, and we check the return code for detecting failure.

        invoke_args = [require_tool("sby"), "-f", sbyName]
        print(f"Running sby -f {' '.join(invoke_args)}...")
        with subprocess.Popen(invoke_args) as proc:
            if proc.returncode is not None and proc.returncode != 0:
                exit(proc.returncode)

Testing locally

I wrote a little script to automate this part, because I includes reformating the sources, packaging and re-installing locally the project, and then launching the tests and compute coverages

# rebuild, install and test
python3 -m build && python3 -m pip install --force-reinstall dist/*.whl && \
python3 -m coverage run --source=amaranth_stuff --branch -m pytest && \
python3 -m coverage report -m && \
python3 -m coverage html 

Github actions

See the reference file in full

The key points when setting up the github actions are :

• the list of dependencies to install, including amaranth-yosys
• the export of some environment variables before running the test in order to use the sby from amaranth_yosys. That is where using the aforementioned amaranth._toolchain.require_tool is coming in handy.

Installation of dependencies

    - name: Install dependencies
      run: |
        sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys FA8E1301F4D3932C
        sudo add-apt-repository 'deb http://ppa.launchpad.net/sri-csl/formal-methods/ubuntu bionic main'
        sudo apt-get update
        sudo apt-get install yices2
        python -m pip install --upgrade pip
        python -m pip install flake8 pytest 
        pip install 'yowasp-yosys==0.20.dev398' # latest version that works on Python 3.7
        pip install 'amaranth @ git+https://github.com/amaranth-lang/amaranth@3a51b612844a23b08e744c4b3372ecb44bf9fe5d'
        pip install 'amaranth-boards @ git+https://github.com/amaranth-lang/amaranth-boards@2d0a23b75ebb769874719297dec65ff07ca9e79f'
        pip install 'amaranth-yosys @ git+https://github.com/amaranth-lang/amaranth-yosys@85067f31288493989d6403527309888e839a65a3'

Running the tests

    - name: Test with pytest
      run: |
        export AMARANTH_USE_YOSYS=builtin YOSYS=yowasp-yosys SBY=yowasp-sby SMTBMC=yowasp-yosys-smtbmc
        PYTHONPATH="$(pwd)/src" pytest

[sporniket]

Erratum : build the test bench, generate the rtlil, and invoke sby

With the described procedure, I could not have failing assertion (most likely, they was never reached because of the evaluation on rst in the m.If ). And the invocation won't exit because proc.returncode will stay at None

⇒ The clock domain's clk and rst signal MUST be part of the ports given to rtlil.convert(...)

⇒ As we don't need to do something fancy during the invocation of sby, just use subprocess.run(...).check_returncode() to raise a CalledProcessError when a verification fails

See the fix commit

Below are fixed parts :

• Instanciate a simple test bench (item 1)
• Generate the RTLIL file
• Invoke sby

---

Instanciate a simple test bench

1. Embed an instance of your Elaboratable module as a submodule of your test bench. A clock domain MUST have been instanciated to be able to get the reset signal for the test.
   For my project, I wrote a little helper to avoid repeating myself, with dut being the elaboratable module to test (Device Under Test), cd being the clock domain, and test being a function that will setup the assertions, see below

class Test:
    @staticmethod
    def _buildTestBench(dut: Elaboratable, test, cd: ClockDomain) -> Module:
        """
        dut : 'Device Under Test'
        test : a function that will add assertions to the test bench
        """
        m = Module()
        m.domains.sync = cd
        m.submodules.dut = dut
        test(m, cd)
        return m

---

Generate the RTLIL file

Given a base name, I will instruct amaranth.back.rtill to generate the specified RTLIL file with :

        ilName = f"tmp.{baseName}.il"

        sync = ClockDomain("sync")
        rst = Signal()
        sync.rst = rst

        m = Test._buildTestBench(dut, test, sync)
        fragment = Fragment.get(m, platform)
        output = rtlil.convert(
            fragment,
            ports=dut.ports() + [sync.rst, sync.clk],
        )
        print(f"Generating {ilName}...")
        with open(ilName, "wt") as f:
            f.write(output)

---

Invoke sby

For now I rely on amaranth._toolchain.require_tool to mimic what is done for the amaranth project, it will be necessary for the github action.

In a subprocess, we launch a simple invocation like sby -f <the-sby-configuration-file>, and we check the return code for detecting failure.

        invoke_args = [require_tool("sby"), "-f", sbyName]
        print(f"Running sby -f {' '.join(invoke_args)}...")
        subprocess.run(invoke_args).check_returncode()

---

That's all (until next time)

[sporniket]

Erratum : Generate the SBY configuration file

For the CI to work, do not use boolector, only smtbmc. I also simplified the file to looks like more the one used by the FHDLTestCase

Here is the fixed part :

---

Generate the SBY configuration file

Each test will require a SBY configuration file in order to target the generated RTLIL. For my project, I wrote a little helper that generate the file from the target RTLIL file and the required depth ; then I use this helper

class Test:
    @staticmethod
    def _generateSbyConfig(sbyName: str, ilName: str, depth: int):
        print(f"Generating {sbyName}...")
        with open(sbyName, "wt") as f:
            f.write(
                "\n".join(
                    [
                        "[options]",
                        "mode bmc",
                        f"depth {depth}",
                        "",
                        "[engines]",
                        "smtbmc",
                        "",
                        "[script]",
                        f"read_ilang {ilName}",
                        "prep -top top",
                        "",
                        "[files]",
                        f"{ilName}",
                    ]
                )
            )

---