2017 Co-located with the Design Automation Conference

26th International Workshop on Logic & Synthesis June 17 – 18, 2017 Thompson Conference Center — Austin, TX

Our sponsors

The International Workshop on Logic and Synthesis is the premier forum for research in synthesis, optimization, and verification of integrated circuits and systems. Research on logic synthesis for emerging technologies and for novel computing platforms, such as nanoscale systems and biological systems, is also strongly encouraged. The workshop encourages early dissemination of ideas and results. The workshop accepts complete papers highlighting important new problems in the early stages of development, without providing complete solutions. The emphasis is on novelty and intellectual rigor.

Call for Papers in PDF

Topics of interest include, but are not limited to: hardware synthesis and optimization; software synthesis; hardware/software co-synthesis; power and timing analysis; testing, validation and verification; synthesis for reconfigurable architectures; hardware compilation for domain-specific languages; design experiences. Submissions on modeling, analysis and synthesis for emerging technologies and platforms are particularly encouraged.

The workshop format includes paper presentations, posters, invited talks, social lunch and dinner gatherings, and recreational activities. Accepted papers are distributed exclusively to IWLS participants.

The technical program consists of 16 regular talks, 4 posters, 2 keynotes and 1 special session.

Keynotes

DA Perspectives and Futures: An Update [slides] Andrew B. Kahng, UC San Diego Over the past two years, an IEEE CEDA initiative has sought to create a sustained focus on how the DA field and community can evolve and flourish beyond its “classical” topics and scope. Two distinct types of outcomes are envisioned from this. First, the initiative seeks to develop an inventory of future application areas for design automation theory and technologies, along with a repeatable process for identifying and advancing topics of high importance to the field. Second, the initiative seeks to better understand history and lessons learned regarding possible structural inefficiencies in (i) interactions among academia, industry and governmental entities, and (ii) interactions between design automation and the applications – systems – integration – technology stack, that waste time and resources today. This talk will review efforts of a working group whose activities were summarized at an ICCAD-2015 special session, as well as outcomes from the first “Design Automation Futures” Workshop which focused on design automation for emerging memory, memory-based computing, and neuromorphic computing systems. Andrew B. Kahng is Professor of CSE and ECE at UC San Diego, where he holds the endowed chair in High-Performance Computing. He has served as visiting scientist at Cadence (1995-1997) and as founder/CTO at Blaze DFM (2004-2006). He is the coauthor of 3 books and over 400 journal and conference papers, holds 33 issued U.S. patents, and is a fellow of ACM and IEEE. He has served as general chair of DAC, ISQED, ISPD and other conferences. His research interests include IC physical design and performance analysis, the IC design-manufacturing interface, combinatorial algorithms and optimization, and the roadmapping of systems and technology.

Machine Learning in Formal Verification [slides] Manish Pandey, Synopsys Formal verification is an integral part of the verification strategy for digital designs today. Advances in automated proof techniques and reachability analysis, debug methodologies and specialized formal 'apps' have brought the power of formal verification to verification and design engineers to detect and debug design errors. Improving the capabilities of these formal tools and increasing the verification productivity requires that we look at new techniques developed in areas such as machine learning and distributed systems. We talk about advances in these areas and their potential to transform formal verification. We start with basics of machine learning, including backbox classifier training with gradient descent, and proceed on to deep network training and simple convolutional neural networks. Next, we discuss how machine learning can be performed at scale, overcoming the performance and throughput limitations of traditional compute and storage systems. Finally, we describe several ways in which machine learning can be applied for improving formal tools performance and enhance their debug capabilities. 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 has been the recipient of the IEEE Transaction in CAD Outstanding Young author award, and holds over two dozen patents and refereed publications.

Special Session on Advances in Formal Verification

	Programming Constraint Services with Z3 Nikolaj Bjorner, Microsoft Many program verification, analysis, testing and synthesis queries reduce to solving satisfiability of logical formulas. Yet there are several applications that rely on information that goes beyond a model, unsatisfiable core or proof. Examples of useful additional information include interpolants, models that satisfy optimality criteria, generating strategies for solving quantified formulas, enumerating and counting solutions. We will cover some of the newer features in Z3 that expose constraint services in the context of Satisfiability Modulo Theories. For applications in product configuration, Z3 includes specialized solvers for finding backbones under assumptions, for solving quantified formulas Z3 contains elements of partial quantifier elimination methods based on models, and for solving optimization modulo background theories, Z3 contains dedicated MaxSAT algorithms. Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Network Verification. His current main line of work with Leonardo de Moura and Christoph Wintersteiger is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS in 2014. Another main line of activities are focused on Network Verification with colleagues in Azure, Karthick Jayaraman, and George Varghese at UCLA. Previously, he developed the DFSR, Distributed File System - Replication, part of Windows Server since 2005 and before that worked on distributed file sharing systems at a startup XDegrees, and program synthesis and transformation systems at the Kestrel Institute. He received his Master's and Ph.D. degrees in computer science from Stanford University, and spent the first three years of university at DTU and DIKU.
	Industrial Scale Formal Verification Using ACL2 Theorem Prover [slides] Anna Slobodova, Centaur Technology Centaur Technology is one of many hardware design companies that adopted formal verification as a part of their production flow. Our company designs Intel compatible x86-64 microprocessors. It does it with a relatively small team. To assure the quality of the design, a lot of effort is spent in the process of validation. Since new additions to IA 64 instruction set architecture widened the data on which instructions are performed, classic simulation provides even less coverage with respect to all possible inputs to the system than a few years ago. At the same time, the capacity of formal tools has reached a level where they can be successful even on industrial scale designs. There are also more publicly available off-shelf formal point tools (SAT, SMT, Model-checkers, etc.) that can be incorporated into more complex validation system. In my talk, I will describe our verification framework that is built on top of the ACL2 theorem prover. Many decision procedures including packages to manipulate Binary Decision Diagrams and And-Inverter Graphs are built in the logic of ACL2. Our framework also has a term-level symbolic simulator called GL that can automate the proof of theorems over finite domains. GL can be combined with word-level symbolic simulation of a hardware model to prove that the model satisfies its specification. Our FV framework is used to verify correctness of the implementation of individual micro-operations, cache-coherency protocol and microcode. It has also been applied to various other problems arising in the design process. Anna Slobodova leads the formal verification team at Centaur Technology that is based in Austin, Texas, USA. Centaur Technology design Intel 64 Architecture compatible micro-processors. Before joining Centaur Technology, Dr. Slobodova spent seven years at Intel, where she was involved in various design projects. In the late 1990s, she was one of the industrial formal methods pioneers as a part of the Alpha development team at DEC and Compaq. In the previous years she was an assistant professor and a researcher at the University of Trier and adjacent institute ITWM-Trier in Germany. Anna Slobodova holds PhD in Computer Science from Comenius University, Bratislava, Slovakia. She has served as a program committee member for a number of conferences concerned with formal methods, e.g. Computer-Aided Verification (CAV) and Formal Methods in Computer-Aided Design (FMCAD).
	Safety across the HW/SW interface – can Formal Methods meet the challenge? [slides] Wolfgang Kunz, University of Kaiserslautern In current practices of SoC design a trend can be observed to integrate more and more low-level software components into the hardware at different levels of granularity. The implementation of important control functions is frequently shifted from the SoC’s hardware into its firmware. This calls for new methods for verification and safety analysis based on a joint analysis of hardware and software. In this talk, we describe a method to inject faults into hardware (HW) and to formally analyze their effects on the software (SW) behavior. We describe how this analysis can be implemented based on a HW-dependent software model called program netlist (PN). We show how program netlists can be extended to formally model the behavior of a program in the event of one or more hardware faults. A PN-level analysis is presented capturing the effects of faults in the architectural states of the system and at the software level. Then, it is shown how these results can be related precisely with gate-level faults located anywhere in the hardware. We present a method that exploits standard gate-level ATPG in combination with constraints obtained from PN-level analysis to determine hardware faults at the gate level that are “application-redundant”. Our experimental results show the feasibility of the proposed approach and point out its application in formal safety analysis for embedded systems. Wolfgang Kunz received the Dipl.-Ing. degree in Electrical Engineering from the University of Karlsruhe, Germany, in 1989 and the Dr.-Ing. degree in Electrical Engineering from the University of Hannover, Germany, in 1992. From 1993 to 1998, he was with Max Planck Society, Fault-Tolerant Computing Group at the University of Potsdam, Germany. From 1998 to 2001 he was a professor of Computer Science at the University of Frankfurt/Main. Since 2001 he is a professor at the Department of Electrical & Computer Engineering at Technische Universität Kaiserslautern. Wolfgang Kunz conducts research in the area of System-on-Chip design and verification collaborating with several industrial partners including AbsInt, Alcatel-Lucent, Atrenta, Audi, Bosch, Infineon and OneSpin Solutions. For his research activities Wolfgang Kunz has received several awards including the Berlin Brandenburg Academy of Science Award and the Award of the German IT Society. Wolfgang Kunz is a Fellow of the IEEE.

Registration

				Until May 18		From May 19
ACM/IEEE members:		Students		$200		$300
		Others		$350		$450
Non ACM/IEEE members:		Students		$300		$400
		Others		$/500		$650

The cost of registration includes breakfasts, lunches, social event and coffee break service.

Register for IWLS on the DAC registration page following the instructions below:

If you are not registered at DAC:

1. Go to https://reg.mpassociates.com/reglive/PromoCode.aspx?confid=223 and click on "Register". This will direct you to the registration page.
2. Complete all the contact information and enter your membership status. Click "Select Your Participation". This will bring you to the product choice page.
3. Open the "Colocated Conferences" tab, select the IWLS option, and click on "Checkout" to proceed to checkout.

If you are registered at DAC and would like to add an IWLS registration:

1. Go to https://reg.mpassociates.com/reglive/locateorder.aspx?confid=223, enter your email account and confirmation number and click on "Locate Order". This will direct you to the registration page.
2. Open the "Colocated Conferences" tab, select the IWLS option, and click on "Checkout" to proceed to checkout.

It is mandatory to register a paper by submitting an abstract before the deadline below.

Paper abstract submission:		March 5, 2017
Full paper submission:		March 12, 2017 @ 11.59pm Anywhere on Earth
Notification of acceptance:		April 16, 2017
Final version due:		May 14, 2017

The submission deadline is final. There will be no extension.

Only complete papers with original and previously unpublished material are permitted. Submissions must be no longer than 8 pages, double column, 10-point font. Accepted papers are distributed only to IWLS participants.

EasyChair IWLS 2017 submission page

In 2017, the IWLS organizing committee set up a programming contest. To participate, please follow these steps:

1. Read the contest description.


2. Write an algorithm that translates benchmarks in either Verilog, Aiger, or Blif format into YIG files. Some benchmarks for training are available in the examples directory.


3. We will send additional contest benchmarks on April 26, 2017. These will be used to evaluate your algorithms.
4. You need to submit your binary or source code and the resulting YIG files for the contest benchmarks until May 3, 2017. Please send everything via email to Mathias Soeken. We must be able to reproduce your results on our machines within a timeout of 10 minutes.


5. We will submit the generated YIG files from your submissions until May 10, 2017 and announce all the results on this webpage.


6. The submissions are rated according the number of gates in the YIGs. If for some benchmark no YIG exists or the algorithm reaches the timeout limit, we take the worst case size over all submissions and multiply it by 1.5. If for some benchmark an incorrect YIG exists, we take the worst case size over all submissions and multiply it by 2.


7. You are encouraged to share your source code with the IWLS community, but it's not required or has any effect on the rating. If you want to share, you can either point us to an online repository that we will link to this and the IWLS webpage. If you prefer to share the source code only among the IWLS participants, we will copy your code onto the proceeding pen drives.

Awards

Awarded students are required to participate at IWLS and present their algorithms and results.

For more information, please refer to the contest website: https://github.com/msoeken/iwls2017-contest

Best Student Paper Award:		IWLS 2017 will be giving a Best Student Paper Award to a work of outstanding quality presented at the Workshop whose first author is a student. The award consists of US$ 150 and a certificate.
Awardee:		Utkarsh Gupta, Priyank Kalla and Vikas Rao, with the paper entitled "Boolean Grobner Basis Reductions on Datapath Circuits Using the Unate Cube Set Algebra".
Student Travel Grants:		IWLS 2017 will be giving travel grants of US$ 250 for students.
Awardees:		Utkarsh Gupta, Winston Haaswijk, Ivo Halecek, Yen-Sheng Ho, Chuan Jiang, Nian-Ze Lee, Rafael Trapani Possignolo, Augusto Neutzling Silva, Gilson Webber, Cunxi Yu.

Please, contact Andre Reis (andre dot reis at inf dot ufrgs dot br) if you have any question regarding student travel grants.

General Chair		Jie-Hong Roland Jiang		National Taiwan University, Taiwan
Program Committee Co-Chair		Rolf Drechsler		University of Bremen/DFKI GmbH, Germany
Program Committee Co-Chair		Robert Wille		Johannes Kepler University Linz, Austria
Special Sessions Chair		Pierre-Emmanuel Gaillardon		University of Utah, USA
Contest Chair		Mathias Soeken		EPFL, Switzerland
Finance Chair		Andre Reis		UFRGS, Brazil
Local Arrangement Chair		Mihir Choudhury		IBM, USA
Publicity Chair		Jody Maick Matos		UFRGS, Brazil

Dirk Stroobandt		Ghent University, Belgium
Andre Reis		UFRGS, Brazil
Rolf Drechsler		University of Bremen/DFKI GmbH, Germany
Ilya Wagner		Intel, US
Valeria Bertacco		University of Michigan, US
Alan Mishchenko		University of California Berkeley, US