.. _examples:

Repository of Examples
======================================

The FVM provides a repository of examples to showcase how a number of designs
of increasing complexity can be verified with it. While a small number of
designs have been developed by the methodology authors, the majority of the
designs come from third-party libraries or developers.

Examples developed by the FVM team are provided in the FVM repository and
covered by the same :ref:`license` as the rest of the provided code.

Examples developed by third parties have their own Free/Open-Source license and
are not provided in the FVM repository. Instead, ``git clone`` commands are run
from the relevant ``formal.py`` scripts in order to download the code.

In this section, the most relevant aspects of each example and how to approach
its verification are explained, but users can find the complete commented
properties and ``formal.py`` script in the FVM repository.

Suggested order
---------------

Examples are shown in this section in the suggested order for users, organized
in difficulty levels:

+--------------+---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
| Complexity   | Example             | Library / Developer | Difficulty                                                                                              | 
+==============+=====================+=====================+=========================================================================================================+
| Trivial      | Counter             | FVM team            | Simple logic with a single path                                                                         |
+              +---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
|              | Priority arbiter    | Open Logic          | Static arbitration scheme with low complexity                                                           |
+              +---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
|              | Dualcounter         | FVM team            | Structure remains simple despite duplication of logic                                                   |
+              +---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
|              | Round robin arbiter | Open Logic          | Moderate complexity due to round-robin policy                                                           |
+--------------+---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
| Easy         | UART transmitter    | FVM team            | Finite state machine with sequential behavior                                                           |
+              +---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
|              | AXI4-lite slave     | Open Logic          | Multiple interfaces must be simultaneously verified                                                     |
+--------------+---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
| Medium       | SDRAM controller    | Joshua Bassett      | Control and timing behavior is dependent on the issued commands                                         |
+              +---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
|              | Linear interpolator | FVM team            | Requires data integrity checks over 12 cycles                                                           |
+              +---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
|              | Synchronous FIFO    | Open Logic          | Unbounded timing relation between read and write complicates proofs                                     |
+--------------+---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
| Intermediate | 32-bit divider      | GRLIB               | High arithmetic complexity significantly increases the state space                                      |
+              +---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
|              | Asynchronous FIFO   | Open Logic          | Multi-clock domain interactions                                                                         |
+--------------+---------------------+---------------------+---------------------------------------------------------------------------------------------------------+
| Difficult    | IPv6 transceiver    | Pile of Cores       | Protocol complexity due to buffering and large headers with variable latency                            |
+--------------+---------------------+---------------------+---------------------------------------------------------------------------------------------------------+


Trivial examples
----------------

Counter
~~~~~~~

The first trivial example was the counter, explained in :ref:`firstexample`.

As this design is trivial and a counter is not too suited to be modeled in
terms of input/output transactions, ``drom2psl`` is not used for this design.

- Link: https://gitlab.com/fvmformal/fvm/-/tree/main/examples/counter

Dualcounter
~~~~~~~~~~~

This *dualcounter* compares whether the most significant bit of two counters
is equal and shows the result in the output ``equalmsb``. In the
``reachability`` step, we can see that the ``equalmsb = '0'`` toggle is
unreachable, so we know that the output of this dualcounter will always be
correct.

- Link: https://gitlab.com/fvmformal/fvm/-/tree/main/examples/dualcounter

Priority Arbiter
~~~~~~~~~~~~~~~~

This example verifies a simple priority arbiter from the Open Logic library:
https://github.com/open-logic/open-logic. In this example, many things can
be checked simply with assertions, for example, that the output always has 0
or 1 bit asserted; that if there is no request, the output is 0; that if there
is a request, the output is one-hot... Additionally, to fully test the
functionality, we can create a function that returns the expected value for the
arbiter result. This can be done either in the PSL file or in a VHDL package,
although the latter is recommended (by defining the function in a VHDL package,
the PSL files are simpler and we can easily reuse the function in simulation if
needed).

- Link: https://gitlab.com/fvmformal/fvm/-/tree/main/examples/arbiter_prior

.. _round_robin_arbiter:

Round Robin Arbiter
~~~~~~~~~~~~~~~~~~~

This example also belongs to the OpenLogic library. Again, it's a simple
example, and some of the priority arbiter's priorities can be reused. However,
this case is more complicated due to the round-robin algorithm and the control
logic, which requires a handshake. We can define a sequence for the handshake
since it will be reused quite a bit. Thus, this will be the first example
design in which we will use ``drom2psl``.

Again, it is very convenient to define a function that models the round-robin
behavior, since it's very simple, so we'll define it in a VHDL package.

Let's try creating a sequence with
``drom2psl``.  We want to ensure that if there has been a valid grant before, the
next grant (whenever it happens) will be successful. The function that predicts
the round robin needs the request and the last grant as inputs.

.. figure:: _static/examples/rr_arbiter.svg

   Wavedrom diagram for the ``last_valid_grant`` sequence. Cycles where the
   clock signal has the two wavy lines mean "0 or more cycles". The data type
   for ``Out_Grant`` is specified in the `JSON file
   <https://gitlab.com/fvmformal/fvm/-/blob/main/examples/arbiter_rr/last_valid_grant.json>`_
   as an extra field, ``type``, of the ``Out_Grant`` wavelane.

This is the generated PSL:

.. code-block:: vhdl

   vunit last_valid_grant {

   sequence last_valid_grant (
      hdltype std_logic_vector(Width_g-1 downto 0) last_grant
   ) is {
      ((Out_Ready = '1') and (Out_Valid = '1') and (Out_Grant = last_grant))[*1];  -- 1 cycle
      ((Out_Ready = '0') and (Out_Valid = '0'))[*];  -- 0 or more cycles
      ((Out_Ready = '0') and (Out_Valid = '1'))[*];  -- 0 or more cycles
      ((Out_Ready = '1') and (Out_Valid = '1'))[*1]  -- 1 cycle
   };

   }

With this, we can ensure that if we have a grant and then we have another
(which can happen in any possible cycle), the actual grant will be equal to the
output of the function that predicts it. We can verify that the property holds
true for all possible values by creating a symbolic constant ``last_grant``
(explained in :ref:`symbolic-constants` in :ref:`complexityreduction`).

.. code-block:: vhdl

   assert always ( {last_valid_grant(last_grant)} |->
                   {Out_Grant = round_robin_arbiter(In_Req, last_grant) } ) abort Rst;

- Link: https://gitlab.com/fvmformal/fvm/-/tree/main/examples/arbiter_rr

Easy examples
--------------

UART transmitter
~~~~~~~~~~~~~~~~

This example is still simple, but it already includes a state machine,
albeit one with very linear behavior. With ``drom2psl`` we can define the input
transaction in the `Precond` group and the output transaction in the `Cond`
group (or `Cond_non_overlap`) if we want to generate a property with an
implication.

.. image:: _static/examples/uart.svg

The generated PSL is as follows:

.. code-block:: vhdl

   vunit uart_prop {

   sequence uart_prop_Precond (
      hdltype std_logic_vector(7 downto 0) d
   ) is {
      ((rd_en = '1'))[*1];  -- 1 cycle
      ((data = d))[*1]  -- 1 cycle
   };

   sequence uart_prop_Cond_non_overlap (
      hdltype std_logic_vector(7 downto 0) d;
      hdltype std_logic parity_value
   ) is {
      ((TX = '0'))[*2];  -- 2 cycles
      ((TX = d(0)))[*2];  -- 2 cycles
      ((TX = d(1)))[*2];  -- 2 cycles
      ((TX = d(2)))[*2];  -- 2 cycles
      ((TX = d(3)))[*2];  -- 2 cycles
      ((TX = d(4)))[*2];  -- 2 cycles
      ((TX = d(5)))[*2];  -- 2 cycles
      ((TX = d(6)))[*2];  -- 2 cycles
      ((TX = d(7)))[*2];  -- 2 cycles
      ((TX = parity_value))[*2];  -- 2 cycles
      ((TX = '1'))[*2]  -- 2 cycles
   };

   -- Relational operands between sequences may be, among others:
   --   && : both must happen and last exactly the same number of cycles
   --   & : both must happen, without any requirement on their durations
   --   |-> : implication: both must happen, with the first cycle of the second occurring during the last cycle of the first
   --   |=> : non-overlapping implication: both must happen, with the first cycle of the second occuring the cycle after the last cycle of the first
   property uart_prop (
      hdltype std_logic_vector(7 downto 0) d;
      hdltype std_logic parity_value;
      hdltype std_ulogic fvm_rst
   ) is
      always ( uart_prop_Precond(d) |=> uart_prop_Cond_non_overlap(d, parity_value) ) abort (fvm_rst = '1');

   }

From our PSL, the property can be used simply with:

.. code-block:: vhdl

  assert_tx:
    assert uart_prop(data_uart, calc_parity(data_uart), rst);

.. caution::
   Note that the automatic property reset is active high. If your design uses
   an active low reset, you can use
   `assert uart_prop(data_uart, calc_parity(data_uart), not rst);`

This property verifies the entire functionality of the design, but it must be
noted that in the property's precondition there is an output (``rd_en``) and,
**when a precondition of a property depends on a design output, you must make
sure that that specific design output is activated when expected**, to avoid
verification gaps. So, we need to verify somehow that ``rd_en`` is activated
when we want it to be; the example code shows how we do this in this case.

.. note::

   For clarity of the wavedrom diagrams, a sequence where each bit lasts for
   two clock cycles has been used for the documentation. The actual VHDL has a
   generic, ``BIT_DURATION``, which is set to a default value of 5. Depending
   on the actual clock frequency used and the desired baudrate, this
   ``BIT_DURATION`` generic could be set to different values, for example using
   a design configuration, as explained in :ref:`designconfigurations`.

   Future versions of ``drom2psl`` may support stretching parts of the sequences
   to accomodate sequences where some durations are set by generics, but in the
   meantime engineers can always manually call ``drom2psl``, modify the generated
   PSL file by changing all the ``[*5]`` to ``[*BIT_DURATION]``, and add the
   modified PSL source instead of the JSON source to the fvm framework
   instance.

- Link: https://gitlab.com/fvmformal/fvm/-/tree/main/examples/uart_tx

AXI-4 Lite Slave
~~~~~~~~~~~~~~~~~

This example also belongs to the OpenLogic library.
This AXI Slave has a state machine that is no longer as linear (it has both
TX and RX) and also has quite a few interfaces. This makes writing sequences
for reuse more important, both in terms of speed and clarity.

A very interesting way to use ``drom2psl`` is to define one of the
functionalities of our design in wavedrom, in this case READ, and ``cover`` it
to see if it can occur:

.. image:: _static/examples/axi_s_read_3.svg

With the wavedrom, we can generate assertions to write, either manually or
with ``drom2psl``. In this case, it's clear that three things happen:
**1) The AR channel requests data from an address, 2) The data is read from the
register bank for the requested address, and 3) the R channel reads the data**.
Furthermore, we can observe that in **1)** the input transaction could be the
AR channel (let's call it ``a``) and the output transaction the read portion of
the register bank (let's call it ``b``); in **2)** the input transaction is the
read portion of the register bank and the output transaction is the write
portion of the register bank (let's call it ``c``); and in **3)** the input
transaction is the write portion of the register bank and the output
transaction is the R channel (let's call it ``d``). So, conceptually, we want
assertions that relate ``a -> b``, ``b -> c``, and ``c -> d``, and with those
we verify all parts of the READ functionality.

Medium examples
---------------

SDRAM controller
~~~~~~~~~~~~~~~~

This example comes from a popular Github repo: https://github.com/nullobject/sdram-fpga.
This is the first example where complexity reduction techniques are applied,
although it's quite easy. There's a startup delay of over 2000 cycles
parameterized with a generic, so it can simply be reduced without affecting
the design at all, as it's just a startup delay. Regarding the design, it's
similar to the AXI slave with many states (``WRITE``, ``READ``, ``REFRESH``...)
and many interfaces, so using sequences remains essential.

With ``drom2psl`` we can easily ``assert`` a write, with an input transaction
using the user interface and an output transaction using the SDRAM interface:

.. image:: _static/examples/sdram_write.svg

``drom2psl`` generates the following code:

.. code-block:: vhdl

   vunit write_seq {

   sequence write_seq_Precond (
      hdltype unsigned(22 downto 0) addr_value;
      hdltype std_logic_vector(31 downto 0) data_value
   ) is {
      ((addr = addr_value) and (data = data_value) and (we = '1') and (req = '1') and (ack = '0'))[*1];  -- 1 cycle
      ((addr = addr_value) and (data = data_value) and (we = '1') and (req = '1') and (ack = '1'))[*1]  -- 1 cycle
   };

   sequence write_seq_Cond (
      hdltype unsigned(22 downto 0) addr_value;
      hdltype std_logic_vector(31 downto 0) data_value
   ) is {
      ((sdram_a = addr_value(20 downto 8)) and (sdram_ba = addr_value(22 downto 21)) and (sdram_cs_n = '0') and (sdram_ras_n = '0') and (sdram_cas_n = '1') and (sdram_we_n = '1'))[*1];  -- 1 cycle
      ((sdram_a = "0010" & addr_value(7 downto 0) & '0') and (sdram_ba = addr_value(22 downto 21)) and (sdram_dq = data_value(31 downto 16)) and (sdram_cs_n = '0') and (sdram_ras_n = '1') and (sdram_cas_n = '0') and (sdram_we_n = '0'))[*1];  -- 1 cycle
      ((sdram_dq = data_value(15 downto 0)) and (sdram_cs_n = '0') and (sdram_ras_n = '1') and (sdram_cas_n = '1') and (sdram_we_n = '1'))[*1]  -- 1 cycle
   };

   -- Relational operands between sequences may be, among others:
   --   && : both must happen and last exactly the same number of cycles
   --   & : both must happen, without any requirement on their durations
   --   |-> : implication: both must happen, with the first cycle of the second occurring during the last cycle of the first
   --   |=> : non-overlapping implication: both must happen, with the first cycle of the second occuring the cycle after the last cycle of the first
   property write_seq (
      hdltype unsigned(22 downto 0) addr_value;
      hdltype std_logic_vector(31 downto 0) data_value;
      hdltype std_ulogic fvm_rst
   ) is
      always ( write_seq_Precond(addr_value, data_value) |-> write_seq_Cond(addr_value, data_value) ) abort (fvm_rst = '1');

   }

And with just one line of code we can verify that the writes are working
properly!

.. code-block:: vhdl

   write_is_correct:
      assert write_seq(addr_sig, data_sig, reset);

- Link: https://gitlab.com/fvmformal/fvm/-/tree/main/examples/sdram

Linear interpolator
~~~~~~~~~~~~~~~~~~~~

This designs makes a linear interpolation betwen two inputs, which are
fixed-point complex numbers defined as a VHDL ``record`` type that has two
fields: ``re`` (for the real part) and ``im`` (for the imaginary part). If the
input ``valid`` is asserted, the ``inferior`` and ``superior`` inputs are
interpolated for 12 cycles.

This example will be the first where assumptions are crucial. Due to how the
design works, while it is interpolating:

* its ``inferior`` and ``superior`` inputs must not change, and
* its ``valid`` input cannot be asserted

Thus, we use assumptions to ensure that if ``valid`` is asserted, the
``superior`` and ``inferior`` inputs remain stable during the 12 interpolation
cycles. Similarly, if ``valid`` is asserted, it will not be re-asserted in the
next 12 cycles.

.. code-block:: vhdl

   -- Assume inferior and superior do not change during the 12 cycles output
   assume always ({valid} |=> {stable(inferior)[*12]}) abort rst;
   assume always ({valid} |=> {stable(superior)[*12]}) abort rst;

   -- Assume the interpolator will not be activated on the 12 cycles after
   -- being activated (the interpolator needs 12 cycles to output the 12
   -- interpolated data)
   assume_not_activated_when_interpolating:
      assume always {valid} |=> {(not valid)[*12]};

In addition to this, this example is the first with some computational
complexity, due to its 10-bit by 5-bit multipliers.

Using ``drom2psl`` we can generate a property with these transactions:

.. image:: _static/examples/interpolator_prop.svg

And we can use the property this way (note that ``interpolator_predict`` is a
function that we define to predict the interpolated values):

.. code-block:: vhdl

   interpolator_works_correctly:
      assert interpolator_prop(input_tran, interpolator_predict(input_tran), rst);

- Link: https://gitlab.com/fvmformal/fvm/-/tree/main/examples/linearinterpolator

Synchronous FIFO
~~~~~~~~~~~~~~~~~

This example also belongs to the OpenLogic library.
This example is one of the most important, since FIFOs and memories are a
recurring element in most designs, and will be responsible for a large part
of their difficulty.

First, we need to understand why memory complicates our designs so much.
Taking the example of a relatively small memory, 256x8 bits, that already
gives us 2048 state bits, which is quite a lot in itself. Furthermore,
with 256 memory locations, if it's accessed once per cycle, it will take at
least 256 cycles for the properties to verify that all memory locations are
accessible, resulting in high latency. In fact, memory locations are often
more detrimental due to the latency they generate than the data size, since
the latter can be simplified by using symbolic constants.

The section :ref:`complexityreduction` offers several tips for
dealing with memory. The PSL code for this FIFO also reveals which techniques
are used.

- Link: https://gitlab.com/fvmformal/fvm/-/tree/main/examples/fifo_sync

Intermediate examples
----------------------

32-bit divider
~~~~~~~~~~~~~~~

This example belongs to the GRLIB IP library from Gaisler:
https://www.gaisler.com/grlib-ip-library. This is the first example in which
several libraries are used; the sources must be added in the order the
libraries are compiled, as explained in
:py:func:`fvm.FvmFramework.add_vhdl_source`.

This case presents enormous computational complexity: a 64-bit dividend
divided by a 32-bit divisor. This will make it impossible to verify data
integrity for all combinations (2\ :sup:`96`), just as it would be impossible
to do so with simulation.

Therefore, to verify data integrity, we need to reduce the state space,
that is, the possible combinations. The best way to do this is to use
assumptions, although it would be advisable for the assumptions to occupy
random bins so that different values are used during different executions.
With 2\ :sup:`24` combinations, the property takes 1 hour. With 2\ :sup:`21`
combinations, it takes 10 minutes.

.. code-block:: vhdl

   -- We can assume some bits are always constant, although we should
   -- randomize it for different executions
   assume always ( divi.y(29 downto 20) = "0101010101" );
   assume always ( divi.op1(29 downto 20) = "1101011010" );
   assume always ( divi.op2(29 downto 20) = "0100001110" );

   -- Or we can directly assume ranges
   assume always ( 10000 > signed(divi.y) >= -10000);
   assume always ( 20000 > signed(divi.op1) >= 0);

- Link: https://gitlab.com/fvmformal/fvm/-/tree/main/examples/div32

Asynchronous FIFO
~~~~~~~~~~~~~~~~~

This example also belongs to the OpenLogic library.
If we specify the clock and reset domains in ``formal.py``, the steps
``resets`` and ``clocks`` are very useful for checking clock and reset
domain crossing.

Regarding FIFO handling, it's the same as the synchronous FIFO. The difference
lies in the clocks. Until now, we defined the default clock at the top of the
PSL file, and all properties used that clock. Now we'll have to define the
clock in each property (although PSL allows for more than one clock in a
property, it's not recommended, and most tools probably won't support it):

.. code-block:: vhdl

   -- Assert the FIFO level calculated on the write side is always
   -- less than the depth of the FIFO
   assert_in_level_within_bounds:
      assert always ( (unsigned(In_Level) <= Depth_g) abort In_Rst) @rising_edge(In_Clk);

So, what do we do if we want a property that relates signals from different
clock domains? Well, we can pass either of the two signals through a
synchronizer (it can be a single-stage synchronizer because in formal
verification there is no metastability) and implement the property on the
clock of both. But what if we want an input to only move within one clock
domain, something the formal solver doesn't necessarily know? Some tools
allow us to specify clock domains for inputs, but in PSL we can do something
similar by creating a signal and assigning it to the desired clock domain
(without specifying any value), and then making an assumption relating that
signal to the original:

.. code-block:: vhdl

  signal out_ready_reg, out_ready_reg_in_clk : std_logic;
  process (In_Clk)
  begin
      if rising_edge(In_Clk) then
          out_ready_reg_in_clk <= out_ready_reg;
      end if;
  end process;

  assume always (Out_Ready = out_ready_reg_in_clk);

- Link: https://gitlab.com/fvmformal/fvm/-/tree/main/examples/fifo_async

Difficult examples
------------------

IPv6 transceiver
~~~~~~~~~~~~~~~~~

This example belongs to the PoC (Pile of Cores) library:
https://github.com/VLSI-EDA/PoC.
This is the most complicated of all, both because of its size and because it
has some of the complexity elements at the same time: bigger state space, a number of
memories inside, and a latency which cannot be arbitrarily reduced due to the
fact that the frames require specific headers. This results in greater
verification efforts, requiring more and more complex properties. Therefore,
using sequences and reusing code becomes more necessary.

- Link: https://gitlab.com/fvmformal/fvm/-/tree/main/examples/ipv6