Keynotes
Recent Advances in Model Checking
Prof. Robert K. Brayton, University of California, Berkeley
Model checking, either for property checking or equivalence checking, continues to advance towards shorter runtimes and the ability to handle larger problem instances. These advances have been due to:
- improved underlying engines such as SAT solvers, BMC, and semi-formal simulation,
- new methods such as property directed reachability - IC3/PDR,
- improved data structures for representing logic,
- improved synthesis methods, such as signal correspondence, retiming, reparametrization, use of isomorphism
- improved abstraction methods, such as localization and speculation,
- use of parallelism and general availability of multi-core servers.
This progress is partially documented by the annual hardware model checking competitions and the growing set of competition categories, such as the liveness checking and multi-output categories. These competitions have also encouraged contributions of challenging industrial examples, all of which has greatly stimulated research and development in the model checking area.
This talk will discuss the various advances of the past few years and give examples of the progress made.
Speaker Bio
Robert Brayton received the BSEE degree from Iowa State University in 1956 and the Ph.D. degree in mathematics from MIT in 1961. From 1961 to 1987 he was a member of the Mathematical Sciences Department of the IBM T. J. Watson Research Center. In 1987 he joined the EECS Department at Berkeley, where he is the Cadence Distinguished Professor of Engineering and the director of the SRC Center of Excellence for Design Sciences.
He has authored over 400 technical papers, and 9 books.
Dr. Brayton held the Edgar L. and Harold H. Buttner Endowed Chair in Electrical Engineering at Berkeley from 1996-1999. He is a member of the National Academy of Engineering, and a Fellow of the IEEE and the AAAS. He received the 1991 IEEE CAS Technical Achievement Award, and five best paper awards, including the 1971 IEEE Guilleman-Cauer award, and the 1987 ISCAS Darlington award. He was the editor of the Journal on Formal Methods in Systems Design from 1992-1996. He received the CAS Golden Jubilee Medal and the IEEE Millennium Medal in 2000.
Past contributions have been in analysis of nonlinear networks, electrical simulation and optimization of circuits, and asynchronous synthesis. Current research involves combinational and sequential logic synthesis for area/performance/testability, formal design verification and logical/physical synthesis for DSM designs.
