Z3 Constraints

AVL uses Z3 to implement a full constraintsolver.

Previous Python implementations have use python-constraints which is a perfectly good solution and users are free to do the same.

The limitation of python-constraints is that it selects a suitable from a list of possible solutions. This is fine for many applications but when modelling hardware with 32bit (2**32) or 64bit (2**64) possible options, this is infeasible on most servers in a realistic timeframe.

AVL supports randomization of the same variable types as System Verilog, but only extensions of avl.Var types are supported:

bit / int / logic

arrays (lists) / dynamic arrays (lists) / associative arrays (dicts)

enums

In addition real (float) types are supported, and implemented to common accuracies:

half precision (16bit)

single precision (32bit)

double precision (64bit)

This documents will not go into details of the Z3 Solver as they provide excellent documentation.

Constraints should be defined using lamda functions. This means the function is evaluated when the randomize function is called not when the constraint is defined.

Constraints can be applied directly to a variable or within the class that variable is instanced. Constraints local to the variable are always inherited by the class.

Both soft and hard constraints are supported.

When randomizing only variables that have constraints are bound using the Optimize() function of the z3 solver. Otherwise a random value between min() and max() of that data type is used. This is to improve performance when randomizing large classes with many variables.

Also note that for the floating point representations, the final casting using numpy handles the precision and rounding.

A more complete list of examples is included in the example directory, but a basic usage is shown below:

# Copyright 2024 Apheleia
#
# Description:
# Apheleia attributes example


import avl
import cocotb
from z3 import And, Implies, Or


class example_env(avl.Env):
    def __init__(self, name, parent):
        super().__init__(name, parent)

        self.a = avl.Logic(0, width=8, fmt=hex)
        self.b = avl.Logic(0, width=8, fmt=hex)

        self.add_constraint("c_0", lambda x: Or(x == 0, x == 100), self.a)
        self.add_constraint("c_1", lambda x: And(x >= 5, x <= 100), self.b)
        self.add_constraint("c_2", lambda x, y: Implies(x == 0, y == 10), self.a, self.b)


@cocotb.test
async def test(dut):
    e = example_env("env", None)
    for _ in range(100):
        e.randomize()
        assert e.a == 0 or e.a == 100
        assert e.b >= 5 and e.b <= 100
        assert e.b == 10 if e.a == 0 else True

Distributions

Python naturally supports a much richer range of mathematical functions to define distributions.

To create a simple, weighted distribution, similar to System Verilog, the following can be used:

class example_env(avl.Env):
   def __init__(self, name, dut, parent=None):
       super().__init__(name, dut, parent)

       self.a = avl_logic('a', 0, width=8, fmt=hex)
       self.a.add_constraint('d_0', lambda x : x == random.choices([0,1,2,3],
                                    k=1,
                                    weights=[1,2,4,8])[0])

Providing the following distribution:

For more complex distributions, the numpy library can be used. This is a very powerful library and can be used to define any distribution you can think of.

class example_env(avl.Env):
   def __init__(self, name, dut, parent=None):
       super().__init__(name, dut, parent)

       self.b = avl.Logic('b', 0, width=32, fmt=hex)
       self.b.add_constraint('d_1', lambda x : x == int(np.random.normal(100, 3)))

Providing the following distribution:

Debugging Unsatisfied Constraints

If a constraint fails to be satisfied the user can enable debugging:

export AVL_CONSTRAINT_DEBUG=1

This enables variable tracking and details the conflicting constraints. This feature should not be enabled by default. There is a performance overhead enabling the variable tracking, so it should only be used once an issue has been identified.

0.00ns WARNING  cocotb.Test test0.test0            Failed to randomize
                                                   CONFLICTING CONSTRAINT: 1 == 100
                                                           Variable 1 == e ($HOME/avl/examples/constraints/conflict/cocotb/example.py:23
                                                   CONFLICTING CONSTRAINT: 1 == 200
                                                           Variable 1 == e (/$HOME/avl/examples/constraints/conflict/cocotb/example.py:23

# Copyright 2024 Apheleia
#
# Description:
# Apheleia attributes example


import avl
import cocotb
import os


class example_env(avl.Env):
    def __init__(self, name, parent):
        super().__init__(name, parent)

        self.b = avl.Logic(0, width=8, fmt=hex)
        self.a = avl.Logic(0, width=8, fmt=hex)
        self.add_constraint("c_0", lambda x: x == 100, self.a)
        self.add_constraint("c_1", lambda x: x == 200, self.a)
        self.add_constraint("c_2", lambda x: x == 200, self.b)

@cocotb.test(expect_error=Exception)
async def test0(dut):
    os.environ["AVL_CONSTRAINT_DEBUG"] = "1"
    e = example_env("env", None)
    e.randomize()

@cocotb.test(expect_error=Exception)
async def test1(dut):
    os.environ["AVL_CONSTRAINT_DEBUG"] = "1"
    e = example_env("env", None)
    e.b.add_constraint("c_0", lambda x: x == 0x00)
    e.b.add_constraint("c_1", lambda x: x == 0x11)
    e.b.randomize()