=========================== Quality assurance component =========================== * :ref:`Input component ` * **QualityAssurance component** * :ref:`Approximation component ` * :ref:`Estimation component ` * :ref:`Search component ` * :ref:`Output ` .. QualityAssurance component .. ========================== .. _user_guide_qa: Component description --------------------- The *QualityAssurance* component is responsible for the validation of approximated circuits, i.e., checking if the circuits resulting from the approximation process satisfy the specified quality constraints. Generally, we distinguish between testing-based approaches and formal approaches. Testing-based approaches evaluate the quality of a circuit by applying a set of input vectors (or input sequences for sequential circuits). However, testing-based approaches are usually not able to adopt all possible input vectors; thus, the error of a circuit (or its quality) can only be estimated. Formal verification methods, on the other side, are able to provide a mathematical prove to guarantee that the circuit adheres to the specified error bounds. This guarantee, however, often comes at costs of higher runtimes. CIRCA supports testing-based approaches as well as formal methods. Currently, however, only formal methods are provided: ``abc_dprove``, ``abc_pdr``, and ``yosys_ic3``. The three approaches utilize the inductive solvers of the external programs `ABC `_ and `Yosys `_. abc_dprove, abc_pdr, and yosys_ic3 ---------------------------------- CIRCA's standard quality assurance implementations proceed in the same way to verify the quality of a circuit: they generate a so-called *sequential quality constraint circuit* (*SQCC*) (see :ref:`figure below (left) `) and apply a formal verification method on it, i.e., ABC's dprove, ABC's PDR, or Yosys' IC3. The SQCC comprises of the original input circuit, the circuit-under-test (*CUT*), the quality evaluation circuit (QEC), and three configurable blocks. The QEC compares the output of the original circuit and the CUT (see :ref:`figure below (right) `). Error bounds encoded in the QEC evaluate the error of the CUT, e.g., worst-case error (WC), and the results of all evaluations are OR-ed to produce a single output bit, the *error'* signal. The *error'* signal signals an error bound violation if at least one error bound is violated. The three configurable blocks (*start sequence*, *Capture block*, and *Output block*) enable CIRCA to support different circuit types, e.g., streaming or run-to-completion. The Start sequence block can implement a commonly used startup protocol (a reset signal followed by a start signal) to reduce the runtime of the verification by reducing the number of possible states and state transitions. The Capture block ensures that only the valid output signals of the circuits are evaluated by the QEC. The output signal of the QEC is only made present at the output of the SQCC, if the signal is valid. This is ensured by the Output block. .. todo: Fix link to pdf .. figure:: ../images/circa_sqcc_qec.pdf :alt: circa_sqcc_qec.pdf :name: circa_sqcc_qec Overview of CIRCA's sequential quality constraint circuit (*SQCC*) (left) and a detailed view of the quality evaluation circuit (*QEC*). (`Open the PDF here <../_static/circa_sqcc_qec.pdf>`_ if it is not displayed.) For more information, please read the `paper on CIRCA `_. Configuration options --------------------- The three implementations use the SQCC, and thus, share the same parameter set. :``Medthod``: ``abc_dprove``, ``abc_pdr``, or ``yosys_ic3`` :``QualityConstraints``: The global error bounds and steps which will be applied to the whole circuit. At least one error metric must be listed and each error metric must have a ``bound`` specified. The ``step`` parameter is optional and the error metric's default step size will be used if it is left out. The syntax of quality constraint specifications is described in the :ref:`user guide's subsection about the configuration file `. All error metrics mentioned there are supported. :``CircuitType``: The circuit type of the input circuit. Supported circuit types are ``combinational``, ``run_to_completion`` and ``streaming``. :``OutputSignal``: The case-sensitive name of the circuit's primary output signal. Any string that is a valid signal name in Verilog is permitted. :``OutputIsSigned``: Set to ``1`` if the circuit's primary output signal is signed, and to ``0`` if it is not. :``ValidSignal``: (optional for each ``CircuitType`` except ``run_to_completion``) The case-sensitive name of the circuit's signal that signals valid data at the output. :``OutputSignalConcat``: (optional) If the circuit's output signal is a concatenation of multiple signals, you can specify a list of *msb*-*lsb* pairs. The pairs are separated by ``,`` with optional whitespace. A pair-entry must contain two integer numbers separated by any non-integer character other than ``,``. Example: .. code-block:: none OutputSignalConcat = [31:16], [15:0] :``ResetSignal``: (optional) The case-sensitive name of the circuit's reset signal. :``ResetSignalIsHighActive``: (mandatory if ``ResetSignal`` is specified) Set to ``1`` if the circuit's reset signal is high-active and to ``0`` if it is low-active. :``StartSignal``: (optional) The case-sensitive name of the circuit's start signal. :``StartSignalIsHighActive``: (mandatory if ``StartSignal`` is specified) Set to ``1`` if the circuit's start signal is high-active and to ``0`` if it is low-active. .. admonition:: Notes and restrictions * The circuit type, the name of the output signal, and the information whether it is signed or not must be supplied in the configuration file. * If the circuit type is ``run_to_completion``, the circuit must have a valid signal. This is an unsigned output signal of size 1 which assumes the logic value ``1`` as soon as the circuit's computation is completed. Its name must be specified in the configuration file. ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ :ref:`Back to the User Guide `