FMCAD 2013
Formal Methods in Computer-Aided Design
Portland, OR, USA
October 20-23, 2013

Keynotes
Speaker Talk Title
Pranav Ashar Static Verification Based Signoff - A Key Enabler for Managing Verification Complexity in the Modern SoC
Lori A. Clarke Using Process Modeling and Analysis Techniques to Reduce Errors in Healthcare

See the program for the complete FMCAD'13 schedule.


Speaker: Pranav Ashar [Top]

Chief Technology Officer, Real Intent

Talk Title:

Static Verification Based Signoff - A Key Enabler for Managing Verification Complexity in the Modern SoC

Abstract:

Application-based verification, i.e. partitioning the verification process by verification concerns, has become an important approach for managing verification complexity in the billion-transistor SoC. This new verification paradigm has truly come into focus with the proliferation of layers of complexity in an SoC beyond the baseline complexity of its constituent components. In a sense, the nature of chip complexity has shifted from how much goes into a chip to what goes into a chip. Given a narrow verification concern like clock-domain verification, power, dft, reset analysis etc, the specification, analysis and debug dimensions of the verification problem become meaningfully solvable. This is a new paradigm in a sense because it focuses technologists toward the development of complete solutions and closure for the problem at hand as a whole rather than on just nuts-and-bolts technologies like simulation and ABV. Static formal analysis is able to play a key role in this paradigm for various reasons. With the narrow focus on a specific verification problem, much of the specification becomes precise and implicit. In addition, the limited scope allows the formal analysis to be controlled and nominally tractable. Further, even when the formal analysis remains bounded, it is still possible to return actionable information to the user. Finally, debug becomes much more precise and actionable in the context of the narrow verification concern being addressed. These aspects all come to fore in the verification of clock domain crossings in the modern SoC. Used to be that a chip would have a handful of clock domains and the clock-domain checking could be done manually. With 100s of clocks domains on chip, that luxury is not available any more. No SoC gets taped out today without a dedicated sign-off of clock-domain crossings using verification tools specialized for this problem. Another reason clock-domain verification is good to highlight as an example of the new paradigm is that it is at the intersection of chip functionality and timing. This verification task cannot be completed by just functional simulation or just by static timing analysis. It needs a specialized solution, with static formal analysis at its core, to do justice to it.

Speaker Bio:

Dr. Pranav Ashar is the Chief technology Officer at Real Intent Inc., a System-on-Chip verification company. Pranav received his Ph.D. in EECS with emphasis on EDA from the University of California, Berkeley in 1991. He was then at NEC Labs in Princeton, NJ for 13 years where he developed a number of EDA technologies that have influenced the industry. Pranav has authored about 70 refreed publications with more than 1000 citations, and co-authored a book titled "Sequential Logic Synthesis". He has 35 patents granted and pending. Pranav was an adjunct faculty in the CSEE department at Columbia University where he has taught graduate and undergraduate courses on VLSI design automation, VLSI Verification, and VLSI design.


Speaker: Lori A. Clarke [Top]

Professor, University of Massachusetts, Amherst

Talk Title:

Using Process Modeling and Analysis Techniques to Reduce Errors in Healthcare

Abstract:

As has been widely reported in the news lately, healthcare errors are a major cause of death and suffering. In the University of Massachusetts Medical Safety Project, we are exploring the use of process modeling and analysis technologies to help reduce medical errors and improve efficiency. Specifically, we are modeling healthcare processes using a process definition language and then analyzing these processes using model checking, fault-tree analysis, discrete event simulation, and other techniques. Working with the UMASS School of Nursing and the Baystate Medical Center, we are undertaking in-depth case studies on error-prone and life-critical healthcare processes. In many ways, these processes are similar to complex, distributed systems with many interacting, concurrent threads and numerous exceptional conditions that must be handled carefully.

This talk describes the technologies we are using, discusses case studies, and presents our observations and findings to date. Although presented in terms of the healthcare domain, the described approach could be applied to human-intensive processes in other domains to provide a technology-driven approach to process improvement.

Speaker Bio:

Lori A. Clarke is chair of the School of Computer Science at the University of Massachusetts, Amherst and is co-director of the Laboratory for Advanced Software Engineering Research (LASER). She is a Fellow of the ACM and IEEE, and a board member of the Computing Research Association’s Committee on the Status of Women in Computing Research (CRA-W). She received the 2012 ACM Special Interest Group on Software Engineering (SIGSOFT) Outstanding Research Award, the 2011 University of Massachusetts Outstanding Accomplishments in Research and Creative Activity Award, the 2009 College of Natural Sciences and Mathematics Outstanding Faculty Service Award, the 2004 University of Colorado, Boulder Distinguished Engineering Alumni Award, the 2002 SIGSOFT Distinguished Service Award, a 1993 University Faculty Fellowship, and the 1991 University of Massachusetts Distinguished Faculty Chancellor’s Medal. She is a former vice chair of the Computing Research Association (CRA), co-chair of CRA-W, IEEE Publication Board member, associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and IEEE Transactions on Software Engineering (TSE), member of the CCR NSF advisory board, ACM SIGSOFT secretary/treasurer, vice-chair and chair, IEEE Distinguished Visitor, and ACM National Lecturer. She has written numerous papers, served on many program committees, and was program co-chair of the 14th and general chair of the 25th International Conference on Software Engineering. She has been a Principal Investigator on a number of NSF, DoD, and DARPA projects.

Dr. Clarke’s research is in the area of software engineering, primarily focusing on verification and requirements engineering for human-intensive systems. She has been investigating techniques for detecting errors and safety and security vulnerabilities in complex processes in domains such as healthcare and digital government. She is also involved in several efforts to increase participation of underrepresented groups in computing research.