The tutorials will take place on October 22, 2019.
Avi Ziv, IBM
Challenges and Solutions in Post-Silicon Validation of High-end Processors
Abstract: Due to the complexity of designs, post-silicon validation remains a major challenge with few systematic solutions. In this tutorial, we describe the main challenges in post-silicon validation of high-end processors and provide an overview of the state-of-the-art post silicon validation process used by IBM to verify its latest IBM POWER9 processor. We focus on numerous innovations that led to discovery of 30% more bugs in 20% less time over the previous generation. We demonstrate our methodology by describing several bugs from fail detection to root cause.
Bio: Dr. Avi Ziv is a Research Staff Member in the Hardware Verification Technologies Department at the IBM Research Laboratory in Haifa, Israel. Since joining IBM in 1996, Avi has been working on developing technologies and methodologies for various topics of simulations-based functional verification including stimuli generation, checking, functional coverage, coverage directed generation and post-silicon validation.
Avi received the B.Sc. degree in Computer Engineering from the Technion - Israel Institute of Technology in 1990 and the M.Sc. and Ph.D. degrees in Electrical Engineering from Stanford University in 1992 and 1995, respectively. He is the author of more than 50 papers and the inventor of more than 10 patents, mostly in the area of functional verification.
Mark Greenstreet, UBC
Integrating SMT with Theorem Proving for Verification of Analog and Mixed-Signal Circuits
Abstract: The complementary strengths of interactive theorem proving and SMT solvers have motivated several efforts at integration including Sledgehammer for Isabelle/HOL, CoqSMT. The goal of these efforts is to combine the generality of interactive theorem provers, especially support for inductive proofs, with the automation of SMT solvers for discharging tedious subgoals. In practice, such efforts have been hindered by the gaps between the logic of the theorem prover and the SMT solver. Typically, goals in the theorem prover are expressed in an untyped logic, making often making extensive use of recursive functions and quantifiers. In contrast, the logic of SMT solvers is first-order, many-sorted, and lacks recursive functions. In practice, the effort to transform proof goals into formulations that are amenable to SMT techniques can dominate the proof effort.
This tutorial describes Smtlink, our integration of Z3 into ACL2, and presents examples demonstrating the effectiveness of the approach. Smtlink makes extensive use of reflection. By inspecting proof goals and extracting already proven facts, Smtlink automates much of the translation of goals from the untyped logic of ACL2 to the many-sorted logic of Z3. From the user’s perspective, Smtlink can discharge goals that include user-defined data types, recursive functions, and whose proofs build on previously established theorems.
We present several examples from analog and mixed-signal circuits. We also present a simple proof of the Cauchy-Schwartz inequality. In our experience, these proofs were surprisingly straightforward: we identified the obvious, inductive lemmas, and these lemmas were discharged without further effort by the user. As we will show with these examples, the SMT integration makes the theorem proving process productive and fun.
This tutorial is based on joint work with Carl Kwan and Yan Peng.
Bio: Mark Greenstreet is a Professor in the Department of Computer Science at the University of British Columbia. His research interests span a wide range of topics in formal verification and VLSI design, especially, analog, mixed-signal, and asynchronous circuits. Dr. Greenstreet earned his Ph.D. at Princeton University (1992) and his B.Sc. at Caltech (1981). Between Caltech and Princeton, he was a chip designer at ESL, a TRW subsidiary, and a guest researcher at Aarhus University, in Denmark. While at UBC, Dr. Grenstreet has enjoyed collaborations with R&D groups at many companies including Intel, Oracle, Rambus, and SUN Microsystems.
Nadia Polikarpova, UCSD
SuSLik: Synthesis of Safe Pointer-Manipulating Programs
Abstract: SuSLik is a program synthesizer that generates provably safe pointer-manipulating programs automatically from high-level specifications. More precisely, the input to SuSLik is a pair of assertions in separation logic, which describe what the heap looks like before and after executing the program. Using only this information, SuSLik is able to synthesize a wide range of operations on linked data structures, such as singly- and doubly-linked lists, sorted lists, and trees. In this tutorial you will get hands-on experience with SuSLik (bring your laptops!) and learn how synthesis is made possible by a novel proof system we call synthetic separation logic. Experience with separation logic and program synthesis is helpful but not required.
Bio: Nadia Polikarpova is an assistant professor at CSE, and a member of the Programming Systems group. She received her Ph.D. in computer science from ETH Zurich in 2014. She then spent three years as a postdoctoral researcher at MIT. Dr. Polikarpova’s work spans the areas of programming languages and formal methods; in particular, she is interested in building practical tools and techniques that make it easier for programmers to construct secure and reliable software.-