This paper gives a brief survey of current state-of-the-art techniques for formal verification of arithmetic circuits with suggestions for future work. In contrast to standard BDD or SAT-based approach that require a reference circuit it concentrates on Symbolic Computer Algebra (SCA) and related techniques that verify the circuits w.r.t. its abstract arithmetic specification. We examine the original computer algebra method; review the algebraic techniques of forward and backward rewriting; and AIG rewriting. We also propose a "hardware rewriting" method, which replaces algebraic rewriting by hardware synthesis of the circuit under verification appended with an inverse of the circuit, expecting it to be reduced to a redundant one.

The paper addresses the formal verification of gate-level square-root circuits. Division and square root functions are some of the most complex arithmetic operations to implement and proving the correctness of their hardware implementation is of great importance. In contrast to standard approaches that use satisfiability and equivalence checking techniques, the presented method verifies whether the gate-level square-root circuit actually performs a root operation, instead of checking equivalence with a reference design. The method extends the algebraic rewriting technique developed earlier for multipliers and introduces a novel technique of implicit hardware rewriting. The tool called SPEAR based on hardware rewriting enables the verification of a 256-bit gate-level square-root circuit with 0.26 million gates in under 18 minutes.

This paper addresses theoretical aspects of arithmetic circuit verification based on algebraic rewriting. Its goal is to advance the understanding of algebraic techniques for arithmetic circuit verification in the context of symbolic computer algebra. The paper offers a new insight into the arithmetic circuit verification problem, by viewing the computation performed by the circuit as the flow of digital data. In the proposed bit-flow model, the circuit is modeled as a network of logic components satisfying a bit-flow conservation law. We prove that the value of the flow of data in the circuit is invariant throughout the circuit and use this to prove soundness and completeness of the rewriting technique, independently from the computer algebra arguments. The efficiency of the method is illustrated with impressive results for large integer multipliers. The verification system and benchmarks are offered in an open source software environment.

This paper presents a fast and effective computer algebraic method for analyzing and verifying non-linear integer arithmetic circuits using a novel algebraic spectral model. It introduces a concept of algebraic spectrum, a numerical form of polynomial expression; it uses the distribution of coefficients of the monomials to determine the type of arithmetic function under verification. In contrast to previous works, the proof of functional correctness is achieved by computing an algebraic spectrum combined with local rewriting of word-level polynomials. The speedup is achieved by propagating coefficients through the circuit using And-Inverter Graph (AIG) datastructure. The effectiveness of the method is demonstrated with experiments including standard and Booth multipliers, and other synthesized non-linear arithmetic circuits up to 1024 bits containing over 12 million gates.

Division is one of the most complex arithmetic operations to implement and its hardware implementation requires thorough verification at the gate level. Dividers are difficult to verify using standard Boolean methods, such as equivalence checking or SAT-based techniques, as they require “bit-blasting” onto bit-level netlists. Other methods, such as theorem provers, concentrate mostly on proving correctness of the division algorithm. However, verification of low-level hardware implementations has received only a limited attention. This paper addresses the problem of verifying gate-level divider circuits by extending an algebraic model, successfully used to prove multipliers and other arithmetic circuits, to dividers. The method verifies whether the gate-level divider circuit actually performs a division, without a need for a reference design.

Requirements elicitation is one of the essential steps towards software design and construction. Business analysts and stakeholders often face challenges in gathering or conveying key software requirements. There are many methods and tools designed by researchers and practitioners but with the persistent development of new technologies, there is a need to make requirements gathering and design‐rationale process more efficient and adaptable. Storytelling is an emerging concept and researchers are witnessing its effectiveness in education, community building, information system, and requirement elicitation. Objectives of this study are to devise a method for requirements elicitation and improving design‐rationales using story‐based techniques and evaluate the effectiveness of the proposed activity. To answer the research objectives, the authors have conducted open‐ended interviews to get feedback on the proposed method; the authors have case requirement from a running project to map how this method can be useful; and performed empirical evaluation of the proposed card‐based activity. The estimated regression model, in our study, has shown that participants' perception about the simplicity/easiness and the joy of playing the game has an eventual positive effect on requirements elicitation through enhancing user's desire to play the game, which in turn increases the collaborative learning outcomes of the game.

The paper presents a novel method to verify and debug gate-level arithmetic circuits implemented in Galois Field arithmetic. The method is based on forward reduction of the specification polynomials of the circuit in GF(2m) using GF(2) models of its logic gates. We define a forward variable order “FO >” and the rules of forward reduction that enable verification, bug detection, and automatic bug correction in the circuit. By analyzing the remainder generated by forward reduction, the method can determine whether the circuit is buggy, and finds the location and the type of the bug. The experiments performed on Mastrovito and Montgomery multipliers show that our debugging method is independent of the location of the bug(s) and the debugging time is comparable to the time needed to verify the bug-free circuit.

The paper describes a practical software tool for the verification of integer arithmetic circuits. It covers different types of integer multipliers, fused add-multiply circuits, and constant dividers - in general, circuits whose computation can be represented as a polynomial. The verification uses an algebraic model of the circuit and is accomplished by rewriting the polynomial of the binary encoding of the primary outputs (output signature), using the polynomial models of the logic gates, into a polynomial over the primary inputs (input signature). The resulting polynomial represents arithmetic function implemented by the circuit and hence can be used to extract functional specification from its gate-level implementation. The rewriting uses an efficient And-Inverter Graph (AIG) representation to enable extraction of the essential arithmetic components of the circuit. The tool is integrated with the popular ABC system. Its efficiency is illustrated with impressive results for integer multipliers, fused add-multiply circuits, and divide-by-constant circuits. The entire verification system is offered in an open source ABC environment together with an extensive set of benchmarks.

In this paper, we address the problem of timing speculation for multi-threaded workloads executing on a multi-core processor. Our approach is based on a new observation --- heterogeneity in path sensitization delays across different threads in multi-threaded programs. Leveraging this heterogeneity, we propose Synergistic Timing Speculation (SynTS) to jointly optimize the energy and execution time of multithreaded applications. In particular, SynTS uses a sampling based online error probability estimation technique, coupled with a polynomial time algorithm, to optimally determine the voltage, frequency and the amount of timing speculation for each thread. Our experimental evaluations, based on detailed cross-layer simulations, demonstrate that SynTS reduces energy delay product by up to 21%, compared to existing timing speculation schemes.