Recent Findings in Boolean Techniques

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.

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.

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.

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.

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.

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.

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.

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.