Formal Verification

Under the term formal verification we comprise the techniques used to reason formally about the behavior of digital systems. In a general way, the verification problem may be stated as follows: Given a specification of the behavior of a system and an implementation, verify formally that the implementation satisfies the specification. This definition is very general in the sense that there may be different types of specification, different types of implementations, and also, the concept of "satisfaction" may be interpreted in different ways. 
The main focus of our group is in the area of Model Checking and Language Containment. The former assumes a temporal logic formulation of the specification and it tries to prove that the implementation is a model of the specification. The latter models both the specification and implementation as automata defining languages, and it tries to prove that the language accepted by the implementation is contained on the language accepted by the specification. 
As an example of where formal verification can be applied is the (in)famous error in the Intel Pentium Chip. The processor computed an incorrect division whenever certain combination of operands were present. Formal verification specifically tries to avoid this kind of error by guaranteeing that the final product is "correct". 

VLSI Design and EDA

With the relentless advance of VLSI processing technology to Deep Sub-micron (DSM) dimensions, many new problems are being encountered which force us to rethink the manner in which VLSI design is performed. 
Our research in VLSI design focuses on novel VLSI design/layout techniques for digital/analog design designs. We address several of the problems that plague DSM VLSI design. Our focus on Electronic Design Automation (EDA) focuses on logical and physical design automation for DSM VLSI systems. 
The current focus of our group includes areas like Extreme low-power VLSI design, Datapath Design Automation, Cross-talk in DSM VLSI design, High-speed I/O Interfaces, Silicon-on- Insulator CMOS Design, Mixed-signal Testing using Multi-valued Satisfiability techniques, Layout Fabrics for Deep Sub-micron IC Design, VLSI Routing, Timing Analysis in the presence of Cross-talk, SPFDs and their application to Logic Synthesis, Multi-valued Logic and Hierarchical Synthesis. 

Binary Decision Diagrams (BDDs)

Decision Diagrams are used to represent switching functions as well as functions ranging from {0,1}^n to an arbitrary set:. Our research in decision diagrams includes (but not limited to) Binary Decision Diagrams (BDDs), Algebraic Decision Diagrams (ADDs), and Zero-suppressed Binary Decision Diagrams (ZDDs). CU Decision Diagram (CUDD), a decision diagram package developed by our group,  is being used widely in industry and academia.