Quality assurance component

• Input component
• QualityAssurance component
• Approximation component
• Estimation component
• Search component
• Output

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 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 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.

Overview of CIRCA’s sequential quality constraint circuit (SQCC) (left) and a detailed view of the quality evaluation circuit (QEC).

(Open the PDF here 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 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:

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.

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.

---

Back to the User Guide