We present an approach to partial logic synthesis of arithmetic circuits. Its targeted applications are rectification of buggy circuits, and computing care and don't care sets at internal nets of the circuit. The approach models the circuit by way of polynomial ideals in rings with coefficients in the field of rationals (ℚ). Techniques from commutative algebra are applied to compute internal patch functions as polynomials over ℚ. We describe how the care set and the don't care conditions manifest in the algebraic setting, and show how to generate corresponding Boolean functions from polynomials over ℚ. Experiments are conducted over various integer multiplier architectures which demonstrate the efficacy of our approach, where SAT/interpolation based techniques are infeasible.

As silicon photonic integrated circuits (PICs) increase in complexity, ensuring their reliability against manufacturing and operational variations necessitates robust Design-for-Test (DfT) strategies. We present an adaptable methodology for DfT insertion in large-scale PICs, centered on physics-informed hypergraph partitioning. Our approach uniquely leverages hypergraph-based weighting derived from process sensitivities (e.g. etch, doping) and operational drifts (e.g. thermal, injection), quantified using partial derivatives from foundry data or Transfer Matrix Method (TMM) simulations. This assigns actionable risk values to both devices (nodes) and interconnects (hyperedges). We employ k-way partitioning to achieve finer sub-network isolation and targeted test access, crucial for vulnerability localization in complex PICs like multi-level ring resonator networks or large MZI-based crossbars. Experiments performed on PIC designs demonstrate the application of the proposed risk coverage metric to vulnerability localization and test point insertion, achieved with quantifiable and moderate overhead.

This paper proposes a design-for-test (DFT) methodology and architecture for testing and validation of silicon photonic integrated circuits (PICs). We describe the design of silicon photonic circuits and components that comprise the proposed DFT architecture. The designs are extensively simulated and validated as test-access and fault-detection circuitry. We demonstrate how the DFT approach can be deployed on photonic integrated circuits and how they can be tested for correct operation, in terms of signal power and phase. The application is demonstrated on two distinct types of designs – an optical neural network comprising optical devices in a feed-forward topology, and an optical logic circuit with feedback loops.

This paper proposes a symbolic algebra approach for multi-target rectification of integer arithmetic circuits. The circuit is represented as a system of polynomials and rectified against a polynomial specification with computations modeled over the field of rationals. Given a set of nets as potential rectification targets, we formulate a check to ascertain the existence of rectification functions at these targets. Upon confirmation, we compute the patch functions collectively for the targets. In this regard, we show how to synthesize a logic sub-circuit from polynomial artifacts generated over the field of rationals. We present new mathematical contributions and results to substantiate this synthesis process. We present two approaches for patch function computation: a greedy approach that resolves the rectification functions for the targets and an approach that explores a subset of don’t care conditions for the targets. Our approach is implemented as custom software and utilizes the existing open-source symbolic algebra libraries for computations. We present experimental results of our approach on several integer multipliers benchmark and discuss the quality of the patch sub-circuits generated.

This paper addresses the rectification of faulty finite field arithmetic circuits by computing patch functions at internal nets using techniques from polynomial algebra. Contemporary approaches that utilize SAT solving and Craig interpolation are infeasible in rectifying arithmetic circuits. Given candidate nets, prior algebra-based techniques can ascertain whether the circuit admits multi-fix rectification at these nets but cannot compute patch functions. We show how the algebraic computing model facilitates the exploration of admissible rectification functions, collectively, for the nets. This model also enables the exploitation of don’t care conditions for the synthesis and realization of the patches. Experimental results on large operand width finite field benchmarks, as used in cryptography, substantiate our approach.

When formal verification identifies the presence of a bug in a design, it is required to rectify the circuit at some net(s). Modern approaches formulate the rectification test as an unsatisfiability proof, and then use Craig interpolants (CI) in propositional logic to compute the corresponding rectification functions. Boolean SAT and CI engines are infeasible in rectification of finite field arithmetic circuits, where polynomial algebra is more suitable. Recently, it was shown that CI exist in polynomial algebra in finite fields. This paper presents a detailed theory and algorithms for CI in finite fields, and characterizes the lattice of all algebraic interpolants. Using the Gröbner basis algorithm, we present techniques to traverse the interpolant lattice. This allows to explore various interpolants for efficient synthesis of rectification functions for finite field arithmetic circuits. Experimental results are presented that demonstrate the efficacy of our approach.

Recent developments in formal verification of arithmetic datapaths make efficient use of symbolic computer algebra algorithms. The circuit is modeled as an ideal in polynomial rings, and Gröbner basis (GB) reductions are performed over these polynomials to derive a canonical representation. As they model logic gates of the circuit, the ideals comprise largely of Boolean (or pseudo-Boolean) polynomials. This paper considers a logic synthesis analogue of GB reductions over Boolean polynomials, by interpreting symbolic algebra as the unate cube set algebra over characteristic sets. By representing Boolean polynomials as characteristic sets using zero-suppressed binary decision diagrams (ZDDs), implicit algorithms are efficiently designed for GB-reduction for datapath circuits. We show that the imposition of circuit-topology-based monomial orders exposes a special structure on the ZDD representation of the polynomials. The subexpressions employed in the GB-reduction are readily visible as subgraphs on the ZDDs, which are directly used to compose the result. Our division algorithms effectively cancel multiple monomials implicitly in one-step, simplify the search for divisors, and avoid intermediate size explosion. Experiments performed over various finite field arithmetic architectures demonstrate the efficiency of our algorithms and implementations; our approach is orders of magnitude faster as compared to conventional methods.

Formal verification of arithmetic circuits checks whether or not a gate-level circuit correctly implements a given specification model. In cases where this equivalence check fails - the presence of a bug is detected - it is required to: i) debug the circuit, ii) identify a set of nets (signals) where the circuit might be rectified, and iii) compute the corresponding rectification functions at those locations. This paper addresses the problem of post-verification debugging and correction (rectification) of finite field arithmetic circuits. The specification model and the circuit implementation may differ at any number of inputs. We present techniques that determine whether the circuit can be rectified at one particular net (gate output) - i.e. we address single-fix rectification.Starting from an equivalence checking setup modeled as a polynomial ideal membership test, we analyze the ideal membership residue to identify potential single-fix rectification locations. Subsequently, we use Nullstellensatz principles to ascertain if indeed a single-fix rectification can be applied at any of these locations. If a single-fix rectification exists, we derive a rectification function by modeling it as the synthesis of an unknown component problem. Our approach is based upon the Gröbner basis algorithm, which we use both as a decision procedure (for rectification test) as well as a quantification procedure (for computing a rectification function). Experiments are performed over various finite field arithmetic circuits that demonstrate the efficacy of our approach, whereas SAT-based approaches are infeasible.

When formal verification of arithmetic circuits identifies the presence of a bug in the design, the task of rectification needs to be performed to correct the function implemented by the circuit so that it matches the given specification. This paper addresses the problem of rectification of buggy finite field arithmetic circuits. The problems are formulated by means of a set of polynomials (ideals) and solutions are proposed using concepts from computational algebraic geometry. Single-fix rectification is addressed - i.e. the case where any (set of) bugs can be rectified at a single net (gate output). We determine if single-fix rectification is possible at a particular location, formulated as the Weak Nullstellensatz test. Subsequently, we introduce the concept of Craig interpolants in polynomial algebra over finite fields and show that the rectification function can be computed using algebraic interpolants. Experimental results demonstrate the superiority of our approach against SAT-based approaches.

This paper introduces a technique to derive a word-level abstraction of the function implemented by a combinational logic circuit. The abstraction provides a canonical representation of the function as a polynomial${Z} {= {\mathcal {F}}(A)}$over the finite field$ {{\mathbb {F}}_{2^{k}}}$, where${Z}$and$ {A}$represent the${k}$-bit output and input bit-vectors (words) of the circuit, respectively. This canonical abstraction can be utilized for formal verification and equivalence checking of combinational circuits. Our approach to abstraction is based upon concepts from computational commutative algebra and algebraic geometry. We show that the abstraction${Z} {= {\mathcal {F}}(A)}$can be derived by computing a Gröbner basis of the polynomials corresponding to the circuit, using a specific elimination term order derived from the circuit’s topology. Computing Gröbner bases using elimination term orders is infeasible for large circuits. To overcome this limitation, we describe an efficient symbolic computation to derive the word-level polynomial. Our algorithms exploit: 1) the structure of the circuit; 2) the properties of Gröbner bases; 3) characteristics of finite fields$ {{\mathbb {F}}_{2^{k}}}$; and 4) modern algorithms from symbolic algebra, to derive the canonical polynomial representation. This approach is employed to verify (and detect bugs in) large combinational finite field arithmetic circuits, where contemporary verification techniques are known to be infeasible.

Algebraic geometry is the study of the geometry of solutions to a system of multivariate polynomial equations. Modern algebraic geometry does not explicitly solve the system of equations to enumerate the solutions, but rather reasons about the presence, absence, dimensions or intersection properties of the solution-sets, etc. Abstract and computational algebra is often used for this purpose - particularly the theory and technology of Grobner bases, which provides a very powerful set of tools to solve many polynomial decision problems. In this talk, I will present a tutorial on how some of these techniques from algebraic geometry and commutative algebra can be used for formal verification of RTL datapaths and arithmetic circuits. Datapath designs implement arithmetic computations over finite word-length operands, say, over k-bit vectors. These circuits implement functions that are mappings over k-dimensional Boolean spaces f : Bk → Bk. Such functions can also be construed as mappings over: i) finite integer rings of the type Z2k≡ Z (mod 2k), i.e. as functions f : Z2k→ Z2k; or ii) as functions over the Galois field of 2k elements, i.e. f : F2k→ F2k. The designs can then be modeled as a system of polynomial functions over Z2kor F2k, and Grobner basis techniques can be applied for verification by reasoning about the solutions (functions) of the polynomial systems (circuits). Given the arithmetic nature of the designs, such an approach provides a natural word-level abstraction which can enable efficient verification. While Grobner basis techniques are very powerful, the computation suffers from high complexity. Therefore, the main focus of the tutorial will be on how to overcome this complexity. I will describe: . How to formulate various verification problems using ideal membership, Nullstellensatz, elimination theory and Grobner bases; . How to exploit the number-theoretic properties of finite rings and fields to simplify the problems; . How to analyze the structure/topology of the given circuits to get more theoretical insights into the corresponding polynomial ideals, and use this information to improve the computation; and . How to implement the aforementioned concepts using modern symbolic computation algorithms, e.g. Faugere's F4-style reductions, for practical datapath verification. Arithmetic datapaths are usually custom designed, and they often exhibit some structure or symmetry in the implementations. Grobner bases can help identify this inherent symmetry. By exploiting this information, efficient symbolic computation algorithms can then be devised for scalable verification. The verification context will be motivated by applications such as elliptic curve cryptography, error correcting circuits, polynomial signal processing, word-level RTL synthesis, etc. I will provide information on various resources - publications, design benchmarks and the verification tools developed by us - so that interested participants can explore this exciting area of work. I will conclude by describing important unsolved problems in this specific area, and the challenges that need to be overcome to fully exploit the potential of the theory and technology.

Design automation (DA) is at a historical moment where it has a chance - after mathematics, statistics, and computer science - to establish itself as the fourth universal approach with widespread applications in a variety of scientific, engineering, and economic domains. We start by outlining some of the most important research contributions and industrial applications of the design automation; we identify key conceptual DA techniques and describe how they interact to form synthesis and analysis flows. Next, we discuss the most attractive emerging and pending DA domains by analyzing several recent technologies, applications, and conceptual trends. Our emphasis is not just on the most challenging research or the most lucrative application areas but also on the technological trends relevant to DA. Furthermore, we elaborate on the types of new DA techniques and tools that are required for further fundamental progress and improved practical relevance. In order to provide a balanced picture of DA, we also identify the most pronounced dangers in false starts and false research in DA. Finally, we briefly discuss the need for a DA educational reform and community social reorganization that are beneficial for rapid and impactful research and development contributions.

Custom arithmetic circuits designed over Galois fields F2k are prevalent in cryptography, where the field size k is very large (e.g. k = 571-bits). Equivalence checking of such large custom arithmetic circuits against baseline golden models is beyond the capabilities of contemporary techniques. This paper addresses the problem by deriving word-level canonical polynomial representations from gate-level circuits as Z = F (A) over F2k, where Z and A represent the output and input bit-vectors of the circuit, respectively. Using algebraic geometry, we show that the canonical polynomial abstraction can be derived by computing a Gröbner basis of a set of polynomials extracted from the circuit, using a specific elimination (abstraction) term order. By efficiently applying these concepts, we can derive the canonical abstraction in hierarchically designed, custom arithmetic circuits with up to 571-bit datapath, whereas contemporary techniques can verify only up to 163-bit circuits.

Photonic ring-resonators are key components of many on-chip optical-interconnect wavelength division multiplexing (WDM) network architectures. Thermal interactions between on-chip heat-sources and ring resonators pose significant operational and integration challenges, as these devices are extremely sensitive to temperature-induced changes in refractive index. Contemporary literature proposes active compensation for such refractive index variations (e.g. carrier-injection based tuning and/or WDM channel remapping); however, these are costly in terms of power and area. This paper presents a thermal-aware synthesis approach for ring-resonator compensation. We show how ring-resonators are analyzed in the presence of external thermal gradients, and employ a perturbation analysis to derive an equivalent, trimming-enabled, ring-resonator design. Our methodology produces a design-template that can be used to compensate for thermal variations through modifications to the waveguide's geometric structure. This approach complements active compensation techniques, and the synthesis is compatible with contemporary lithographic methods. Using this approach, we perform design space exploration with respect to variations to the waveguide structure and their effect on the range and precision of thermal compensation.

Increasing scope and applications of integrated optics necessitates the development of automated techniques for physical design of optical systems. A key area of integrated optic design is waveguide routing, which currently lacks the level of automation found in VLSI design. Unlike VLSI, where signal nets are routed with metal layers and vias, integrated optics is a planar technology and lacks the inherent signal restoration capabilities of static-CMOS. Waveguides suffer signal loss due to planar (perpendicular) waveguide crossings and also from sharp bends. Therefore, in contrast to area or wire length, signal loss minimization - as a function of waveguide crossings and bends - is a primary objective of any routing solution. Our studies show that waveguide routing problems can be suitably formulated as planar channel routing. This paper investigates channel routing for integrated optical waveguides fabricated in a planar substrate. We present routing techniques where crossings, bends, and area are accounted for in an integrated solution. Two distinct channel routing techniques are presented: 1) a new channel router based on net sorting and utilizing non-Manhattan routing grids and 2) a router based on crossing-aware graph-constrained track assignment that also exploits waveguide curves to improve track utilization. Both techniques are crossing-minimal, and are also constrained suitably to reduce bend loss and area. We compare and evaluate the performance of our channel routers on a number of optical design benchmarks.

Galois field arithmetic is a critical component in communication and security-related hardware, requiring dedicated arithmetic architectures for better performance. In many Galois field applications, such as cryptography, the data-path size in the circuits can be very large. Formal verification of such circuits is beyond the capabilities of contemporary verification techniques. This paper addresses formal verification of combinational arithmetic circuits over Galois fields of the type${\BBF}_{2^{k}}$using a computer-algebra/algebraic-geometry-based approach. The verification problem is formulated as membership testing of a given specification polynomial in a corresponding ideal generated by the circuit constraints. Ideal membership testing requires the computation of a Gröbner basis, which is computationally very expensive. To overcome this limitation, we analyze the circuit topology and derive a term order to represent the polynomials. Subsequently, using the theory of Gröbner bases over${\BBF}_{2^{k}}$, we show that this term order renders the set of polynomials itself a minimal Gröbner basis of this ideal. Consequently, the verification test reduces to a much simpler case of Gröbner basis reduction via polynomial division, significantly enhancing verification efficiency. To further improve our approach, we exploit the concepts presented in the$F4$algorithm for Gröbner basis, and show that the verification test can be formulated as Gaussian elimination on a matrix representation of the problem. Finally, we demonstrate the ability of our approach to verify the correctness of, and detect bugs in, up to 163-bit circuits in${\BBF}_{2^{163}}$—whereas verification utilizing contemporary techniques proves infeasible.

Galois field arithmetic finds application in many areas, such as cryptography, error correction codes, signal processing, etc. Multiplication lies at the core of most Galois field computations. This paper addresses the problem of formal verification of hardware implementations of (modulo) multipliers over Galois fields of the type F(2k), using a computer-algebra/algebraic-geometry based approach. The multiplier circuit is modeled as a polynomial system in F(2k)[x1, x2, ... , xd] and the verification problem is formulated as a membership test in a corresponding (radical) ideal. This requires the computation of a Gröbner basis, which can be computationally intensive. To overcome this limitation, we analyze the circuit topology and derive a term order to represent the polynomials. Subsequently, using the theory of Gröbner bases over Galois fields, we prove that this term order renders the set of polynomials itself a Gröbner basis of this ideal - thus significantly improving verification. Using our approach, we can verify the correctness of, and detect bugs in, upto 163-bit circuits in F(2163); whereas contemporary approaches are infeasible.

As silicon photonics technology matures, optical devices will be available on a scale never before seen or utilized. It is therefore imper-ative to develop automated methods for synthesizing optical devices for large-scale designs. We present design and synthesis method-ologies for implementing digital logic using conventional integrated optical components, specifically optical cross-bar routing devices based on Mach-Zehnder Interferometry. Our design methodologies utilize the unique advantages of these optical devices, while also addressing the limitations of the technology. We extend these design concepts to include technology-specific logic sharing, and provide automated techniques for logic design implementation, evaluating the efficacy of our techniques on a number of logic designs. Through the convergence of communications and computing, optical devices are utilized on scales beyond traditional optic design.

Common sub-expression elimination (CSE) serves as a useful optimization technique in the synthesis of arithmetic datapaths described at RTL. However, CSE has a limited potential for optimization when many common sub-expressions are not exposed. Given a suitable transformation of the polynomial system representation, which exposes many common sub-expressions, subsequent CSE can offer a higher degree of optimization. The objective of this paper is to develop algebraic techniques that perform such a transformation, and present a methodology to integrate it with CSE to further enhance the potential for optimization. In our experiments, we show that this integrated approach outperforms conventional methods in deriving area-efficient hardware implementations of polynomial systems.

No abstract available.

This paper addresses the problem of solving finite word-length (bit-vector) arithmetic with applications to equivalence verification of arithmetic datapaths. Arithmetic datapath designs perform a sequence of add, mult, shift, compare, concatenate, extract, etc., operations over bit-vectors. We show that such arithmetic operations can be modeled, as constraints, using a system of polynomial functions of the type f : Z2n1times Z2n2timesldrldrldrtimes Z2ndrarr Z2m. This enables the use of modulo-arithmetic based decision procedures for solving such problems in one unified domain. We devise a decision procedure using Newtonpsilas p-adic iteration to solve such arithmetic with composite moduli, while properly accounting for the word-sizes of the operands. We describe our implementation and show how the basic p-adic approach can be improved upon. Experiments are performed over some communication and signal processing designs that perform non-linear and polynomial arithmetic over word-level inputs. Results demonstrate the potential and limitations of our approach, when compared against SAT-based approaches.

This paper addresses simulation-based verification of high-level [algorithmic, behavioral, or register-transfer level (RTL)] descriptions of arithmetic datapaths that perform polynomial computations over finite word-length operands. Such designs are typically found in digital signal processing (DSP) for audio/video and multimedia applications; where the word-lengths of input and output signals (bit-vectors) are predetermined and fixed according to the desired precision. Initial descriptions of such systems are usually specified as Matlab/C code. These are then automatically translated into behavioral/RTL descriptions for subsequent hardware synthesis. In order to verify that the initial Matlab/C model is bit-true equivalent to the translated RTL, how many simulation vectors need to be applied? This paper derives some important results that show that exhaustive simulation is not necessary to prove/disprove their equivalence. To derive these results, we model the datapath computations as polynomial functions over finite integer rings of the form , where corresponds to the bit-vector word-length. Subsequently, by exploring some number theoretic and algebraic properties of these rings, we derive an upper bound on the number of simulation vectors required to prove equivalence or to identify bugs. Moreover, these vectors cannot be arbitrarily generated. We identify exactly those vectors that need to be simulated. Experiments are performed within practical computer-aided design (CAD) settings to demonstrate the validity and applicability of these results.

This paper presents an approach to area optimization of arithmetic datapaths that perform polynomial computations over bit-vectors with finite widths. Examples of such designs abound in DSP for audio, video and multimedia computations where the input and output bit-vector sizes are dictated by the desired precision. A bit-vector of size m represents integer values reduced modulo 2m(%2m). Therefore, finite word-length bit-vector arithmetic can be modeled as algebra over finite integer rings, where the bit-vector size dictates the ring cardinality. This paper demonstrates how the number-theoretic properties of finite integer rings can be exploited for optimization of bit-vector arithmetic. Along with an analytical model to estimate the implementation cost at RTL, two algorithms are presented to optimize bit-vector arithmetic. Experimental results, conducted within practical CAD settings, demonstrate significant area savings due to our approach.

Polynomial computations over fixed-size bitvectors are found in many practical datapath designs. For efficient RTL synthesis, it is important to identify good decompositions of the polynomial into smaller/simpler units. Symbolic computer algebra algorithms and tools have been used for this purpose. However, fixed-size (m) bit-vector arithmetic is polynomial algebra over the finite integer ring Z2m, which is a non-unique factorization domain (non-UFD). While non-UFDs provide an extra freedom to search for decompositions, they complicate polynomial manipulation as traditional division-based algorithms are inapplicable. This paper presents new mathematical concepts for polynomial decomposition over Z2m, for RTL synthesis over fixedsize m-bit vectors. Given a polynomial, we identify a specific set of linear expressions and compute the Gröbner bases of their ideal (over non-UFD Z2m) using syzygies. This basis serves as good building-blocks for the given computation. A decomposition is identified by subsequent Gröbner basis reduction. Experimental results demonstrate significant area savings due to our approach, as compared against contemporary datapath synthesis techniques.

This article presents an approach to area optimization of arithmetic datapaths at register-transfer level (RTL). The focus is on those designs that perform polynomial computations (add, mult) over finite word-length operands (bit-vectors). We model such polynomial computations over m -bit vectors as algebra over finite integer rings of residue classes Z 2 m . Subsequently, we use the number-theoretic and algebraic properties of such rings to transform a given datapath computation into another, bit-true equivalent computation. We also derive a cost model to estimate, at RTL, the area cost of the computation. Using the transformation procedure along with the cost model, we devise algorithmic procedures to search for a lower-cost implementation. We show how these theoretical concepts can be applied to RTL optimization of arithmetic datapaths within practical CAD settings. Experiments conducted over a variety of benchmarks demonstrate substantial optimizations using our approach.

This paper addresses the problem of equivalence verification of RTL descriptions that implement arithmetic computations (add, mult, shift) over bit-vectors that have differing bit-widths. Such designs are found in many DSP applications where the widths of input and output bit-vectors are dictated by the desired precision. A bit-vector of size n can represent integer values from 0 to 2n- 1; i.e. integers reduced modulo 2n. Therefore, to verify bit-vector arithmetic over multiple word-length operands, we model the RTL datapath as a polynomial function from Z2n1times Z2n2times ... Z2ndto Z2m. Subsequently, RTL equivalence f equiv g is solved by proving whether (f - g) equiv 0 over such mappings. Exploiting concepts from number theory and commutative algebra, a systematic, complete algorithmic procedure is derived for this purpose. Experimentally, we demonstrate how this approach can be applied within a practical CAD setting. Using our approach, we verify a set of arithmetic datapaths at RTL where contemporary approaches prove to be in feasible

This paper addresses simulation-based verification of high-level descriptions of arithmetic datapaths. Instances of such designs are commonly found in DSP for audio, video and multimedia applications, where the word-lengths of input/output bit-vectors are fixed according to the desired precision. Initial descriptions of such systems are usually specified as Matlab/C code. These are then automatically translated into behavioural/RTL descriptions (HDL) for subsequent hardware synthesis. In order to verify that the initial Matlab/C model is bit-true equivalent to the translated RTL, how many simulation vectors need to be applied? This paper explores results from number theory and commutative algebra to show that exhaustive simulation is not necessary for testing their equivalence. In particular, we derive an upper bound on the number of simulation vectors required to prove equivalence or identify bugs. These vectors cannot be arbitrarily generated; we determine exactly those vectors that need to be simulated. Extensive experiments are performed within practical CAD settings to demonstrate the validity and applicability of these results

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

This paper addresses the problem of equivalence verification of RTL descriptions. The focus is on datapath-oriented designs that implement polynomial computations over fixed-size bit-vectors. When the size (m) of the entire datapath is kept constant, fixed-size bit-vector arithmetic manifests itself as polynomial algebra over finite integer rings of residue classes Z/sub 2//sup m/. The verification problem then reduces to that of checking equivalence of multi-variate polynomials over Z/sub 2//sup m/. This paper exploits the concepts of polynomial reducibility over Z/sub 2//sup m/ and derives an algorithmic procedure to transform a given polynomial into a unique canonical form modulo 2/sup m/. Equivalence testing is then carried out by coefficient matching. Experiments demonstrate the effectiveness of our approach over contemporary techniques.

This paper addresses the problem of equivalence verification of high-level/RTL descriptions. The focus is on datapath-oriented designs that implement univariate polynomial computations over fixed-size bit-vectors. When the size (m) of the entire datapath is kept constant, fixed-size bit-vector arithmetic manifests itself as polynomial algebra over finite integer rings of residue classes Z/sub 2//sup m/. The verification problem then reduces to that of checking equivalence of over Z/sub 2//sup m/ in other words, to prove f(x)%2/sup m/ /spl equiv/ g(x)%2/sup m/. This paper transforms the equivalence verification problem into proving (f(x) - g(x))%2/sup m/ /spl equiv/ 0. Exploiting the theory of vanishing polynomials over finite integer rings, a systematic algorithmic procedure is derived to establish whether or not a given polynomial vanishes (always evaluates to 0) over Z/sub 2//sup m/. Experiments demonstrate the effectiveness of our approach over contemporary techniques.

Contemporary techniques to identify a good variable order for SAT rely on identifying minimum tree-width decompositions. However, the problem finding a minimal width tree decomposition for an arbitrary graph is NP complete. The available tools and methods are impratical, as they cannot handle large and hard-to-solve CNF-SAT instances. This paper proposes a novel hypergraph partitioning based constraint decomposition technique as an alternative to contemporary methods. We model the CNF-SAT problem on a hypergraph and apply min-cut based bi-partitioning. Clause-variable statistics across the partitions are analyzed to further decompose the problem, iteratively. The resulting tree-like decomposition provides a variable order for guiding CNF-SAT search. Experiments carried out over a large and varied set of benchmarks demonstrate that our partitioning procedure is very fast and scalable. The variable order derived through the partitioning results in significant increase in performance (often orders of magnitude) of the SAT engine.

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

Contemporary FPGA synthesis is a multiphase process that involves technology-independent logic optimization followed by FPGA-specific mapping to a target FPGA technology. Conventional technology-independent transformations target standard cells and are unable to optimize circuits with constraints and goals specific to FPGA architectures. This article describes an FPGA-specific logic synthesis approach, which unites multilevel logic transformation, decomposition, and optimization techniques into a single synthesis framework. This system performs network transformation, decomposition, and optimization at an early stage to generate a network that can be directly mapped onto FPGAs. Our techniques are built upon a BDD-based logic decomposition system. With this system, both AND-OR decompositions and AND-XOR decompositions can be identified, resulting in large area savings for synthesized XOR-intensive circuits. To induce good decompositions, a maximum fanout free cone (MFFC) -based partial clustering and collapsing technique is used. This step is followed by an area-minimizing variable partitioning heuristic that decomposes collapsed nodes into LUT-feasible subfunctions. As a postprocessing step, a performance-driven resynthesis phase is performed to alleviate increased delay caused by excessive logic sharing. We compare the quality of results obtained using our techniques with those of academic (BoolMap, SIS) and industry (Altera Quartus) FPGA synthesis tools. Experimental results indicate that the circuits generated by our techniques are not only smaller, but are also significantly faster than those synthesized by conventional FPGA synthesis tools. Furthermore, the computation times required by our techniques are significantly smaller than those of previous techniques.

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.

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.

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.

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.

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.