Sharad Malik

http://www.princeton.edu/~sharad

 

Contact Information

Department of Electrical Engineering  

Princeton University  

Princeton, NJ 08544                                                                   

(609) 258-4625

(609) 258-3745 FAX 

sharad@princeton.edu

Research Interests

Design methodology for computing systems; system verification; reliable systems.

 

Education

  • Ph.D. in Computer Science, Univ. of California, Berkeley, December 1990
  • M. S. in Computer Science, Univ. of California, Berkeley, May 1987
  • Bachelor of Technology in Electrical Engineering, Indian Institute of Technology, New Delhi, May 1985

 

Professional Experience

Princeton University Department of Electrical Engineering 

  • George Van Ness Lothrop Professor of Engineering: September 2005 – present
    • July 2012-present: Chair, Department of Electrical Engineering
    • December 2012-July 2016: Associate Director, Center for Future Architectures Research (C-FAR) (www.futurearchs.org)
    • November 2009-November 2012: Director, Gigascale Systems Research Center (GSRC)
    • September 2006-August 2011: Director, Keller Center for Innovation in Engineering Education (kellercenter.princeton.edu)
  • Professor - July 1999 to August 2005
  • Associate Professor - July 1996 to June 1999 
  • Assistant Professor - February 1991 to June 1996 

University of California, Berkeley, Computer Science Department 

  • Post-Graduate Researcher - May 1986 to December 1990
  • Teaching Assistant - August 1985 to May 1986

AT&T Bell Labs, Murray Hill, NJ  

Summer Research Intern - May 1989 to August 1989

Awards and Honors

  • Intel Corporate Research Council Outstanding Researcher Award (Security and Software Sector), 2018
  • University of California Berkeley, Department of Electrical Engineering and Computer Science, Distinguished Alumni Award in Electrical Engineering, 2019
  • IEEE CEDA A. Richard Newton Technical Impact Award in Electronic Design Automation, 2017
  • “Evaluating the Security of Logic Encryption Algorithms,” (co-authored with P. Subramanyan and S. Ray), Best Student Paper Award, IEEE International Symposium on Hardware Oriented Security and Trust (HOST), 2015
  • “On computing minimal independent support and its applications to sampling and counting,” (co-authored with A. Irvii, K. Meel and M. Vardi), Best Student Paper Award, 21st International Conference on Principles and Practice of Constraint Programming (CP), 2015
  • “Hardware Trojan detection for gate-level ICs using signal correlation based clustering,” (co-authored with B. Cakir), Best Paper Award in Application Design, Design Automation and Test in Europe (DATE), 2015
  • ACM Fellow 2015
  • The IEEE/ACM Design Automation Conference 50th Anniversary Most Cited Paper Award: (with M. W. Moskewicz, C. F. Madigan, Y. Zhao and L. Zhang) For publishing the most cited paper in DAC's 50 year history, 2013
  • The IEEE/ACM Design Automation Conference 50th Anniversary Award: For the Author with the Second Most Citations from DAC Publications in DAC's 50-year history, 2013
  • The IEEE/ACM Design Automation Conference 50th Anniversary Prolific Author Award For publishing 20 or more papers at the Design Automation Conference, 2013
  • “Accelerating Boolean Satisfiability with Configurable Hardware,” (co-authored with P. Zhong, M. Martonosi and P. Ashar), selected for inclusion in “Significant Contributions from 20 Years of the International IEEE Symposium on Field-Programmable Custom Computing Machines (1993-2013),” 2013
  • “Efficient Conflict-Driven Learning in a Boolean Satisfiability Solver,” (co-authored with L. Zhang, M. Moskewicz and C. Madigan), IEEE/ACM International Conference on Computer-Aided Design, Ten Year Retrospective Most Influential Paper Award, 2011
  • Princeton University President’s Award for Distinguished Teaching, 2009
  • Distinguished Alumni Award, Indian Institute of Technology Delhi, 2009
  • Computer-Aided Verification (CAV) Award for fundamental contributions to the development of high-performance Boolean satisfiability solvers, 2009
  • IBM Faculty Award, 2007, 2006, 1991
  • Princeton University, School of Engineering and Applied Sciences, Distinguished Teacher Award, 2005.
  • “Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications,” (co-authored with L. Zhang), Best Paper Award, IEEE/ACM Design Automation and Test in Europe (DATE), 2003.
  • “Power Analysis of Embedded Software: A First Step Towards Software Power Minimization,” (co-authored with V. Tiwari and A. Wolfe), selected to be included in “The Best of ICCAD – 20 Years of Excellence in Computer-Aided Design,” 2003
  • IEEE Fellow, 2002
  • “Using register-transfer paths in code generation for heterogeneous memory-register architectures”, (with G. Araujo and M. T-C. Lee), Best Paper Award, IEEE/ACM Design Automation Conference June 1996.
  •  NSF Young Investigator Award, May 1994
  • Rheinstein Faculty Award, School of Engineering and Applied Sciences, Princeton University, May 1994
  • Engineering Council Excellence in Teaching Award, Princeton University, January 1996, May 1994, May 1993
  • Walter C. Johnson Prize for Teaching Excellence, Dept. of Electrical Engineering, Princeton University, May 1993
  • NSF Research Initiation Award, August 1992
  • Best Paper Award, IEEE International Conference on Computer Design, 1992
  • “Delay Computation in Combinational Logic Circuits: Theory and Algorithms,” (co-authored with K. Keutzer and S. Devadas), Distinguished Paper Citation, International Conference on Computer-Aided Design, 1991
  • University of California Regents Fellowship, 1985 and 1986
  • President of India's Gold Medal, IIT Delhi, 1985 for undergraduate academic excellence

Patents and Inventions

  • US Patent 6,961,916, November 1, 2005: “Placement method for integrated circuit design using topo-clustering”
  • US Patent 6,874,135, March 29, 2005: “Method for design validation using retiming”
  • US Patent 6,651,234, November 18, 2003: “Partition based decision heuristics for SAT and image computation using SAT and BDDs”
  • US Patent 6,449,756, September 10, 2002: “Method for accurate and efficient updates of timing information in logic synthesis, placement and routing for integrated circuit design”
  • US Patent 6,442,743, August 27, 2002: “Placement method for integrated circuit design using topo-clustering”
  • US Patent 6,367,051, April 2, 2002: “System and method for concurrent buffer insertion and placement of logic gates”
  • US Patent 6,286,128, September 4, 2001: “Method for design optimization using logical and physical information”
  • US Patent 6,247,164, June 12, 2001: “Configurable hardware system implementing Boolean Satisfiability and method thereof”
  • US Patent 6,192,508, Feb 20, 2001: “Method for Logic Optimization for Improving Timing and Congestion During Placement in Integrated Circuit Design”
  • US Patent 5,937,183, August 10, 1999: “Enhanced Binary Decision Diagram Based Functional Simulation”
  • US Patent 5,841,673, November 24, 1998: “System and method for processing graphic delay data of logic circuit to reduce topological redundancy”
  • US Patent 6,038,392, May 27, 1998: “Implementation of Boolean satisfiability with non-chronological backtracking in reconfigurable hardware”
  • US Patent 6,035,109, April 22, 1997: “Method for using complete-1-distinguishability for FSM equivalence checking”
  • US Patent 5,522,063, May 28, 1996: “Method of Finding Minimum Cost Feedback Vertex Sets for a Graph for Partial Scan Testing without Exhaustive Cycle Enumeration”
  • US Patent 5,457,638, October 10, 1995: “Timing Analysis of VLSI Circuits”
  • US Patent 5,448,497, September 5, 1995: “Exploiting multi-cycle false paths in the performance optimization of sequential circuits”

Program Committee Assignments

  • Workshop on Resiliency of Embedded Electronic Systems (REES): 2015
  • International Conference on Runtime Verification (RV): 2012
  • Haifa Verification Conference (HVC): 2006, 2007, 2008, 2009 Awards Committee Chair
  • International Conference on Computer-Aided Verification: 2005, 2008 (co-chair)
  • The International Conference on Theory and Applications of Satisfiability Testing (SAT): 2003, 2004, 2005, 2006, 2015
  • International Conference on Embedded and Hybrid Systems: 2004
  • Design Automation and Test in Europe (DATE): 2004
  • Workshop on Bounded Model Checking: 2003, 2004, 2005
  • Workshop on Parallel and Distributed Model Checking: 2003, 2004
  • The ACM SIGBED International Conference on Embedded Software (EMSOFT): 2003
  • IEEE/ACM Design Automation Conference: 1994, 1995, 1996, 1997, 1998, 1999. Program Co-Chair, DAC 2000 and DAC 2001. Panels Chair 2002. General Chair 2004.
  • Constraints in Formal Verification: 2002
  • IEEE International Conference on Computer-Aided Design: 1992, 1993, 1994, 1995 (Chair, sub-committee on timing analysis and optimization, 1994, 1995)
  • Asia-Pacific Design Automation Conference: 1997, 1998
  • IEEE/ACM International Symposium on Low Power Electronics and Design: 1997, 1999, 2000
  • ACM International Workshop on Logic Synthesis: 1991, 1993, 1997 (Technical Program Chair), 1998
  • ACM International Workshop on Timing Issues in the Specification, Design and Synthesis of Digital Systems: 1992 (Workshop chair), 1993, 1995, 1997
  • ACM SIGPLAN Workshop on Languages, Compilers and Tools for Embedded Systems: 2000.
  • Asynchronous Design Symposium: 2000
  • European Design and Test Conference: 1994, 1995
  • IEEE International Conference on Computer Design: 1992, 1994
  • International Workshop on Low Power Design: 1995
  • IEEE International Conference on VLSI Design: 1992

 

Editorial Boards

  • Foundations and Trends in Electronic Design Automation, NOW Publishers, Editor-in-Chief: 2005-2011
  • IEEE Transactions on VLSI Systems: 2007-2009
  • ACM Transactions on Design Automation of Electronic Systems: 2005-2008
  • Formal Methods in System Design, Springer-Verlag: 2005 - present
  • IEEE Design and Test: 2001 – 2008
    • Guest Editor: Special Issue on “Exploring Synergies for Design Verification,” November-December 2004
  • Journal on Satisfiability, Boolean Modeling and Computation (IOS Press): 2003-present
  • Design Automation of Embedded Systems, Kluwer Academic Publishers: 1995 - present
  • Journal of VLSI Signal Processing, Kluwer Academic Publishers: 1996 - 2005
    • Guest Editor: Journal of VLSI Signal Processing, Special Issue on Asynchronous Circuits, Kluwer Academic Publishers, October 1993.

 

Invited Presentations

Talks

  • “Instruction-Level Abstraction (ILA):A Uniform Specification for System-on-Chip (SoC) Verification,” Keynote Talk, Jasper Users Group Conference, October 11, 2018
  • “Specification and Modeling for Systems-on-Chip Security Verification,” Invited Talk, Design Automation Conference, June 6-8, 2016.
  • “Detecting Hardware Trojans: A Tale of Two Techniques,” Invited Talk, Formal Methods in Computer-Aided Design, September 29, 2015.
  • “Boolean Satisfiability: From Theoretical Hardness to Practical Success,” ECE Distinguished Lecture, Boston University, January 29, 2014
  • “Boolean Satisfiability: From Theoretical Hardness to Practical Success,” Weber Lecture, NYU Poly, October 31, 2013

§  “Verification of Computer Switching Networks: An Overview,” Invited Talk, Tenth International Symposium on Automated Technology for Verification and Analysis, ATVA 2012

  • “Runtime Verification: A Computer Architecture Perspective,” Invited Talk, International Conference on Runtime Verification, 2011, San Francisco.
  • “Boolean Satisfiability Solvers and Extensions,” Invited Talk, Advanced Study Institute of the NATO Science for Peace and Security Programme, Tools for Analysis and Verification of Software Safety and Security, August 2011, Marktoberdorf, Germany.
  • “Boolean Satisfiability: From Theoretical Hardness to Practical Success,” Invited Seminar, Summer Research Institute, School of Computer and Communication Sciences, École Polytechnique Fédérale de Lausanne (EPFL), June 20, 2011
  • “Design Debugging using Boolean Satisfiability,” Invited Talk, First International SAT/SMT Solver Summer School 2011, MIT, June 2011
  • “Managing State Explosion through Runtime Verification,” Hardware Verification Workshop (in association with Computer-Aided Verification), July 15, 2010, Edinburgh.
  • “Design Methodology and Verification in the Context of Third Party IP,” DARPA Trust Third Party IP Workshop, November 20, 2008
  • “SAT and QBF Solvers,” NSF Workshop on Symbolic Computation for Constraint Satisfaction Problems, November 14, 2008
  •  “Hardware Verification: Techniques, Methodology and Solutions,”
    • Keynote Talk, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), April 4, 2008, Budapest.
    • Invited Seminar, Cornell University, May 19, 2008.
  • “SAT Solvers: Efficient Implementations,” NSA DoD SAT Workshop, Baltimore, MD, March 3, 2008
  • “Verification Driven Formal Architecture and Microarchitecture Modeling,”
    • IBM Research, Yorktown Heights, December 12, 2008.
    • Intel Annual Symposium, Haifa, July 10, 2007.
  • “Optimization and Relaxation in SAT Search,” Workshop on Satisfiability Solvers and Program Verification, Seattle, August 11th 2006.
  • “A Case for the Runtime Validation of Hardware,” Keynote Speaker, IBM Verification Conference, Haifa, November 13th 2005.
  • “Experiences with QBF Solvers,” Workshop on Bounded Model Checking, Edinburgh, July 11th 2005.
  • “The Quest for Efficient SAT Solvers,” Carnegie-Mellon University, School of Computer Science, Distinguished Lecture Series, The Gaschnig/Oakley Memorial Lecture, April 22, 2004.
  • “Gigascale Silicon Design: Challenges and Opportunities,” Keynote Speaker, Intel Design and Test Conference, Portland, July 29th, 2003.
  • “Embedded Software Implementation Tools for Fully Programmable Application-Specific Systems,” Workshop on Embedded Software (EMSOFT), Grenoble, October 9th, 2002.
  • “The Quest for Efficient SAT Solvers,” Computer-Aided Verification/Conference on Automated Deduction (Joint Invited Talk), Copenhagen, July 29th, 2002
  • “Chaff: Engineering an Efficient SAT Solver.”
    • Intel Logic Verification Symposium, 24th July, 2001, Weizmann Institute of Science, Israel.
    • Compaq Corp., Shrewsbury MA, 7th June, 2001
  • “Enabling Fully Programmable Application Specific Solutions through MESCAL: Modern Embedded Systems, Compilers, Architectures and Languages.”
    • Motorola Circuits Systems and Architectures Futures Forum, October 16, 2000
    • Enabling Technologies for System-on-Chip Development, Tampere University of Technology, November 15, 2000
  • “Power Analysis for Embedded Software”, Plenary Talk, PATMOS, September 1997
  • “Worst-Case Static Timing Analysis - From Gates to Instructions”, ACM/IEEE Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, December 1997

Panels

  • “ESL HW/SW Verification: A Reality Check,” Panel Chair, ACM/IEEE Design Automation Conference, June 9, 2011
  • National Academy of Engineering, Frontiers of Engineering Education, 2009 (Invited Participant)
  • “Why Do We Still Have Bugs? Challenges from Design through System Software,” P=ac^2 Workshop, IBM Research, March 31, 2008
  • “Computer-Aided Verification in Many-Core Parallel Software,” Workshop on Exploiting Concurrency Correctly and Efficiently, 2008
  • “Building a Verification Test Plan – Trading Brute Force for Finesse,” Panel Chair, IEEE/ACM Design Automation Conference, 2006
  • “Embedded Systems Education,” Panel Chair, IEEE/ACM Design Automation Conference, 2000
  •  “Compilers for Systems on a Chip,” Panel Chair, IEEE International Conference on Computer Design, October 1997

 

Tutorials

  • “CAD Techniques for Embedded Systems”, IEEE VLSI Design, January 1999
  • “Static Timing Analysis of Embedded Software”, ACM Design Automation Conference, June 1997
  • “Optimization Techniques for Low Power VLSI Circuits”, IEEE International Conference on Computer-Aided Design, November 1995
  • “Register Transfer Level Synthesis: From Theory to Practice”, IEEE International Conference on VLSI Design, January 1996
  • “A Survey of Optimization Techniques Targeting Low Power VLSI Circuits”, ACM Design Automation Conference, June 1995
  • “Embedded Systems Performance Analysis”, IEEE International Conference on Computer Design, October 1993
  • “Multi-level Logic Synthesis”, IEEE International Conference on Computer-Aided Design, November 1991, November 1992
  • “Sequential Logic Synthesis”, IEEE International Conference on VLSI Design, January 1991

 

Publications 

Books

  • Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings. Lecture Notes in Computer Science 5123 Springer 2008, ISBN 978-3-540-70543-7 (Edited Volume, co-edited with A. Gupta)
  • Performance Analysis of Real-Time Embedded Software, (with Yau-Tsun Steven Li), Kluwer Academic Publishers, 1999.

 

Book Chapters

  • Post-Silicon Fault Localization with Satisfiability Solvers. (with G. Weissenbacher) In: Mishra P., Farahmandi F. (eds) Post-Silicon Validation and Debug. Springer, Cham, 2019
  • Propositional SAT Solving, in Handbook of Model Checking (with J. Marques-Silva) 2018: 247-275
  • Verifying Security Properties in Modern SoCs using Instruction Level Abstractions, in Hardware IP Security and Trust, (with P. Subramanyan), Editors: P. Mishra, S. Bhunia, M. Tehranipoor, Springer, 2017
  • Boolean Satisfiability: Solvers and Extensions, in Software Systems Security, (with G. Weissenbacher and P. Subramanyan), Editors: O. Grumberg, H. Seidl, M. Irlbeck, Publisher: IOS Press, NATO Science for Peace and Security Series, 2014
  • Boolean Satisfiability Solvers: Techniques and Extensions, in Tools for Analysis and Verification of Software Safety and Security, (with G. Weissenbacher), Editors: T. Nipkow, O. Grumberg, B. Hauptmann, G. Kalus, Publisher: IOS Press, NATO Science for Peace and Security Series, Spring 2012
  • Conflict-Driven Clause Learning, SAT Solvers, in Handbook of Satisfiability, (with J. Marques-Silva and I. Lynce), Edited by A. Biere, H. van Maaren, and T. Walsh, Production editor M. Heule, IOS Press, 2008
  • MADL: An ADL based on a Formal and Flexible Concurrency Model, in Processor Description Languages: Applications and Methodologies, Morgan Kaufman Publishers, (with W. Qin, S. Rajagopalan), Morgan Kaufman, P. Mishra, N. Dutt, Editors, 2008
  • Architecture Description Languages for Retargetable Compilation, (with W. Qin), in The Compiler Design Handbook: Optimizations & Machine Code Generation, CRC Press, Second Edition 2007, Y. N. Srikant and Priti Shankar, Editors
  • A Retargetable VLIW Compiler Framework for DSPs, (with S. Rajagopalan), in The Compiler Design Handbook: Optimizations & Machine Code Generation, CRC Press, Second Edition, 2007, Y. N. Srikant and Priti Shankar, Editors
  • Boolean Satisfiability: Creating Solvers Optimized for Specific Problem Instances, (with P. Zhong and M. Martonosi), Reconfigurable Computing: The Theory and Practice of FPGA Computation, Editors: S. Hauck and A. DeHon, Elsevier Publishers, 2007
  • A Case for Runtime Validation of Hardware, Hardware and Software, Verification and Testing: First International Haifa Verification Conference, Haifa, Israel, November 13-16, 2005, Revised Selected Papers, Lecture Notes in Computer Science, Springer Volume 3875/2006, Editors:  S. Ur, E. Bin, Y. Wolfsthal
  • ZChaff2004: An Efficient SAT Solver, (with Y.Mahajan, Z. Fu), Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004. Selected Revised Papers Series: Lecture Notes in Computer Science
  • Analysis of Search Based Algorithms for Satisfiability of Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems, (with D. Tang, Y. Yu and D. Ranjan), Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004. Selected Revised Papers Series: Lecture Notes in Computer Science
  • Cache Performance of SAT Solvers: A Case Study for Efficient Implementation of Algorithms,” (with L. Zhang), Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers Series: Lecture Notes in Computer Science, Vol.  2919, 2004, Giunchiglia, E.; Tacchella, A. (Eds.)
  • Modeling and Integration of Peripheral Devices in Embedded Systems, (with S. Wang and R. A. Bergamaschi), in Embedded Software for SoC, Kluwer Academic Publishers, 2003, A. Jerraya, S. Yoo, N. Wehn, and D. Verkest, Editors
  • SAT and ATPG: Algorithms for Boolean Decision Problems, (with W. Kunz and J. Marques-Silva), in Logic Synthesis and Verification, Kluwer Academic Publishers, 2001, S. Hassoun and T. Sasao, Editors
  • Instruction Level Power Analysis and Optimization of Software, (with V. Tiwari, A. Wolfe and M. T-C. Lee), in    Technologies for Wireless Computing, Kluwer Academic Publishers, 1996, A. P. Chandrakasan and R. W. Brodersen, Editors
  • Code Generation and Optimization Techniques for Embedded Digital Signal Processors, (with S. Liao, S. Devadas, K. Keutzer, S. Tjiang, A. Wang, G. Araujo, A. Sudarsanam, V. Ziviojnovic, H. Meyr) in Hardware Software Codesign, Kluwer Academic Publishers, NATO-ASI Series, 1996, G. DeMicheli and M. Sami, Editors
  • Performance Analysis of Embedded Systems, (with W. Wolf, A. Wolfe, Y-T S. Li, T-Y Yen), in Hardware Software Codesign, Kluwer Academic Publishers, NATO-ASI Series, 1996, G. DeMicheli and M. Sami, Editors
  • Challenges in Code Generation for Embedded Processors (with G. Araujo, S. Devadas, K. Keutzer, S. Liao, A. Sudarsanam, S. Tjiang, A. Wang) in Code Generation for Embedded Processors, Kluwer Academic Publishers, 1995, P. Marwedel and G. Goossens, Editors

 

Refereed Journal and Conference Papers

1.      “Sparse Matrix to Matrix Multiplication: A Representation and Architecture for Acceleration,” (with. A. Golnari), The 30th IEEE International Conference on Application-specific Systems, Architectures and Processors (ASAP) 2019

2.      “Revealing Cluster Hierarchy in Gate-level ICs Using Block Diagrams and Cluster Estimates of Circuit Embedding,” (with B. Cakir), ACM Transactions on Design Automation of Electronic Systems (TODAES), (accepted for publication).

3.      “Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification,” (with B-Y. Huang, H. Zhang, P. Subramanyan, Y. Vizel, and A. Gupta), ACM Transactions on Design Automation of Electronic Systems (TODAES), 24(1): 10:1-10:24 (2019)

4.      “ILAng: A Modeling Platform for SoC Verification using Instruction-Level Abstractions,” (with B-Y. Huang, H. Zhang, and A. Gupta), 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2019

5.      “SpFlow: Memory-Driven Data Flow Optimization for Sparse Matrix-Matrix Multiplication,” (with Q. Nie), IEEE International Symposium on Circuits and Systems, 2019

6.      “Morpheus: A Vulnerability-Tolerant Secure Architecture Based on Ensembles of Moving Target Defenses with Churn,” (with M. Gallagher, L. Biernacki, S. Chen, Z. B. Aweke, S. F. Yitbarek, M. T. Aga, A. Harris, Z. Xu, B. Kasikci, V. Bertacco, M. Tiwari, T. Austin, 24th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '19), 2019

7.       “A Formal Instruction-Level GPU Model for Scalable Verification,” (with Y. Xing, B-Y Huang, and A. Gupta), IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2018

8.      (Invited Paper) “Vulnerability-Tolerant Secure Architectures,” (with T. Austin, V. Bertacco, B. Kasikci, and M. Tiwari), IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2018

9.      “ Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification,” with H. Zhang, C. Trippel, Y Manerkar, A. Gupta, and M Martonosi, Formal Methods in Computer-Aided Design (FMCAD), 2018

10.   “Lazy Self-Composition for Security Verification,” with W. Yang, P. Subramanyan, Y. Vizel and A. Gupta, International Conference on Computer-Aided Verification (CAV), 2018

11.   “Reverse Engineering Digital ICs Through Geometric Embedding of Circuit Graphs,” with B. Cakir, ACM Transactions on Design Automation of Electronic Systems (TODAES), TODAES, Volume 23 Issue 4, July 2018

12.    “Formal Security Verification of Concurrent Firmware in SoCs using Instruction-Level Abstraction for Hardware,” with B-Y. Huang, J. Fung, S. Ray and A. Gupta, ACM/IEEE Design Automation Conference (DAC) 2018

13.   “MemFlow: Memory-Driven Data Scheduling with Datapath Co-design in Accelerators for Large-Scale Inference Applications,” with Q. Nie, ACM/IEEE 23rd Asia and South Pacific Design Automation Conference (ASP-DAC) 2018

14.   “Template-based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification,” with P. Subramanyan, B-Y. Huang, Y Vizel and A. Gupta, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2017

15.   “Trace-based Analysis of Memory Corruption Malware Attacks,” with Z. Xu and A. Gupta, Thirteenth Haifa Verification Conference (HVC), 2017

16.   “Solving Linear Arithmetic with SAT-based Model Checking,” with Y Vizel and A. Nadel, Formal Methods in Computer-Aided Design (FMCAD), 2017

17.   “PPU: A Control Error-Tolerant Processor for Streaming Applications with Formal Guarantees,” with A. Golnari, Y. Yetim, Y. Vizel and M. Martonosi, ACM Journal on Emerging Technologies in Computing Systems, Special Issue on Alternative Computing Systems, Volume 13, Issue 3, 2017.

18.   “IC3 - Flipping the E in ICE,” with Y. Vizel, A. Gurfinkel, S. Shoham, 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2017.

19.   “Malware Detection using Machine Learning Based Analysis of Virtual Memory Access Patterns,” with Z. Xu, S. Ray and P. Subramanyan, Design, Automation & Test in Europe Conference (DATE), 2017.

20.   “Evaluating Matrix Representations for Error-Tolerant Computing,” with A. Golnari, Design, Automation & Test in Europe Conference (DATE), 2017.

21.   “Model Checking Unbounded Concurrent Lists,” (with D. Sethi and M. Talupur), International Journal on Software Tools for Technology Transfer 18 (4), 375-391, 2016

22.    “A Science of Network Configuration,” (with S. Narain, D. Chee, B. Coan, B. Falchuk, S. Gordon, J. Kang, J. Kirsch, A. Naidu, K. Sinkar, S. Tsang, S. Zhang, V. Rajabian-Schwart, W. Tirenin), Journal of Cyber Security and Information Systems, vol. 4 no. 1, 2016.

23.   “INVITED: Specification and Modeling for Systems-on-Chip Security Verification,” (with P. Subramanyan), IEEE/ACM Design Automation Conference (DAC), 2016

24.   “On computing minimal independent support and its applications to sampling and counting,” (with A. Ivrii, K. S. Meel, and M. Vardi), Constraints, 21(1), 41-58, 2016

25.   “Verifying Information Flow Properties of Firmware Using Symbolic Execution,” (with  P. Subramanyan, H. Khattri, A. Maiti and J. Fung), Design, Automation & Test in Europe Conference (DATE), 2016

26.   “Boolean Satisfiability Solvers and Their Applications in Model Checking,” (with Y. Vizel and G. Weissenbacher), Proceedings of the IEEE, Volume 103, Number 11, pages 2021-2033, November 2015

27.   “Template-based Synthesis of Instruction-Level Abstractions for SoC Verification,” (with P. Subramanyan, Y. Vizel, and S. Ray), Formal Methods in Computer-Aided Design (FMCAD), 2015

28.   “Error-Tolerant Processors: Formal Specification and Verification,” (with A. Golnari and Y. Vizel), In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2015

29.   “On Computing Minimal Independent Support and its Applications to Sampling and Counting,” (with A. Irvii, K. Meel and M. Vardi), Best Student Paper Award, 21st International Conference on Principles and Practice of Constraint Programming (CP), 2015

30.   “Completeness bounds and sequentialization for model checking of interacting firmware and hardware,” (with S. Ahn and A. Gupta), ACM International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), 2015

31.   “Statistical Information Processing: Extending the Limits of Approximate Computing,” (with N. Verma, S. Mitra and S. Shanbhag), Refereed Position Paper, WAX 2015: Workshop on Approximate Computing Across the Stack

32.   “Fast Interpolating BMC,” (with Y. Vizel and A. Gurfinkel), International Conference on Computer-Aided Verification (CAV), 2015

33.   “Evaluating the Security of Logic Encryption Algorithms,” (with P. Subramanyan and S. Ray), Best Student Paper Award, IEEE International Symposium on Hardware-Oriented Security and Trust (HOST), 2015

34.   “CommGuard: Mitigating Communication Errors in Error-Prone Parallel Execution,” (with Y. Yetim and M. Martonosi), 20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2015

35.   “Hardware Trojan Detection for Gate-level ICs Using Signal Correlation Based Clustering,” (with B. Cakir), Best Paper Award, Design, Automation & Test in Europe Conference (DATE), 2015

36.   “Optimizing Dynamic Trace Signal Selection Using Machine Learning and Linear Programming,” (with S. Zhu), Design, Automation & Test in Europe Conference (DATE), 2015

37.   “Template-based Circuit Understanding,” (with A. Gascon, A. Tiwari, B. Dutertre, P. Subramanyan and D. Jovanovic), Formal Methods in Computer-Aided Design (FMCAD), 2014

38.   “In-Band Update for Network Routing Policy Migration,” (with S. Zhang, S. Narain and L. Vanbever), The 22nd IEEE International Conference on Network Protocols (ICNP), 2014

39.   “Reduction of resolution refutations and interpolants via subsumption,” (with R. Bloem, M. Schlaipfer, and G. Weissenbacher), In Hardware and Software: Verification and Testing (pp. 188-203). Springer International Publishing, 2014

40.   “Effective Abstraction for Response Proof of Communication Fabrics,” (with S. Ray), Eighth IEEE/ACM International Symposium on Networks-on-Chip (NoCS), 2014

41.   “Silicon Fault Diagnosis Using Sequence Interpolation with Backbones,” (with S. Zhu and G. Weissenbacher), IEEE/ACM 33rd International Conference on Computer-Aided Design (ICCAD), 2014

42.   “Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom,” (with D. Sethi and M. Talupur), 12th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2014

43.   “Automated Firmware Testing using Firmware-Hardware Interaction Patterns,” (with S. Ahn), ACM International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), 2014

44.   “A Relational Assertion language for Debugging and Monitoring SDN Applications,” (with R. Beckett , K. Zou, S. Zhang, D. Walker and J. Rexford), ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking (HotSDN), 2014

45.   “An Adaptable Rule Placement for Software-Defined Networks,” (with S. Zhang, F. Ivancic, C. Lumezanu, A. Gupta), The 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), 2014

46.   “All-SAT Using Minimal Blocking Clauses,” (with Y. Yu, P. Subramanyan, N. Tsiskaridze), 27th International Conference on VLSI Design, 2014

47.   “Reverse Engineering Digital Circuits Using Structural and Functional Analyses,” (with P. Subramanyan, N. Tsiskaridze, W. Li, A. Gascon, W. Y. Tan, A. Tiwari, N. Shankar, S. Seshia), IEEE Transactions on Emerging Topics in Computing, vol.2, no.1, pp.63-80, March 2014

48.   “Modeling Firmware as Service Functions and Its Application to Test Generation,” (with S. Ahn), Ninth Haifa Verification Conference (HVC), 2013

49.   “Abstractions for Model Checking SDN Controllers,” (with D. Sethi and S. Narayana) Formal Methods in Computer-Aided Design, Formal Methods in Computer-Aided Design (FMCAD), 2013

50.   “SAT Based Verification of Network Data Planes,” (with S. Zhang), Eleventh International Symposium on Automated Technology for Verification and Analysis (ATVA), 2013

51.   “Model Checking Unbounded Concurrent Lists,” (with D. Sethi and M. Talupur), The 20th International SPIN Workshop on Model Checking of Software (SPIN), 2013

52.   “WordRev: Finding Word-Level Structures in a Sea of Bit-Level Gates,” (with W. Li, A. Gascon, P. Subramanyan, W. Y. Tan, A. Tiwari, N. Shankar and S. A. Seshia), IEEE International Symposium on Hardware-Oriented Security and Trust (HOST), 2013

53.   “Extracting Useful Computation From Error-Prone Processors For Streaming Applications,” (with Y. Yetim and M. Martonosi), Design, Automation & Test in Europe Conference (DATE), 2013

54.   “Reverse Engineering Digital Circuits Using Functional Analysis,” (with P. Subramanyan, N. Tsiskaridze, K. Pasricha, D. Reisman and A. Susnea), Design, Automation & Test in Europe Conference (DATE), 2013

55.   “Coverage-based Trace Signal Selection for Fault Localisation in Post-Silicon Validation,” (with S. Zhu and G. Weissenbacher), Eighth Haifa Verification Conference (HVC), 2012

56.   “Verification and Synthesis of Firewalls Using SAT and QBF,” (with S. Zhang, A. Mahmoud and S. Narain), The 2nd International Workshop on Rigorous Protocol Engineering (WRiPE), 2012

57.   “Efficient Predictive Analysis for Detecting Nondeterminism in Multi-Threaded Programs,” (with A. Sinha and A. Gupta), Formal Methods in Computer-Aided Design (FMCAD), 2012

58.   “Verification of Computer Switching Networks: An Overview,” (with S. Zhang and R. McGeer), Invited Paper, Tenth International Symposium on Automated Technology for Verification and Analysis (ATVA), 2012

59.   “Parallel Assertions for Architectures with Weak Memory Models,” (with D. Schwartz-Narbonne and G. Weissenbacher), Tenth International Symposium on Automated Technology for Verification and Analysis (ATVA), 2012

60.   “Parameterized Model Checking of Fine Grained Concurrency,” (with D. Sethi, M. Talupur and D. Schwartz-Narbonne), The 19th International SPIN Workshop on Model Checking of Software (SPIN), 2012

61.   “PASSERT: A tool for debugging parallel programs,” (with D. Schwartz-Narbonne, F. Liu and D. August), 24th Computer-Aided Verification Conference (CAV), 2012

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

63.   “WOLVERINE: Battling Bugs with Interpolants,” (with G. Weissenbacher and D. Kroening), 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012

64.   “EPROF: An Energy/Performance/Reliability Optimization Framework for Streaming Applications,” (with Y. Yetim and M. Martonosi), IEEE/ACM 17th Asia and South Pacific Design Automation Conference (ASP-DAC), 2012

65.   “Predicting Serializability Violations: SMT-based Search vs. DPOR-based Search,” (with A. Sinha, A. Gupta and C. Wang), Haifa Verification Conference (HVC), 2011

66.   “Runtime Verification: A Computer Architecture Perspective,” Invited Paper, International Conference on Runtime Verification (RV), 2011

67.   “SAT-based Techniques for Determining Backbones for Post-Silicon Fault Localisation,” (with C. S. Zhu, G. Weissenbacher and D. Sethi), IEEE Workshop on High Level Design Validation and Test (HLDVT), 2011

68.   “Post-Silicon Fault Localisation Using Maximum Satisfiability and Backbones,” (with S. Zhu, G. Weissenbacher), Formal Methods in Computer-Aided Design (FMCAD), 2011

69.   “Specification and Encoding of Transaction Interaction Properties,” (with D. Sethi and Y. Mahajan), Formal Methods in System Design, 2011-10-01, Springer Netherlands, Issn: 0925-9856, Volume: 39, Issue: 2

70.   “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 (MEMOCODE), 2011

71.   “Predictive Analysis for Detecting Serializability Violations through Trace Segmentation,” (with A. Sinha, A. Gupta and C. Wang), ACM/IEEE Ninth International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2011

72.   “Towards Eliminating Configuration Errors in Cyber Infrastructure.” (with S. Narain, and E. Al-Shaer), In SafeConfig. 2011

73.   “Utility of Transaction-Level Hardware Models in Refinement Checking,” (with Y. Mahajan), IEEE International High Level Design Validation and Test Workshop, 2010.

  1. “Checking Serializability in Software Transactional Memory,” (with A. Sinha), IEEE International Parallel and Distributed Processing Symposium (IPDPS), 2010
  2. “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 (CODES), 2009
  3.  “Boolean Satisfiability: From Theoretical Hardness to Practical Success,” (with L. Zhang), Invited Paper, Communications of the ACM, Volume 52, Number 8, August 2009
  4.  “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
  5. “Runtime Validation of Transactional Memory,” (with K. Chen and P. Patra), 9th International Symposium on Quality Electronic Design (ISQED), 2008.
  6. “Exploiting Circuit Reconvergence through Static Learning in CNF SAT Solvers,” (with Y. Yu and C. Brien), IEEE/ACM 21st International Conference on VLSI Design, 2008
  7. “Runtime Validation of Memory Ordering Using Constraint Graph Checking,” (with K. Chen and P. Patra), IEEE 14th International Symposium on High-Performance Computer Architecture (HPCA), 2008
  8. “A Hierarchical Modeling Framework for On-Chip Communication Architectures of Multiprocessing SoCs,” (with X. Zhu), ACM Transactions on Design Automation of Electronic Systems, Volume 12, Number 1, 2007
  9. “Automating Hazard Checking in Transaction-Level Microarchitecture Models,” (with Y. Mahajan), IEEE Formal Methods in Computer-Aided Design (FMCAD), 2007
  10. “Verification Driven Formal Architecture and Microarchitecture Modeling,” (with Y. Mahajan, C. Chan, A. Bayazit and W. Qin), IEEE/ACM Seventh International Conference on Formal Methods and Models for Codesign (MEMOCODE) 2007
  11. “Extracting Logic Circuit Description from Conjunctive Normal Form Descriptions,” (with Z. Fu),  IEEE/ACM 20th International Conference on VLSI Design, 2007
  12. “The Liberty Simulation Environment: A Deliberate Approach to High-Level System Modeling,” (with M. Vachharajani, N. Vachharajani, D. A. Penry, J. A. Blome, and D. I. August), ACM Transactions on Computer Systems (TOCS), Volume 24, Number 3, August 2006
  13. “Dependable Multithreaded Processing Using Runtime Validation,” (with K. Chen), 12th Pacific Rim International Symposium on Dependable Computing (PRDC), 2006
  14. “Modeling Operation and Microarchitecture Concurrency for Communication Architectures with Application to Retargetable Simulation,” (with X. Zhu and W. Qin), IEEE Transactions on VLSI Systems, pages 707-716, Volume 14, Number 7, July 2006
  15. “Understanding the Dynamic Behavior of Modern DPLL SAT Solvers through Visual Analysis,” (with C. Brien), Formal Methods in Computer-Aided Design (FMCAD), 2006
  16. “On Learning in SMT,” (with Y. Yu), 9th International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science (LNCS), Volume 4121/2006
  17. “Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares,” (with D. Tang), 9th International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science (LNCS), Volume 4121/2006
  18.  “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
  19.  “Solving the Minimum-Cost Satisfiability Problem using SAT Based Branch-and-Bound Search,” (with Z. Fu), IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2006
  20. “Achieving Structural and Composable Modeling of Complex Systems,” (with D. I. August, L-S. Peh, V. Pai, M. Vachharajani and P. Willmann), Invited Paper, The International Journal of Parallel Programming, Kluwer Academic Publishers, Volume 33, Numbers 2-3, June 2005
  21. “A Study of Architecture Description Languages from a Model Based Perspective,” (with W. Qin), IEEE Workshop on Microprocessor Test and Verification (MTV), 2005
  22. “Complementary Use of Runtime Validation and Model Checking,” (with A. Bayazit), IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2005
  23. “Bounds on Power Savings using Runtime Dynamic Voltage Scaling: An Exact Algorithm and a Linear-time Heuristic Approximation,” (with F. Xie and M. Martonosi), Proceedings of the International Symposium of Low Power Electronic Design (ISLPED), 2005
  24. “Symmetry Reduction in SAT-based Model Checking,” (with D. Tang, A. Gupta and N. Ip),  Lecture Notes in Computer Science, Springer-Verlag, Volume 3576 / 2005, Proceedings of the 17th International Conference on Computer Aided Verification (CAV) 2005. Editors:  Kousha Etessami, Sriram K. Rajamani
  25. “Considering Circuit Observability Don’t Cares in CNF Satisfiability,” (with Z. Fu and Y. Yu), Design Automation and Test in Europe (DATE), 2005
  26. “A Technology-aware and Energy-oriented Topology Exploration for On-chip Networks,” (with H. Wang and L-S. Peh), Design Automation and Test in Europe (DATE), 2005
  27. “Verifying the Correctness of Quantified Boolean Formula (QBF) Solvers: Theory and Practice,” (with Y. Yu), Asis-Pacific Design Automation Conference (ASP-DAC), 2005
  28. “Intra-program dynamic voltage scaling: Bounding opportunities with analytical modeling,” (with F. Xie and M. Martonosi), p323-367, Volume 1, Issue 3, ACM Transactions on Architecture and Code Optimization (TACO), September, 2004
  29. “Dynamically Reconfigurable Datapath Co-processor Design for Embedded Systems,” (with Z. Huang, N. Moreano and G. Araujo), ACM Transactions on Embedded Computer Systems, Volume 3 ,  Issue 2  (May 2004), Pages: 361 - 384
  30. “Facilitating Reuse in Hardware Models with Enhanced Type Inference,” (with M. Vachharajani, N. Vachharajani and D. I. August), IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), 2004
  31. “Modeling Operation and Microarchitecture Concurrency for Communication Architectures with Application to Retargetable Simulation,” (with X. Zhu and W. Qin), IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), 2004
  32. “Analysis of Search Based Algorithms for Satisfiability of Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems,” (with D. Tang, Y.Yu and D. Ranjan), The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT), 2004
  33. “A Comparative Study of 2QBF Algorithms,” (with D. Tang and D. Ranjan), The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT), 2004
  34. “A Formal Concurrency Model Based Architecture Description Language for Synthesis of Software Development Tools,” (with W. Qin and S. Subramanian), ACM SIGPLAN/SIGBED 2004 Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), 2004
  35. “Using a Communication Architecture Specification in an Application-driven Retargetable Prototyping Platform for Multiprocessing,” (with X. Zhu), Design Automation and Test in Europe (DATE), 2004
  36. “Power-driven Design of Router Microarchitectures in On-chip Networks,” with H. Wang and L-S. Peh, The 36th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), 2003
  37. “Generating Operating System based Device Drivers for Peripheral Devices in Embedded Systems,” (with S. Wang), IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), 2003
  38. “Automated Synthesis of Efficient Binary Decoders for Retargetable Software Toolkits,” (with W. Qin), IEEE/ACM Design Automation Conference (DAC), 2003
  39. “Cache Performance for SAT Solvers: A Case Study for Efficient Implementation of Algorithms,” (with L. Zhang), The International Conference on Theory and Applications of Satisfiability Testing (SAT), 2003
  40. “Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formulas,” (with L. Zhang), The International Conference on Theory and Applications of Satisfiability Testing (SAT), 2003
  41. “Compile-Time Dynamic Voltage Scaling: Opportunities and Limits,” (with F. Xie and M. Martonosi), PLDI 2003
  42. “Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications,” (with L. Zhang), Best Paper Award, Design Automation and Test in Europe (DATE), 2003
  43. “Flexible and Formal Modeling of Micro-processors with Application to Retargetable Simulation,” (with W. Qin), Design Automation and Test in Europe (DATE), 2003.
  44. “Modeling and Integration of Peripheral Devices in Embedded Systems,” (with S. Wang), Design Automation and Test in Europe (DATE), 2003
  45. “A Disciplined Approach to the Development of Platform Architectures,” (with D. I. August, K. Keutzer and A. R. Newton), Invited Article, Microelectronics Journal, Vol. 33 (2002), Pages 881-890
  46. “Limits of using signatures for permutation independent Boolean comparison”, (with J. Mohnke and P. Molitor), Formal Methods in System Design, Kluwer Academic Publishers, 2002
  47. “Conflict Driven Learning in a Quantified Boolean Satisfiability Solver,” (with L. Zhang), IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2002
  48. “A Hierarchical Modeling Framework for On-Chip Communication Architectures,” (with X. Zhu), IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2002
  49. “Datapath Merging and Interconnect Sharing for Reconfigurable Architectures,” (with N. Moreano, G. Araujo and Z. Huang), In Proceedings of International Symposium on System Synthesis (ISSS) 2002
  50. “Orion: A dynamic power simulator for interconnection networks - power-performance tradeoffs for emerging microprocessor systems,” (with H. Wang, X. Zhu and L-S. Peh),  IEEE MICRO 2002.
  51. “Design Tools for Application-Specific Embedded Processors,” (with W. Qin, S. Rajagopalan, M. Vachharajani, H. Wang, X. Zhu, D. August, K. Keutzer, and L-S. Peh), Invited Paper, In Proceedings of EMSOFT 2002.
  52. “From ASIC to ASIP: The Next Design Discontinuity,” (with K. Keutzer and A. R. Newton), Invited Paper, In Proceedings of ICCD 2002.
  53. “Towards Symmetric Treatment of Satisfaction and Conflict in Quantified Boolean Formula Evaluation,” (with L. Zhang), In Proceedings of the 8th International Conference on Principles and Practices of Contraint Programming, 2002 (CP2002).
  54. “A Power Model for Routers: Modeling Alpha 21364 and Infiniband Routers”, (with H. Wang and L-S. Peh), IEEE Hot Interconnects, 2002.
  55. “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.
  56. “Combining Strengths of Circuit-based and CNF-based Algorithms for a High-Performance SAT Solver,” (with M. Ganai, L. Zhang, P. Ashar and A. Gupta), DAC 2002.
  57. “Exploiting Operation Level Parallelism through Dynamically Reconfigurable Datapaths,” (with Z. Huang), DAC 2002.
  58. “A Re-targetable VLIW Compiler Framework for DSPs with Instruction Level Parallelism,” (with S. Rajagopalan, S. P. Rajan, K. Takayama, S. Rigo and G. Araujo), IEEE Transactions on Computer-Aided Design, Volume 20, Number 11, November 2001, pages 1319-1328.
  59.  “Using Complete 1-Distinguishability for FSM Equivalence Checking”, (with A. Gupta and P. Ashar), ACM Transactions on Design Automation for Electronic Systems, Vol. 6, No. 4, pp. 569-590, October 2001.
  60. “Application of BDDs in Formal Matching Techniques for Formal Logic Combinational Verification”, (with J. Mohnke and P. Molitor), International Journal on Software Tools for Technology Transfer, Volume 3, Number 2, pages 207-216, May 2001.
  61. “A Disciplined Approach to the Development of Platform Architectures,” (with D. I. August, K. Keutzer and A. R. Newton), Invited Paper, SASIMI 2001.
  62. “Partition Based Decision Heuristics for Image Computation Using SAT and BDDs,” (with A. Gupta, Z. Yang, P. Ashar and L. Zhang), ICCAD 2001.
  63. “Efficient Constraint Driven Learning in a Boolean Satisfiability Solver,” (with L. Zhang, C. Madigan, M. Moskewicz), ICCAD 2001. ICCAD Ten Year Retrospective Most Influential Paper Award, 2011.
  64. “Accelerating Boolean Satisfiability through Application Specific Processing”, (with Y. Zhao, M. Moskewicz, C. Madigan), ISSS 2001.
  65. “Matching Architecture to Application via Configurable Processors: A Case Study with the Boolean Satisfiability Problem”, (with Y. Zhao, A. Wang, M. Moskewicz and C. Madigan), ICCD 2001.
  66. “Retargetable Static Timing Analysis for Embedded Software”, (with K. Chen and D. August), ISSS 2001.
  67. “Addressing the System-on-a-Chip Interconnection Woes through Communication Based Design”, (with M. Sgroi, M. Sheets, A. Mihal, K. Keutzer, J. Rabaey and A. Sangiovanni-Vincentelli), Invited Paper, DAC 2001.
  68. “Chaff: Engineering an Efficient SAT Solver”, (with M. W. Moskewicz, C. F. Madigan, Y. Zhao and L. Zhang), DAC 2001. The IEEE/ACM Design Automation Conference 50th Anniversary Most Cited Paper Award, 2013.
  69. “Optimal Live Range Merge for Address Register Allocation in Embedded Programs”, (with G. Ottoni, S. Rigo, G. Araujo and S. Rajagopalan), International Conference on Compiler Construction (CC01), 2001.
  70. “Using the IMPACT VLIW Compiler Framework to Implement a Compiler for a Fixed Point DSP”, (with S. Rajagopalan, S. P. Rajan, G. Araujo, S. Rigo), SCOPES 2001.
  71. “Managing Dynamic Reconfiguration Overhead in Systems-on-a-Chip Design Using Reconfigurable Datapaths and Optimized Interconnection Networks”, (with Z. Huang), DATE 2001.
  72. “System Level Design: Orthogonolization of Concerns and Platform-Based Design”, (with K. Keutzer, J. M. Rabaey, A. R. Newton and A. Sangiovanni-Vincentelli), IEEE Transactions on Computer-Aided Design, Vol. 19, No. 12, December 2000.
  73. “Exact Memory Size Estimation for Array Computations”, (with Y. Zhao), IEEE Transactions on VLSI Systems, Vol. 8, No. 5, pp 517-521, October 2000.
  74. “Simultaneous Reference Allocation in Code Generation for Dual Data Memory Bank ASIPs” (with A. Sudarsanam), ACM Transactions on Design Automation for Electronic Systems, Volume 5, Number 2, April 2000.
  75. “Handling Irregular ILP Within Conventional VLIW Schedulers Using Artificial Resource Constraints”, (with S. Rajagopalan, M. Vachharajani) CASES 2000, November 2000.
  76. “Incremental CAD”, (with O. Coudert, J. Cong, M. Sarrafzadeh), Invited Paper, IEEE International Conference on Computer-Aided Design 2000.
  77. “Processor Evaluation in an Embedded Systems Design Environment”, (with T. V. K. Gupta, P. Sharma and M. Balakrishnan), IEEE VLSI 2000.
  78. “Cache Miss Equations: A Compiler Framework for Analyzing and Tuning Memory Behavior”, (with S. Ghosh and M. Martonosi), ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 21, No. 4, July 1999, Pages 702-745.
  79. “Using Configurable Computing to Accelerate Boolean Satisfiability”, (with P. Zhong, M. Martonosi and P. Ashar), IEEE Transactions on Computer-Aided Design, Volume 18, Number 6, pp 861-868, June 1999.
  80. “Performance estimation of embedded software with instruction cache modeling”, (with Y-T S. Li and A. Wolfe), ACM Transactions on Design Automation of Electronic Systems, Pages 257-279, Volume 4, Number 3, 1999.
  81. “A Retargetable Compilation Methodology for Embedded Digital Signal Processors Using a Machine-Dependent Code Optimization Library”, (with A. Sudarsanam and M. Fujita), Kluwer Design Automation for Embedded Systems, Volume 4, Number 2/3, March 1999.
  82. “Paged Absolute Addressing Mode Optimizations for Embedded DSP Programs Using Post-pass Data-flow Analysis”, (with A. Sudarsanam, S. Tjiang and S. Liao) Kluwer Design Automation for Embedded Systems, Volume 4, Number 1, January 1999.
  83. “Establishing latch correspondence for sequential circuits using distinguishing signatures”, (with J. Mohnke and P. Molitor), Integration, the VLSI Journal, Volume 27, Pages 33-46, 1999.
  84. “Exact memory size estimation for array computations without loop unrolling”, (with Y. Zhao), Proceedings of the Design Automation Conference, June 1999.
  85. “Development of a High-Quality Compiler for a Fujitsu Fixed-Point Digital Signal Processor”, (with S.P. Rajan, M. Fujita, A. Sudarsanam), 7th International Workshop on Hardware/Software Codesign, May 1999.
  86. “Guarded Evaluation: Pushing power management to the Logic Synthesis/Design Level”, (with V. Tiwari and P. Ashar), IEEE Transactions on Computer-Aided Design, October 1998.
  87. “Code generations for embedded DSP processors”, (with G. Araujo), ACM Transactions on Design Automation for Electronic Systems, April 1998.
  88. “Precise Miss Analysis for Program Transformations with Caches of Arbitrary Associativity”, (with S. Ghosh and M. Martonosi), Proceedings of the Eighth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-VIII), October 1998.                
  89. “Using Reconfigurable Computing Techniques to Accelerate Problems in the CAD Domain: A Case Study with Boolean Satisfiability”, (with P. Zhong, M. Martonosi and P. Ashar), DAC 98.
  90. “Accelerating Boolean Satisfiability with Configurable Hardware”, (with P. Zhong, M. Martonosi and P. Ashar), FCCM 98. Selected for inclusion in “Significant Contributions from 20 Years of the International IEEE Symposium on Field-Programmable Custom Computing Machines (1993-2013).
  91. “Solving Boolean Satisfiability with Dynamic Hardware Configurations”, (with P. Zhong, M. Martonosi and P. Ashar), FPL 98.
  92. “Performance analysis of embedded software using implicit path enumeration”, (with Y-T Li), IEEE Transactions on CAD, December 1997.
  93. “Delay abstraction in combinational logic circuits”, (with N. Kobayashi), IEEE Transactions on CAD, October 1997.
  94. “Power Analysis and Minimization Techniques for Embedded DSP Software”, (with T-C. Lee, V. Tiwari and M. Fujita), IEEE Transactions on VLSI Systems, March 1997.
  95. “Cinderella: A Retargetable Environment for Performance Analysis of Real-Time Software”, (with Y-T. S. Li and A. Wolfe), Euro-Par 1997.
  96. “Static Timing Analysis of Embedded Software”, (with M. Martonosi and Y-T Li), ACM Design Automation Conference, June 1997.
  97. “Toward Formalizing a Simulation Based Verification Methodology”, (with A. Gupta and P. Ashar), ACM Design Automation Conference, June 1997.
  98. “Cache Miss Equations: An Analytical Representation of Cache Misses”, (with Somnath Ghosh and Margaret Martonosi), ACM International Conference on Supercomputing, 1997. An earlier version was presented at: Workshop on Interaction between Compilers and Computer Architectures, Third International Symposium on High-Performance Computer Architecture (HPCA-3), February 1997.
  99. “Optimization of Embedded DSP Programs Using Post-pass Data-flow Analysis”, (with Ashok Sudarsanam, Steven Tjiang and Stan Liao), IEEE International Conference on Acoustics, Speech, and Signal Processing, April 1997.
  100. “Dynamic Power Management for Microprocessors: A Case Study”, (with V. Tiwari and R. Donnelley), IEEE VLSI Design, January 1997.
  101. “Cache Modeling for Real-Time Software: Beyond Direct Mapped Instruction Caches”, (with Y-T S. Li and A. Wolfe), IEEE Real-Time Systems Symposium, January 1997.
  102. “Technology mapping for low power”, (with V. Tiwari and P. Ashar), Integration, The VLSI Journal, July 1996
  103. “Instruction Level Power Analysis and Optimization of Software”, (with V. Tiwari, A. Wolfe and M. T-C. Lee), Journal of VLSI Signal Processing, Kluwer Academic Publishers, August/September 1996.
  104. “Using Complete-1-Distinguishability for FSM equivalence checking”, (with P. Ashar and A. Gupta), ACM/IEEE International Conference on Computer-Aided Design, November 1996.
  105. “The Case for Retiming with Explicit Reset Circuitry”, (with V. Singhal and R. K. Brayton), ACM/IEEE International Conference on Computer-Aided Design, November 1996.
  106. “Instruction set design and optimizations for address computation in DSP architectures”, (with G. Araujo and A. Sudarsanam), International Symposium on System Synthesis, 1996.
  107. “Using register-transfer paths in code generation for heterogeneous memory-register architectures”, (with G. Araujo and M. T-C. Lee), Best Paper Award, IEEE/ACM Design Automation Conference June 1996.
  108. “Practical analysis of cyclic combinational circuits”, (with A. Srinivasan), IEEE Custom Integrated Circuits Conference, 1996.
  109. “Efficient microarchitecture modeling and path analysis for real-time software”, (with Y-T S. Li and A. Wolfe), IEEE Real-Time Systems Symposium, January 1996.
  110. “Test Generation for Cyclic Combinational Circuits”, (with A. Raghunathan and P. Ashar), IEEE Transactions on Computer-Aided Design, November 1995.
  111. “Exploiting multi-cycle false paths in the performance optimization of sequential circuits”, (with P. Ashar and S. Dey), IEEE Transactions on Computer-Aided Design, September 1995.
  112. “Functional timing analysis using ATPG”, (with P. Ashar and S. Rothweiler), IEEE Transactions on Computer-Aided Design, August 1995.
  113. “Performance estimation of embedded software with instruction cache modeling”, (with Y-T S. Li and A. Wolfe), ACM/IEEE International Conference on Computer-Aided Design, November 1995.
  114. “Memory bank and register allocation in software synthesis for ASIPs”, (with A. Sudarsanam), ACM/IEEE International Conference on Computer-Aided Design, November 1995.
  115. “Fast functional simulation using branching programs”, (with P. Ashar), ACM/IEEE International Conference on Computer-Aided Design, November 1995.
  116. “Limits of using signatures for permutation independent Boolean comparison”, (with J. Mohnke and P. Molitor), ASP Design Automation Conference, 1995.  Earlier versions have been presented at the following workshops: International Workshop on Logic Synthesis, 1995 and in German as “Ueber den Nutzen von Signaturen beim permutationsunabhaengigen Vergleich Boolescher Funktionen” at the Application of Formal Methods to Hardware Design, Passau, March, 1995.
  117. “Delay abstraction in combinational logic circuits”, (with N. Kobayashi), ASP Design Automation Conference, 1995.
  118. “Power Analysis and Low-Power Scheduling Techniques for Embedded DSP Software”, (with T-C. Lee, V. Tiwari and M. Fujita), International Symposium on System Synthesis, 1995.
  119. “Optimal Code Generation for Embedded Memory Non-Homogeneous Register Architectures”, (with G. Araujo), International Symposium on System Synthesis, 1995.
  120. “Guarded Evaluation: Pushing power management to the Logic Synthesis/Design Level”, (with V. Tiwari and P. Ashar), International Symposium on Low Power Design, 1995.
  121. “Performance analysis of embedded software using implicit path enumeration”, (with Y-T Li), ACM Design Automation Conference, June 1995.
  122. “A Survey of Optimization Techniques Targeting Low Power VLSI Circuits”, (with S. Devadas), ACM Design Automation Conference, June 1995.
  123. “Prediction of Interconnect Delay in Logic Synthesis”, (with H-F. Jyu), European Design and Test Conference, February 1995.
  124. “Test Generation for Cyclic Combinational Circuits”, (with A. Raghunathan and P. Ashar), IEEE VLSI Design, January 1995.
  125. “Power Analysis of Embedded Software: A First Step Towards Software Power Minimization”, (with V. Tiwari and A. Wolfe), IEEE Transactions on VLSI Systems, December 1994.
  126. “Certified timing verification and the transition delay of a circuit”, (with S. Devadas, K. Keutzer and A. Wang), IEEE Transactions on VLSI Systems, September 1994.
  127. “Analysis of cyclic combinational circuits”, IEEE Transactions on Computer-Aided Design, July 1994.
  128. “Event suppression: Improving the efficiency of timing simulation for synchronous digital circuits”, (with S. Devadas, K. Keutzer, and A. Wang), IEEE Transactions on Computer-Aided Design, June 1994.
  129. “Compilation Techniques for Low Energy: An Overview”, (with V. Tiwari and A. Wolfe), IEEE Solid States Council Symposium on Low Power Electronics, 1994.
  130. “Power Analysis of Embedded Software: A First Step Towards Software Power Minimization”, (with V. Tiwari and A. Wolfe), IEEE International Conference on Computer-Aided Design, November 1994. Selected for inclusion in “The Best of ICCAD – 20 Years of Excellence in Computer-Aided Design,” 2003.
  131. “Harnessing the performance of microprocessors for real-time applications”,  (with A. Wolfe) Proc. ISCA '94 Workshop on Architectures for Real-Time Applications, April 1994.
  132. “Statistical timing modeling for logic circuits”, (with H-F. Jyu), ACM Design Automation Conference, June 1994.
  133. “Implicit computation of minimum-cost feedback-vertex sets for partial scan and other applications”, (with P. Ashar), ACM Design Automation Conference, June 1994.
  134. “Permutation and phase independent Boolean comparison”, (with J. Mohnke), Integration, The VLSI Journal, North-Holland Publishing, 1993.
  135. “Computation of floating mode delay in combinational logic circuits: theory and algorithms”, (with S. Devadas, and K. Keutzer), IEEE Transactions on Computer-Aided Design, December 1993.
  136. “Computation of floating mode delay in combinational logic circuits: practice and implementation”, (with S. Devadas, K. Keutzer and A. Wang), IEEE Transactions on Computer-Aided Design, December 1993.
  137. “Statistical timing analysis of combinational logic circuits”, (with S. Devadas, H-F. Jyu and K. Keutzer), IEEE Transactions on VLSI Systems, June 1993.
  138. “Verification of asynchronous interface circuits with bounded wire delays”, (with S. Devadas, K. Keutzer, and A. Wang), Journal of VLSI Signal Processing, October 1993.
  139. “A synthesis-based test generation and compaction algorithm for multifaults”, (with S. Devadas and K. Keutzer), Journal of Electronic Testing: Theory and Applications, January 1993.
  140. “Performance optimization of pipelined circuits using peripheral retiming and resynthesis”, (with K. J. Singh, R. K. Brayton and A. Sangiovanni-Vincentelli), IEEE Transactions on Computer-Aided Design, May 1993.
  141. “Analysis of cyclic combinational circuits”, IEEE International Conference on Computer-Aided Design, November 1993.
  142. “Statistical timing optimization of combinational logic circuits”, (with H-F Jyu), IEEE International Conference on Computer Design, Best Paper Award, October 1993.
  143. “Technology mapping for low power”, (with V. Tiwari and P. Ashar), ACM Design Automation Conference, June 1993.
  144. “Functional timing analysis using ATPG”, (with P. Ashar and S. Rothweiler), European Conference on Design Automation, Feb. 1993.
  145. “Permutation and phase independent Boolean comparison”, (with J. Mohnke), European Conference on Design Automation, Feb. 1993.
  146. “Symbolic minimization of multi-level logic and the input encoding problem”, (with L. Lavagno, R. K. Brayton and A. Sangiovanni-Vincentelli). IEEE Transactions on Computer-Aided Design, July 1992.
  147. “Exploiting multi-cycle false paths in the performance optimization of sequential circuits”, (with P. Ashar and S. Dey), IEEE International Conference on Computer-Aided Design, Nov. 1992.
  148. “Verification of asynchronous interface circuits with bounded wire delays”, (with S. Devadas, K. Keutzer, and A. Wang), IEEE International Conference on Computer-Aided Design, Nov. 1992.
  149. “Statistical timing analysis of combinational logic circuits”, (with S. Devadas, H-F. Jyu and K. Keutzer), International Conference on Computer Design, October 1992.
  150. “Computation of floating mode delay in combinational logic circuits: practice and implementation”, (with S. Devadas, K. Keutzer and A. Wang), International symposium on Logic Synthesis and Microprocessor Architecture, July 1992.
  151. “Certified timing verification and the transition delay of a circuit”, (with S. Devadas, K. Keutzer and A. Wang), ACM Design Automation Conference, June 1992.
  152. “Event suppression: Improving the efficiency of timing simulation for synchronous digital circuits”, (with S. Devadas, K. Keutzer and A. Wang), MIT/Brown VLSI Conference, March 1992.
  153. “Is redundancy necessary to reduce delay?” (with K. Keutzer and A. Saldanha) IEEE Transactions on Computer-Aided Design , April 1991.
  154. “Retiming and resynthesis:  Optimization of sequential networks with combinational techniques”, (with E. Sentovich, R. K. Brayton and A. Sangiovanni-Vincentelli). IEEE Transactions on Computer-Aided Design, January 1991.
  155. “Delay computation for combinational logic circuits: theory and algorithms”, (with S. Devadas and K. Keutzer), Distinguished Paper Citation, IEEE International Conference on Computer-Aided Design, Nov. 1991.
  156. “A synthesis-based test generation and compaction algorithm for multifaults”, (with S. Devadas and K. Keutzer), Design Automation Conference, June 1991.
  157. “ MIS-MV: Optimization of multi-level logic with multiple-valued inputs”, (with L. Lavagno, R. K. Brayton and A. Sangiovanni-Vincentelli). International Conference on Computer-Aided Design, November 1990.
  158. “Performance optimization of pipelined circuits”, (with K. J. Singh, R. K. Brayton and A. Sangiovanni-Vincentelli). International Conference on Computer-Aided Design, November 1990.
  159. “Algorithms for discrete function manipulation”, (with A. Srinivasan, T. Kam and R. K. Brayton). International Conference on Computer-Aided Design, November 1990.
  160. “Is redundancy necessary to reduce delay?” (with K. Keutzer and A. Saldanha). Design Automation Conference, June 1990.
  161. “Retiming and resynthesis:  Optimization of sequential networks with combinational techniques”, (with E. Sentovich, R. K. Brayton and A. Sangiovanni-Vincentelli). Hawaii International Conference on System Sciences, January 1990.
  162. “Encoding symbolic inputs for multi-level logic implementation”, (with R. K. Brayton and A. Sangiovanni-Vincentelli). IFIP International Conference on Very Large Scale Integration, 1989.
  163. “Boolean factoring using kernels and rectangle covering”, (with C. L. Berman and N. Maeda). International Symposium on Circuits and Systems, 1989.
  164. “Logic Verification using binary decision diagrams in a logic synthesis environment”, (with A. Wang, R. K. Brayton and A. Sangiovanni-Vincentelli), International Conference on Computer-Aided Design, November 88.

238.                    “Combining multi-level decomposition and topological partitioning for PLA's”, (with R. H. Katz), International Conference on Computer-Aided Design, November 87.

 

Others                                                           

  • “Challenges and Solutions for Late- and Post- Silicon Design,” (with J. Rabaey), IEEE Design and Test of Computers, Volume 25, Number 4, July/August 2008. Invited Paper.
  •  “A Disciplined Approach to the Development of Architectural Platforms,” (with A. Mihal, C. Kulkarni, C. Sauer, K. Vissers, M. Moskewicz, M. Tsai, N. Shah, S. Weber, Y. Jin, and K. Keutzer). IEEE Design & Test of Computers, 19(6):6--16, November-December 2002.
  • “Adapting to a shifting verification scene,” Integrated System Design, CMP Publishers, April 2, 2002.
  •  “Programmable ASICs to Reduce Costs”, (with D. August, K. Keutzer, R. Newton). EE Times, November 11, 2000.