Transcript Joyner - UT Computer Science

Formal Methods in Computer Aided Design
Austin, TX, USA
November 11 - 14
FMCAD 2027:
Will the 'FM' Have a Real Impact
on the 'CAD'?
Moderator: William Joyner
Panelists: Carl Pixley
Robert Jones
Andreas Kuehlmann
SRC
Synopsys
Intel
Cadence
SRC Program Entities
Semiconductor Research Corporation
SRC TRC
Global
Research
Collaboration
Focus Center
Research
Program
Nanoelectronics
Topical
Research Initiative Research
Collaboration
Education
Alliance
2
SRC-GRC Members and Partners
3
Sweden
Finland
Poland
Germany
Canada
UK
Russia
Switzerland
Netherlands
USA
Spain
Austria
China
Italy
Israel
Japan
India
Taiwan
Qatar
Colombia
Singapore
Brazil
Australia
Current
Completed
SRC-GRC Research Worldwide
January 2008
SRC-GRC Research Program Structure
 Developing
verification needs
Nanomanufacturing
document
Sciences (NMS)
and Test Sciences (CADTS)
 Computer-Aided Design
 Logical and Physical Design
 Test and Testability
 Verification
 Integrated Circuit and
System Sciences (ICSS)
 Circuit Design
 Integrated Systems Design
 Device Sciences (DS)





Digital CMOS
Memory Technologies
Modeling and Simulation
Compact Modeling
Analog/Mixed-Signal Devices





Multi-core
Patterning
System/high-level
Factory Systems verification
Analog/mixed
signal
ESH
Hardware/software
Post-silicon validation
 Interconnect and Packaging
Sciences (IPS)
Solicitations
Packaging
 Late
Dec System-level (including verif)
Back-End
Processes
 Late
Jan Verification
 Cross-Disciplinary
Semiconductor Research
(CSR)
5
SRC Receives National Medal of Technology
Office of Science and Technology Policy
Executive Office of the President
New Executive Office Building
Washington, DC 20502
FOR IMMEDIATE RELEASE
June 12, 2007
PRESIDENT BUSH ANNOUNCES THE RECIPIENTS OF THE
2005 NATIONAL MEDAL OF TECHNOLOGY
SRC is recognized for constructing the world's largest
WASHINGTON-- Today President George W. Bush
and most successful university research force in support
announced the recipients of the Nation's highest
of the rapidly growing semiconductor industry; for proving
honor for technology, naming the recipients of the
the worth of collaborative research as the first high-tech
2005 National Medal of Technology. This prestigious
research consortium; and for creating the concept and
award honors America’s leading innovators. The
methodology that evolved into the International
award is given to individuals, teams, and/or
Technology Roadmap for Semiconductors.
companies/divisions for their outstanding
contributions to the nation’s economic, environmental
and social well-being through the development and
commercialization of technology products, processes
and concepts; technological innovation; and
development of the Nation’s technological manpower.
The Department of Commerce administers the award,
which was established by an act of Congress in
1980. For more information about the National
Medal of Technology visit:
www.technology.gov/medal/
SRC CEO Larry Sumney and President Bush at the White House
July 27, 2007
6
More money for
formal
methods!
The Handshake
The Medal
The Whisper
The Past
George Santayana
“Those who cannot remember the past are
condemned to repeat it.”
“History is a pack of lies about events that never
happened told by people who weren't there.”
William Faulkner
“In the South, the past isn’t dead –
it’s not even past!”
8
Hansel and Gretel
(with thanks to Bob Brayton)
9
The Future
Niels Bohr
“Prediction is very difficult,
especially about the future.”
Albert Einstein
“I never think of the future.
It comes soon enough.”
Dan Quayle
“The future will be better
tomorrow.”
Dan Quisenberry
“I’ve seen the future, and it’s much
like the present – only longer.”
10
Other Quotes
Edsger Dijkstra
“Testing can be used to show the presence of
bugs, but never to show their absence.”
Donald Knuth
“Beware of bugs in the above code;
I have only proved it correct, not
tried it.”
Kurt Keutzer
“Functional correctness is the most
fundamental requirement because the speed
and reliability of an incorrectly functioning
electronic system are of no interest.”
11
Other Quotes
Dan Beece
?
“Formal methods will always be restricted to
specialized design components and will occupy
a relatively small niche in design verification.”
Alan Hu
“It's important not to keep redefining formal
verification to mean whatever we can't quite
do yet.”
Farid Najm
“This model is useless, but its theoretical
aspects may be appealing to this audience.”
12
Complexity
Formal Verification Comes of Age!
Year
13
Superexponential Design Complexity
Functionality + Testability
Thousands
Functionality + Testability + Wire Delay
# Transistors
Functionality + Testability + Wire Delay + Power Mgmt
Functionality + Testability + Wire Delay + Power Mgmt
+ Embedded software
Functionality + Testability + Wire Delay + Power Mgmt + Embedded
software + Signal Integrity
Functionality + Testability + Wire Delay + Power Mgmt + Embedded
software + Signal Integrity + Hybrid Chips
Functionality + Testability + Wire Delay + Power Mgmt + Embedded software
+ Signal Integrity + Hybrid Chips + RF
Billions
Functionality + Testability + Wire Delay + Power Mgmt + Embedded software +
Signal Integrity + Hybrid Chips + RF + Packaging
Functionality + Testability + Wire Delay + Power Mgmt + Embedded software + Signal
Integrity + Hybrid Chips + RF + Packaging + Mgmt of Physical Limits
 Exponentially growing number of elements (devices & wires)
 Design complexity is exponential function of element count
14
Carl Pixley
 Group Director in
Advanced Technology
Group, Synopsys
 Taught at UT Austin and
Southwest Texas State
 Formerly at Burroughs,
MCC, Mitsubishi, Motorola
 Ph.D., SUNY Binghamton
15
Robert Jones
 Senior Principal Engineer
at Intel
 Strategic planner for
Intel's internal EDA group
 Previously at Intel's
Strategic CAD Labs
 Ph.D., Stanford
16
Andreas Kuehlmann
 Cadence Fellow and
Director, Cadence
Laboratories
 Dr.-Ing. habil in EE,
University of Technology,
Ilmenau, Germany
 Adjunct Professor,
UC Berkeley
 Worked at Fraunhofer
Institute and IBM
17