Education:
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
Former Students
- Dissertation Title: Rectification of Arithmetic Circuits using Computer Algebra Techniques.
- Dissertation title: Rectification of Finite Field Arithmetic Circuits with Craig Interpolation using Algebraic Geometry
- Formal Verification of Sequential Arithmetic Circuits.
- Dissertation Title: Word-Level Abstraction from Combinational
Circuits using Algebraic Geometry.
- Thesis Title: Thermal Characterization Abstraction for Integrated Optoelectronics.
- Dissertation Title: Design Automation for Integrated Optics.
- Dissertation Title: Scalable Formal Verification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
- Dissertation Title:
High-Level Synthesis of Polynomial Datapaths using Finite Integer
Algebras.
- Dissertation Title: Equivalence Verification of
Arithmetic Datapaths using Finite Ring Algebra.
-
Dissertation topic: Improving SAT Solving by Analyzing
Constraint-Variable Dependencies.
Publications and Presentations
Teaching:
- Fall 2021: ECE/CS 5745/6745: Testing and Verification of Digital
Circuits
- Subtitle: Hardware Verification using Symbolic Computation
- Class Webpage
- Spring 2020: ECE/CS 3700: Fundamentals of Digital System Design
- Spring 2019: ECE/CS 5740/6740: CAD of Digital Circuits --- Logic Synthesis and Optimization
- Fall 2018: ECE/CS 3710: Computer Design Lab
- 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 Sept 2021:
free website counters