International Workshop on Design and Implementation of Formal Tools and Systems

Portland, OR October 19, 2013

co-located with FMCAD and MEMOCODE

DIFTS (Design and Implementation of Formal Tools and Systems) workshop emphasizes insightful experiences in formal tools and systems design. The first DIFTS workshop was held in 2011, DIFTS11. It provides a forum for sharing challenges and solutions that are original with ground breaking results.

Often the design and implementation of tools for formal analysis require non-trivial engineering decisions. Many challenges are faced, which often can only be met with ingenious implementation techniques. These techniques actually play a crucial role in making the idea work in practice. The workshop provides an opportunity for discussing engineering aspects and various design decisions required to put such formal tools and systems in practical use. DIFTS takes a broad view of the formal tools/systems area, and solicits contributions from domains including, but not restricted to,

  • decision procedures
  • verification
  • testing
  • validation
  • diagnosis
  • debugging
  • synthesis

This workshop encourages and appreciates system development activities, and facilitates transparency in the experimentation. It will also serve as a platform to discuss open problems and future challenges in practicing formal methods.

DIFTS is co-located with FMCAD13. Call for Paper CFP (txt). Call for Participation CFPart (txt).
  • Abstract Submission: July 24, 2013.
  • Paper Submission: July 31, 2013. (extended until August 4, 2013) Submission Page
  • Author Notification: August 31, 2013
  • Camera Ready Version: September 20, 2013

General and Program Chairs

Program Committee

  • Rance Cleaveland, Reactive Systems Inc., USA
    Rance Cleaveland Professor, Dept. of Computer Science, Univ. Maryland and Exec. and Scientific Dir., Fraunhofer USA Ctr. for Exp. Software Eng.

    In model-based testing, (semi-)formal models of systems are used to drive the derivation of test cases to be applied to the system-under-test (SUT). The technology has long been a part of the traditional hardware-design workflows, and it is beginning to find application in embedded-software development processes also. In automotive and land-vehicle control-system design in particular, models in languages such as MATLAB(r) / Simulink(r) / Stateflow(r) are used to drive the testing of the software used to control vehicle behavior, with tools like Reactis(r), developed by a team including the speaker, providing automated test-case generation support for this endeavor.
    This talk will discuss how test-case generation capabilities may also be used to help verify that models meet formal specifications of their behavior. The method we advocate, Instrumentation-Based Verification (IBV), involves the formalizaton of behavior specifications as models that are used to instrument the model to be verified, and the use of coverage testing of the instrumented model to search for specification violations. The presentation will discuss the foundations of IBV, the test-generation approach and other features in Reactis that are used to support IBV, and the results of several case studies involving the use of the methods.

    Speaker bio:
    Rance Cleaveland is Professor of Computer Science at the University of Maryland at College Park, where he is also Executive and Scientific Director of the Fraunhofer USA Center for Experimental and Software Engineering. Prior to joining the Maryland faculty in 2005, he held professorships at the State University of New York at Stony Brook and at North Carolina State University. He also co-founded Reactive Systems, Inc., in 1999 to commercialize tools for model-based testing of embedded software; Reactive Systems currently has numerous customers worldwide in the automotive and aerospace industries. In 1992 he received Young Investigator Awards from the National Science Foundation and from the Office of Naval Research, and in 1994 he was awarded the Alcoa Engineering Research Achievement prize at North Carolina State University. He has published over 125 papers in the areas of software verification and validation, formal methods, model checking, software specification formalisms, model-based testing, and verification tools. Cleaveland received B.S. degrees in Mathematics and Computer Science from Duke University in 1982 and his M.S. and Ph.D. degrees from Cornell University in 1985 and 1987 respectively.

  • Masahiro Fujita, The University of Tokyo, Japan

  • Title:
    Diagnosis and correction of buggy hardware/software with formal approaches

    There have been intensive researches on debugging hardware as well as software. Some are very ad-hoc and based on simple heuristics, but others utilize formal methods and are mathematically modeled. In this talk, we first review various proposals on debugging from historical viewpoints, and then summarize the state-of-the-art in terms of both diagnosis and automatic correction of designs. In particular we show various approaches with SAT-based formulations of diagnosis and correction problems. We also discuss about them in relation to manufacturing test techniques. That is, if the design errors are within the pre-determined types and/or areas, there could be very efficient ways to formally verify, diagnosis and correction methods with small numbers of test vectors. In the last part of the talk, future perspectives including post-silicon issues are discussed.

    Speaker bio:
    Dr. Masahiro Fujita serves as Technical Advisor of Vennsa Technologies, Inc. Dr. Fujita has been Technical advisor at Atrenta. He served as Director of CAD in Fujitsu Laboratories of America, where he served for 15 years. From 1993 to 2000, he was assigned to Fujitsu's US research office and directed the CAD research group. Dr. Fujita has been a Member of Technical Advisory Board of Calypto Design Systems, K.K. since February 2005. He serves as a Member of the Advisory Board at Real Intent, Inc., and NextOp Software, Inc. He serves as Member of Technical Advisory Board of Calypto Design Systems, Inc. He serves as a Member of the Technical Advisory Board for Averant, Inc. He served as Member of Technical Advisory Board of Zenasis Technologies, Inc. Dr. Fujita has been Professor in the Department of Electronic Engineering in VLSI Design and Education Center (VDEC) of University of Tokyo since March 2000. Dr. Fujita joined University of Tokyo in 2000. He has co-authored 2 books, and has over 150 publications. He has participated and chaired many prestigious conferences in CAD and VLSI designs. He has extensive high-level contacts in Japanese industry and academia. He has written over 100 technical papers on all aspects of logic design CAD. Dr. Fujita has received several awards from Japanese major scientific societies on his works in formal verification and logic synthesis. His doctor degree thesis was written in early 1980's and on model checking. Since then, he has been involved in many research projects on various aspects of formal verification. He has done innovative work in the areas of digital design verification at higher level design stages, hardware/software co-design and also digital/analog co-design, synthesis, and testing. Dr. Fujita received his Ph.D. degree in Information Engineering from the University of Tokyo in 1985.

  • Dhiraj Goswami, Synopsys Inc., USA

  • Stimulus generation, enhancement and debug in constraint random verification.

    Verification cost in an IC design team occupies 60-80% of the entire working resources and efforts. Functional verification, posed at the foremost stage of the IC design flow, determines the customers' ability to find bugs quickly and thereby their time-to-results (TTR) and cost-of-results (COR). Consequently, functional verification has been the focus of the EDA industry for the last several decades.
    Constrained random simulation methodologies have become increasingly popular for functional verification of complex designs, as an alternative to directed-test based simulation. In a constrained random simulation methodology, random vectors are generated to satisfy certain operating constraints of the design. These constraints are usually specified as part of a testbench program (using industry-standard testbench languages, like SystemVerilog from Synopsys, e from Cadence, OpenVera, etc.). The testbench automation tool (TBA) is then expected to generate random solutions for specified random variables, such that all the specified constraints over these random variables are satisfied. These random solutions are then used to generate valid random stimulus for the Design Under Verification (DUV). This stimulus is simulated using industry-standard simulation tools, like VCS from Synopsys, NC-Verilog from Cadence, etc. The results of simulation are then typically examined within the testbench program to monitor functional coverage, which gives a measure of confidence on the verification quality and completeness.
    In this talk we will review the challenges of stimulus and configuration generation using constraint random verification methodology. We will also explore why state-of-the-art debug solutions are important to handle complexity and improve the quality of stimulus.

    Speaker bio:
    Dhiraj Goswami received his B.Tech degree from IIT Kanpur and his MS degree from the University of Southern California. He has over 20 years of R&D experience at in EDA. He is currently a Synopsys Scientist and he is leading the research and development of constrained random verification and accelerated verification by massively parallel hardware. He has received numerous awards over the years, including the Intel Discovery Award, the Synopsys Excellence Award, and the Synopsys Top Inventor Award.
The workshop specifically solicits contributions with substantial engineering details that often do not get published but has significant practical impact.

Papers in the following two categories are solicited: (a) system category (10 pages, double column, 11pt), and (b) tool category (8 pages, double column, 11pt).

In the system category, we invite papers that have original ideas accompanied with novel integration techniques, adequate design/implementation details, important design choices made and explored, and good experimental results.

In the tool category, we invite papers that focus primarily on the engineering aspects of some known/popular algorithm, with significant emphasis on the design/implementation details, and various design choices made to advance current state-of-the-art approaches.

The page limit for submissions in the system category is 10 pages in double column format and for submissions in the tool category is 8 pages in double column format.

Submission of papers should be made electronically in PDF format via EasyChair. Submission Page

All accepted contributions will be included in informal proceedings. High quality submissions will be considered for a special issue of journals such as FMSD (Formal Methods in System Design) or IEEE TC (Transactions on Computers).

Niklas Een and Alan Mishchenko, A Fast Reparameterization Procedure

Jiang Long, Robert Brayton and Michael Case, LEC: Learning driven data-path equivalence checking

Marco Palena, Gianpiero Cabodi and Alan Mishchenko, Trading-off Incrementality and Dynamic Restart of Multiple Solvers in IC3

Mathias Preiner, Aina Niemetz and Armin Biere, Lemmas on Demand for Lambdas

Sonali Dutta, Moshe Y. Vardi and Deian Tabakov, CHIMP: a Tool for Assertion-Based Dynamic Verification of SystemC Models

In-Ho Moon and Kevin Harer, Abstraction-Based Livelock/Deadlock Checking for Hardware Verification

Registration Page


Here is a link to DIFT'13 pictures. Pictures
Proceedings are published as CEUR-WS Volume 1130