Search results for: Priyank Kalla
chapter
Reachability analysis is a tool for formal equivalence and model checking of sequential circuits. Conventional techniques are mostly bit-level, in that the reachable states, transition relations and property predicates are all represented using Boolean variables and functions. The problem suffers from exponential space and time complexities; therefore, some form of abstraction is desirable. This paper...
article
IEEE Transactions on Computer-Aided Design of Integrated Circuits and... > 2016 > 35 > 7 > 1206 - 1218
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,...
chapter
Lecture Notes in Computer Science > Tools and Algorithms for the Construction and Analysis of Systems > Decision Procedures and Theorem Provers > 618-631
This paper presents a CNF SAT-formulae transformation technique employing Gröbner bases as a means to analyze the problem structure. Gröbner-bases have been applied in the past for SAT; however, their use was primarily restricted to analyzing entire problems for proof-refutation. In contrast, this technique analyzes limited subsets of problems, and uses the derived Gröbner bases to yield new constraint-information...
chapter
Lecture Notes in Computer Science > Theory and Applications of Satisfiability Testing > Preface > 415-422
This paper presents a new technique to derive an initial static variable ordering for efficient SAT search. Our approach not only exploits variable activity and connectivity information simultaneously, but it also analyzes how tightly the variables are related to each other. For this purpose, a new metric is proposed – the degree of correlation among pairs of variables. Variable activity and correlation...
chapter
Advanced Techniques in Logic Synthesis, Optimizations and Applications > Logic Optimization > 251-266
Datapath designs that perform polynomial computations over bit-vectors are found in many practical applications, such as in Digital Signal Processing, communication, multi-media, and other embedded systems. With the growing market for such applications, advancements in synthesis and optimization techniques for polynomial datapaths are desirable. Common sub-expression extraction (CSE) serves as a useful...
chapter
Hybrid integration of opto-electronic integrated circuits (OEICs) with CMOS electronics requires the modeling and characterization of thermal interactions. The thermal-gradient generated by the electronic layer causes modulation of the refractive index of the optical layers. This requires a thermal characterization for thermal-aware integration of OEICs. Full-scale, coupled, 3D electromagnetic and...
chapter
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...
chapter
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...
chapter
Sequential Galois field (F2k) arithmetic circuits take k-bit inputs and produce a k-bit result, after k-clock cycles of operation. Formal verification of sequential arithmetic circuits with large datapath size is beyond the capabilities of contemporary verification techniques. To address this problem, this paper describes a verification method based on algebraic geometry that: i) implicitly unrolls...
chapter
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...
article
IEEE Transactions on Computer-Aided Design of Integrated Circuits and... > 2014 > 33 > 6 > 814 - 825
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...
chapter
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...
chapter
Silicon photonics technology is progressing at a rapid pace. Despite greatly expanded manufacturing capability, physical design of integrated optical circuits currently lacks the level of automation found in VLSI design. A key component of integrated optic design is waveguide routing; however, unlike VLSI, where signal nets are routed with metal layers and vias, photonic waveguides are fabricated...
chapter
Increasing scope and applications of integrated optics necessitates the development of automated techniques for physical design of optical systems. This paper presents an automated, planar channel routing technique for integrated optical waveguides. Integrated optics is a planar technology and lacks the inherent signal restoration capabilities of static-CMOS. Therefore, signal loss minimizationas...
article
IEEE Transactions on Computer-Aided Design of Integrated Circuits and... > 2013 > 32 > 9 > 1409 - 1420
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...
chapter
Advancements in silicon photonics technology are enabling large scale integration of electro-optical circuits and systems. To fully exploit this potential, automated techniques for design space exploration and physical synthesis for integrated optics must be developed. This paper investigates how conventional VLSI physical design automation techniques can be adapted for integrated optics applications...
chapter
Finite (Galois) field arithmetic finds applications in cryptography, error correction codes, signal processing, etc. Multiplication usually lies at the core of all Galois field computations and is a high-complexity operation. This paper addresses the problem of formal verification of hardware implementations of modulo-multipliers over Galois fields of the type ${\mathbb{F}}_{2^k}$, using a computer-algebra/algebraic-geometry...
chapter
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 F2k, using a computer-algebra/algebraic-geometry based approach. The...
chapter
Galois field computations abound in many applications, such as in cryptography, error correction codes, signal processing, among many others. Multiplication usually lies at the core of such Galois field computations, and is one of the most complex operations. Hardware implementations of such multipliers become very expensive. Therefore, there have been efforts to reduce the design complexity by decomposing...
chapter
Welcome to the 2009 IEEE International High Level Design Validation and Test Workshop, the 14th in a series of events that explores emerging trends, innovative research and scalable solutions in the areas of validation and test for electronic systems. The two day technical program includes exciting sessions on topics such as design validation approaches at RTL and at system-level, high-level modeling...
