Formal Methods for Exact Analysis of Approximate Circuits

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F19%3APU134968" target="_blank" >RIV/00216305:26230/19:PU134968 - isvavai.cz</a>

Result on the web

<a href="https://www.fit.vut.cz/research/publication/12133/" target="_blank" >https://www.fit.vut.cz/research/publication/12133/</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/ACCESS.2019.2958605" target="_blank" >10.1109/ACCESS.2019.2958605</a>

Result language

angličtina

Original language name

Formal Methods for Exact Analysis of Approximate Circuits

Original language description

Approximate circuits are digital circuits that are intentionally designed in such a way that the specification is violated in terms of functionality in order to obtain some improvements in power consumption, performance or area, in comparison with fully functional circuits.  To design the approximate circuits, the synthesis tools rely on the availability of a procedure checking, whether the synthesized circuits meet a specification and/or provides information about circuit quality. Compared to the traditional circuit design flow, the nature of the approximate circuits involves replacing the strict functional equivalence checking with a more advanced approach that enables us to quantify or guarantee the degree of similarity. The most common technique is to employ a circuit simulator for analysing responses for all input vectors. This approach allows us to simultaneously perform checking and quality assessment, but the exhaustive enumeration of the input vectors is tractable only for a small number of inputs. To avoid excessive run-times, a subset of all possible input vectors is typically used for complex circuits. This causes us, however, to lose the ability to guarantee that the quality of the synthesized circuits is within an acceptable range given in the specification.  The main goal of this paper is to show how to adopt formal methods such as binary decision diagrams and satisfiability solvers for exhaustive analysis of approximate circuits without explicit enumeration of all input vectors. We survey the methods for exact computation of the most important error parameters used in the context of approximate computing, propose improved algorithms and provide a detailed analysis of their performance.  The methods are benchmarked on a large set of key approximate circuits consisting of nearly 2,000 unique arithmetic instances with 8-, 12-, 16-, and 32-bit operands which helps us to identify the best algorithm and method for computation of a

Czech name

—

Czech description

—

Type

J_imp - Article in a specialist periodical, which is included in the Web of Science database

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GA19-10137S" target="_blank" >GA19-10137S: Designing and exploiting libraries of approximate circuits</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2019

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

IEEE Access

ISSN

2169-3536

e-ISSN

—

Volume of the periodical

7

Issue of the periodical within the volume

1

Country of publishing house

US - UNITED STATES

Number of pages

23

Pages from-to

177309-177331

UT code for WoS article

000509405300071

EID of the result in the Scopus database

2-s2.0-85077180957