Z3 Constraints
==============

AVL uses `Z3 <https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/>`_ to implement a full constraint\
solver.

Previous Python implementations have use `python-constraints <https://python-constraint.github.io/python-constraint/>`_ 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 :doc:`avl.Var </modules/avl._core.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 <https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/>`_ \
as they provide excellent documentation.

Constraints should be defined using `lamda functions <https://realpython.com/python-lambda/>`_. 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:

.. literalinclude:: ../../../examples/constraints/simple/cocotb/example.py
    :language: python


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:

.. code-block:: python

 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:

.. image:: /images/simple_distribution.png
   :align: center

For more complex distributions, the `numpy <https://numpy.org/doc/stable/index.html>`_ library can be used. This is a very powerful library \
and can be used to define any distribution you can think of.

.. code-block:: python

 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:

.. image:: /images/normal_distribution.png
   :align: center


Debugging Unsatisfied Constraints
---------------------------------

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

.. code-block:: bash

    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.

.. code-block:: bash

     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

.. literalinclude:: ../../../examples/constraints/conflict/cocotb/example.py
    :language: python