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

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

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 / ideas

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