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).

Decision Diagrams (DDs) are among the most popular representations for Boolean functions. They are widely used in the synthesis and verification of digital circuits. The size (i.e., number of nodes) and computation time (required time for performing operations) are two important parameters that determine the efficiency of a DD in different applications. It has been proven that some DDs can represent specific functions in polynomial space or perform certain operations in polynomial time. For example, Binary Decision Diagrams (BDDs) are capable of representing a wide variety of functions (e.g. integer addition) in polynomial space with respect to the input size. However, there are also some functions (e.g., integer multiplication) for which the exponential lower-bounds have been proven for the BDD sizes. In this paper, we investigate the space complexity of representing an integer addition, where one of the operands is shifted to the right by an arbitrary value. We call this function the shifted addition. This function is widely used in many digital circuits, e.g., floating point adders. We prove that the size of the BDD representing a shifted addition has exponential space complexity with respect to the input size. It is an important step towards clarifying the reasons behind the failure of BDD-based verification and synthesis when they are applied to the circuits containing shifted addition, e.g., floating point adders. • BDDs reach exponential size when symbolically simulating a floating point adder. • The lower bound for BDDs representing a shifted addition is exponential ( 2 n / 4 ). • The proof is performed by using fooling sets.

With the rapid growth in the size and complexity of digital circuits, the possibility of bug occurrence has significantly increased. In order to avoid the enormous financial loss due to the production of buggy circuits, using scalable formal verification methods is essential. The scalability of a verification method for a specific design is proven by showing that the method has polynomial space and time complexities. Unfortunately, not all verification methods have a polynomial complexity, particularly when it comes to the verification of large and complex designs. In this paper, we propose a divide-and-conquer strategy for Polynomial Formal Verification (PFV) of complex circuits. Instead of using a monolithic proof engine to verify the entire design, we break the verification task down into several problems, which can be solved in polynomial space and time using a hybrid proof engine. As a case study, we investigate the PFV of the ALU in a RISC-V processor using our divide-and-conquer strategy.

In this paper, we present our verifier that takes advantage of Binary Decision Diagrams (BDDs) with case splitting to fully verify a floating point adder. We demonstrate that the traditional symbolic simulation using BDDs has an exponential time complexity and fails for large floating point adders. However, polynomial bounds can be ensured if our case splitting technique is applied in the specific points of the circuit. The efficiency of our verifier is demonstrated by experiments on an extensive set of floating point adders with different exponent and significand sizes.

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.

With the growing demands for highly area-efficient, delay-optimized, and low-power designs, the complexity of digital circuits is increasing as well. Especially, a wide variety of arithmetic circuits, including different types of adders, multipliers, and dividers have been proposed to meet the demands in applications such as cryptography and Artificial Intelligence (AI). Some of these arithmetic circuits have highly parallel architectures and contain millions of gates; as a result, they are extremely error-prone. In the last 30 years, several formal verification methods have been proposed to verify arithmetic circuits. These methods report very good results when it comes to the verification of adders and structurally simple multipliers. Moreover, their space and time complexities are polynomial, i.e, they are scalable. However, when it comes to the verification of structurally complex multipliers, the story is different.In this paper, we investigate the space and time complexity of verifying a structurally complex multiplier using a word-level verification method. We prove that the space and time complexity is always exponential. Then, we introduce a new verification strategy that takes advantage of several verification engines. We show that the polynomial formal verification of the complex multiplier becomes possible if the correctness of each stage is verified using the proper verification method. Our verification strategy can be applied to other complex digital circuits.

Recently, a lot of effort has been put into developing formal verification approaches by both academic and industrial research. In practice, these techniques often give satisfying results for some types of circuits, while they fail for others. A major challenge in this domain is that the verification techniques suffer from unpredictability in their performance. The only way to overcome this challenge is the calculation of bounds for the space and time complexities. If a verification method has polynomial space and time complexities, scalability can be guaranteed.

The demand for optimized and efficient embedded software is increasing in many applications such as the Internet of Things (IoT) or other Cyber-Physical Systems (CPS). Hence, early performance analysis of embedded software is essential to perform Design Space Exploration (DSE), ensure efficiency, and meet time-to-market constraints. Designers usually use real hardware, simulators, or static analyzers to obtain the performance. However, these methods suffer from serious drawbacks as real hardware is not available in the early stage of the design process, simulators either do not support any timing accuracy or require large execution time, and static analyzers need details of the hardware microarchitecture. In this paper, we present a novel Artificial Neural Network (ANN)-based approach that allows a fast and accurate performance estimation of embedded software for RISC-V processors in the early design phases. This can significantly reduce the burden on designers to perform DSE. The proposed approach takes advantage of the dynamic analysis technique and analytical models and does not require any microarchitecture-related parameters such as cache misses, cache hits, and memory-level parallelism. We compare our proposed microarchitecture-independent approach with state-of-the-art in terms of speed and accuracy. Our experiments on various benchmarks demonstrate that the proposed approach achieves a speed-up of$4.41\times$compared to a RISC-V Virtual Prototype (VP) at the Electronic System Level (ESL), while the estimation results have only a Mean Absolute Percentage Error (MAPE) of 2%.

With the growing complexity of digital circuits, formal verification has become a crucial task after the design in order to ensure the correctness of a circuit. Many existing verification methods suffer from unpredictability in their performance. It is not clear whether they have to be run for seconds, hours, or days to return the verification results or whether they fail in the end. The unpredictability can only be resolved by ensuring complexity bounds. To guarantee scalability we are in particular interested in Polynomial Formal Verification (PFV), where the space and time complexities have polynomial bounds with respect to the size of the circuit.The information about the design hierarchy is usually vital for PFV. Complex digital circuits consist of several components that cannot be verified with an individual verification technique in polynomial space and time. However, with additional knowledge about the boundaries of components, PFV becomes possible through the step-wise verification of sub-components and the use of different formal proof engines. In this paper, we first introduce PFV and clarify its importance. We consider the verification of several flattened gate-level arithmetic circuits and illustrate the challenges of PFV when no design hierarchy is available. Then, we show how these challenges can be overcome by preserving design hierarchy information including the boundaries of the components.

The formal verification of integer multipliers is one of the important but challenging problems in the verification community. Recently, the methods based on symbolic computer algebra (SCA) have shown very good results in comparison to all other existing proof techniques. However, when it comes to verification of huge and structurally complex multipliers, they completely fail as an explosion happens in the number of monomials. The reason for this explosion is the generation of redundant monomials known as vanishing monomials. This article introduces the SCA-based approach RevSCA-2.0 that combines reverse engineering and local vanishing removal to verify large and nontrivial multipliers. For our approach, we first come up with a theory for the origin of vanishing monomials, i.e., we prove that the gates/nodes where both outputs of half adders (HAs) converge are the origins of vanishing monomials. Then, we propose a dedicated reverse engineering technique to identify atomic blocks including HAs. The identified HAs are the basis for detecting converging cones and locally removing vanishing monomials, which finally results in a vanishing-free global backward rewriting. The efficiency of RevSCA-2.0 is demonstrated using an extensive set of multipliers with up to several million gates.

Nowadays, prefix adders are widely used in different designs and applications due to their flexible carry propagation hardware. The variety of these adders makes it possible to find the best choice based on the design parameters, e.g., area, delay, number of wiring tracks. Proving the correctness of prefix adders is an important task after their design as they usually have a complex and error-prone structure. It has been experimentally shown that Binary Decision Diagrams (BDDs) are very efficient in the formal verification of adders, including prefix adders. However, it has been never proved theoretically. In this paper, we calculate the computational complexity of proving the correctness of prefix adders using BDDs. Based on these calculations, we show that the formal verification of prefix adders can be done in time polynomial in n, where n is the size of the adder (i.e., the number of bits per input). We also compare the theoretical calculations with the experimental results to clarify the differences between the complexities in theory and practice.

Despite the recent success of formal verification methods, the computational complexity of most of them is still unknown. It raises serious questions regarding the scalability of the approaches. One of the most successful formal methods to prove the correctness of adders is Binary Decision Diagram (BDD)-based verification. It reports very good results for verification of different adder architectures. However, the computational complexity of BDD-based verification has not been yet fully investigated. In this paper, we calculate the complexity of verifying one of the fastest available adders, i.e., conditional sum adder. Then, we show that the verification of this architecture is possible in polynomial time. Finally, we confirm our theoretical calculations by experimental results.

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).

High-level Synthesis (HLS) using system-level modeling language SystemC at the Electronic System Level (ESL) is being increasingly adopted by the semiconductor industry to raise design productivity. However, errors in the high-level design can propagate down to the low-level implementation and become very costly to fix. Thus, SystemC HLS verification and debugging are necessary and important. While monitoring simulation behavior is a straightforward solution to debug a given design in the case of an error (results of verification), it can become a very time-consuming process as a large amount of data that is not necessarily relevant to the source of error is analyzed.In this paper, we propose a fast and automated debugging-aware visualization approach, enabling designers to monitor the portion of a given SystemC HLS design’s simulation behavior that is related to the erroneous output(s). Experimental results including an extensive set of standard SystemC HLS designs show the effectiveness of our approach in localizing the designs’ simulation behavior in terms of the number of visualized variables. In comparison to traditional visualization methods, our proposed approach obtains up to 96% and 91% reduction in the search space for single and multiple faulty outputs, respectively.

Verifying the functional correctness of a circuit is often the most time-consuming part of the design process. Recently, world-level formal verification methods, e.g., Binary Moment Diagram (BMD) and Symbolic Computer Algebra (SCA) have reported very good results for proving the correctness of arithmetic circuits. However, these techniques still frequently fail due to memory or time requirements. The unknown complexity bounds of these techniques make it impossible to predict before invoking the verification tool whether it will successfully terminate or run for an indefinite amount of time.

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.

In order to meet time-to-market constraints and to raise the design productivity, High-level Synthesis (HLS) is being increasingly adopted by the semiconductor industry. HLS designs, which can be automatically translated into Register Transfer Level (RTL), are typically written in SystemC at the Electronic System Level (ESL). However, this modern design flow still has weaknesses, in particular, due to the significant manual effort involved for verification and the subsequent debugging process which are both time-consuming and error-prone. In this paper, we propose ASCHyRO, a fully automated semiformal fault localization approach for SystemC HLS designs. ASCHyRO takes advantage of a hybrid rank ordering technique to derive a reduced ordered set of potential fault locations. The reduced order set is obtained by calculating a Confidence Score (CS) for each fault candidate based on a combination of static and dynamic fault probability analysis. Experimental results including an extensive set of standard SystemC HLS designs show the effectiveness of our approach in localizing even multiple faults with high confidence in a short execution time.

In recent years, formal methods based on Symbolic Computer Algebra (SCA) have shown very good results in verification of integer multipliers. The success is based on removing redundant terms (vanishing monomials) early which allows to avoid the explosion in the number of monomials during backward rewriting. However, the SCA approaches still suffer from two major problems: (1) high dependence on the detection of Half Adders (HAs) realized as AND-XOR gates in the multiplier netlist, and (2) extremely large search space for finding the source of the vanishing monomials. As a consequence, if the multiplier consists of dirty logic, i.e. for instance using non-standard libraries or logic optimization, the existing SCA methods are completely blind on the resulting polynomials, and their techniques for effective division fail.

Nowadays, a variety of multipliers are used in different computationally intensive industrial applications. Most of these multipliers are highly parallelized and structurally complex. Therefore, the existing formal verification techniques fail to verify them. In recent years, formal multiplier verification based on Symbolic Computer Algebra (SCA) has shown superior results in comparison to all other existing proof techniques. However, for non-trivial architectures still a monomial explosion can be observed. A common understanding is that this is caused by redundant monomials also known as vanishing monomials. While several approaches have been proposed to overcome the explosion, the problem itself is still not fully understood. In this paper we present a new theory for the origin of vanishing monomials and how they can be handled to prevent the explosion during backward rewriting. We implement our new approach as the SCA-verifier PolyCleaner. The experimental results show the efficiency of our proposed method in verification of non-trivial million-gate multipliers.

Field-programmable gate arrays (FPGAs) could outperform microprocessors on floating point computations due to massive parallelism, freedom on the selection of exponent/mantissa width, and utilization of simplified adders and multipliers. However, optimized use of resources and accuracy of the final implemented expression are two important issues in the implementation of floating point arithmetic expressions on FPGAs. High-level optimizations such as changing the form of floating point initial expression by arithmetic rules or deciding on the exponent and mantissa widths have significant effects on the resource usage, accuracy, and efficiency of the final implementation. In this paper, we introduce an optimization framework called OptiFEX, which enables designers to optimize an initial floating point expression in terms of the resource usage and the exponent and mantissa widths based on: 1) input intervals; 2) the smallest presentable number in the implementation; and 3) the maximum permitted error interval provided by the designer. First, we come up with some techniques to generate equivalent expressions for the initial expression, and we make use of some heuristics to speed up the process of equivalent expressions' generation. We also propose a method to estimate the mantissa width. Finally, we introduce an algorithm to choose the best expressions in terms of the resource usage based on the estimated mantissa and exponent widths.