Priyank Kalla portrait
  • Professor, Elect & Computer Engineering
801-587-7617

Publications

  • Pratishtha Agnihotri (2022). Transfer-Matrix Abstractions to Analyze the Effect of Manufacturing Variations in Silicon Photonic Circuits. IEEE. Published, 07/2022.
  • V. K. Rao, H. Ondricek, P. Kalla & F. Enescu (2021). Rectification of Integer Arithmetic Circuits using Computer Algebra Techniques. Intl. Conf. on Computer Design (ICCD). 1-8. Published, 10/2021.
  • V. K. Rao, H. Ondricek, P. Kalla & F. Enescu (2021). Algebraic Techniques for Rectification of Finite Field Circuits. Intl. Conf. on VLSI (VLSI-SoC). 1-6. Published, 10/2021.
  • V. K. Rao, H. Ondricek, P. Kalla & F. Enescu (2021). On the Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques. Intl. Workshop Logic and Synthesis (IWLS). 1-8. Published, 06/2021.
  • Vikas Rao, I. Ilioaea, H. Ondricek, P. Kalla & F. Enescu (2021). Word-Level Multi-Fix Rectifiability of Finite Field Arithmetic Circuits. IEEE/ACM Intl. Symp. on Quality Electronic Design. 1-6. Published, 04/2021.
  • Utkarsh Gupta, Priyank Kalla, Irina Ilioaea & Florian Enescu (2019). Exploring Algebraic Interpolants for Rectification of Finite Field Arithmetic Circuits using Groebner Bases. IEEE. 6. Published, 05/2019.
  • Utkarsh Gupta, Priyank Kalla & Vikas Rao (2019). Boolean Groebner Basis Reductions on Finite Field Datapath Circuits using the Unate Cube Set Algebra. IEEE Trans. on CAD. Vol. 38(3), 576-588. Published, 03/2019.
  • V. Rao & U. Gupta, I. Ilioaea, A. Srinath, P. Kalla, F. Enescu (2018). Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques. Intl. Conf. on Formal Method in Computer-Aided Design (FMCAD). 1-8. Published, 11/2018.
    https://ieeexplore.ieee.org/document/8603018
  • Utkarsh Gupta & I. Ilioaea, V. Rao, A. Srinath, P. Kalla, F. Enescu (2018). On the Rectifiability of Arithmetic Circuits using Craig Interpolants in Finite Fields. IEEE/IFIP/AICA Intl. Conf. on VLSI (VLSI-SoC). 1-6. Published, 10/2018.
    http://www.ece.utah.edu/~kalla/papers/vlsisoc18.pd...
  • Utkarsh Gupta & I Ilioaea, P. Kalla, F. Enescu, V. Rao, A. Srinath (2018). Craig Interpolants in Finite Fields using Algebraic Geometry: Theory and Application. Intl. Workshop Logic Synthesis. 8. Published, 06/2018.
    http://www.ece.utah.edu/~kalla/papers/CI_with_Appl...
  • Utkarsh Gupta & Priyank Kalla, Vikas Rao (2018). Boolean Groebner Basis Reductions on Finite Field Datapath Circuits using the Unate Cube Set Algebra. IEEE Trans. on CAD. Published, 03/23/2018.
    https://ieeexplore.ieee.org/document/8323221
  • R. Wille, Krishnendu Chakraborty, Rolf Drechsler & Priyank Kalla (2017). Emerging Circuit Technologies: An Overview on the Next Generation of Circuits. (pp. 43-67). Springer Intl. Pub. AG. Published, 11/2017.
    https://link.springer.com/chapter/10.1007/978-3-31...
  • Utkarsh Gupta, Priyank Kalla & Vikas Rao (2017). Boolean Groebner Basis Reductions on Datapath Circuits using the Unate Cube Set Algebra. IEEE/CEDA. 124-131. Published, 06/2017.
  • Xiaojun Sun, Priyank Kalla and Florian Enescu, “Word-Level Traversal of Finite State Machines using Al- gebraic Geometry”, in Proc. Intl. High-Level Design Validation and Test Workshop, HLDVT 2016, pp. 142-149. Published, 10/2016.
  • Xiaojun Sun, Irina Ilioaea, Priyank Kalla and Florian Enescu. “Finding Unsatisfiable Cores of a Set of Polynomials using The Gro ̈bner Basis Algorithm”, in Proc. Intl. Conf. Principles and Practise of Constraint Programming, pp. 859-875, CP 2016. Published, 09/2016.
  • Tim Pruss, Priyank Kalla and Florian Enescu, “Efficient Symbolic Computation for Word-Level Abstraction from Combinational Circuits for Verification over Finite Fields”, in IEEE Trans. CAD, vol. 35, no. 7, pp. 1206-1218, July 2016. Published, 07/2016.
  • L. Schlitt, P. Kalla, S. Blair, "A Methodology for Thermal Characterization Abstraction for Integrated Opto-Electronic Layouts", in Proc. Intl. conf. VLSI Design, 2016. Published, 01/2016.
  • M. Potkonjak, D. Chen, P. Kalla, S. Levitan. "DA Vision: From here to Eternity", invited paper in special session, Intl. Conf. CAD, ICCAD 2015. Published, 11/2015.
  • P. Kalla, "Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation", invited tutorial paper, in Proc. Formal Methods in CAD, FMCAD 2015. Published, 09/2015.
  • "Design Automation for On-Chip Nanophotonic Integration", book chapter in the book "More than Moore Technologies for Next Generation Computer Design", Springer, Editor: Rasit Topaloglu. April 2015. Published, 04/2015.
  • Thermal Aware Synthesis of Integrated Photonic Ring Resonators, Intl Conf on CAD (ICCAD) pp 557-564, 2014. Published, 11/2014.
  • Equivalence Verification of Large Galois Field Arithmetic Circuits using Word-Level Abstraction via Groebner Bases, in Proc. Design Automation Conference, pp 1-6, DAC 2014. Published, 06/2014.
  • Crossing-aware Channel Routing for Integrated Optics. C. Condrat, P. Kalla, and S. Blair. IEEE Trans. on CAD, special issue on Optical Interconnects, June 2014, pp. 814-825, vol 33, issue 9. Published, 06/2014.
  • Leveraging Groebner bases and SAT for Hardware/Software Verification. Invited Tutorial presented at the Banff International Research Station Workshop on Theoretical Foundations of Applied SAT Solving, Jan 2014. Published, 01/2014.
    https://www.birs.ca/workshops/2014/14w5101/files/k...
  • J. Lv, P. Kalla and F. Enescu, "Efficient Groebner Basis Reductions for Formal Verification of Galois Field Arithmetic Circuits," IEEE Trans. CAD, Sept 2013, 1409 - 1420. Published, 09/2013.
  • "Crossing-aware Channel Routing for Photonic Waveguides". C. Condrat, P. Kalla, S. Blair. In Conf. Proc. IEEE Midwest Symposium on Circuits and Systems (MWSCAS), pp. 649 - 652, 2013. Recipient of Best paper with student as first author award.. Published, 08/2013.
  • Tim Pruss, Priyank Kalla and Florian Enescu, "Word-Level Abstraction from Bit-Level Circuits using Groebner Bases", in Proc. Intl. Workshop on Logic and Synthesis, June 2013. Published, 06/2013.
  • Channel Routing for Integrated Optics. C. Condrat, P. Kalla and S. Blair. In Proc. ACM/IEEE System-Level Interconnect Prediction (SLIP) 2013. Published, 06/2013.
  • C. Condrat, P. Kalla and S. Blair. A Methodology for Physical Design Automation for Integrated Optics, in Proc. IEEE Mid-West Symposium on Circuits and Systems (MWSCAS), 2012, pp. 598-601. (Invited Paper). Published, 08/2012.
  • C. Condrat, P. Kalla, F. Enescu. Efficient Groebner Basis Reductions for Formal Verification of Galois Field Multipliers. IEEE/ACM Design Automation and Test in Europe (DATE) Conf. 2012. Published, 03/2012.
  • J. Lv, P. Kalla, Formal Verification of Galois Field Multipliers using Computer Algebra Techniques. IEEE Intl. Conf. on VLSI Design, India, 2012. Published, 01/2012.
  • Formal Verification of Galois Field Multipliers using Computer Algebra Techniques. Published, 01/2012.
  • Verification of Composite Galois Field Multipliers over GF( (2^m)^n ) using Computer Algebra Techniques. Published, 11/2011.
  • C. Condrat, P. Kalla, S. Blair, "Logic Synthesis for Integrated Optics", ACM Great Lakes Symposium on VLSI, 2011. Published, 05/2011.
  • S. Gopalakrishnan and P. Kalla, "Algebraic Techniques to Enhance Common Sub-Expression Extraction for Polynomial System Synthesis". Invited Chapter in Book, "Advanced Techniques in Logic Synthesis, Optimizations and Applications". Editors: K. Gulati and S. Khatri. Springer New York. [Was submitted in June 2010, revised in Sept 2010, was to be published Nov 2010, printing delayed to 2011]. Published, 11/2010.
    http://www.springer.com/engineering/circuits+%26+s...
  • C. Condrat, P. Kalla, S. Blair, "Exploring Design and Synthesis in Optical Digital Logic," in Intl. Workshop on Logic and Synthesis (IWLS), 2010, pp. 47-54. Published, 06/2010.
  • N. Shekhar, P. Kalla, M. B. Meredith, F. Enescu. Simulation Bounds for Equivalence Verification of Polynomial Datapaths with Finite Word-Length Operands, in IEEE Trans. on VLSI, Special Section on Verification and Validation, vol 16, issue 4, pp 376-387. Published, 04/01/2008.
  • S. Gopalakrishnan and P. Kalla. "Optimization of Polynomial Datapaths using Finite Ring Algebra". in ACM Transactions on Design Automation of Electronic Systems, vol 12, issue 4, article 49, September 2007. Published, 09/2007.
  • N. Shekhar, P. Kalla and F. Enescu. "Equivalence Verification of Polynomial Datapaths using Ideal Membership Testing." IEEE Trans. CAD, pp. 1320-1330, vol. 26, number 7, July 2007. Published, 07/2007.
  • M. Ciesielski, P. Kalla, S. Askar. "Taylor Expansion Diagrams: A Canonical Representation for Verification of Dataflow Designs". IEEE Trans. on Computers, Vol. 55, Issue 9, pp. 1188-1201, Sept. 2006. Published, 09/2006.
  • S. Gopalakrishnan, P. Kalla, F. Enescu. "Optimizing Fixed-Size Bit-Vector Arithmetic using Finite Ring Algebra". In Intl. Workshop on Logic and Synthesis, IWLS, June 2006. Published, 06/2006.

Research Statement

Formal Verification of Hardware Implementations of Cryptography Primitives over Galois Fields using Computer Algebra and Algebraic Geometry

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

Design Automation for Integrated Optics:

Logic Design and Synthesis in Si-Photonics
Physical Design Automation for Si-Photonics Integration
Thermal issues in Si-Photonics Design Automation

Formal Verification of RTL descriptions:  

Equivalence Checks, RTL-Satisfiability, Assertion Checking.

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.

Presentations

  • Design and Automation for Silicon Photonics Integration. Invited Talk/Keynote, Presented, 05/20/2021.
    https://tss.date.upb.de/tss2021/pages/program.php
  • Design Automation for Large Scale Silicon Nanophotonic Integration. Presented at the R&D Center of Advantest Systems, Japan. Invited Talk/Keynote, Presented, 08/2018.
  • Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation. Presented at the Kyoto University Informatics Colloquium. Invited Talk/Keynote, Presented, 07/13/2018.
  • "What can Algebraic Geometry Tell us about the Function Implemented by a Circuit?" Presented at the 3rd Workshop on Design Automation for Understanding Hardware Designs (DUHDe). Invited Talk/Keynote, Presented, 03/2017.
  • Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation, invited tutorial, Formal Methods in CAD, 2015. Invited Talk/Keynote, Presented, 09/2015.
  • Algebraic Techniques to enhance Common Sub-Expression Extraction for Polynomial System Synthesis, in Proc. Design, Automation and Test in europe Conf., April 2009. Conference Paper, Other, 04/2009.
  • N. Tew, P. Kalla, N. shekhar, S. Gopalakrishnan. Verification of Arithmetic Datapaths using Polynomial Function Models and congruence Solving. In Proc. Intl. Conf. on CAD (ICCAD), Nov 2008. Conference Paper, Other, 11/07/2008.
  • RTL Verification of Arithmetic Datapaths using Finite Integer Algebras. Invited keynote talk at the Fifth Intl. Workshop on Constraints in Formal Verification, pp. 16-21, aug 2008. Invited Talk/Keynote, Presented, 08/13/2008.
  • S. Gopalakrishnan and P. Kalla. Integrating Common Sub-expression Elimination with Algebraic Methods for Polynomial System Synthesis. In Proc. Intl. Workshop on Logic and Synthesis (IWLS), pp. 31-38, June 2008. Conference Paper, Other, 06/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. Acceptance rate ~26%. Conference Paper, Other, 11/2007.
  • "Verification of Arithmetic Datapaths using Finite Integer Algebras". Invited Seminar at Calypto Design Systems, Santa Clara, CA. Invited Talk/Keynote, Presented, 11/2007.
  • C. Condrat and P. Kalla. "A Groebner Basis Approach to CNF formulae Preprocessing". Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science (LNCS) vol. 4424, pp. 618-631, March 2007 Acceptance Rate: 26%. Conference Paper, Other, 03/2007.
  • 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. Acceptance rate: 31%. Conference Paper, Other, 01/2007.
  • N. Shekhar, P. Kalla, B. Meredith and F. Enescu. "Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with Finite Word-Length Operands". In Proc. Formal Methods in Computer-Aided Design, FMCAD, pp 185-191, 2006. Acceptance Rate: ~21%. Conference Paper, Other, 11/2006.
  • V. Durairaj and P. Kalla. "Guiding CNF-SAT Search by Analyzing Constraint-Variable Dependencies and Clause Lengths". In Proc. High-Level Design Validation and Test Workshop, HLDVT 2006. Acceptance rate: ~50%. Conference Paper, Other, 11/2006.
  • "Synthesis & Verification of Arithmetic Datapaths using Finite Ring Algebra". Invited Seminar, Dept. of Mathematics and Statistics, Georgia State University, Atlanta, GA. Invited Talk/Keynote, Presented, 04/2006.
  • N. Shekhar, P. Kalla, F. Enescu. "Equivalence Verification of Arithmetic Datapaths with Multiple Word-Length Operands". In Proceedings of the Design Automation and Test in Europe (DATE) Conf., March 2006. Acceptance rate: ~25%. Conference Paper, Other, 03/2006.
  • "Synthesis & Verification of Arithmetic Datapaths using Finite Ring Algebra". Invited Seminar, ECE Dept. Univ. of Massachusetts at Amherst. Invited Talk/Keynote, Presented, 03/2006.

Research Groups

  • Pratishtha Agnihotri, Graduate Student. ECE. 01/01/2021 - present.
  • Xiaojun Sun, Graduate Student. ECE/PhD. 01/2013 - present.

Software Titles

  • Word-Level Abstraction Tool for Digital Circuits. A CAD tool for canonical word level abstraction from gate-level circuit designs. Used for abstraction and verification of circuits over finite fields. Release Date: 05/2015. Inventors: Tim Pruss and Priyank Kalla.
  • Computer-Algebra based Design Verification Tool for Arithmetic Circuits. Freely available CAD tools for the hardware verification community for formal verification of Arithmetic Circuits. Tools, Design Benchmarks, and various design-interpretation scripts available at: http://www.ece.utah.edu/~lv/uugb.html Original distribution 03/2012, updates 01/2013. Next update: 06/2014. Release Date: 01/2013. Inventors: Jinpeng Lv and Priyank Kalla.