Verification procedure
======================

The following formal test are performed to verify ISA compliance of
RISC-V processors with ``riscv-formal``. Depending on aspects like the
strength of safety properties present in the core, the overall
complexity of the core, and the verification requirements for the given
application, the following tests might be set up as bounded model checks
or as unbounded verification tasks.

For most cores the easiest approach is to create a wrapper HDL module
and a ``checks.cfg`` file and use the ``genchecks.py`` scripts to create
the formal checks. See ``cores/picorv32/`` for an
example implementation. The checks generated by ``genchecks.py`` are
bounded model checks which use sby for verification.

.. _procedure-config:

Configuring check generation
----------------------------

A config file with extension ``.cfg`` is used to configure the
``genchecks.py`` script. By default, the name of this config file is
expected to be ``checks``. Calling ``genchecks.py`` with an argument
will instead use the provided name. For example,
``python3 ../../checks/genchecks.py tests`` will load config settings
from a file named ``tests.cfg``. Note that the script will generate a
folder with the same config name in the directory it is run.

It is expected for ``genchecks.py`` to be called from a subdirectory of
the ``cores`` folder, such that the script is called as
``../../checks/genchecks.py``, and the subdirectory is the name of the
core. This core name will be used for naming certain intermediary files,
but is otherwise arbitrary and does not need to match anything else.

The config file consists of a number of sections, with each section
starting with the name of the section in square brackets. Some of these
sections are shared between tests, and some are used only for specific
formal checks. The shared sections will be covered here, while check
specific details will be covered in the relevant section below.

Comments can be included in the config file by prefixing a line with a
``#`` character.

``[options]``
~~~~~~~~~~~~~

This section primarily contains options which describe the core under
test. Possible options are listed below, along with their expected
value. For options with no expected value, simply including the option
enables the specified effect.

+---------------------+------------------+-----------------------------+
| Option              | Value            | Description                 |
+=====================+==================+=============================+
| isa                 | String           | ISA extensions,             |
|                     |                  | e.g. \ ``RV64IMAFD``, or    |
|                     |                  | ``rv32i``. Refer to the     |
|                     |                  | :ref:`proc-isa` section     |
|                     |                  | below for more information. |
+---------------------+------------------+-----------------------------+
| nret                | Integer          | The number of channels for  |
|                     |                  | the RVFI port. Defaults to  |
|                     |                  | 1.                          |
+---------------------+------------------+-----------------------------+
| blackbox            | None             | Signifies register file and |
|                     |                  | ALU should be black-boxed.  |
+---------------------+------------------+-----------------------------+
| solver              | String           | Name of solver, defaults to |
|                     |                  | ``boolector``.              |
+---------------------+------------------+-----------------------------+
| dumpsmt2            | None             | Passed to ``smtbmc`` engine |
|                     |                  | to output SMT2 trace.       |
+---------------------+------------------+-----------------------------+
| abspath             | None             | Generated makefile will use |
|                     |                  | absolute path of generated  |
|                     |                  | files.                      |
+---------------------+------------------+-----------------------------+
| mode                | String           | Solver mode, currently      |
|                     |                  | supports either ``bmc`` or  |
|                     |                  | ``prove``, and defaults to  |
|                     |                  | ``bmc``.                    |
+---------------------+------------------+-----------------------------+

.. _proc-isa:

Supported ISAs
^^^^^^^^^^^^^^

The following RISC-V ISA modules are supported for testing:

.. list-table::
   :widths: auto
   :header-rows: 1

   * - Module
     - Version
     - Notes
   * - rv32i
     - 2.1
     - Base integer instruction set (32bit).
   * - rv64i
     - 2.1
     - Base integer instruction set (64bit).
   * - c
     - 2.0
     - Extension for compressed instructions.
   * - m
     - 2.0
     - Extension for integer multiplication and division.
   * - Zicsr
     - 2.0
     - CSRs are handled separately and "Zicsr" should not be included in
       the ``isa`` string.  See :ref:`proc-csrs`.
   * - b
     - 1.0
     - Extension for bit manipulation, comprising instructions provided
       by the Zba, Zbb, and Zbs extensions.
   * - Zba
     - 1.0
     - Address generation.
   * - Zbb
     - 1.0
     - Basic bit-manipulation.
   * - Zbc
     - 1.0
     - Carry-less multiplication.
   * - Zbs
     - 1.0
     - Single-bit instructions.
   * - Zbkb
     - 1.0
     - Bit-manipulation for cryptography.
   * - Zbkc
     - 1.0
     - Carry-less multiplication for cryptography.
   * - Zbkx
     - 1.0
     - Crossbar permutations.

.. Implementation of I C and M extensions pre-date ratification (2019), so I'm not 100% sure on version

Instruction tests are available for each extension with both rv32i and
rv64i base instruction sets, e.g. ``isa rv32iZbc``.  Support for
multiple extensions in the same configuration file is currently limited,
with only the following combinations available by default:

- rv32imc
- rv32iZba_Zbb_Zbc_Zbs
- rv32iZbkb_Zbkc_Zbkx
- rv64imc
- rv64iZba_Zbb_Zbc_Zbs
- rv64iZbkb_Zbkc_Zbkx

.. warning::

   The ``isa`` string is currently case-sensitive and should match
   values in the above table exactly for instruction test generation.

Generating new combinations locally
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Additional combinations can be generated locally as needed with the
``insns/generate.py`` script.  First off, find the following section of
code:

.. code-block:: python3

   ## Additional ISA combinations
   isa_propagate("Zba_Zbb_Zbc_Zbs")
   isa_propagate("Zbkb_Zbkc_Zbkx")

Add the desired combination(s), e.g. ``isa_propagate("mcb")``, and then
run the script with ``python3 generate.py``.  Each combination should
generate a corresponding ``.txt`` and ``.v`` file that are used for
testing.

``[depth]``
~~~~~~~~~~~

This section provides the execution depth to be used by the solver for
each test. The name of the check is listed, followed by one or more
integers separated by a space. For formal checks that expect multiple
values to be provided here, the meaning of each will be defined in the
relevant section.

For cores with multiple channels, the channel number can be used in the
name of the check by appending ``_ch#``. Note that a more specific name
will be used over a less specific name. For example, if
``insn <depth0>`` and ``insn_ch1 <depth1>`` are both listed, ``insn``
tests on channel 1 will use ``depth1``, while all other channels will
use ``depth0``.

If a formal check does not have a corresponding depth listed, it will
not be generated. For example, providing ``reg_ch2 <values>`` but not
``reg <values>`` will run the ``reg`` check *only* on channel 2.

``[groups]``
~~~~~~~~~~~~

This section defines a list of group names which are prepended to all
check names which can then be used for grouping multiple checks
together. These groups can then be used for testing with multiple depth
values. Each group must be separated by whitespace.

As an example, if groups ``a`` and ``b`` are listed with depth settings
of ``a_insn <x>``, ``b_insn_bne <y>``, then all instructions will be
tested with depth ``x``, and the ``bne`` instruction will be tested to
both depths ``x`` and ``y``.

``[sort]``
~~~~~~~~~~

If this section is included, any listed checks will be run in the order
they appear in this list, and will be run *before* any un-listed checks.
Each item should be placed on its own line. When multiple checks match
the same ordering, alphabetical order will be used.

Note that regex is used to search for a match of the *full* check name,
including group and channel. This can be used to, for example, list all
checks on channel 2 before any others by adding ``.*?_ch2`` as the first
item. If the user is unfamiliar with regex, simply providing the names
of checks verbatim will also work.

Note that this sorting also determines the order in which checks are
generated in the makefile. The order in which tests are started should
be maintained by Make, however if parallelism is enabled then there is
no guarantee that tests will *complete* in this order.

``[filter-checks]``
~~~~~~~~~~~~~~~~~~~

Specific checks can be enabled or disabled by adding them to this
section prefixed with either a ``+`` or ``-`` and a space. As with
``[sort]`` above, regex is used for matching against each line. Note
that the *first* match returns. For example, if ``+ insn_(mul|div)_ch1``
is listed before ``- insn_.*_ch1``, then the ``mul`` and ``div``
instructions will be enabled for testing on channel 1, while all other
instructions are disabled.

``[assume]``
~~~~~~~~~~~~

Each line of this section provides a two value tuple. The first value is
the regex pattern used to match the current check name, while the second
value is code to be included in the file ``assume_stmts.vh``. If the
first value begins with a ``!``, the code is used for all checks that
*do not* match the pattern, otherwise the code is used for all checks
that *do* match. This file is included verbatim at the end of the
``rvfi_testbench`` module in ``checks/rvfi_testbench.sv``, and so should
be valid System Verilog code.

Verbatim sections
~~~~~~~~~~~~~~~~~

A number of sections are included in the sby script essentially as-is.
These sections are formatted with a few keyword substitutions. If using
these substitutions, the keywords should be prepended and appended with
a ``@`` symbol, e.g. \ ``@basedir@/cores/@core@/wrapper.sv`` is using
the ``basedir`` and ``core`` keywords to define the path.

Possible keywords include:

-  basedir: the root directory of riscv-formal
-  core: the name of the directory from which the script is executed
-  ilang_file: filename of intermediary output
-  channel: the current rvfi channel
-  check: the current check, e.g. \ ``csrc``
-  checkch: the full name of the current check,
   e.g. \ ``a_csrc_misa_ch0``

``[script-defines]``
^^^^^^^^^^^^^^^^^^^^

This section is included at the *start* of the sby ``[script]`` section.
Check specific code can also be included as
``[script-defines <check>]``, where ``<check>`` is the current check.

``[verilog-files]`` and ``[vhdl-files]``
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

These sections list all of the core source files which should be
included in testing. All verilog files will be listed after
``read -sv``, while all vhdl files will be listed after ``read -vhdl``.

``[script-sources]``
^^^^^^^^^^^^^^^^^^^^

This section can be used to add any other source files which do not fit
under ``-sv`` or ``-vhdl``, and is included *before* the ``prep``
command.

``[script-link]``
^^^^^^^^^^^^^^^^^

This section is included *after* the ``prep`` command and *before*
``chformal``.

``[defines]``
^^^^^^^^^^^^^

This section is included as part of ``[file defines.sv]``. Check
specific code can also be included as ``[defines <check>]``, where
``<check>`` is the current check.

Standard checks
---------------

The following checks are managed by ``genchecks.py`` and can be
implemented using the standard RVFI wrapper interface.

Instruction checks
~~~~~~~~~~~~~~~~~~

The majority of formal checks needed to verify a core with riscv-formal
are instruction checks (one per RVFI channel and RISC-V instruction
supported by the core).

Instruction checks test if the instruction (``rvfi_insn``) matches the
state transistion described by the other RVFI signals.

PC checks
~~~~~~~~~

There are two PC checks: ``pc_fwd`` and ``pc_bwd``. Both of them are run
for each RVFI channel.

The ``pc_fwd`` check assumes that the core retires an instruction at the
end of the bounded model check, and that the previous instruction in the
program (``rvfi_order-1``) was retired earlier. It then tests if
``rvfi_pc_wdata`` of the previous instruction matches ``rvfi_pc_rdata``
of the next instruction.

``pc_bwd`` is like ``pc_fwd`` but for pairs of instructions that have
been executed out of order: The check assumes that the core retires an
instruction at the end of the bounded model check, and that the next
instruction in the program (``rvfi_order+1``) was retired earlier. It
then tests if ``rvfi_pc_wdata`` of the previous instruction matches
``rvfi_pc_rdata`` of the next instruction.

``[depth]`` section
^^^^^^^^^^^^^^^^^^^

Expects two values: first is the number of cycles to reset for; second
is the execution depth.

Register checks
~~~~~~~~~~~~~~~

This checks if writes to and reads from the register file are consistent
with each other, i.e. if the value written to a register matches the
value read from the register file by a later instructions.

This check assumes that the last instruction at the end of the bounded
model check, reads a register. It then checks that the value read is
consistent with the matching write to the same register by an earlier
instruction.

.. _depth-section-1:

``[depth]`` section
^^^^^^^^^^^^^^^^^^^

Expects two values: first is the number of cycles to reset for; second
is the execution depth.

Causality
~~~~~~~~~

There are three causality checks: ``causal``, ``causal_mem`` and
``causal_io``.

The core may retire instructions out-of-order as long as causality is
preserved. (This means a write must be retired before the reads that
depend on it.)

The ``causal`` check tests if the instruction stream is causal with
respect to registers. The ``causal_mem`` check tests if the instruction
stream is causal with respect to memory. The ``causal_io`` check tests
if the instruction stream is causal with respect to i/o memory, where
every i/o memory access is assumed to depend on all earlier i/o memory
accesses.

Which areas of the adress space are considered to be i/o memory can be
configured using the ``RISCV_FORMAL_IOADDR(addr)`` macro.

.. _depth-section-2:

``[depth]`` section
^^^^^^^^^^^^^^^^^^^

Expects two values: first is the number of cycles to reset for; second
is the execution depth.

Liveness
~~~~~~~~

This check makes sure that the core never freezes (unless an instruction
with ``rvfi_halt`` asserted is retired): This check assumes that an
instruction is retired at a configurable trigger point in the middle of
the bounded model check. It then checks that the next instruction
(``rvfi_order+1``) is also retired at some point during the span of the
bounded model check.

It might be neccessary to add some bounded fairness constraints to the
design for this check to succeed.

.. _depth-section-3:

``[depth]`` section
^^^^^^^^^^^^^^^^^^^

Expects three values: first is the number of cycles to reset for; second
is the trigger depth; and third is the execution depth.

Uniqueness
~~~~~~~~~~

This check makes sure that no two instructions with the same
``rvfi_order`` are retired by the core.

.. _depth-section-4:

``[depth]`` section
^^^^^^^^^^^^^^^^^^^

Expects three values: first is the number of cycles to reset for; second
is the trigger depth; and third is the execution depth.

Faults
~~~~~~

This check makes sure that dynamically occuring memory faults are
handled. It requires defining ``RISCV_FORMAL_MEM_FAULT`` and the
``rvfi_mem_fault``, ``rvfi_mem_fault_rmask`` and
``rvfi_mem_fault_wmask`` signals. When the ``mcause`` CSR is exposed via
RVFI, this will also check that it is correctly updated on a memory
fault.

.. _depth-section-5:

``[depth]`` section
^^^^^^^^^^^^^^^^^^^

Expects two values: first is the number of cycles to reset for; second is the execution depth.

Cover
~~~~~

A formal check using ``cover()`` SystemVerilog statements for various
interesting RVFI events or sequences of events. The purpose of this
formal check is to collect some data about the required bounds to reach
certain states to set the bounds for the other bounded model checks.
This check can also be used for creating witness traces, for example to
examine the conditions under which a specific CSR bit goes high.

.. _depth-section-6:

``[depth]`` section
^^^^^^^^^^^^^^^^^^^

Expects two values: first is the number of cycles to reset for; second
is the execution depth.

``[cover]`` section
^^^^^^^^^^^^^^^^^^^

All code in this section is included verbatim in the file
``cover_stmts.vh``, which is included verbatim in
``checks/rvfi_cover_check.sv``, and so should be valid System Verilog
code.

Standard bus checks
-------------------

The following checks are managed by ``genchecks.py`` and can be
implemented using the standard RVFI wrapper interface when implementing
the RVFI_BUS extension.

Instruction bus memcheck
~~~~~~~~~~~~~~~~~~~~~~~~

The ``bus_imem`` check adds a memory abstraction that only emulates a
single word of memory (at an unconstrained address). This memory word is
read-only and has an unconstrained value. The check makes sure that
instructions fetched from this memory word are handled correctly and
that the data from that memory word makes its way into ``rvfi_insn``
unharmed.

When the granularity of access faults as observed from the core is
coarser than the width of the bus, ``RISCV_FORMAL_FAULT_WIDTH`` needs to
be defined and set to the corresponding width in bytes. E.g. for a setup
where a single word fault the monitored bus means that from the
perspective of the core, any access of the corresponding cache line will
fault, you would define ``RISCV_FORMAL_FAULT_WIDTH`` to be the width of
a cache line in bytes.

Instruction bus fault memcheck
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The ``bus_imem_fault`` check adds a memory abstraction that has a single
always faulting word of memory (at an unconstrained address). The check
makes sure that executing from this address causes an “instruction
access fault” trap.

The RVFI signalling for the instruction with a faulting fetch requires
an all-zero ``rvfi_insn`` value with ``rvfi_trap`` set. When
``RISCV_FORMAL_MEM_FAULT`` is defined the associated signals must also
be set correctly.

Data bus memcheck
~~~~~~~~~~~~~~~~~

This ``bus_dmem`` check adds a memory abstraction that only emulates a
single word of memory (at an unconstrained address). The memory word is
read/write. The check tests if writes to and reads from the memory
location (as reported via RVFI) are consistent. Additionally it checks
that an initial value as reported via RVFI matches the fetched value on
the bus. This check does not require writes to appear on the bus and is
thus compatible with caches between the core and the observed bus.

When the granularity of access faults as observed from the core is
coarser than the width of the bus, ``RISCV_FORMAL_FAULT_WIDTH`` needs to
be defined. See “Instruction Bus Memcheck” above for more details.

Data bus fault memcheck
~~~~~~~~~~~~~~~~~~~~~~~

The ``bus_dmem_fault`` check adds a memory abstraction that has a single
always faulting word of memory (at an unconstrained address). The check
makes sure that reading from or writing to this address causes a “load
access fault” or “store/AMO access fault” trap respectively.

The RVFI signalling for an instruction causing either fault has
``rvfi_trap`` and does not include a register update or memory write,
even if the instruction would have performed one if the memory access
didn't fault. When ``RISCV_FORMAL_MEM_FAULT`` is defined the associated signals must also be set correctly.

Data bus I/O checks
~~~~~~~~~~~~~~~~~~~

These checks can provide stronger guarantees on data bus accesses that
are not required to hold in general, but should often hold for i/o
memory regions. Depending on the use-case only a subset may be
applicable or some checks may only be applicable for certain areas of
the address space. The memory addresses for which these checks are run
can be configured using the ``RISCV_FORMAL_IOADDR(addr)`` macro.

Data bus I/O reads
^^^^^^^^^^^^^^^^^^

The ``bus_dmem_io_read`` check makes sure that every retired
non-faulting i/o memory read access appears as an individual read on the
bus. The whole read has to appear on its own in a single RVFI_BUS cycle.
A read is allowed to also read adjacent bytes within the same RVFI_BUS
cycle.

Data bus I/O read faults
^^^^^^^^^^^^^^^^^^^^^^^^

The ``bus_dmem_io_read_fault`` check makes sure that every retired
faulting i/o memory read access appears as an individual faulting read
on the bus.

Data bus I/O writes
^^^^^^^^^^^^^^^^^^^

The ``bus_dmem_io_write`` check makes sure that every retired
non-faulting i/o memory write access appears as an individual write on
the bus. The whole write has to appear on its own in a single RVFI_BUS
cycle and may not write any additional adjacent bytes.

Data bus I/O write faults
^^^^^^^^^^^^^^^^^^^^^^^^^

The ``bus_dmem_io_write_fault`` check makes sure that every retired
faulting i/o memory write access appears as an individual faulting write
on the bus.

Data bus I/O ordering
^^^^^^^^^^^^^^^^^^^^^

The ``bus_dmem_io_order`` check makes sure that all i/o memory accesses
appear in-order on the bus. This is done by checking that every pair of
adjacent i/o memory accesses (as observed via RVFI) corresponds to
adjacent i/o memory accesses on the bus. Non-i/o accesses are ignored by
this check, so they can be arbitrarily reordered relative to i/o
accesses and relative to each other.

.. _proc-csrs:

CSR checks
----------

The following checks are managed by ``genchecks.py`` and can be
implemented using the standard RVFI wrapper interface. All checks
operate on one channel at a time and may not work correctly if a CSR is
able to be modified by more than one channel.

CSR instruction check
~~~~~~~~~~~~~~~~~~~~~

The ``csrw`` check validates that CSR instructions modify the correct
rvfi signal ports. ``RISCV_FORMAL_CSRW_NAME <csrname>`` must be defined
for the CSR under test, along with
``csr_{m,s,u}index_<csrname> <csraddr>``. If the CSR has a corresponding
'h' register containing the upper bits, ``RISCV_FORMAL_CSRWH`` and
``csr_{m,s,u}indexh_<csrname> <csraddr>`` should also be defined.

As per the standard CSR address mapping convention: the top two bits
(csr[11:10]) indicate whether the register is read/write (00, 01, or 10)
or read-only (11); and the next two bits (csr[9:8]) encode the lowest
privilege level that can access the CSR.

A valid read instruction must assign ``rvfi_csr_<csrname>_rdata`` to
``rvfi_rd_wdata``, as well as the correct ``rvfi_rd_addr``. A valid
write instruction must assign the correct value to
``rvfi_csr_<csrname>_wdata``. And any illegal accesses should result in
a trap.

Illegal CSR access
~~~~~~~~~~~~~~~~~~

The ``csr_ill`` check validates illegal access exceptions are raised for
access to CSRs which are not available through the RVFI wrapper
interface, including those which may not be implemented.
``RISCV_FORMAL_ILL_CSR_ADDR <csraddr>`` must be defined for the CSR
under test. Defining ``RISCV_FORMAL_ILL_{M,S,U}MODE`` specifies which
modes should be tested for access, and ``RISCV_FORMAL_ILL_{WRITE,READ}``
specifies what accesses are expected to be illegal.

CSR consistency checks
~~~~~~~~~~~~~~~~~~~~~~

These checks perform multiple reads/writes and compare the values on
``rvfi_csr_<csrname>_rdata`` and ``rvfi_csr_<csrname>_wdata`` during the
``check`` cycle.

In each case, ``RISCV_FORMAL_CSRC_NAME <csrname>`` must be defined for
the CSR under test, along with the corresponsing
``csr_{m,s,u}index_<csrname> <csraddr>``.

CSR write-any
^^^^^^^^^^^^^

The ``csrc_any`` check tests whether any value written to a CSR is then
able to be read-back exactly as written.

CSR increments
^^^^^^^^^^^^^^

The ``csrc_inc`` check tests whether the value in a CSR is always
greater than or equal to a previous read/write of the csr. By
constraining the most significant bit to be 0, this check can verify
that the value of a CSR can never decrease except by writing to it.
This is particularly useful for hardware performance monitors.

CSR up-counter
^^^^^^^^^^^^^^

The ``csrc_upcnt`` check is similar to the CSR increments check but with
more constraints.  First, no writes of the csr under test are allowed.
Second, the test value *must* be greater than the previously read value.
Without fairness guarantees this has limited use, but can verify some
hpm functions, especially ``mcycle`` and ``minstret``.

CSR hpm event cover check
^^^^^^^^^^^^^^^^^^^^^^^^^

Unlike most of the other checks, ``csrc_hpm`` is a cover check.
Similarly to the CSR up-counter check, the value of a hpm counter CSR is
compared with a previously stored value and must increase. However,
because this is a cover check this tests that the CSR *can* increase,
not that it *must* increase.  Used in conjunction with a ``csrc_inc``
test of the corresponding hpm counter CSR, this can verify that the hpm
is able to increase and unable to decrease.

This check must be performed on a hpm event CSR, with
``RISCV_FORMAL_CSRC_NAME mhpmevent#`` and ``RISCV_FORMAL_CSRC_HPMCOUNTER
mhpmcounter#``.  The event must be defined by
``RISCV_FORMAL_CSRC_HPMEVENT <value>``.  Note that both
``RISCV_FORMAL_CSR_MHPMCOUNTER#`` and ``RISCV_FORMAL_CSR_MHPMEVENT#``
must be defined and the corresponding rvfi signals connected.

CSR read-constant
^^^^^^^^^^^^^^^^^

The ``csrc_const`` check tests whether the value in a CSR is always the
same, ignoring any value which may be written.
``RISCV_FORMAL_CSRC_CONSTVAL <value>`` must be defined as the value to
be expected. For CSRs which can take any value so long as it remains
constant during operation, a value of ``rdata_shadow`` can be assigned
which will compare with the previously read value.

CSR read-zero
^^^^^^^^^^^^^

The ``csrc_zero`` check is similar to the CSR read-constant check, but
exclusively tests for a constant value of all zero.

genchecks config
~~~~~~~~~~~~~~~~

.. _depth-1:

``[depth]``
^^^^^^^^^^^

The ``csrw`` and ``csr_ill`` checks expect one value, indicating the
maximum depth of the Bounded Model Checker (BMC).

All ``csrc_*`` checks expect two values, with the first being the number
of cycles to hold reset for, and the second being the maximum depth of
the BMC.

Depth can be specified for all tests of one type, e.g. \ ``csrc_zero``,
or individual to a particular CSR, e.g. \ ``csrw_mcycle``.

Any test without a corresponding value in the ``depth`` section will not
be run.

``[csrs]``
^^^^^^^^^^

The ``csrs`` config section lists all standard CSRs which can be tested.
By default, all CSRs will be run through the CSR instruction check
(``csrw``). Consistency checks can be defined as a space seperated list
after the csr name. For checks which expect a value, using quotation
marks will allow for verbatim values.

e.g. \ ``misa zero const="32'h 0"`` declares two tests for the ``misa``
CSR. First using the ``csrc_zero_check``, and then using the
``csrc_const_check`` with ``RISCV_FORMAL_CSRC_CONSTVAL`` defined as
``32'h 0``.

Each named CSR must be connected as described in the :doc:`rvfi`.

Consistency checks can be appended with ``_mask=`` with a verilog
expression which will be applied to the CSR as a bit mask before testing
the return value. Note that ``_mask`` must be defined *after* any other
value assignment for the check. For example, the statement
``misa const=0_mask="32'h 0aaa_ffff"`` masks the ``misa`` CSR and then
checks for a constant value of 0. A mask value is currently only
supported in the ``const``, ``zero``, and ``any`` checks.

``const`` supports value assignment, while ``hpm`` requires it.  If no
value is provided for ``const``, a value of ``rdata_shadow`` will be
assigned such that any value is accepted provided it is constant. In the
case of ``hpm`` the value is assigned to the hpmevent register prior to
testing if the hpmcounter register is able to increase.

``[custom_csrs]``
^^^^^^^^^^^^^^^^^

Platform defined CSRs can be included for testing in the ``custom_csrs``
section. Each line is a space separated list of values defining one CSR
and the corresponding tests. The first value is the CSR address in
hexadecimal, and the second value is the privilege modes in which the
CSR is available. The rest of the line follows the same format as the
``csrs`` config section with the CSR name followed by any tests in
addition to ``csrw``.

e.g. \ ``fc0 m custom_ro const="32'h dead_beef"`` defines a CSR in the
machine-level custom read-only address space at address ``0xFC0`` called
``custom_ro`` which can be accessed from machine mode and should be
tested for a constant value of ``0xdeadbeef`` using
``csrc_const_check``.

As with the standard CSRs, each of the custom CSRs must be connected
through the RVFI wrapper.

Note that the privilege modes defined will not prevent the CSR
instruction check from expecting an illegal access exception based on
the address.

``[illegal_csrs]``
^^^^^^^^^^^^^^^^^^

The ``illegal_csrs`` section lists unnamed CSRs not available through
the RVFI wrapper interface. Each line lists one CSR address to be tested
with ``csr_ill``, along with the relevant modes to check. Three space
separated values are expected; the first provides the address in
hexadecimal, the second is the privilege modes to test, and the third
indicates whether to test reads and writes or just writes.

e.g. \ ``fff msu rw`` defines a test at address oxFFF for machine,
supervisor, and user modes which should cause an illegal access
exception on both reads and writes.

CSR spec test generation
^^^^^^^^^^^^^^^^^^^^^^^^

By setting ``csr_spec`` in the ``options`` section, it is possible to
automatically generate tests for all CSRs to match the specification
recommendations/requirements. This option will add all defined CSRs to
be tested under ``csrw`` as well as generating corresponding ``csrc``
tests where relevant. For those CSRs which should only exist in certain
conditions, e.g. if U mode is available, then those CSRs are included if
the ``isa`` option includes them, otherwise the addresses are checked as
being an expected illegal access exception. Optional CSRs are not
automatically tested and will need to be specified as described above.
CSRs which are defined with certain bits being reserved for future use
(either WPRI or WARL) are tested as being constant zero, masking for
just the reserved bits.

At present the only supported value for ``csr_spec`` is ``1.12``,
corresponding to version 1.12 of the Machine ISA, as defined in the
20211203 Priveleged Architecture document.

Other checks
------------

The following checks are not yet managed by ``genchecks.py`` and can not
be implemented using the standard RVFI wrapper interface. Some of them
may be integrated with ``genchecks.py`` in the future.

Instruction memcheck
~~~~~~~~~~~~~~~~~~~~

This check adds a memory abstraction that only emulates a single word of
memory (at an unconstrained address). This memory word is read-only and
has an unconstrained value. The check makes sure that instructions
fetched from this memory word are handled correctly and that the data
from that memory word makes its way into ``rvfi_insn`` unharmed.

See ``imemcheck.sv`` in ``cores/picorv32/`` for an
example implementation.

This check is superseded by the equivalent standard bus check above.

Data memcheck
~~~~~~~~~~~~~

This check adds a memory abstraction that only emulates a single word of
memory (at an unconstrained address). The memory word is read/write. The
check tests if writes to and reads from the memory location (as reported
via RVFI) are consistent.

See ``dmemcheck.sv`` in ``cores/picorv32/`` for one
possible implementation of this test.

This check is superseded by the equivalent standard bus check above.

Checking for equivalence of core with and without RVFI
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

An equivalence check of the core with and without RVFI (with respect to
the non-RVFI outputs) is performed. This proves that the verification
results for the core with enabled RVFI also prove that the (non-RVFI)
production core is correct without extra burden on the core designer to
isolate the RVFI implementation from the rest of the core.

See ``equiv.sh`` in ``cores/picorv32/`` for an
example implementation.

Complete
~~~~~~~~

An additional check to make sure the core can not (without trap) retire
any instructions that are not covered by the riscv-formal instruction
checks.

See ``complete.sv`` in ``cores/picorv32/`` for one
possible implementation of this test.

Verification of riscv-formal models against spike models
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The checks in ``tests/spike/`` use the Yosys SimpleC back-end and CBMC
to check the ``riscv-formal`` models and the C instruction models from
spike for equivalence.
