14th International Workshop on Boolean Problems | Times are in CEST (Central European Summer Time)
Proceedings: Download


Thursday | September 24

16:30 - 16:45 Opening

16:45 - 17:45 | Keynote 1
Chair: Daniel Große

Formal Verification of Integer Multiplier Circuits using SAT and Computer Algebra
Dr. Daniela Kaufmann, Johannes Kepler University Linz, Austria

Digital circuits are extensively used in computers and digital systems and it is of high importance to guarantee that these circuits are correct in order to prevent issues like the famous Pentium FDIV bug. Formal verification can be used to derive the correctness of a given circuit with respect to a certain specification. However arithmetic circuits, and most prominently gate-level multipliers, impose a challenge for existing verification techniques. Approaches which purely rely on SAT solving or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. Currently one of the most effective techniques is based on algebraic reasoning. In this approach the circuit is modeled as a set of pseudo-Boolean polynomials and the word-level specification is reduced by a Gröbner basis which is implied by the polynomial representation of the circuit. However parts of the multiplier, i.e., final stage adders, are hard to verify using computer algebra. In our approach we combine SAT and computer algebra to substantially improve automated verification of integer multipliers. Complex final stage adders are detected and replaced by simple adders. The correctness of the replacement is verified by SAT solvers and the simplified multiplier is verified by computer algebra techniques. Nonetheless the verification process might not be error-free. Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. In order to validate verification results we show how proof certificates can be obtained as a by-product of verifying multiplier circuits in our reduction engine, which can be checked with our independent proof checker tool.

17:45 - 19:05 | Session 1
Chair: Gerhard Dueck

Constant multiplication based on Boolean minimization
Danila Gorodecky and Petr Bibilo

Fast Optimal Synthesis of Symmetric Index Generation Functions
Bernd Steinbach and Christian Posthoff

The First-Order Theory of Boolean Differentiation
Felix Weitkämper

Construction of Binary Bent Functions by FFT-like Permutation Algorithms
Radomir S. Stankovic, Milena Stankovic, Claudio Moraga and Jaakko Astola

Friday | September 25

16:30 - 17:30 | Keynote 2
Chair: Rolf Drechsler

Reliability Challenges in upcoming Sub-7nm Technologies and Future Computing in Emerging Technologies
Junior Professor Dr. Hussam Amrouch, University of Stuttgart, Germany

The inability of transistors to switch faster than 60mV/decade is the fundamental limit in physics for technology scaling, which prevents the continuation of Dennard's scaling. As a result, on-chip power densities continuously increase with every new generation leading to excessive temperatures that seriously degrade the reliability of chips. In addition, technology scaling is reaching limits in which displacing few atoms within transistors, due to aging phenomena, provokes uncertainty that may cause catastrophic errors during operation. Due to the inevitable need to include wider and wider guardbands towards sustaining reliability for the entire projected lifetime, the customary trend in which performance is gained with technology scaling becomes profound, if not impossible.

In this talk, we will demonstrate how reliability degradations can be investigated from physics, where they do originate, all the way up to the system level, where they ultimately cause errors. We will show how we can bring reliability awareness to existing commercial EDA tool flows in order to contain guardbands. We will also demonstrate how nondeterministic aging-induced errors can be translated into deterministic and controlled approximations instead, allowing designers to narrow or even remove their guardbands.

Finally, we will discuss how Negative Capacitance Field-Effect Transistor (NCFET), which is a recent emerging technology that suppresses the fundamental limit of 60mV/decade, can reshape the future trends in processor design and rescue technology scaling.

17:30 - 18:50 | Session 2
Chair: Oliver Keszocze

Graph methods for extracting logical networks from transistor circuits
Dmitry Cheremisinov and Liudmila Cheremisinova

Nonlinear codes for test patterns compression: the old school way
Jan Schmidt and Petr Fišer

A Preliminary Study of Transformation Based Synthesis of Reversible Circuits with Positive and Negative Controls
Michael Miller and Gerhard Dueck

Hybrid Control of Toffoli and Peres Gates
Caudio Moraga