Priyank Kalla

Assistant Professor

Education:

Ph.D., University of Massachusetts at Amherst, 2002.
M.S., University of Massachusetts at Amherst, 1998.
B.E., Birla Vishvakarma Mahavidyala, 1993.

Research Interests
My area of work is related to automated synthesis and optimization, validation and verification of digital VLSI systems:

Formal Verification of RTL descriptions

Equivalence Checks, RTL-Satisfiability, Assertion Checking.

Application of Finite Ring Algebra to Synthesis and Verification of Arithmetic Datapaths with Finite Word-Length Operands:

Modeling Bit-Vector Arithmetic as Polynomial Functions over Finite Integer Rings
Decision Procedures based on Algorithmic Analysis of Polynomial Ideals and their Varieties

New Techniques to Guide CNF-SAT Search:

Static and Dynamic Variable Orderings, Constraint Partitioning
Proving UNSAT by Directly Searching for UNSAT Cores.

Using Groebner's Proof Systems for Simplification of Design Verification and SAT solving.
Logic Synthesis for Optical and Photonic Logic

Funding for Our Research

NSF, GOALI Supplement Grant 2008-2010.
NSF Faculty Early Career Development (CAREER) Award 2006.
NSF, CISE/CCF, 1-Year Grant, 2005-2006. Expired.
University of Utah Research Foundation, SEED Grant, 2005-2006. Expired.

Graduate Students

Sivaram Gopalakrishnan - MS 2004, PhD student. High-Level Synthesis of Arithmetic Datapaths.
Chris Condrat - BS/MS 2007, PhD student. Logic Synthesis for Optical and Photonic Technologies.
Neal Tew - BS 2008. Moving on to MS.
Former Students

Namrata Shekhar - PhD, Completed Aug 2007. Senior R & D Engineer, Synopsys, Formality Group, Marlborough, MA. Dissertation Title: Equivalence Verification of Arithmetic Datapaths using Finite Ring Algebra.
Vijay Durairaj - ME 2004, PhD summer 2008. Senior R & D Engineer, Synopsys ESP Group . Dissertation topic: Improving SAT Solving by Analyzing Constraint-Variable Dependencies.

Conferences

I am chairing the Technical Program for HLDVT 2008. Please consider submitting your work to HLDVT. Link to Conference Website .

Invited Talks

Upcoming seminar on datapath verification using finite integer algebras, at the Intl. Workshop on Constraints in Verification, Aug 2008.

Synthesis and Verification of Arithmetic Datapaths using Finite Ring Algebra - ECE Dept., University of Massachusetts at Amherst and Dept. of Mathematics and Statistics, Georgia State University, April 2006.

Publications and Presentation Slides

Journal Publications

Simulation Bounds for Equivalence Verification of Polynomial Datapaths using Finite Ring Algebra . Namrata Shekhar, Priyank Kalla, M. Brandon Meredith and Florian Enescu. Accepted for publication, to appear in IEEE Trans. on VLSI, special section on Design Validation and Verification.

Optimization of Polynomial Datapaths using Finite Ring Algebra. Sivaram Gopalakrishnan and Priyank Kalla. ACM Trans. on Design Automation of Electronic Systems (ACM-TODAES), vol 12, issue 4, article 49, September 2007.

Equivalence Verification of Polynomial Datapaths using Ideal Membership Testing. Namrata Shekhar, Priyank Kalla and Florian Enescu. IEEE Trans. on CAD, pp. 1320-1330, vol. 26, number 7, July 2007.

Taylor Expansion Diagrams: A Canonical Representation for Verification of Dataflow Designs . Maciej Ciesielski, Priyank Kalla and Serkan Askar. IEEE Transaction on Computers, Vol. 55, Issue 9, pp. 1188-1201, Sept. 2006.

BDD-Based Logic Synthesis for LUT-Based FPGAs. Navin Vemuri, Priyank Kalla, Russell Tessier. ACM Transaction on Design Automation of Electronic Systems, Special Issue on Reconfigurable Systems. Oct 2002.

A Comprehensive Approach to the Partial Scan Problem using Implicit State Enumeration. Priyank Kalla and Maciej Ciesielski. IEEE Transaction on CAD, July 2002.

Strategies for Solving the Boolean Satisfiability Problem using Binary Decision Diagrams. Journal of Systems Architecture, Euromicro Journal, vol. 47/6, pp. 491-503, September 2001.

Logic Testing. Invited Article, Wiley Encyclopedia of Electrical and Electronics Engineering, John Wiley and Sons, Inc., Ed. John G. Webster, vol. 11, pp. 591-597, 1999.
Conference Publications

Verification of Arithmetic Datapaths using Polynomial Function Models and Congruence Solving. Neal Tew, Priyank Kalla, Namrata Shekhar and Sivaram Gopalakrishnan. Accepted, to appear at Intl. Conf. on Computer-Aided Design (ICCAD) 2008.

Integrating Common Sub-expression Elimination with Algebraic Methods for Polynomial System Synthesis. Sivaram Gopalakrishnan and Priyank Kalla. Intl. Workshop on Logic and Synthesis (IWLS), pp. 31-37, 2008.

Finding Linear Building-Blocks for RTL Synthesis of Polynomial Datapaths with Fixed-Size Bit-Vectors. Sivaram Gopalakrishnan, Priyank Kalla, M. Brandon Meredith and Florian Enescu. In Proc. IEEE/ACM Intl. Conf. on Computer-Aided Design (ICCAD), pp. 413-418, 2007.

A Groebner Basis Approach to CNF formulae Preprocessing. Chris Condrat and Priyank Kalla. Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), O. Grumberg and M. Huth (Eds.) Lecture Notes in Computer Science (LNCS) vol. 4424, pp. 618-631, March 2007. [© Springer-Verlag].

Optimization of Arithmetic Datapaths with Finite Word-Length Operands. Sivaram Gopalakrishnan, Priyank Kalla and Florian Enescu. In Proc. Asia/South-Pacific Design Automation Conference (ASP-DAC) pp. 511-516, 2007.

Guiding CNF-SAT Search by Analyzing Constraint-Variable Dependencies and Clause Lengths. Vijay Durairaj and Priyank Kalla. In Proc. High-Level Design Validation and Test Workshop, HLDVT, pp. 155-161, 2006.

Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with Finite Word-Length Operands. Namrata Shekhar, Priyank Kalla, Brandon Meredith and Florian Enescu. In Proc. Formal Methods in Computer-Aided Design, FMCAD, pp. 179-186, 2006.

Optimizing Fixed-Size Bit-Vector Arithmetic using Finite Ring Algebra. Sivaram Gopalakrishnan, Priyank Kalla and Florian Enescu. In Proc. Intl. Workshop on Logic and Synthesis, IWLS, pp. 110-117, 2006.

Equivalence Verification of Arithmetic Datapaths with Multiple Word-Length Operands. Namrata Shekhar, Priyank Kalla and Florian Enescu. Proceedings of the Design Automation and Test in Europe (DATE) Conf., March 2006.

Equivalence Verification of Polynomial Datapaths with Fixed-Size Bit-Vectors using Finite Ring Algebra. Namrata Shekhar, Priyank Kalla, Florian Enescu and Sivaram Gopalakrishnan. In Proceedings of the Intl. Conf. on Computer-Aided Design ICCAD, Nov. 2005. The powerpoint presentation delivered at ICCAD .

Exploiting Vanishing Polynomials for Equivalence Verification of Fixed-Size Arithmetic Datapaths. Namrata Shekhar, Priyank Kalla, Florian Enescu and Sivaram Gopalakrishnan. In Proceeding of the Intl. Conf. on Computer Design ICCD, Oct. 2005. The powerpoint presentation delivered at ICCD .

Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies. Vijay Durairaj and Priyank Kalla. Int'l. Conf. on Theory and Applications of Satisfiability Testing, F. Bacchus and T. Walsh (Eds); LNCS 3569, pp. 415-422, SAT 2005. Submitted version [© Springer-Verlag].

Dynamic Analysis of Constraint-Variable Dependencies to Guide SAT Diagnosis . Vijay Durairaj and Priyank Kalla. International Workshop on High-Level Design Validation and Test, HLDVT, Nov. 2004.

Exploiting Hypergraph Partitioning for Efficient Boolean Satisfiability . Vijay Durairaj and Priyank Kalla. International Workshop on High-Level Design Validation and Test, HLDVT, Nov. 2004.

Guiding CNF-SAT search via Efficient Constraint Partitioning . Vijay Durairaj and Priyank Kalla. International Conference on Computer-Aided Design, ICCAD, Nov. 2004.

Integrating CNF and BDD Based SAT Solvers . Sivaram Gopalakrishnan, Vijay Durairaj and Priyank Kalla. In High-Level Design Validation and Test Workshop, HLDVT 2003.

High-Level Design Verification using Taylor Expansion Diagrams: First Results. Priyank Kalla, Maciej Ciesielski, Emmanuel Boutillon, Eric Martin. High-Level Design Validation and Test Workshop, 2002.

Taylor Expansion Diagrams: A Compact Canonical Representation with Applications to Symbolic Verification. Maciej Ciesielski, Priyank Kalla, Zhihong Zeng and Bruno Rouzyere. Design Automation and Test in Europe, 2002.

Taylor Expansion Diagrams: A Compact Canonical Representation for RTL Verification. Maciej Ciesielski, Priyank Kalla, Zhihong Zeng and Bruno Rouzyere. High-level Design Validation and Test Workshop, 2001.

LPSAT: A Unified Approach to RTL Satisfiability. Zhihong Zeng, Priyank Kalla, and Maciej Ciesielski. Design Automation and Test in Europe, 2001.

A BDD-Based Satisfiability Infrastructure using the Unate Recursive Paradigm Priyank Kalla, Zhihong Zeng, Maciej Ciesielski and Chilai Huang. Design Automation and Test in Europe, 2000.

Performance Driven Resynthesis by Exploiting Retiming-Induced State Register Equivalence Priyank Kalla, and Maciej Ciesielski. Design Automation and Test in Europe, 1999.

A Comprehensive Approach to the Partial Scan Problem using Implicit State Enumeration. Priyank Kalla, and Maciej Ciesielski. International Test Conference, 1998.

Testability of Sequential Circuits with Multi-cycle False Paths. Priyank Kalla, and Maciej Ciesielski. VLSI Test Symposium, 1997.

Teaching:

Spring 2008: ECE/CS 5740/6740: CAD of Digital Circuits. Class notes, Lecture Slides, HW and Lab assignments and all other information can be found on the above link.
Fall 2007: ECE/CS 3710: Computer Design Lab.
Spring 2007: ECE/CS 3700: Fundamentals of Digital System Design.
Fall 2006: ECE/CS 5745/6745 Testing and Verification of Digital Circuits. .

If you would like to boost/deflate my ego, please (do not?) hesistate to send me Email at: KALLA@ece.utah.edu

Accesses to this page since March 1, 2007: