My research deals with developing design methodologies for future generations of computing systems. This involves understanding the challenges in system design that arise from the capabilities and constraints of future computing technologies (silicon transistor-based and beyond) as well as the requirements of emerging application areas. My current work focuses on developing systems that are resilient in the face of a diverse set of failures. These include functional failures arising from design bugs, as well as operational failures arising from soft errors, severe process variations, and device aging. This work spans the traditional areas of design verification and resilient system design. In the PriM Project, my group is developing a micro-architectural-level design methodology that raises the level of design entry above the traditional register-transfer-level design. This offers several advantages in design verification. In the Runtime Verification Project, my group is developing a range of solutions for online checking and recovery for hardware, software, and mixed hardware-software systems. In this area, our focus is on correctness in the face of complex concurrency errors. In the Post-Silicon Validation Project, my group is developing practical scalable techniques for post-silicon validation that are based on formal methods. In the Approximate Computing Project, my group is exploring design methodologies that exploit application-level flexibility to reduce the cost of resiliency and/or enhance key design metrics such as power and performance. In the past my group has worked on fundamental problems in hardware verification. Our results in propositional logic satisfiability (Chaff Project) and functional timing verification have been widely used in academic and industrial research as well as in industrial practice. I am also the Director of the Gigascale Systems Research Center (GSRC), one of six centers that comprise the Focus Center Research Program (FCRP), a joint industry-government initiative. GSRC is addressing the chip-scale system design challenges with an eight- to 12-year horizon. Princeton serves as the lead university of this 17-university center that brings together 34 faculty and over 50 graduate students across the US.
“Efficient Predictive Analysis for Detecting Nondeterminism in Multi-Threaded Programs,” (with A. Sinha and A. Gupta), Formal Methods in Computer-Aided Design, FMCAD, 2012
“Specification and Synthesis of Hardware Checkpointing and Rollback Mechanisms,” (with C. Chan, D. Schwartz-Narbonne and D. Sethi), 49th IEEE/ACM Design Automation Conference (DAC), 2012
"Runtime Verification: A Computer Architecture Perspective,” Invited Paper, International Conference on Runtime Verification (RV), 2011
“Post-Silicon Fault Localisation Using Maximum Satisfiability and Backbones,” (with S. Zhu, G. Weissenbacher), Formal Methods in Computer-Aided Design (FMCAD), 2011
“Parallel Assertions for Debugging Parallel Programs,” (with D. Schwartz-Narbonne, F. Liu, T. Pondicherry and D. August), ACM/IEEE Ninth International Conference on Formal Methods and Models for Codesign, 2011
“Supporting RTL Flow Compatibility in a Microarchitecture-Level Design Framework,” (with C. Chan, D. Schwartz-Narbonne, and Y. Mahajan), IEEE/ACM International Conference on Hardware/Software Codesign and System Synthesis, 2009
“Boolean Satisfiability: From Theoretical Hardness to Practical Success,” (with L. Zhang), Invited Paper, Communications of the ACM, Volume 52, Number 8, August 2009.
“Declarative Infrastructure Configuration Synthesis and Debugging,” (with S. Narain, G.Levin, V. Kaul), Invited Paper, Journal of Network and Systems Management, Special issue on security configuration management, Springer, DOI 10.1007/s10922-008-9108-y, 2008
“Runtime Validation of Transactional Memory,” (with K. Chen and P. Patra), 9th International Symposium on Quality Electronic Design, 2008
“On Solving the Partial MAX-SAT Problem,” (with Z. Fu), 9th International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science (LNCS), Volume 4121/2006
“Compile-Time Dynamic Voltage Scaling: Opportunities and Limits,” (with F. Xie and M. Martonosi), PLDI 2003
“Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications,” (with L. Zhang), DATE 2003
“Limits of using signatures for permutation independent Boolean comparison”, (with J. Mohnke and P. Molitor), Formal Methods in System Design, Kluwer Academic Publishers, 2002
“The Quest for Efficient Boolean Satisfiability Solvers”, (with Lintao Zhang), Invited Paper and Presentation, In, Proceedings of CADE 2002 and also in Proceedings of CAV 2002
“Efficient Constraint Driven Learning in a Boolean Satisfiability Solver,” (with L. Zhang, C. Madigan, M. Moskewicz), ICCAD 2001