Research Projects
Curent Projects
Formal Verification and Debugging of Array Dividers
We propose a formal verification and debugging technique of arithmetic divider circuits. This method relies on assigning specific signals to predetermined constants to simplify the design into easily verifiable circuit components. Equivalence checking and SAT verification are then employed to validate these components at a functional level, without resorting to reverse engineering techniques. Unlike prior methods, our approach enables precise bug localization during debugging without accessing the internal structure. The method is applicable to both Restoring and Non-restoring array dividers. Our results demonstrate substantial reductions in verification and debugging times compared to existing methods. The method can verify dividers upto 1024 bits in about 16 minutes.
Index Terms—Formal verification, Arithmetic verification, Dividers, SAT, Equivalence checking.
Previous Projects
Formal Verification of Divider Circuits by Hardware Reduction
This work introduces a novel verification method of gate-level hardware implementation of divider circuits. The method, called hardware reduction, accomplishes the verification by appending the divider circuit with another circuit, which implements its arithmetic inverse, followed by logic synthesis. If the circuit under verification is correct, the resulting resynthesized circuit becomes trivially redundant (composed of wires or buffers only). This method outperforms the established Boolean satisfiability, SAT-based and equivalence checking techniques and does not require a reference design.
Index Terms—Formal Verification, Algebraic rewriting, Dividers, Arithmetic verification
Formal verification of constrained arithmetic circuits using computer algebraic approach
This work presents a novel verification method for arithmetic circuits subjected to some user or application constraints. The verification problem is solved in an algebraic domain rather than in a Boolean domain by representing circuit specification and its implementation as polynomials. The concept of deterministic terms is introduced to describe the constraints imposed on the circuit. Based on this concept, a case splitting analysis is proposed to resolve the memory problem during algebraic rewriting. The computational complexity of the method is analyzed, and two techniques are proposed to accelerate the verification process. The experimental results for constrained arithmetic circuits up to 128 bits, and the comparison with the state-of-the-art SAT solver demonstrate the effectiveness and the scalability of the proposed method.
Index Terms—Formal Verfication, Constrained arithmetic circuits, SAT, Algebraic rewriting
SPEAR: hardware-based implicit rewriting for square-root circuit verification
This work 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.
Index Terms—Algebraic rewriting, Square-root, Arithmetic verification, Formal verification
Functional verification of hardware dividers using algebraic model
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 work 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.
Index Terms—Functional Verfication, Dividers, SAT, Algebraic model
Understanding Algebraic Rewriting for Arithmetic Circuit Verification: A Bit-Flow Model
This work 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.
Index Terms—Algebraic rewriting, Arithmetic verification, Formal verification
Spectral approach to verifying non-linear arithmetic circuits
This work 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.
Index Terms—Functional Verfication, Spectral method, Multipliers
Rewriting Environment for Arithmetic Circuit Verification
This work 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.
Index Terms—Formal verification, Rewriting, Gate-level arithmetic circuits
Computer algebraic approach to verification and debugging of Galois field multipliers
This work 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(2 m ) 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.
Index Terms—Computer Algebra, Formal Verfication, Debugging, Multipliers, Galois field
Logic debugging of arithmetic circuits
This work presents a novel diagnosis and logic debugging method for gate-level arithmetic circuits. It detects logic bugs in a synthesized circuit caused by using a wrong gate ("gate replacement" error), which change the functionality of the circuit. The method is based on modeling the circuit in an algebraic domain and computing its algebraic "signature". The location and type of the bug is determined by comparing signatures computed in both directions, using forward (PI to PO) and backward (PO to PI) rewriting. It will also perform automatic correction for the detected bugs. The approach is demonstrated and tested on a set of integer combinational arithmetic circuits.
Index Terms—Formal verification, Functional verification, Debugging, Arithmetic verification, Bit-level arithmetic
Verification of gate-level arithmetic circuits by function extraction
The work presents an algebraic approach to functional verification of gate-level, integer arithmetic circuits. It is based on extracting a unique bit-level polynomial function computed by the circuit directly from its gate-level implementation. The method can be used to verify the arithmetic function computed by the circuit against its known specification, or to extract the arithmetic function implemented by the circuit. Experiments were performed on arithmetic circuits synthesized and mapped onto standard cells using ABC system. The results demonstrate scalability of the method to large arithmetic circuits, such as multipliers, multiply-accumulate, and other elements of arithmetic datapaths with up to 512-bit operands and over 2 Million gates. The procedure has linear runtime and memory complexity, measured by the number of logic gates.
Index Terms—Formal Verfication, Function extraction, Arithmetic circuits
ABL Function Computing
These works investigate formal verification for arithmetic bit-level circuits (ABL). The circuit is modeled as a network of adders and basic Boolean gates, and the computation performed by the circuit is viewed as a flow of binary data through such a network. The verification problem is cast as a Network Flow problem and solved using symbolic term rewriting and simple algebraic techniques. Functional correctness is proved by showing that the symbolic flow computed at the primary inputs is equal to the flow computed at the primary outputs. Experimental results show a potential application of the method to certain classes of arithmetic circuits.
Index Terms—Formal verification, Functional verification, Arithmetic verification, Bit-level arithmetic
Parallel Simulation and Verification
Simulation of the RTL model is one of the first and mandatory steps of the design verification flow. Such a simulation needs to be repeated often due to the changing nature of the design in its early development stages and after consecutive bug fixing. Despite its relatively high level of abstraction, RTL simulation is a very time consuming process, often requiring nightly or week-long regression runs. In this work, we propose an original approach to accelerating RTL simulation that leverages parallelism offered by multi-core machines. However, in contrast to traditional, parallel distributed RTL simulation, the proposed method accelerates RTL simulation in temporal domain by dividing the entire simulation run into independent simulation slices, each to be run on a separate core. It is combined with fast simulation model at ESL level that provides the required initial state for each independent simulation slice. The paper describes the basic idea of the method and provides some initial experimental results showing its effectiveness in improving RTL simulation performance in an automated way.
Index Terms—Simulation; Verfication, RTL, Verilog, ESL, C, SystemC, Testbench
TDS: A Behavioral Transformation System based on Canonical Dataflow Representation
TDS is an experimental software tool for behavioral transformations of designs specified on algorithmic and behavioral levels. It transforms the initial design specifications into a data flow graph (DFG) optimized for a particular objective (latency, resource utilization, etc.) prior to high- level synthesis. The behavioral transformations are based on graph-based canonical representation, Taylor Expansion Diagram (TED), and are followed by structural transformations of the resulting DFG network. The system is intended for data-flow and computation-intensive designs used in digital signal processing applications.
Index Terms—Algebraic optimizations, common-subexpression elimination (CSE), data-flow graphs (DFGs), high-level synthesis, Taylor expansion diagrams (TEDs)
BDS (BDD-based Logic Synthesis system)
BDS(BDD-based Logic Synthesis system) is our fast and efficient logic synthesis tool, based on a novel theory of BDD-based bi-decomposition. It provides both algebraic and Boolean decomposition of several types: AND, OR, XOR, and MUX. It handles random and control logic (AND-OR intensive) functions as well as arithmetic (XOR-intensive) functions. Its unique approach to partitioned BDD's allows it to handle very large circuits. Source code of BDS-1.2 is now available upon request for non-commercial, academic use only. Please contact Prof. Maciej Ciesielski at ciesiel@ecs.umass.edu to obtain the code.
Index Terms—BDD, logic optimization, synthesis