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.
Note
avl.Uint data types are implemented as Z3 Int and not as you may suspect as Z3 BitVec. This is because Z3 BitVec are already supported in avl.Logic.
Z3 Ints can be faster to randomize than Z3 BitVecs, and are more flexible in terms of constraints.
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:
Freezing / Unfreezing constraints
By default variables to be randomized, constraints and ranges are re-calculated each time an object is randomized. This allows for uses to change constraints and classes dynamically, unlike System Verilog.
However, this can be slow for large classes with many variables and constraints. To speed up randomization, constraints can be frozen. This means the constraints are only calculated once, and then used for all future randomizations.
To freeze constraints, the Object.freeze_constraints method can be used. This will freeze all constraints on the variable and all constraints on the class that the variable is instanced in.
To unfreeze constraints, the Object.unfreeze_constraints method can be used. This will unfreeze all constraints on the variable and all constraints on the class that the variable is instanced in.
An example of the benefit can be seen in the following example:
# Copyright 2024 Apheleia
#
# Description:
# Apheleia attributes example
import time
import avl
import cocotb
from z3 import And, If
class example_env(avl.Env):
def __init__(self, name, parent):
super().__init__(name, parent)
# Size array to maximum size required
self.a = [avl.Int32(0) for i in range(8)]
# Declare a var to randomize the size of the array
self.size = avl.Int32(0)
# Constrain the size of the array
self.add_constraint(
"size_c",
lambda x: And(x > 0, x <= 8),
self.size
)
# Constrain the first element of the array to a random number between 0 and 100
self.add_constraint(
"a0_c",
lambda x: And(x >= 0, x <= 100),
self.a[0]
)
# Constrain the rest of the elements of the array to be one greater than the previous element
for i in range(1, len(self.a)):
self.add_constraint(
f"a{i}_c",
lambda x, y, z, idx=i: If(idx < z, x == y + 1, x == 0),
self.a[i],
self.a[i - 1],
self.size
)
@cocotb.test
async def test(dut):
e = example_env("env", None)
start = time.time()
for _ in range(10):
e.randomize()
assert(e.size > 0 and e.size <= 8)
for i in range(0, int(e.size)):
if i == 0:
assert e.a[i] >= 0 and e.a[i] <= 100
else:
assert e.a[i] == e.a[i - 1] + 1
end = time.time()
print(f"Time taken (unfrozen constraints): {end - start:.2f} seconds")
e.freeze_constraints()
start = time.time()
for _ in range(10):
e.randomize()
assert(e.size > 0 and e.size <= 8)
for i in range(0, int(e.size)):
if i == 0:
assert e.a[i] >= 0 and e.a[i] <= 100
else:
assert e.a[i] == e.a[i - 1] + 1
end = time.time()
print(f"Time taken (frozen constraints): {end - start:.2f} seconds")
Time taken (unfrozen constraints): 6.29 seconds
Time taken (frozen constraints): 0.95 seconds
Note
When constraints are frozen, references to literals and other non-randomized variables are not updated (including those not within the scope of the randomization). This means that if the value of a literal changes, the constraint will not be updated. This is a trade-off for speed, and should be used with care. Equally, new variables added to the class after the constraints are frozen will not be included in the randomization process. If you need to update the value of a literal, you should unfreeze the constraints, update the value, and then freeze the constraints again. This is not an issue for randomized variables, as they are always updated when the variable is randomized.