Skip to main content

About this book

This book describes recent findings in the domain of Boolean logic and Boolean algebra, covering application domains in circuit and system design, but also basic research in mathematics and theoretical computer science. Content includes invited chapters and a selection of the best papers presented at the 14th annual International Workshop on Boolean Problems.

Table of Contents


Formal Verification of Integer Multiplier Circuits Using Algebraic Reasoning: A Survey

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 multipliers, impose a challenge for existing verification techniques. 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. The circuit is correct if and only if the final result is zero. 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 this paper we survey the current state of the art of this work. We give an overview over recent solving techniques, available benchmarks, and include a comprehensive evaluation.
Daniela Kaufmann

The Vital Role of Machine Learning in Developing Emerging Technologies

In this chapter, we demonstrate how Machine Learning (ML) approaches play a major role when it comes to developing emerging technologies that go beyond the existing CMOS technology. As an example of such emerging technologies, we focus on the Negative Capacitance Field-Effect Transistor (NC-FET) technology, which is rapidly evolving and attracting a significant attention from both industry and academia. This is due to its ability to suppress one of the fundamental limit in technology scaling related to Boltzmann’s tyranny. The vital role that machine learning will play stems from overcoming the following key challenges. (1) The secrecy of foundries with respect to their new transistor compact models and standard cell information, (2) The difficulties in creating mature physics-based models for emerging technologies especially at the early stages of the development cycle, and (3) accelerating the Design-Technology Co-Optimization (DTCO) process. In the following, we demonstrate how ML can be employed to replace mature transistor compact model as well as to replace complex standard cell library characterization. Such ML models, trained at the foundry side, allow later designers to investigate how the new emerging technology impacts the efficiency of their circuits without the need to expose and unveil either the confidential information of transistor modeling or the standard cell netlists. We also demonstrate how such trained ML models enable circuit designers to perform rapid design-space exploration (due to the very fast inference), which is essential during DTCO towards bringing any emerging technology to a more mature level. Our presented ML approaches provide transistor modeling with 95% accuracy and standard cell characterization with 98% accuracy.
Victor M. van Santen, Florian Klemme, Hussam Amrouch

Fast Optimal Synthesis of Symmetric Index Generation Functions

Index generation functions are needed in many applications to reduce the number of variables used to select the related result. Examples of such applications are switches that route the packages of the internet, the detection of viruses of computers, or the analysis of DNA sequences. Several approaches have been suggested to find the decomposition into the linear part L and the general part G of circuits for the special case of symmetric index generation functions \(S^n_1(\mathbf {x})\). Recently an approach for this task has been published by Nagayama et al. that found exact solutions much faster than known approaches, but is also limited in the number n of variables of the symmetric function due to the needed computation time. In this chapter, we suggest an approach that solves the same task in such a short time (less than 1 μs for n = 1, 000, 000, 000) so that no restriction in the number n of variables x of the decomposed symmetric functions \(S^n_1(\mathbf {x})\) must be taken in to account anymore. We created extremely fast algorithms using our already published method of a very deep analysis of the given problem.
Bernd Steinbach, Christian Posthoff

Axiomatizing Boolean Differentiation

In this chapter, we give a complete axiomatization of Boolean differentiation. More precisely, for each \(n\in \mathbb {N}\) and each Boolean algebra K, we will state axioms that determine up to isomorphism the Boolean algebra with n linearly independent derivatives δ i with \(\stackrel [i=1]{n}{\bigcap }\ker (\delta _{i})\cong K\). Furthermore, we give a complete first-order theory \(T_{n}^{K}\) of n Boolean derivatives where \(\stackrel [i=1]{n}{\bigcap }\ker (\delta _{i})\) is a model of the theory T K. These theories can be obtained by adding just a finite list of axioms to those of T K, and any model of T K extends uniquely to a model of \(T_{n}^{K}\). Moreover, we will also provide a theory of the additive reduct equipped with n Boolean derivatives, and we will see that these theories are categorical in every infinite cardinality. We then show that the theories are indeed the asymptotic theories of the class of the algebras of switching functions equipped with any of the ordinarily used notions of derivative. Furthermore, we see that for the case n = 1, they also axiomatize the Fraisse limit of the finite switching functions with a derivative, and we use this fact to deduce quantifier elimination.
Felix Weitkämper

Construction of Binary Bent Functions by FFT-Like Permutation Algorithms

The set of all binary bent functions in a given number of variables can be split into two subsets with respect to the two possible numbers of non-zero values in their truth-vectors. Functions in a subset are mutually related by permutations. By knowing the structure of the permutation matrices expressing these permutations, bent functions in a subset can be derived from each other by permuting their truth-vectors. In this chapter, we point out that permutation matrices relating bent functions with the same number of non-zero values have a structure that corresponds to the structure of sparse factor matrices describing steps in the Good-Thomas decomposition of the Cooley-Tukey fast Fourier transform (FFT). This observation opens a way for fast constructing different bent functions from a given bent function by using either vectors or decision diagrams as underlying data structures to perform permutations.
Radomir S. Stanković, Milena Stanković, Claudio Moraga, Jaakko Astola

Nonlinear Codes for Test Patterns Compression: The Old School Way

The problem is to design a nonlinear code for test vectors expander, with the requirement of all r-tuples possible in the output. We formulated the problem as a clique cover problem. The instances of the problem have a high degree of symmetry, which offers the possibility of analytical solution or better heuristic construction. To benefit from the degrees of freedom in the problem, assigning expander inputs to the produced vectors has been identified as a multi-valued (MV) variable encoding problem. Experimental evaluation shows that good MV encoding is important for small r. Instances up to n = 32 and r = 6 were solved, with the resulting expander widths i mostly equal to or better than existing solutions. For the synthesis of the expanders, both the classical minimization-decomposition and resynthesis approaches can be used. The produced circuits were larger than corresponding linear expanders.
Jan Schmidt, Petr Fišer

Translation Techniques for Reversible Circuit Synthesis with Positive and Negative Controls

This chapter presents translation techniques that can be applied to a reversible Boolean function to enhance the synthesis of a reversible circuit with positive and negative controls realizing that function. A mapping inverting selected input-output pairs and a second mapping involving the permutation of input-output pairs are introduced. Peres gates are generalized to have negative as well as positive controls, and techniques for simplifying reversible circuits with positive and negative controls are examined.
Experimental results for all 3-variable reversible functions and for selected worst case functions are presented and evaluated with regard to quantum circuit realization using the NCV quantum gate library. The experiments are conducted using various forms of transformation-based synthesis including a novel search-based approach. The results show the methods presented have promise and should likely be considered for use with more sophisticated reversible circuit synthesis methods.
D. Michael Miller, Gerhard W. Dueck

Hybrid Control of Toffoli and Peres Gates

Toffoli and Peres reversible gates are known to operate based on the conjunction of the control signals. It will be recalled that a disjunctive control is also possible although not well known. The main focus of the chapter will be on the realization of these gates, which at least at the symbolic level will have a mixture of conjunctive and disjunctive control. This will be called hybrid control. Straightforward realizations as well as efficient realizations based on a Barenco et al. type quantum model will be presented. Some aspects of scalability will be discussed.
Claudio Moraga

GenMul: Generating Architecturally Complex Multipliers to Challenge Formal Verification Tools

Despite the success of formal verification methods in the last 20 years, the proof of correctness of arithmetic hardware blocks involving multiplication still drives the verification tools into their limits. At the moment, the most promising methods for verification are based on Symbolic Computer Algebra (SCA), and they have shown very good results even for large and architecturally complex multipliers. To allow the community a broad comparison when verifying different multiplier architectures, open, configurable, and scalable multiplier benchmarks are needed.
In this chapter, we present the multiplier generator GenMul, which outputs multiplier circuits in Verilog. The input size of a multiplier and each multiplier stage can be configured with GenMul. In addition, GenMul is open source under MIT-license to ease for adding new architectures. Overall, this allows to challenge formal methods as shown by experiments which compare recent verification approaches.
Alireza Mahzoon, Daniel Große, Rolf Drechsler


Additional information