Go to page

Bibliographic Metadata

Links
Abstract

Approximate computing hat sich als ein Weg herauskristallisiert, die Verarbeitungsleistung von Rechensystemen weiter zu steigern, indem die Qualität einer Anwendung gegen eine Zielmetrik eingetauscht wird. Diese Dissertation betrachtet approximate computing auf der Hardwareebene, auf der es approximierte Schaltungen generiert und als approximate logic synthesis (ALS) bezeichnet wird. Konkret leistet die Arbeit fünf Beiträge und betrachtet automatisierte, suchbasierte ALS Prozesse, die in vier Schritten modelliert werden: suchen, approximieren, verifizieren und abschätzen. Zunächst stellt die Dissertation das Framework CIRCA vor, das den ALS Prozess allgemeingültig und konfigurierbar implementiert und so eine Umgebung für den Vergleich von ALS Methoden bereitstellt. Anschließend wird das Suchverfahren jump search diskutiert, das approximierte Schaltungen schnell generiert, indem es Synthesen und Verifikationen mittels Domänenwissen minimiert. Des Weiteren wird die Approximationstechnik MUSCAT vorgestellt, die auf formaler Verifikation basiert und Schaltungen hinsichtlich ihrer Qualität korrekt konstruiert. Ferner betrachtet die Arbeit den Verifikationsschritt und stellt das Konzept von proof-carrying approximate circuits vor, das die Felder approximate computing und proof-carrying hardware vereint. Abschließend behandelt die Arbeit ein auf formaler Verifikation basierendes Verfahren, das vorab den Suchraum von approximierten Schaltungen für den ALS Prozess charakterisiert.

Abstract

Approximate computing has emerged as one way to meet the challenge of improving a computing systems performance by trading off an applications quality against a target metric. This dissertation focuses on approximate computing at hardware level, where it is referred to as approximate logic synthesis (ALS) and has the goal of generating approximate circuits; specifically, this dissertation makes five contributions and comprehensively considers automated search-based ALS processes that are modeled with four main steps: search, approximate, verify, and estimate. Firstly, this dissertation contributes the CIRCA framework that implements a general and fully configurable ALS process to provide an environment for comparing different ALS methods. Secondly, we propose the jump search methodology that minimizes syntheses and verifications by exploiting domain knowledge to rapidly generate approximate circuits. Thirdly, the technique MUSCAT contributes to the approximation step and utilizes formal verification techniques to construct approximate circuits that are valid-by-construction regarding their quality. The fourth contribution considers the verification step and is the concept of proof-carrying approximate circuits, which brings together the fields of approximate computing and proof-carrying hardware. Finally, this dissertation proposes a formal verification-based methodology that characterizes the search space of approximate circuits prior to the ALS process.