Abstract Using Symbolic Computer Algebra (SCA) enabled a huge progress in formal verification of arithmetic circuits in recent years. Several different approaches have been proposed showing great success especially for the verification of multipliers. Some of them are based on precomputing and simplifying polynomials for specific circuit structures like converging cones while others take advantage of known or detected hierarchy information to replace and simplify particular subcircuits of the design. In this paper we propose a new method that avoids the use of such methods and applies only two dynamic approaches: (1) choosing a good substitution order for the backward rewriting process and (2) adjusting the phases of signals occurring in the intermediate polynomials during the verification process. Both methods are simply based on a greedy local search taking the sizes of intermediate polynomials into account. Our experimental results show that this method is very competitive with already existing tools and it improves their robustness, e.g. against optimizations of the verified circuits using logic synthesis.

Abstract Recent methods based on Symbolic Computer Algebra (SCA) have shown great success in formal verification of multipliers and—more recently—of dividers as well. In this paper we enhance known approaches by the computation of satisfiability don’t cares for so-called Extended Atomic Blocks (EABs) and by Delayed Don’t Care Optimization (DDCO) for optimizing polynomials during backward rewriting. Using those novel methods we are able to extend the applicability of SCA-based methods to further divider architectures which could not be handled by previous approaches. We successfully apply the approach to the fully automatic formal verification of large dividers (with bit widths up to 512).

In this article, we revisit the topic of generalizing proof obligations (POs) in bit-level property directed reachability (PDR). We provide a comprehensive study which: 1) determines the complexity of the problem; 2) thoroughly analyzes limitations of existing methods; 3) introduces approaches to PO generalization that have never been used in the context of PDR; 4) compares the strengths of different methods from a theoretical point of view; and 5) intensively evaluates the methods on various benchmarks from the hardware model checking as well as from AI planning.

Modular multipliers are the essential components in cryptography and Residue Number System (RNS) designs. Especially, 2n - 1 and 2n + 1 modular multipliers have gained more attention due to their regular structures and a wide variety of applications. However, there is no automated formal verification method to prove the correctness of these multipliers. As a result, bugs might remain undetected after the design phase.

If embedded systems are used in safety-critical environments, they need to meet several standards. For example, in the automotive domain the ISO 26262 standard requires that the software running on such systems does not contain unreachable code. Software model checking is one effective approach to automatically detect such dead code. Being used in a commercial product, iSAT3 already performs very well in this context. In this paper we integrate IC3 into iSAT3 in order to improve its dead code detection capabilities even further.

In this paper we build on methods based on Symbolic Computer Algebra that have been applied successfully to multiplier verification and more recently to divider verification as well. We show that existing methods are not sufficient to verify optimized non-restoring dividers and we enhance those methods by a novel optimization method for polynomials w. r. t. satisfiability don't cares. The optimization is reduced to Integer Linear Programming (ILP). Our experimental results show that this method is the key for enabling the verification of large and optimized non-restoring dividers (with bit widths up to 512).

During the last few years Symbolic Computer Algebra (SCA) delivered excellent results in the verification of large integer and finite field multipliers at the gate level. In contrast to those encouraging advances, SCA-based divider verification has been still in its infancy and awaited a major breakthrough. In this paper we analyze the fundamental reasons that prevented the success for SCA-based divider verification so far and present SAT Based Information Forwarding (SBIF). SBIF enhances SCA-based backward rewriting by information propagation in the opposite direction. We successfully apply the method to the fully automatic formal verification of large non-restoring dividers.

Formal verification methods have made huge progress over the last decades. However, proving the correctness of arithmetic circuits involving integer multipliers still drives the verification techniques to their limits. Recently, Symbolic Computer Algebra (SCA) methods have shown good results in the verification of both large and non-trivial multipliers. Their success is mainly based on (1) reverse engineering and identifying basic building blocks, (2) finding converging gate cones which start from the basic building blocks and (3) early removal of redundant terms (vanishing monomials) to avoid the blow-up during backward rewriting. Despite these important accomplishments, verifying optimized and technology-mapped multipliers is an almost unexplored area. This creates major barriers for industrial use as most of the designs are area and delay optimized. To overcome the barriers, we propose a novel SCA-method which supports the formal verification of a large variety of optimized multipliers. Our method takes advantage of a dynamic substitution ordering to avoid the monomial explosion during backward rewriting. Experimental results confirm the efficiency of our approach in the verification of a wide range of optimized multipliers including industrial benchmarks.

Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. This enables a succinct encoding of decision problems in the NEXPTIME complexity class. As solving general DQBFs is NEXPTIME complete, in contrast to the PSPACE completeness of QBF solving, characterizing DQBF subclasses of lower computational complexity allows their effective solving and is of practical importance.Recently a DQBF proof calculus based on a notion of fork extension, in addition to resolution and universal reduction, was proposed by Rabe in 2017. We show that this calculus is in fact incomplete for general DQBFs, but complete for a subclass of DQBFs, where any two existential variables have either identical or disjoint dependency sets over the universal variables. We further characterize this DQBF subclass to be ΣP3 complete in the polynomial time hierarchy. Essentially using fork extension, a DQBF in this subclass can be converted to an equisatisfiable 3QBF with only a linear increase in formula size. We exploit this conversion for effective solving of this DQBF subclass and point out its potential as a general strategy for DQBF quantifier localization. Experimental results show that the method outperforms state-of-the-art DQBF solvers on a number of benchmarks, including the 2018 DQBF evaluation benchmarks.

We describe a thoroughly interweaved forward and backward version of PDR/IC3 called fbPDR. Motivated by the complementary strengths of PDR and Reverse PDR and by related work showing the benefits of collaboration between the two, fbPDR lifts the combination to a new level. We lay the theoretical foundations for sharing information represented by learned lemmas between PDR and Reverse PDR and demonstrate the effectiveness of our approach on benchmarks from the Hardware Model Checking Competition.

Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. Driven by the needs of various applications that can be encoded by DQBFs in a natural, compact, and elegant way, research on DQBF solving has emerged in the past few years. However, most works focus on closed DQBFs in prenex form (where all quantifiers are placed in front of a propositional formula), and non-prenex DQBFs have almost not been studied in the literature. In this paper we provide a formal definition for syntax and semantics of non-closed non-prenex DQBFs and prove useful properties enabling quantifier localization. Moreover, we make use of our theory by integrating quantifier localization into a state-of-the- art DQBF solver. Experiments with prenex DQBF benchmarks, including those from the QBFEVAL'18 competition, clearly show that quantifier localization pays off in this context.

In the last few years IC3 resp. PDR attracted a lot of attention as a SAT-based hardware verification approach without needing to unroll the transition relation as in Bounded Model Checking (BMC). Motivated by different strengths of forward and backward traversal already observed in BDD based model checking and by an exponential complexity gap between original PDR and its reverted counterpart `Reverse PDR' (which starts its analysis with the initial states instead of the unsafe states as in the original PDR), we take a closer look at Reverse PDR and we present a combined forward/backward version of PDR that inherits the advantages of both original and Reverse PDR. Our experimental results on benchmarks from the Hardware Model Checking Competition demonstrate clear benefits of the combined approach.

Craig interpolation has turned out to be an essential method for many applications in formal verification. In this paper we focus on the computation of simple interpolants for the theory of linear arithmetic with rational coefficients. We successfully minimize the number of linear constraints in the final interpolant by several methods including proof transformations, linear programming, and SMT solving. Experimental results comparing the approach to standard methods from the literature prove the effectiveness of the approach and show reductions of up to 70% in the number of linear constraints.

In this work we describe a new memory management concept which allows the use of both virtual and dynamic memory management at the same time in the context of real-time systems. For a fixed size of the virtual address space, the operations of memory allocation, de-allocation and access have a constant complexity. Therefore our approach is highly suited for real-time environments with hard deadlines. We employ efficient data-structures to yield runtimes that are close to traditional static memory management concepts, and - at the same time - provide the user with the full flexibility of both virtual and dynamic memory management. Our approach is based on novel operating system components and a novel real-time aware virtual memory management unit (RTMMU) in hardware. Our experimental results demonstrate the applicability of our concept and compare its performance with a classical approach. The results show that our new approach does not only provide constant-time memory management operations, but is also able to reduce the memory footprint to a large extent.

Craig interpolation has become a powerful and universal tool in the formal verification domain, where it is used not only for Boolean systems, but also for timed systems, hybrid systems, and software programs. The latter systems demand interpolation for fragments of first-order logic. When it comes to model checking, the structural compactness of interpolants is necessary for efficient algorithms. In this paper, we present a method to reduce the size of interpolants derived from proofs of unsatisfiability produced by SMT (Satisfiability Modulo Theory) solvers. Our novel method uses structural arguments to modify the proof in a way, that the resulting interpolant is guaranteed to have smaller size. To show the effectiveness of our approach, we apply it to an extensive set of formulas from symbolic hybrid model checking.

We consider the partial equivalence checking problem (PEC), i. e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied. Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC.We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far.

We consider the problem of checking whether an incomplete design (i.e., a design containing "unknown parts", so-called Black Boxes) can still be extended to a complete design satisfying a given property or whether the property is satisfied for all possible extensions. There are many applications of property checking for incomplete designs, such as early verification checks for unfinished designs, error localization in faulty designs and the abstraction of complex parts of a design in order to simplify the property checking task. To process incomplete designs we present an approximate, yet sound algorithm. The algorithm is flexible in the sense that for every Black Box a different approximation method can be chosen. This permits us to handle less relevant Black Boxes (in terms of the property) with larger approximation and thus faster, whereas we do not lose important information when the possible effect of more relevant Black Boxes is modeled by more exact methods. Additionally, we present a concept to decide exactly whether Black Boxes with bounded memory can be implemented so that they satisfy a given property. This question is reduced to conventional symbolic model checking. The effectiveness and feasibility of the methods is demonstrated by a series of experimental results.

In this paper we present a method for integrating two complementary solving techniques for QBF formulas, i.e. variable elimination based on an AIG-framework and search with DPLL based solving. We develop a sophisticated mechanism for coupling these techniques, enabling the transfer of partial results from the variable elimination part to the search part. This includes the definition of heuristics to (1) determine appropriate points in time to snapshot the current partial result during variable elimination (by estimating its quality) and (2) switch from variable elimination to search-based methods (applied to the best known snapshot) when the progress of variable elimination is supposed to be too slow or when representation sizes grow too fast. We will show in the experimental section that our combined approach is clearly superior to both individual methods run in a stand-alone manner. Moreover, our combined approach significantly outperforms all other state-of-the-art solvers.

In this paper we present a solver for Quantified Boolean Formulas (QBFs) which is based on And-Inverter Graphs (AIGs). We use a new quantifier elimination method for AIGs, which heuristically combines cofactor-based quantifier elimination with quantification using BDDs and thus benefits from the strengths of both data structures. Moreover, we present a novel SAT-based method for preprocessing QBFs that is able to efficiently detect variables with forced truth assignments, allowing for an elimination of these variables from the input formula. We describe the used algorithm which heavily relies on the incremental features of modern SAT-solvers. Experimental results demonstrate that our preprocessing method can significantly improve the performance of QBF preprocessing and thus is able to accelerate the overall solving process when used in combination with state-of-the-art QBF-solvers. In particular, we integrated the preprocessing technique as well as the quantifier elimination method into the QBF-solver AIGSolve, allowing it to outperform state-of-the-art solvers.

This work considers the problem of minimizing the power consumption for real-time scheduling on processors with discrete operating modes. We provide a model for determining the expected energy demand based on statistical execution profiles which considers both the current and subsequent tasks. If the load after the execution of the current task is expected to be high and slack time is conserved for subsequent tasks, we are able to derive an optimal solution to the energy minimization problem. For the remaining cases we propose a heuristic approach that also achieves a low run time overhead. In contrast to previous work, our scheduling approach is not restricted to single task scenarios, frame-based real-time systems, or pre-computed schedules. Simulations and comparisons with energy-efficient schedulers from literature demonstrate the efficiency of our approach.

In this paper we present a procedure for solving quantified boolean formulas (QBF), which uses And-Inverter Graphs (AIGs) as the core data-structure. We make extensive use of structural information extracted from the input formula such as functional definitions of variables and non-linear quantifier structures. We show how this information can directly be exploited by the symbolic, AIG based representation. We implemented a prototype QBF solver based on our ideas and performed a number of experiments proving the effectiveness of our approach, and moreover, showing that our method is able to solve QBF instances on which state-of-the-art QBF solvers known from literature fail.

Combinational equivalence checking is an essential task in circuit design. In this paper we focus on SAT based equivalence checking making use of incremental SAT techniques which are well known from their application in bounded model checking. Based on an analysis of shared circuit structures we present heuristics which try to maximize the benefit from incremental SAT solving in this application by looking for good orders in which the equivalence of different circuit outputs is checked. Moreover, we present a reset strategy for situations where the benefit from the incremental SAT approach seems to decrease. Experimental results demonstrate that our novel method outperforms traditional methods significantly.

Computing counterexamples is a crucial task for error diagnosis and debugging of sequential systems. If an implementation does not fulfill its specification, counterexamples are used to explain the error effect to the designer. In order to be understood by the designer, counterexamples should be simple, i.e. they should be as general as possible and assign values to a minimal number of input signals. Here we use the concept ofBlack Boxes- parts of the design with unknown behavior - to mask out components for counterexample computation. By doing so, the resulting counterexample will argue about a reduced number of components in the system to facilitate the task of understanding and correcting the error. We introduce the notion of 'uniform counterexamples' to provide an exact formalization of simplified counterexamples arguing only about components which were not masked out. Our computation of counterexamples is based on symbolic methods using AIGs (And-Inverter-Graphs). Experimental results using a VLIW processor as a case study clearly demonstrate our capability of providing simplified counterexamples.

In this paper we present a complete method for verifying properties expressed in the temporal logic CTL. In contrast to the majority of verification methods presented in previous years, we support unbounded model checking based on symbolic representations of characteristic functions. Among others, our method is based on an advanced and-inverter graph (AIG) implementation, quantifier scheduling, and BDD sweeping. For several examples, our method outperforms BDD based symbolic model checking by orders of magnitude. However, our approach is also able to produce competitive results for cases where BDD are known to perform well

We consider the problem of checking whether an implementation which contains parts with incomplete information is equivalent to a given full specification. We study implementations which are not completely specified, but contain boxes which are associated with incompletely specified functions (called Incompletely Specified Boxes or IS-Boxes). After motivating the use of implementations with Incompletely Specified Boxes we define our notion of equivalence for this kind of implementations and present a method to solve the problem. A series of experimental results demonstrates the effectiveness and feasibility of the methods presented.

Reduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [17, 7]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we give a theoretical background for this Multiple Variable Order problem. Moreover, we solve the problem to transform ROBDDs with different variable orders into a good common variable order using dynamic variable ordering techniques.

We consider the problem of checking whether a partial implementation can (still) be extended to a complete design which is equivalent to a given full specification.

Symbolic techniques have revolutionized reachability analysis in the last years. Extending their applicability to handle large, industrial designs is a key issue, involving the need to focus on memory consumption for BDD representation as well as time consumption to perform symbolic traversals of Finite State Machines (FSMs). We address the problem of reachability analysis for large FSMs, introducing a novel technique that performs reachability analysis using a sequence of “distance driven” partial traversals based on dynamically chosen prunings of the transition relation. Experiments are given to demonstrate the efficiency and robustness of our approach: We succeed in completing reachability problems with significantly smaller memory requirements and improved time performance.

In this paper we study the effect of using information about (partial) symmetries for the minimization of reduced ordered binary decision diagrams (ROBDD's). The influence of symmetries for the integration in dynamic variable ordering is studied for both completely and incompletely specified Boolean functions. The problems above are studied from a theoretical and practical point of view. Statistical results and benchmark results are reported to underline the efficiency of the approach. They prove that our techniques lead to improvements of the ROBDD sizes by up to 70%.

Functional decomposition is an important technique in logic synthesis, especially for the design of lookup table based FPGA architectures. We present a method for functional decomposition with a novel concept for the exploitation of don't cares thereby combining two essential goals. The minimization of the number of decomposition functions in the current decomposition step and the extraction of common subfunctions for multi-output Boolean functions. The exploitation of symmetries of Boolean functions plays an important role in our algorithm as a means to minimize the number of decomposition functions not only for the current decomposition step but also for the (recursive) decomposition algorithm as a whole. Experimental results prove the effectiveness of our approach.

Several types of Decision Diagrams (DDs) have been proposed for the verijcation of Integrated Circuits. Recently word-level DDs libBblDs, *BhfDs, HDDs, K*BhiDs and *PHDDs have been attracting more and more interest, e.g., by using *BMDsand *PHDDsit wasfor thejrst time possible to formally verifi integer multipliers and Joating point multipliers of "signi&ant" bitlengths, respectively.On the other hat~it has been unhewn, whether division, the operation inverse to multiplication, can be efiiently represented by some ppe of word-level DDs.In this paper we show that the representational power of any word-level DD is too weak to efficiently represent integer divisiok Thus, neither a clever choice of the variable orderins, the decomposition type or the edse weights, can lead to a polynotnial DD size for divisio~ For the proof we introduce Word-Level Linear Combination Dia-gr~(JVLCDS), a DD, which maybe viewed as a "generic" wordlevel DD. \i@derive an uponential lower bound on the WLCD representation sizefor integer dividers atrdshow how this bound transfers to all other word-level DDs.

In many verification techniques, fast functional evaluation of a Boolean network is needed. We investigate the idea of using binary decision diagrams (BDDs) for functional simulation. The area-time trade-off that results from different minimization techniques of the BDD is discussed. We propose new minimization methods based on dynamic reordering that allow smaller representations with (nearly) no runtime penalty.

No abstract available.

A multilevel logic synthesis technique for multi-output Boolean functions is presented which is based on minimizing the communication complexity. Unlike previous approaches, which in the final analysis decompose each single-output function f/sub i/ of a multi-output function f=(f/sub 1/, ..., f/sub m/) independently of the other single-output functions f/sub j/ (j/spl ne/i), the approach presented in this paper gives special attention to the fact that there possibly exist some decomposition functions which can be used by different outputs during the decomposition of the single-output functions of f. The benchmarking results (taken from 1991 MCNC multilevel logic benchmarks) which close the paper are promising.>