Formal verification has been successfully used to verify different types of digital circuits, including combinational and sequential logic, arithmetic circuits, and datapath designs. However, the verification techniques concentrate on confirming whether the circuit performs its intended function, while the issue of debugging, i.e., detection and correction of functional errors of the design, remains an open problem. Elaborate testing techniques have been developed that target certain types of manufacturing faults, but there are no general techniques that address the debugging issue for functional bugs. This paper addresses the issue of debugging of arithmetic circuits that due to their large size and complexity are particularly hard to verify and debug. Current debugging techniques handle only simple types of bugs: gate replacement, wrong gate polarity, or a missing gate, but cannot handle more realistic faults, such as wrong wiring or using a wrong combination of logic gates. We describe a novel method that combines formal verification and testing techniques to enable efficient identification and correction of faults. The technique involves setting select signals to some predefined constants to reduce the design to easily verifiable circuit components; these components are then verified using logic equivalence checking and SAT tools. The fault can then be identified in form or a small logic area (with a few logic gates) to be replaced by a new, functionally correct logic. The proposed technique is illustrated with debugging of different types of divider circuits up to 1024 bit-wide.

This paper describes an original approach to formal verification of a special class of modular multipliers, namely modulo$(2^{n}-1)$multipliers, critical components of cryptographic and error correction circuits. The proposed method completely avoids the expensive SAT, symbolic computer algebra, and rewriting techniques, typically used in formal verification of arithmetic circuits. Instead, recognizing a regular structure of such multipliers, constructed as an array of adders, the problem is modeled as a system of linear equations. Each adder is represented by a linear equation with an appropriate and easy to compute weight; the resulting linear system is solved by eliminating the intermediate signals, exposing the direct relation between the primary inputs and outputs. The results obtained for large$(2^{n}-1)$modular multiplier circuits show several orders of magnitude improvement in CPU time compared to those in the published literature.

The paper describes a formal verification method for hardware implementation of restoring divider circuits. The method is based on setting select signals to predefined constants to reduce the design to easily verifiable circuit components, followed by their verification using standard equivalence checking and SAT. It is then concluded by a global proof that the composition of those components indeed implements a divider. In contrast to previous approaches, the verification is done on a functional level without any reverse engineering of the internal structure. The results show significant improvement in verification time compared to other methods. The proposed approach can also be used in debugging by localizing the source of a bug. This feature is currently not available in the existing verification tools and will be a subject of future work.

The last few decades marked an explosive growth in the number and importance of cyberphysical and embedded systems. As more and more of those systems become security- and safety-critical, assuring functional correctness and dependability of their digital hardware implementation became critical. Essential elements of those systems are arithmetic circuits: different types of adders, multipliers, and dividers that need to be efficiently designed and optimized for area, delay and power. These circuits become more and more complex, containing millions of logic gates; this makes them extremely errorprone, and require advanced simulation, verification and testing to guarantee their integrity. This keynote addresses some of these issues and concentrates on formal verification of hardware implementation of arithmetic circuits. The presentation gives a brief overview of modern methods used in arithmetic circuit verification, including theorem proving, Boolean methods, satisfiability, and symbolic computer algebra. It shows how these methods evolved from being based on pure mathematical models to practical engineering solutions. It discusses challenges they face and offers a look into the future.

This paper proposes an efficient verification and debugging method for arithmetic divider circuits. The technique involves setting select signals to some predefined constants in order to reduce the design to easily verifiable circuit components. These components are then verified using logic equivalence checking and SAT tools. An important feature of the proposed approach is that it naturally enables debugging by identifying and localizing bugs through proper selection of accessible signals. This method can verify and debug large restoring dividers within single minutes using synthesis and verification tools, such as ABC. The general debugging concept proposed here is applicable to both the restoring and non-restoring dividers. To the best of our knowledge the proposed debugging capability is not offered by any of the existing verification tools.

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.

Galois field (GF) arithmetic circuits find numerous applications in communications, signal processing, and security engineering. Formal verification techniques of GF circuits are scarce and limited to circuits with known bit positions of the primary inputs and outputs. They also require knowledge of the irreducible polynomial P(x), which affects final hardware implementation. This paper presents a computer algebra technique that performs verification and reverse engineering of GF(2m) multipliers directly from the gate-level implementation. The approach is based on extracting a unique irreducible polynomial in a parallel fashion and proceeds in three steps: 1) determine the bit position of the output bits; 2) determine the bit position of the input bits; and 3) extract the irreducible polynomial used in the design. We demonstrate that this method is able to reverse engineer GF(2m) multipliers in m threads. Experiments performed on synthesized Mastrovito and Montgomery multipliers with different P(x), including NIST-recommended polynomials, demonstrate high efficiency of the proposed method.

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.

Constructing algebraic polynomials using computer algebra techniques is believed to be state-of-the-art in analyzing gate-level arithmetic circuits. However, the existing approach applies algebraic rewriting directly to the gate-level netlist, which has potential memory explosion problem. This paper introduces an algebraic rewriting technique based on the and-inverter graph (AIG) representation of gate-level designs. Using AIG-based cut-enumeration and truth table computation, an efficient order of algebraic rewriting is identified, resulting in dramatic simplifications of the polynomial under construction. An automatic approach, which further reduces the complexity of algebraic rewriting by handling redundant polynomials, is also proposed.

Galois field (GF) arithmetic is used to implement critical arithmetic components in communication and security-related hardware, and verification of such components is of prime importance. Current techniques for formally verifying such components are based on computer algebra methods that proved successful in verification of integer arithmetic circuits. However, these methods are sequential in nature and do not offer any parallelism. This paper presents an algebraic functional verification technique of gate-level GF(2m) multipliers, in which verification is performed in bit-parallel fashion. The method is based on extracting a unique polynomial in Galois field of each output bit independently. We demonstrate that this method is able to verify an n-bit GF multiplier in n threads. Experiments performed on pre- and post-synthesized Mastrovito and Montgomery multipliers show high efficiency up to 571 bits.

Current techniques for formally verifying circuits implemented in Galois field (GF) arithmetic are limited to those with a known irreducible polynomial P(x). This paper presents a computer algebra based technique that extracts the irreducible polynomial P(x) used in the implementation of a multiplier in GF(2m). The method is based on first extracting a unique polynomial in Galois field of each output bit independently. P(x) is then obtained by analyzing the algebraic expression in GF(2m) of each output bit. We demonstrate that this method is able to reverse engineer the irreducible polynomial of an n-bit GF multiplier in n threads. Experiments were performed on Mastrovito and Montgomery multipliers with different P(x), including NIST-recommended polynomials and optimal polynomials for different microprocessor architectures.

This paper presents an advanced DAG-based algorithm for datapath synthesis that targets area minimization using logic-level resource sharing. The problem of identifying common specification logic is formulated using unweighted graph isomorphism problem, in contrast to a weighted graph isomorphism using AIGs. In the context of gate-level datapath circuits, our algorithm solves the unweighted graph isomorphism problem in linear time. The experiments are conducted within an industrial synthesis flow that includes the complete high-level synthesis, logic synthesis and placement and route procedures. Experimental results show a significant runtime improvements compared to the existing datapath synthesis algorithms.

Layout-level gate or routing camouflaging techniques have attracted interest as countermeasures against reverse engineering of combinational logic. In order to minimize area overhead, typically only a subset of gate or routing components are camouflaged, and each camouflaged component layout can implement one of a few different functions or connections. The security of camouflaging relies on the difficulty of learning the overall combinational logic function without knowing the functions implemented by the individual camouflaged components of the circuit. In this paper, we expand our previous work on using incremental SAT solving to reconstruct the logical function of a circuit with camouflaged components. Our algorithm uses the standard attacker model in which an adversary knows only the noncamouflaged component functions, and has the ability to query the circuit to learn the correct output vector for any input vector. Our results demonstrate a 10.5× speedup in average runtime over the best known existing deobfuscation algorithm prior to this technique. The results presented go beyond our previous work by showing that this technique, previously applied only to a particular style of gate camouflaging, is general and can be used to deobfuscate three different proposed styles of camouflaging. We give results to quantify the effectiveness of camouflaging techniques on a variety of ISCAS-85 benchmark circuits.

Traditional datapath synthesis for standard-cell designs go through extraction of arithmetic operations from the high-level description, high-level synthesis, and netlist generation. In this paper, we take a fresh look at applying high-level synthesis methodologies in logic synthesis. We present a DAG-Aware synthesis technique for datapaths synthesis which is implemented using And-Inv-Graphs. Our approach targets area minimization. The proposed algorithm includes identifying vector multiplexers, searching for common specification logic, and reallocating multiplexers in the Boolean network. We propose an algorithm to identify common specification logic by using subgraph isomorphism. Experimental results show that our technique can provide over 10% area reduction beyond the traditional design flow. The proposed algorithm is tested on industry designs and academic benchmark suits using IBM 14nm technology.

Abstracting word information from gate-level designs is essential for formal verification, technology mapping and hardware security applications. In this paper, we present a novel method to abstract the word-level information from arithmetic gate-level circuits using a computer algebraic approach. The proposed technique translates the gate-level circuit into algebraic domain and applies algebraic rewriting to extract the arithmetic function. During the iterative rewriting, intermediate Pseudo-Boolean expressions are examined to identify word-level candidates. The proposed algorithm is able to abstract the word components from candidates and to reason about the word operation from the internal expressions. Successful experiments were performed on gate-level datapaths, including multipliers of up to 128-bit widths.

This paper 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 an 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 results show that our approach wins over the state-of-the-art SAT/satisfiability modulo theory solvers by several orders of magnitude of CPU time. The procedure has linear runtime and memory complexity, measured by the number of logic gates.

The paper 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.

The paper describes an efficient method to prove equivalence between two integer arithmetic datapath designs specified at the register transfer level. The method is illustrated with an industrial ALU design. As reported in literature, solving it using a commercial equivalence checking tool required case-splitting, which limits its applicability to larger designs. We show how such a task can be solved as a simpler verification problem without case-splitting. We demonstrate both the word-level and bit-level approach to this problem and show that the method is scalable to large combinational datapath circuits. Experimental results demonstrate the application of the method to large combinational arithmetic circuits.

Traditional dynamic simulation with standard delay format (SDF) back-annotation cannot be reliably performed on large designs. The large size of SDF files makes the event-driven timing simulation extremely slow as it has to process an excessive number of events. In order to accelerate gate-level timing simulation we propose an automated fast prediction-based gatelevel timing simulation that combines static timing analysis (STA) at the block level with dynamic timing simulation at the I/O interfaces. We demonstrate that the proposed timing simulation can be done earlier in the design cycle in parallel with synthesis.

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.

This paper describes a system-level approach to improve the latency of FPGA designs by performing optimization of the design specification on a functional level prior to high-level synthesis. The approach uses Taylor Expansion Diagrams (TEDs), a functional graph-based design representation, as a vehicle to optimize the dataflow graph (DFG) used as input to the subsequent synthesis. The optimization focuses on critical path compaction in the functional representation before translating it into a structural DFG representation. Our approach engages several passes of a traditional high-level synthesis (HLS) process in a simulated annealing-based loop to make efficient cost tradeoffs. The algorithm is time efficient and can be used for fast design space exploration. The results indicate a latency performance improvement of 22% on average versus HLS with the initial DFG for a series of designs mapped to Altera Stratix II devices.

Multilevel temporal-parallel event-driven simulation is a new radically different approach to simulation of designs described in Verilog HDL. It is based on a concept of time-parallel simulation applied to gate-level timing simulation. The simulation is performed in two steps: 1) fast reference simulation that runs on a higher, reference-level design model (typically RTL) and saves the design state at predetermined checkpoints; and 2) target simulation, which runs on a lower, gate-level model and distributes the simulation run slices to individual simulators. The paper addresses a number of important issues that make this approach practical: 1) finding initial state for each simulation slice; 2) resolving initial state mismatches; and 3) handling designs with multiple asynchronous clocks. Experimental results performed on industrial designs demonstrate the validity and efficiency of the method in terms of its performance and the debugging efficiency.

Simulation speedup offered by distributed parallel event-driven simulation is known to be seriously limited by the synchronization and communication overhead. These limiting factors are particularly severe in gate-level timing simulation. This paper describes a radically different approach to gate-level simulation based on a concept of temporal rather than conventional spatial parallelism. The proposed method partitions the entire simulation run into simulation slices in temporal domain and each slice is simulated separately. With each slice being independent from each other, an almost linear speedup is achievable with a large number of simulation nodes. This concept naturally enables “correct by simulation” methodology that explicitly maintains the consistency between the reference and the target specifications. Experimental results clearly show a significant simulation speed-up.

This paper describes a new and efficient solution to a distributed event-driven gate-level HDL simulation. It is based on a novel concept of spatial parallelism using accurate prediction of input and output signals of individual local modules in local simulations, derived from a model at a higher abstraction level (RTL). Using the predicted rather than actual signal values makes it possible to eliminate or greatly reduce the communication and synchronization overhead in a distributed event-driven simulation.

This paper describes an efficient graph-based method to optimize data-flow expressions for best hardware implementation. The method is based on factorization, common subexpression elimination (CSE) and decomposition of algebraic expressions performed on a canonical representation, Taylor Expansion Diagram. The method is generic, applicable to arbitrary algebraic expressions and does not require specific knowledge of the application domain. Experimental results show that the DFGs generated from such optimized expressions are better suited for high level synthesis, and the final, scheduled implementations are characterized, on average, by 15.5% lower latency and 7.6% better area than those obtained using traditional CSE and algebraic decomposition.

An efficient graph-based method to optimize polynomial expressions in data-flow computations is presented. The method is based on the factorization, common-subexpression elimination, and decomposition of algebraic expressions performed on a canonical Taylor expansion diagram representation. It targets the minimization of the latency and hardware cost of arithmetic operators in the scheduled implementation. The generated data-flow graphs are better suited for high-level synthesis than those extracted directly from the initial specification or obtained with traditional algebraic decomposition methods. Experimental results show that the resulting implementations are characterized by better performance and smaller datapath area than those obtained using traditional algebraic decomposition techniques. The described method is generic, applicable to arbitrary algebraic expressions, and does not require any knowledge of the application domain.

Simulation-based functional verification is characterized by two inherently conflicting targets: the signal visibility and simulation performance. Achieving a proper trade-off between these two targets is of paramount importance. Even though HDL simulators are the most widely used verification platform at the RTL and gate level, their major drawback is the low performance in verifying complex SOCs, especially when the high visibility over the design under verification is required. This paper presents a new, fast simulation method as an effective way to achieve both high simulation speed and full signal visibility. It is based on an original two-pass simulation approach. During the 1stpass, with the simulation running at full speed, a set of design states is saved periodically at predetermined checkpoints. During the 2ndpass, another simulation is performed, using any of saved checkpoints and providing 100% signal visibility for debugging. Our method differs from the traditional simulation snapshot approach in the amount and the way the design state is saved. Experimental results show significant speed-up compared to existing traditional simulation methods while maintaining 100% visibility.

An original technique to transform functional representation of the design into a structural representation in form of a data flow graph (DFG) is described. A canonical, word-level data structure, Taylor expansion diagram (TED), is used as a vehicle to effect this transformation. The problem is formulated as that of applying a sequence of decomposition cuts to a TED that transforms it into a DFG optimized for a particular objective. A systematic approach to arrive at such a decomposition is described. Experimental results show that such constructed DFG provides a better starting point for architectural synthesis than those extracted directly from HDL specifications

This paper describes an efficient method to perform factorization of DSP transforms based on Taylor expansion diagram (TED). It is shown that TED can efficiently represent and manipulate mathematical expressions. We demonstrate that it enables efficient factorization of arithmetic expressions of DSP transforms, resulting in a simplification of the computation

A Taylor expansion diagram (TED) is a compact, word-level, canonical representation for data flow computations that can be expressed as multivariate polynomials. TEDs are based on a decomposition scheme using Taylor series expansion that allows one to model word-level signals as algebraic symbols. This power of abstraction, combined with the canonicity and compactness of TED, makes it applicable to equivalence verification of dataflow designs. The paper describes the theory of TEDs and proves their canonicity. It shows how to construct a TED from an HDL design specification and discusses the application of TEDs in proving the equivalence of such designs. Experiments were performed with a variety of designs to observe the potential and limitations of TEDs for dataflow design verification. Application of TEDs to algorithmic and behavioral verification is demonstrated

Yield is normally ignored during the floorplanning stage. Recently, it has been shown that floorplanning can affect the yield with the increased sizes of chips. With the "medium-area clustering" model, yield can be evaluated during the floorplanning stage. Therefore, it's straightforward to incorporate yield in modern floorplanners. However, conventional simulate-annealing (SA) based moves are only designed for the combination of the area and/or the wire length minimizations. In this paper, we proposed a heuristic scheme of "moves" directly targeting on the yield improvement. The experimental results show a great yield improvement with little penalty for the area and/or the total wire length.

In this paper we present a flexible automatic test generation framework to detect a variety of design faults in systems with behavioral VHDL descriptions. Predefined fault models may range from the commonly used state coverage and transition coverage models to any other fault models which can be described as a set of non-linear constraints on the system's behavior. The test generation problem is formulated as a constraint logic programming problem (CLP) and an industrial CLP engine is used to solve it.

In order to improve the testabilities and power consumption, a new state assignment technique based on m-block partition is introduced in this paper. The length and number of feedback cycles are reduced with minimal switching activity on the state variables. Experiment shows significant improvement in power dissipation and testabilities for benchmark circuits.

This paper presents a new, compact, canonical graph-based representation, called Taylor expansion diagrams (TEDs). It is based on a general non-binary decomposition principle using Taylor series expansion. It can be exploited to facilitate the verification of high-level (RTL) design descriptions. We present the theory behind TEDs, comment upon its canonicity property and demonstrate that the representation has linear space complexity. Its application to equivalence checking of high-level design descriptions is discussed.

This paper addresses the problem of layout automation of datapath cells. It presents an analytical approach to transistor placement under full custom design style and demonstrates that it can be applied to practical datapath designs. The presented approach is based on a mathematical model which employs a mixed integer linear programming technique. The placement algorithm adopts the custom design techniques commonly used by datapath layout designers in generating hand-crafted designs. An important aspect of the presented method is the efficient management of the complexity of the underlying mathematical model which makes it applicable to real designs. The authors implemented the presented datapath design technique as an experimental software tool running in the industrial environment. The generated layout results are competitive with manual designs provided by experienced layout designers.

This paper presents a novel technique to evaluate the noncontrollability measures of state registers for partial scan design. Our model uses implicit techniques for finite state machine (FSM) traversal to identify noncontrollable state registers. By implicitly enumerating the states of a machine, we accurately evaluate the noncontrollability of flip-flops by determining exactly what values can or cannot be stored or are difficult to store in the state registers. By doing so, we not only target the untestable faults due to state unreachability of the machine but also the difficult-to-test faults caused by difficult-to-control flip-flops. The values observed in the flip-flops during the implicit FSM traversal are used to evaluate flip-flop controllability measures to support the testability analysis. This technique is programmed as an algorithm called SIMPSON and the authors analyze its effectiveness by carrying out extensive experiments over a large set of MCNC and ISCAS benchmarks. For large circuits, implicit state enumeration becomes infeasible because of computer memory and time limitations. To overcome these limitations, we propose the use of approximate reachability analysis of the circuit to estimate the noncontrollability of state registers. By partitioning a large FSM into smaller sub-FSMs, and implicitly traversing the individual submachines, the reachable state set can be overapproximated as a product of smaller subsets. The values observed in the flip-flops of the submachines during the approximate FSM traversal facilitates the estimation of their noncontrollability measures. An algorithm called SAMSON is proposed for this purpose and its effectiveness is illustrated over some of the larger circuits in the ISCAS benchmark suite. The results demonstrate the superiority of the authors' method over conventional state-of-the-art scan register selection techniques in terms of higher fault coverage achieved by selecting fewer, or an equal number, of partial scan registers.

This paper describes a novel logic decomposition theory and a practical logic synthesis system, BDS. It is based on a new binary decision diagrams (BDD) decomposition technique which supports all types of decomposition structures, including AND, OR, XOR, and complex MUX, both algebraic and Boolean. As a result, the method is very efficient in synthesizing both AND/OR and XOR-intensive functions. It also has a capability to handle very large circuits, as it employs the BDD decomposition in the partitioned Boolean network environment. The experimental results show that BDD-based logic decomposition is a promising alternative to the existing logic optimization approaches. In particular, it offers a superior runtime advantage over traditional logic synthesis systems.

LPSAT is an LP-based comprehensive infrastructure designed to solve the satisfiability (SAT) problem for complex RTL designs containing both word-level arithmetic operators and bit-level Boolean logic. The presented technique uses a mixed integer linear program to model the constraints corresponding to both domains of the design. Our technique renders the constraint propagation between the two domains implicit to the MILP solver thus enhancing the overall efficiency of the SAT framework. The experimental results are quite promising when compared with generic CNF-based and BDD-based SAT algorithms.

This paper describes a new BDD-based logic optimization system, BDS. It is based on a recently developed theory for BDD-based logic decomposition, which supports both algebraic and Boolean factorization. New techniques, which are crucial to the manipulation of BDDs in a partitioned Boolean network environment, are described in detail. The experimental results show that BDS has a capability to handle very large circuits. It offers a superior runtime advantage over SIS, with comparable results in terms of circuit area and often improved delay.

Binary Decision Diagrams have been widely used to solve the Boolean satisfiability (SAT) problem. The individual constraints can be represented using BDDs and the conjunction of all constraints provides all satisfying solutions. However, BDD-related SAT techniques suffer from size explosion problems. This paper presents two BDD-based algorithms to solve the SAT problem that attempt to contain the growth of BDD-size while identifying solutions quickly. The first algorithm, called BSAT, is a recursive, backtracking algorithm that uses an exhaustive search to find a SAT solution. The well known unate recursive paradigm is exploited to solve the SAT problem. The second algorithm is exploited to solve the SAT problem. The second algorithm, called INCOMPLETE-SEARCH-USAT (abbreviated IS-USAT), incorporates an incomplete search to find a solution. The search is incomplete inasmuch as it is restricted to only those regions that have a high likelihood of containing the solution, discarding the rest. Using our techniques we were able to find SAT solutions not only for all MCNC&ISCAS benchmarks, but also for a variety of industry standard designs.

Summary form only given. High noise immunity and level-restoring capabilities of static CMOS gates, combined with small area and low power of PTL cells, make a mixed CMOS/PTL design style an ideal alternative to the all-CMOS technology. However, the synthesis of mixed CMOS/PTL circuits imposes a great challenge to the existing synthesis methodology. Neither traditional techniques based on algebraic factorization nor methods based on direct BDD mapping are applicable to this new circuit style. We have recently proposed a new BDD-based logic optimization method for static CMOS. It is based on iterative BDD decomposition using various dominators which correspond to decomposable BDD structures leading to AND, OR, XOR and MUX decompositions. Synthesis results show that the method is very efficient for both AND/OR- and XOR-intensive functions. Since PTL structures can be easily identified on a BDD, our method can be readily extended to perform logic decomposition leading to mixed CMOS/PTL logic implementation. In contrast to other PTL synthesis techniques, based on direct BDD mapping, our method is not limited to decomposition onto PLTs only; its logic decomposition and optimization is driven by the capabilities of both the static CMOS and PTL logic. Our BDD decomposition method can also account for various parameters associated with circuit performance, thus avoiding drawbacks of direct BDD mapping-based synthesis, such as large fanouts and long transistor chains.

Current sequential optimization techniques apply a variety of logic transformations that mainly target the combinational logic component of the circuit. Retiming is typically applied as a postprocessing step to the gate-level implementation obtained after technology mapping. This paper introduces a new sequential logic transformation which integrates retiming with logic transformations at the technology-independent level. This transformation is based on implicit retiming across logic blocks and fanout stems during logic optimization. Its application to sequential network synthesis results in the optimization of logic across register boundaries. It can be used in conjunction with any measure of circuit quality for which a fast and reliable gain estimation method can be obtained. We immplemented our new technique within the SIS framework and demonstrated its effectiveness in terms of cycle-time minimization on a set sequential benchmark circuits.

This paper presents a retiming and resynthesis technique for cycle-time minimization of sequential circuits with feedback (finite state machines). Operating on the delay critical paths of the circuit, we perform a set of controlled local retimings of registers across fanout stems and logic gates, followed by local node simplifications. We guide the retiming of registers across fanout stems to induce equivalence relations among them, which are exploited for subsequent logic simplification. Our technique is able to analyze correlation of logic across register boundaries during simplification. We strive to minimize the increase in number of registers without sacrificing the cycle-time performance. The results demonstrate a favourable performance/area trade-off when compared with optimally retimed circuits.

Addresses the problem of the layout design automation of a datapath cell. We present a novel approach to the transistor placement problem for custom datapath design and we demonstrate that it can be applied to practical designs. Our approach is based on an analytical model which employs a mixed integer linear programming (MILP) technique. The novelty and originality of the method is the efficient management of the complexity of the underlying mathematical model. Our prototype tool automatically handles transistor merging, folding and intra-cell component sharing.

A unified logic optimization method efficient at handling both AND/OR-intensive and XOR-intensive functions is proposed. The method is based on iterative BDD decomposition using various dominators. Detail analysis of decomposable BDD structures leading to AND/OR, XOR and MUX decompositions are presented. Experiment shows that our synthesis results for AND/OR-intensive functions are comparable to those of SIS, and results for XOR-intensive functions are comparable to those of techniques targetting specifically XOR decomposition.

Article Transistor level placement for full custom datapath cell design Share on Authors: Durgam Vahia Department of Electrical and Computer Engineering, University of Massachusetts, Amherst, MA Department of Electrical and Computer Engineering, University of Massachusetts, Amherst, MAView Profile , Maciej Ciesielski Department of Electrical and Computer Engineering, University of Massachusetts, Amherst, MA Department of Electrical and Computer Engineering, University of Massachusetts, Amherst, MAView Profile Authors Info & Claims ISPD '99: Proceedings of the 1999 international symposium on Physical designApril 1999 Pages 158–163https://doi.org/10.1145/299996.300049Online:12 April 1999Publication History 8citation270DownloadsMetricsTotal Citations8Total Downloads270Last 12 Months0Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

Abs/rucf-Thii paper presents effisient reerscoding and reayntfs-is algorithms for cycle-time mirdmtition of rnrdtilevel tiplensentatimrs of synchronom finite state machines @Shfs)under a tied encoding length.me proposed technique is appficahle to both gate-level and technology independent synchmnom network rep~enfstimrs.We pr~ent two algorithm for identifying srsefulreencmfbrgs-one is based on Boolmn cube reprwentation apptieafrle to technology independent ayrrchmrsmssnetworks and tbe other employs recursive learning techniques appmpfiate for gate ne~.We show that the proposed XOtixNOR based reencadbsg technique mplores a sufficientlyrich set of encodings to identify implementations with smalIer cycle-times.The Boolwn and stmctural interpretations of reencoding are explored and ik relationship to isomorphic sequentially redundant faults is presented.We afso show that the reencoded circuit always has a vatid initial state and present a simple procedureto deriveiL The effectiveness of the proposedtechniqueis iUnstratedon a largeset of benchmarkcircuitswhichindfratman averagecycle-timeimprovement of 15.26%for a smallam overbcadof336Yaoverthat ofperfomsance~rivencombbsatfmsal logicoptimizafiom

This paper presents a novel technique and a practical algorithm for the selection of state registers for partial scan. Our model uses implicit techniques for FSM traversal to identify non-controllable state registers. Non-controllability of registers is evaluated by a systematic analysis of the state transitions and the encoding of the underlying FSM. By using our approach, we can not only identify non-controllable and difficult-to-control flip-flops, but also exploit the information of the unreachable states to judiciously select the minimum number of scan registers for high fault coverage. The effectiveness of our technique is illustrated over a large set of MCNC and ISCAS benchmarks. The results demonstrate the superiority of our method over conventional state-of-the-art scan register selection techniques in terms of higher fault coverage achieved by selecting fewer partial scan registers.

Wave-pipelining is a method of high-performance circuit design which implements pipelining in logic without the use of intermediate latches or registers. The combination of high-performance integrated circuit (IC) technologies, pipelined architectures, and sophisticated computer-aided design (CAD) tools has converted wave-pipelining from a theoretical oddity into a realistic, although challenging, VLSI design method. This paper presents a tutorial of the principles of wave-pipelining and a survey of wave-pipelined VLSI chips and CAD tools for the synthesis and analysis of wave-pipelined circuits.

This paper investigates the relationship between multi-cycle false paths and the testability of sequential circuits. We show that removal of multi-cycle false paths (either by circuit restructuring or by proper state encoding) improves circuit testability, though not as significantly as one would expect. We then investigate the use of partial scan. We demonstrate the inability of current structure-based scan register selection techniques to select the minimum possible set of registers. We propose a novel and efficient way to exploit the causes of multi-cycle false paths to judiciously choose scan registers for maximum possible testability.

This paper presents Metamorphosis-a novel technique for optimal state assignment targeting multi-level logic implementations. We present an elegant matrix formulation and a graph partitioning based synthesis technique which permits both bit-constrained and unconstrained encoding of a symbolic finite state machine (FSM) represented initially with a one-hot code. Optimal state encoding is achieved by controlled retiming/re-encoding and resynthesis of the symbolic FSM. The synthesis is guided directly by the cost function (optimization criterion) rather than speculative estimates of the encoding heuristics on the final design cost. The technique is illustrated through performance driven synthesis of FSM and extensions to handle other cost metrics is outlined.

Wave-pipelining has recently drawn considerable interest from both the academic and industrial communities as a method for high-speed pipelining without the use of intermediate latching. Although high-performance IC technologies, pipelined RISC and DSP architectures, and sophisticated CAD tools have enabled and driven several recent demonstration circuits, significant challenges remain before wave-pipelining will be used extensively in commercial chips. In this forum, we discuss whether these challenges are surmountable, and if so, what are the techniques that will be needed both now and with future VLSI technologies.>

Presents a method to functionally verify a network of interacting finite state machines (FSMs) at any level of abstraction. The verification tool developed can verify the FSM network at various stages of the synthesis process. It can verify the result of FSM decomposition both in the symbolic and binary-coded form. The tool has various options to help the designer in the synthesis of a decomposed sequential machine system. It can generate the decomposed submachines for a given decomposition from the prototype specification. It can also be used to simulate the network. An efficient enumeration-simulation method is used to traverse the state transition graph of the prototype machine in a depth first fashion. The algorithm can be used to verify the decomposed system even if the decomposition information is not known, thus allowing it to verify any FSM network.>

A method using a linear program for adjusting clock delays in individual flip-flops to minimize the clock period through the use of wave pipelining is discussed. Edge-triggered flip-flops are used as the circuit memory elements, and controlled delays are introduced in the time of clock signal arrivals at these elements. Constraints that relate the logic path delays from pairs of input flip-flops are derived. These constraints, in addition to known constraints relating input and output flip-flops, prevent destructive logic signal propagation interference. It is shown that in circuits without feedback the clock period reduction is limited by the shortest paths in the logic and the required signal separation between signals of distinct cycles. Application of this technique to logic with feedback is discussed.>

The problem of finite-state-machine decomposition into a number of smaller submachines is addressed. The number of submachines is decided by the algorithm on the basis of a partition of the outputs. The problem of determining the internal states in each submachine is formulated as a multiway partitioning of the original states using an m-way graph partitioning algorithm described herein. The results show an average of 39% decrease in delay and a small decrease in area for two-level implementations.>

The layer assignment problem arises in printed circuit board (PCB) and integrated circuit (IC) design. It involves the assignment of interconnect wiring to various planes of a PCB or to various layers of interconnect wires in an IC. This paper reviews basic techniques for layer assignment in both PCBs and ICs. Two types of layer assignment are considered: (1) constrained layer assignment in which routing of interconnections is given and the objective is to assign wires to specific layers, and (2) unconstrained, or topological, layer assignment, in which both the physical routing of interconnections and assignment of the wires to layers is sought. Various objective functions, such as via minimization and minimization of signal delays through interconnect lines are discussed.>

An efficient method for PLA decomposition, in which a single two-level Boolean function (PLA) is decomposed into two stages of cascaded PLAs such that the total area of all PLAs is smaller than that of the original PLA, is presented. The first stage may contain an arbitrary number of PLAs (generalized decoders), and the second stage contains a single PLA. Primary inputs are partitioned into disjoint sets of input variables and represented as multiple-valued variables so as to minimize the total PLA area. Two efficient algorithms for assignment of input variables to individual decoders are presented, one based on an integer programming technique and the other on graph partitioning. The constrained input encoding of the second-stage PLA is performed by an efficient procedure based on graph coloring and partitioning theory.>

A new theoretical formulation of the output encoding and state assignment targeting two-level logic implementations is presented.The formulation is based on a uniform representation of the input and output constraints.This allows to solve the input and output encoding problems, inherent in state assignment of FSM, simultaneously.The solution is based on the concept of dichotomy and graph coloring.

A linear program is used to direct the placement of Standard Cells such that the clock period is minimized.Constraints upon the logic path delays and the clock signal arrival times at the flipflops allow multiple signals, corresponding to several clock cycles, to exist simultaneously on the logic signal paths during operation.The linear program constraints relate the clock period to the maximum and minimum logic path delays.Delays are achieved in the clock and logic paths by the use of delay elements and resistive polysilicon wires in the interconnection network.

A novel theoretical formulation of the input encoding problem is presented, based on the concept of compatibility of dichotomies. The input encoding problem is shown to be equivalent to a two-level logic minimization. Three possible techniques to solve the encoding problem are discussed, based on: techniques borrowed from classical logic minimization (generation of prime dichotomies and solving the covering problem); graph coloring applied to the graph of incompatibility of dichotomies; and extraction of essential prime dichotomies followed by graph coloring. The extraction of essential prime dichotomies serves the same purpose as the extraction of essential prime implicants in logic minimization, in the sense that it reduces the size of the covering/graph coloring problem. The conditions of optimality of the solutions to the input encoding problem are discussed. For near-optimum results a powerful heuristic, based on an iterative improvement technique, has been developed and implemented as a computer program: dichotomy-based symbolic input encoding technique (DIET). The test results indicate the DIET compares favorably with KISS and NOVA in terms of the CPU time, is superior to both programs in terms of the encoding length, and requires considerably less memory. This method can be applied to the input encoding of combinational logic and the state assignment of finite state machines (FSMs) in both two-level and multilevel implementations.>

A method for PLA (programmable logic array) decomposition is presented whereby a single two-level Boolean function (PLA) is decomposed into two levels of cascaded PLAs. Primary inputs are partitioned into disjoint sets and represented as multiple-valued variables so as to minimize the total PLA area. Two new algorithms are presented for input variable assignment, based on (a) graph partitioning and (b) a mathematical optimization method. The constrained output encoding of first-level PLAs is performed by a fast and efficient procedure based on a graph-coloring technique.>

A method for the minimization of multiple-valued input Boolean functions is presented. It is based on the reduction of logic minimization problem to graph coloring, applied to the graph of incompatibility of implicants. In this approach, two NP-complete problems encountered in the minimization of Boolean functions, i.e. the generation of prime implicants and the covering problem, are reduced to a single, and better understood, graph coloring problem. A special type of implicants, called minimally split product implicants, is generated from an arbitrary set of input cubes that allow optimum results to be obtained. An important result of this method is that it is analytical, rather than heuristic, and gives more insight into a larger class of logic synthesis problems, such as input encoding and Boolean decomposition.>

A formulation of the layer assignment problem for VLSI circuits is presented in which the objective is to minimize the interconnect delay by taking into account the resistance and capacitance of interconnect wires and contacts. For MOS circuits with two layers of interconnections the problem is shown to be equivalent to that of minimizing a weighted resistance of the corresponding RC network. This formulation readily handles wires with preassigned layers, such as power supply lines or module terminals. With user-defined weights assigned to selected nets, this method can be used to minimize critical path delays. The problem is shown to be NP-complete. A polynomial-time approximation algorithm, based on graph partitioning technique, is presented along with some experimental results. The layer assignment algorithm presented in this paper has been implemented in LISP and tested on several design examples with complexity ranging from tens to a few hundred nets. Computational complexity of this algorithm is on the order of O(n/sup 2/) for building the required data structure, and O(n/sup 1.5/) for actual layer assignment, where n is the number of wire segments in the routing.>

A new graph-theoretic representation of the placement of rectangular IC blocks of arbitrary size and aspect ratio is proposed. This representation, called a relaxed digraph, provides an efficient model for two-dimensional calculations of minimum area layouts. Unlike other digraph models, the structure of the relaxed digraph represents an entire class of layout configurations derivable from a given initial placement of blocks. This model, therefore, provides greater flexibility in block placement than can be obtained from stiff digraph representations. A necessary and sufficient condition is derived for the existence of a nonoverlapping arrangement of rectangular cells in terms of the relaxed digraph representation. Based on this result, a fixed digraph representation can be selected from the relaxed digraphs that minimizes the layout area. The minimization utilizes positional constraints imposed by the relaxed digraphs and estimated routing space requirements. The area minimization is formulated as a quadratic optimization problem and solved using mathematical programming methods. The resulting modified digraph can then be used as a graph model for further calculations of a minimum area and routing-feasible layout.

This paper presents a new method for generating a two-dimensional routing for a class of custom integrated circuits (IC's). The method has been designed for Silc, an experimental silicon compiler currently under development at GTE Laboratories, and is suitable for the design of custom IC's composed of functional blocks. The method is based on an analytical model for generating a one-dimensional distribution of interconnections in irregularly shaped routing channels. The described procedure first determines the channel shapes that minimize the size of the layout and then allocates nets inside the channels while maintaining the required routing topology. One dimension of the layout is optimized at a time. Two-dimensional routing is obtained by coupling the minimization of the vertical and the horizontal dimensions of the layout with a set of additional constraints to ensure routing feasibility. The algorithm that implements this method has polynomial time complexity. The quality of the suboptimal results obtained with this method can be evaluated by comparison with the lower bounds obtained from independent, unconstrained linear programming solutions.

An analytical method is proposed for solving a routing area compaction problem in building block integrated circuits. Related minimization is performed with a linear programming technique. Minimum channel dimensions are calculated for a preliminary routing; these dimensions are used to construct routing constraints. Placement constraints are added for the interrelations between placement and routing. This combined set of constraints leads to a least overestimation of routing area and under certain conditions guarantees routing feasibility. Computational complexity and existence of a solution are discussed.