Skip to main content

AVL - Apheleia Verification Library

License: MIT Python

AVL has been developed by experienced, industry professional verification engineers to provide a methodology
and library of base classes for developing functional verification environments in Python.

AVL is built on the CocoTB framework, but aims to combine the best elements of
UVM in a more engineer friendly and efficient way.

CocoTB 2.0

AVL now supports CocoTB2.0 https://docs.cocotb.org/en/development/upgrade-2.0.html. This was introduced in v0.3.0.

All older versions support v1.9.1 and will fail if run with CocoTB 2.0.

To upgrade follow the instructions given on the link above.


🧬 Mutation Testing

Coverage tells you the testbench ran a line. It does not tell you the testbench would have noticed had that line been wrong.

Mutation testing — known in hardware as functional qualification — answers the second question. avl-mutation-testing takes your golden RTL, writes out a set of copies each carrying exactly one deliberate defect, and re-runs your existing tests against every one. A mutant the tests still pass is a hole in the verification environment: a class of bug that could ship unnoticed. The testbench needs no knowledge of any of this — a mutant is ordinary RTL that happens to be wrong.

avl-mutation-testing --source rtl/*.sv --top my_module --types arith,compare --count 10

Supported mutations

Classes are selected with --types, and avl-mutation-testing --list-types prints them with the syntax each one matches.

Class Mutation Example
arith Swaps an arithmetic operator a + b → a - b
bitwise Swaps a bitwise operator a & b → a | b
compare Swaps a comparison a < b → a <= b
logical Swaps a logical operator a && b → a || b
shift Swaps a shift direction a << 1 → a >> 1
unary Removes a unary operator ~a → a
operand Reverses a non-commutative operator's operands a - b → b - a
condition Holds a branch open, holds it shut, and nudges the comparisons it is built from if (en) → if (1'b1), if (1'b0)
statement Drops a registered assignment, so the register holds y <= d; → ;
pipeline Gives a registered signal an extra stage, so it arrives a cycle late y <= d; → y one cycle late
sign Negates the value assigned to a signed variable y = a + 1; → y = -(a + 1);
width Takes the top bit off a packed declaration logic [8:0] t → logic [7:0] t
array_packed Reverses a packed dimension, renumbering the bits logic [7:0] a → logic [0:7] a
array_unpacked Reverses an unpacked dimension, reordering the elements logic a [0:3] → logic a [3:0]
blocking Makes a nonblocking assignment blocking x <= a; → x = a;
nonblocking Makes a blocking assignment nonblocking x = a; → x <= a;

Every line a mutation changes carries an /* AVL MUTATION - ... */ comment, so a mutant that turns up in an editor, a debugger or a waveform cannot be mistaken for the golden source. Generation also writes mutations.html, a report explaining each mutation in its source context.

Equivalent mutants

Some defects cannot change behaviour — flipping the + in a + 0 to a - is still a. No testbench can ever catch those, so scoring them as survivors reports verification holes that are not there. Where Yosys is installed each mutation is proved to change the design before any simulation time is spent on it, and the ones that do not are reported as equivalent and left out of the score. Yosys is optional; without it the stage is skipped.

Background and tools

Link
Mutation testing Overview of the technique
Hints on Test Data Selection DeMillo, Lipton & Sayward, IEEE Computer 11(4), 1978 — where the idea starts
An Analysis and Survey of the Development of Mutation Testing Jia & Harman, IEEE Transactions on Software Engineering 37(5) — the standard survey
pyslang / slang SystemVerilog frontend used to locate mutation sites
Yosys Proves each mutation changes the design
CocoTB Runs the testbench against each mutant
Verilator Default simulator for the examples

Nineteen worked examples live under examples/mutation_testing, one per mutation class plus a hierarchical ALU, a synchronous FIFO, and a design with a provably equivalent mutant. See its README for the full walkthrough, and the documentation for the complete option reference.


📦 Installation

Using pip

# Standard build
pip install avl-core

# Development build
pip install avl-core[dev]

Install from Source

git clone https://github.com/projectapheleia/avl.git
cd avl

# Standard build
pip install .

# Development build
pip install .[dev]

Alternatively if you want to create a virtual environment rather than install globally a script is provided. This will install, with edit privileges to local virtual environment.

This script assumes you have Verilator, GTKWave and Graphviz installed, so all examples and documentation will build out of the box. Yosys is optional; the mutation testing examples use it to prove each mutation changes the design, and skip that stage without it. The script warns about anything it cannot find.

git clone https://github.com/projectapheleia/avl.git
cd avl
source avl.sh

📖 Documentation

In order to build the documentation you must have installed the development build.

Build from Source

cd docs
make html
<browser> build/html/index.html

🏃 Examples

In order to run all the examples you must have installed the development build.

To run all examples:

cd examples

# To run
make -j 8 sim

# To clean
make -j 8 clean

To run an individual example:

cd examples/THE EXAMPLE YOU WANT

# To run
make sim

# To clean
make clean

The examples use the CocoTB Makefile and default to Verilator with all waveforms generated. This can be modified using the standard CocoTB build system.

WARNING: Due to GNU Make not exporting variables not already in env the user must ensure PYTHONPATH is set in the environment. If you have sourced the avl.sh this is done for you.


🧹 Code Style & Linting

This project uses Ruff for linting and formatting.

Check code for issues:

ruff check .

Automatically fix common issues:

ruff check . --fix

Additional Libraries / UVCs

Library Description
avl-ral Register Abstraction Layer
avl-qemu QEMU Integration
avl-apb AMBA APB UVC
avl-axi-stream AMBA AXI-STREAM UVC
avl-axi AMBA AXI5 UVC
avl-jtag JTAG UVC
avl-spi SPI UVC
avl-riscv-coverage RISCV Coverage collection from trace framework
avl-tutorials AVL Tutorials and introduction presentations

📧 Contact

Metadata

Release files for avl-core 1.2.0

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Source distribution (sdist)

Source distribution for avl-core 1.2.0
File Size Uploaded
avl_core-1.2.0.tar.gz 167.2 kB Details

Built distribution (wheel)

Table of built distributions (wheels) for avl-core 1.2.0
File Interpreter ABI Platform
avl_core-1.2.0-py3-none-any.whl Python 3 none any Details

Total release size: 352.3 kB

Release files / avl_core-1.2.0.tar.gz

Download URL avl_core-1.2.0.tar.gz
Size 167.2 kB
Tags Source
SHA-256 checksum
How to use checksums
81ca592ab1ce5076c997fdd1f987ff020b0590e0b62bbc2812091efd8b910a82
BLAKE2b-256 checksum
How to use checksums
acd893eb0ecd1aefb442d04b00d6a3128591ce5e55035a47b3af966a8a2bbe04
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via twine/7.0.0 CPython/3.12.3

Release files / avl_core-1.2.0-py3-none-any.whl

Download URL avl_core-1.2.0-py3-none-any.whl
Size 185.1 kB
Tags Python 3
SHA-256 checksum
How to use checksums
af70d980e7f1b5255b9be6640262af38dcc14a12b2075901c7fac3d84e2651b4
BLAKE2b-256 checksum
How to use checksums
443b74ccd33aa07b6fd590e2969dc20fd862b9198016ea9e7a2292ab5ac6ea43
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via twine/7.0.0 CPython/3.12.3

Release history Release notifications | RSS feed

This release

1.2.0 This release

2 release files

1.1.1

2 release files

1.1.0

2 release files

1.0.1

2 release files

1.0.0

2 release files

0.5.1

2 release files

0.5.0

2 release files

0.4.3

2 release files

0.4.2

2 release files

0.4.1

2 release files

0.4.0

2 release files

0.3.3

2 release files

0.3.2

2 release files

0.3.1

2 release files

0.3.0

2 release files

0.2.2

2 release files

0.2.1

2 release files

0.2.0

2 release files

0.1.2

2 release files

0.1.1

2 release files

0.1.0

2 release files

Anthropic, PBC Visionary sponsor Bloomberg Visionary sponsor Hudson River Trading Visionary sponsor Meta Visionary sponsor NVIDIA Visionary sponsor Microsoft Sustainability sponsor Depot Continuous Integration AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page