## Associate Professor

Electrical and Computer Engineering Merrill Engineering Bldg., #4512 University of Utah, Salt Lake City, UT-84112 Ph: (801)-587-7617 Email: KALLA@ece.utah.edu

## 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 Hardware Implementations of Cryptography Primitives

- Verification over Galois Fields using Computer Algebra and Algebraic Geometry
- Canonical Word-Level Polynomial Abstractions of Bit-Vector Arithmetic using Groebner Bases
- 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 Optic/Photonic Logic

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

## Funding for our Research

## Graduate Students

Xiaojun Sun - PhD student. Formal Verification of Sequential Arithmetic Circuits.

Utkarsh Gupta - PhD student. Boolean Groebner bases in Synthesis and Verification.

Lawrence Schlitt - BS/MS Student. Interests: Effects of Thermal Stress on Si-Photonic Integration.

- Lawrence's BS project received the Bronze Medal at the ACM Student Research Competition, at the 2012 Design Automation Conference . Congratulations, Larry!
## Former Students

Tim Pruss - PhD Completed Summer 2015. Currently working at Apple as Formal Verification Engineer in Cupertino, CA. Dissertation Title: Word-Level Abstraction from Combinational Circuits using Algebraic Geometry.

Chris Condrat: PhD completed Dec 2013, BS/MS 2007. Currently working at Calypto Design Systems, Catapult-C High-Level Synthesis Group, Portland, OR.

- Dissertation Title: Design Automation for Integrated Optics.

Jinpeng Lv: PhD completed July 2012. Currently working at Cadence, Conformal Verification Group.

- Dissertation Title: Scalable Formal Verification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
Sivaram Gopalakrishnan - MS 2004, PhD Summer 2008. Senior R & D Engineer, Synopsys, Formality Group, Hillsboro, OR. Dissertation Title: High-Level Synthesis of Polynomial Datapaths using Finite Integer Algebras.

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.

## Publications and Presentations

## Teaching:

- Spring 2016: ECE/CS 5740/6740: CAD of Digital Circuits --- Logic Synthesis and Optimization

- Fall 2015: ECE/CS 3710: Computer Design Lab

- Spring 2015: ECE/CS 3700: Fundamentals of Digital System Design

- Fall 2014: ECE/CS 5745/6745: Testing and Verification of Digital Circuits

- Subtitle: Hardware Verification using Symbolic Computation
- Class Webpage

- Spring 2014: ECE/CS 5740/6740: CAD of Digital Circuits

- Fundamental CAD Techniques for Physical Design Automation
- Class Webpage

- Fall 2012: ECE/CS 5745/6745: Testing and Verification of Digital Circuits

- This version covered topics in SAT, BDDs, ATPG, DFT, and Equivalence Checking.

- Fall 2010: Computer Algebra for Electrical Engineers and Computer Scientists

- ECE 5960-001, ECE 6962, CS 5960, CS 6962

## My Recent Conference and Service Activities

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: