Formal Methods in Computer-Aided Design, 3-6 October, 2016, Mountain View, CA, USA

Tutorials

Manish Pandey: Machine Learning and Systems for the Next Frontier in Formal Verification

Slides: [link]

Abstract: This tutorial covers basics of machine learning, systems and infrastructure considerations for performing machine learning at scale, and applications of machine learning to improve formal verification performance and usability. It starts with blackbox classifier training with gradient descent, and proceeds on to deep network training and simple convolutional neural networks. Next, it discusses how machine learning can be performed at scale, overcoming the performance and throughput limitations of traditional compute and storage systems. Finally, the tutorial describes several ways in which machine learning can be applied for improving formal tools performance and enhancing debug capabilities.

Bio: Dr. Manish Pandey completed his B.Tech, in Computer Science from the Indian Institute of Technology Kharagpur and his PhD in Computer Science from Carnegie Mellon University. He currently leads the R&D teams for formal and static technologies, distributed systems and machine learning at Synopsys. He previously led the development of several static and formal verification technologies at Verplex and Cadence which are in widespread use in the industry. He also has extensive experience in distributed systems and computing infrastructure, when he led the display advertising security group at Yahoo, and storage analytics systems at Nutanix. Dr. Pandey is a frequent guest lecturer on systems and security related topics in CMU. Dr. Pandey has been the recipient of the IEEE Transaction in CAD Outstanding Young author award, and holds over two dozen patents and refereed publications.

Bernd Finkbeiner & Markus Rabe: Verifying Hyperproperties of Hardware Systems

Slides: [link]

Abstract: This tutorial presents hardware verification techniques for hyperproperties. The most prominent application of hyperproperties is information flow security: information flow policies characterize the secrecy and integrity of a system by comparing two or more execution traces, for example by comparing the observations made by an external observer on execution traces that result from different values of a secret variable. Such a comparison cannot be represented as a set of traces and thus falls outside the standard notion of trace properties. A comparison between execution traces can, however, be represented as a set of sets of traces, which is called a hyperproperty. Hyperproperties occur naturally in many applications beyond their origins in security: examples include the symmetric access to critical resources in distributed protocols and Hamming distances between code words in coding theory.

The hardware verification approach of the tutorial is based on recently developed temporal logics for hyperproperties. Unlike classic temporal logics like LTL or CTL*, which refer to one computation path at a time, temporal logics for hyperproperties like HyperLTL and HyperCTL* can express properties that relate multiple traces by explicitly quantifying over multiple computation paths simultaneously. We will relate the logics to the linear-branching spectrum of process equivalences, and show that even though the satisfiability problem of the logics is undecidable in general, the model checking problem can be solved efficiently. We will show how the logics can be used to verify real hardware designs, including an I2C bus master, the symmetric access to a shared resource in a mutual exclusion protocol, and the functional correctness of encoders and decoders for error resistant codes.

Bio: Bernd Finkbeiner is a professor of Computer Science at Saarland University, Germany. He received his Ph.D. in Computer Science from Stanford University in 2003. His research interests are the specification and automatic verification and synthesis of reactive systems. He received best paper awards at FSEN 2007 and at ICALP 2009. In 2015, he was awarded an ERC Consolidator Grant.

Markus N. Rabe is a postdoctoral researcher at the University of California at Berkeley. He received his Ph.D. in Computer Science from Saarland University in 2016. His research interests are the specification and algorithmic verification of security-relevant systems and of probabilistic systems.

Pranav Ashar: A Paradigm Shift in Verification Methodology

Slides: [link]

Abstract: Today’s SoCs are driving unprecedented verification complexity. The combination of billions of gates, system-level functionality on a chip, complex design methodologies like asynchronous clock domains and an explosion of untimed paths on a chip, interacting dynamic power domains, aggressive reset schemes etcetera could have been the perfect storm to staunch productivity. Instead it has turned out to be the mother of all necessities that has driven significant innovation in verification and brought about a paradigm shift.

Static sign-off has proven to be a pillar in this new paradigm. This talk will discuss the template for what has made static techniques successful in verifying modern SoCs. The recent successes are, in no small part, due to the FMCAD community that has pursued formal methods doggedly for decades despite glacial practical adoption. Complementing the efforts of the research community has been the equally determined pursuit in the EDA community to bring structure and automation into the verification process. Through this partnership, we have been able to bring about an analysis framework within which a combination of semantic analysis and formal methods enables a systematic verification process that leads to sign-off level confidence for important failure modes. It will be gratifying for the FMCAD audience to realize that SAT, model checking, functional abstraction, QBF etcetera have become essential in being able to tape out some of the most complex chips in the world on time and within budget. The adoption of IC3/PDR into the verification process was almost immediate.

The recent successes represent a strong debut for static methods. What is the vision to extend the promise into bigger slices of the verification pie? System-level verification continues to be an art-form with very little of the automation, process and problem-framing that have proven successful in other domains. May be the FMCAD community should adopt that as its next major challenge.

Bio: Dr. Pranav Ashar is the Chief Technology Officer at Real Intent, Inc. Real Intent has been a pioneer in the development of static tools for SoC verification. Its tools are designed into the sign-off flows of numerous prominent SoC design companies. Previously Pranav was Department Head at NEC Labs in Princeton, NJ where he developed a number of EDA technologies that have influenced the industry. His paper titled “Accelerating Boolean Satisfiability with Configurable Hardware” was selected as one of 25 significant contributions from 20 Years of the IEEE Symposium on Field-Programmable Custom Computing Machines. He has 35 patents granted or pending, a few of which have led to business enablement. Pranav was adjunct CSEE faculty at Columbia University where he has taught VLSI design and verification courses. Pranav received his Ph.D. in EECS from the University of California, Berkeley.

Pavol Černý: Program Synthesis for Networks

Slides: [link]

Abstract: Software is eating the world. But how will we write all the programs to control everything from sensors to data centers? Program synthesis provides an answer. It increases the productivity of programmers by enabling them to capture their insights in a variety of forms, not just in standard code. In this tutorial, we focus on some challenges in programming networks, and we show how program synthesis algorithms can help.

Developing network programs is difficult, as networks are large distributed systems. In particular, implementing programs that update the configuration of a network in response to events is an intricate problem. First, even if initial and final configurations are correct, subtle bugs in update programs can lead to incorrect transient behaviors, including forwarding loops, black holes, and access control violations. Second, if the update program reacts to events occurring near simultaneously in different parts of the network, naive implementations can lead to causality violations and conflicts. We present scalable program synthesis algorithms that produce network programs that are both correct by construction and efficient.

Bio: Pavol Černý is an assistant professor in the ECEE department at the University of Colorado Boulder. Before joining CU Boulder, he was a postdoctoral researcher at the Institute of Science and Technology (IST) Austria. He earned a DEA diploma at Ecole normale superieure in Paris, France, in 2003, and a PhD in Computer Science at the University of Pennsylvania in 2009. His research interests center on program synthesis and computer-aided verification.