Pages: pp. pp. xx-xx
Abstract—This newsletter covers news, research, and events related to the IEEE Council on Electronic Design Automation.
Keywords—design and test, ASP-DAC, DAC, DATE, VLSI-SoC, GLSVLSI, IEEE Embedded Systems Letter, Kaufman Award, CAV Award
The Phil Kaufman Award honors individuals who have made an impact on the field of EDA and pays tribute to Phil Kaufman, the late industry pioneer who turned innovative technologies into commercial businesses that have benefited electronic designers.
This year's Phil Kaufman Award was presented by CEDA and the EDA Consortium to C.L. David Liu for distinguished contributions to EDA. Liu is the William Mong Honorary Chair Professor of Computer Science at National Tsing Hua University in Hsinchu, Taiwan, where he is also a former president.
As chair of the Kaufman Selection Committee and past president of CEDA, I have had the privilege of presiding over the selection of the yearly recipient. C.L. David Liu is a respected figure who has done fundamental and seminal work in EDA and is well-deserving of the honor. He is a distinguished engineer and educator, and an astute business leader. His contributions have been incorporated in many commercial tools and have impacted numerous market segments.
Liu was a professor at the University of Illinois at Urbana-Champaign from 1973 to 1998. After his return to Taiwan in 1998, he became president of National Tsing Hua University until 2002. Many of his students, influenced by his passion for EDA, have made their own impressive marks in our field.
Early in his career, Liu led the transformation from ad hoc EDA to algorithmic EDA. He was an early advocate for more rigorous design automation, reasoning that powerful, formal algorithmic techniques were essential to the effective solution of complex design automation problems. His technical contributions are at the foundation of many current EDA tools within several disciplines, including behavioral synthesis, logic synthesis, and physical design.
Liu's technical impact includes the first floorplanning algorithms and scheduling algorithms for hard real-time tasks. His research on floorplanning received a Best Paper Award at the Design Automation Conference (DAC) in 1986 and has been widely regarded as seminal. His work on rate monotonic scheduling (RMS) is a cornerstone of modern scheduling theory, applicable to the design of real-time operating systems. As of today, his 1973 paper on the subject has had more than 7,000 citations.
Over the past 12 years, Liu's contribution to Taiwan's semiconductor industry has been broad and significant. He serves as chairman of the board of TrendForce, a market intelligence provider in the DRAM, LED, LCD, and solar energy technical segments. He is a member of the board of Powerchip Semiconductor, United Microelectronics Corp. (UMC), MediaTek, and Macronix International. Additionally, he is a member of the board of Anpec Electronics, Andes Corp., and Cadence Methodology Service Company.
If that were not enough, for the past six years he has hosted a weekly radio show in Taiwan on technology, natural science, social science, and literature. He has published three essay collections based on the presentations in this show, and one was a 2011 winner of a prestigious book award in the category of popular science.
—John Darringer, IBM (manager of system-level design) and past president of CEDA
The 2011 Computer-Aided Verification (CAV) Award was presented to Thomas Ball and Sriram Rajamani of Microsoft Research at the 23rd International Conference on Computer-Aided Verification.
The Computer-Aided Verification Conference is the premier international event for reporting research on CAV, a subdiscipline of computer science that is concerned with ensuring that software and hardware systems operate correctly and reliably.
The CAV Award was established in 2008 by the conference steering committee. The annual award, which recognizes a specific fundamental contribution or a series of outstanding contributions to the CAV field, includes a $10,000 prize.
This year's award was presented to Ball and Rajamani with the citation: "for their contributions to software model checking, specifically the development of the SLAM/SDV software model checker, which successfully demonstrated computer-aided verification techniques on real programs."
In the late 1990s, a key challenge for Microsoft was operating system reliability, due in a large part to the low quality of device drivers. By some estimates, drivers caused 70% to 85% of kernel failures. Ball and Rajamani focused their attention on ensuring that device drivers were well-behaved. To do this, they invented a formalism called SLIC (Specification Language for Interface Checking) for expressing correct behavior, built an engine (C2bp) for abstracting C programs to Boolean programs, and wrote a model checker (Bebop) for Boolean programs.
The resulting technology could be applied to programs with tens of thousands of lines of code. They also added a counterexample-driven abstraction refinement step (Newton) and characterized the theoretical power of the method. The project eventually led to the Static Driver Verifier tool, which is used by third-party driver developers and is distributed with the Windows Driver Kit.
This research showed how theorem-proving, model-checking, and static-analysis technology can be applied to the actual action programs of realistic size written in real programming languages. Critics could no longer argue that CAV was limited to hardware or toy programs.
The SLAM (Social Location Application Mobile) project represents a turning point in the acceptance and adoption of software verification technology in industry applications. SLAM has had a large impact within Microsoft, triggering major investments in verification research and leading to new languages and verification tools that are widely adopted within the company.
The project has also significantly influenced research outside Microsoft. It is fair to say that SLAM was instrumental in restarting research by the formal-methods and programming-languages communities in program verification—a subject that had been moribund for quite some time.
It is rare to see a research idea go from conception to industrial impact in such a short duration. The direct contributions of this work, both in developing a new approach to verifying temporal safety properties of software and turning this result into an industrially important software tool, combined with its influence and impact on the research community, make Thomas Ball and Sriram Rajamani worthy recipients of the 2011 CAV Award.
For more information, go to http://www.async.ece.utah.edu/ FAC2011.
The top-five accessed articles from IEEE Embedded Systems Letters in September 2011 were as follows:
CEDA conferences provide excellent opportunities for those interested in learning about the latest technical trends in electronic design and automation. If you'd like to participate or you have an idea about new topics of interest for our conferences, please contact Sani Nassif (firstname.lastname@example.org), CEDA vice president of conferences.
17th Asia and South Pacific Design Automation Conference (ASP-DAC)
30 Jan.–2 Feb. 2012
Design, Automation & Test in Europe (DATE)
12–16 Mar. 2012
Great Lakes Symposium on VLSI (GLSVLSI)
12–16 Mar. 2012