September 2-5, 2014
Planet Hollywood Resort
Las Vegas, Nevada, USA
Newsflash
Final Program available - High-class Panel Discussion confirmed - Google's Paul Eremenko to give Banquet Speech - Only few Hoover Dam Tour Tickets left - Some Sponsorship Opportunities still available......
   |   

T1A: Opportunities and Challenges for Secure Hardware and Verifying Trust in Integrated Circuits

Mohammad (Mark) Tehranipoor, Charles Knapp Associate Professor
Director, Center for Hardware Assurance, Security, and Engineering (CHASE)
Director, Comcast Center of Excellence in Security Innovation (CSI)
University of Connecticut
URL: http://www.chase.uconn.edu/

Abstract: The migration from a vertical to horizontal business model has made it easier to introduce many vulnerabilities to electronic component design and supply chain. In the first part of this tutorial, we discuss the major issues that must be addressed including securing hardware, verifying trustworthiness of integrated circuits, unique key generation, side-channel attacks and more. In the latter two parts of this tutorial, we will place more emphasis on detection and prevention of hardware Trojans and counterfeit electronic parts and discuss how test can help. In this tutorial, we will cover (i) An introduction to hardware security and trust (physically unclonable functions, true random number generation, hardware Trojans, counterfeit ICs, sidechannel attacks, supply chain vulnerabilities, etc.), (ii) Background and motivation for hardware Trojan and counterfeit prevention/detection; (iii) Taxonomies related to both topics; (iv) Existing solutions; (v) Open test challenges; (vi) Design for security and trust, (vii) New and unified solutions to address these challenges.

MarkTMark (Mohammad) Tehranipoor is currently the Charles H. Knapp Associate Professor of Electrical and Computer Engineering Department at the University of Connecticut.. His current research projects include: computer-aided design and test for CMOS VLSI designs, reliable systems design at nanoscale, counterfeit electroincs detection and prevention, supply chain risk management, and hardware security and trust. Dr. Tehranipoor has published over 200 journal articles and refereed conference papers and has given more than 120 invited talks and keynote addresses since 2006. He has published five books and ten book chapters. He is a recipient of several best paper awards as well as the 2008 IEEE Computer Society (CS) Meritorious Service Award, the 2012 IEEE CS Outstanding Contribution, the 2009 NSF CAREER Award, the 2009 UConn ECE Research Excellence Award, and the 2012 UConn SOE Outstanding Faculty Advisor Award. He serves on the program committee of more than a dozen of leading conferences and workshops. He served as Program Chair of the 2007 IEEE Defect-Based Testing (DBT) workshop, Program Chair of the 2008 IEEE Defect and Data Driven Testing (D3T) workshop, Co-program Chair of the 2008 International Symposium on Defect and Fault Tolerance in VLSI Systems (DFTS), General Chair for D3T-2009 and DFTS-2009, and Vice-general Chair for NATW-2011. He cofounded a new symposium called IEEE International Symposium on Hardware-Oriented Security and Trust (HOST) and served as HOST-2008 and HOST-2009 General Chair and Chair of Steering Committee. He is currently serving as an Associate EIC for IEEE Design & Test, an Associate Editor for JETTA, and an Associate Editor for Journal of Low Power Electronics (JOLPE), an IEEE Distinguished Speaker, and an ACM Distinguished Speaker. Dr. Tehranipoor is a Senior Member of the IEEE and Member of ACM and ACM SIGDA. He is currently serving as the director of Center for Hardware Assurance, Security, and Engineering (CHASE) at UCONN.


 

T1B: Wireless NoC as Interconnection Backbone for Multicore Chips: Promises and Challenges

Partha P. Pande1, Alireza Nojeh2, Andre Ivanov2
1School of Electrical Engineering and Computer Science
Washington State University, Pullman WA, USA
This email address is being protected from spambots. You need JavaScript enabled to view it.

2Department of Electrical and Computer Engineering
The University of British Columbia, Vancouver BC, Canada
{This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it.}

Abstract: The continuing progress and integration levels in silicon technologies make complete end-user systems on a single chip possible. This massive level of integration makes modern multi-core chips all pervasive in domains ranging from weather forecasting, astronomical data analysis, and biological applications to consumer electronics and smart phones. NoCs have emerged as communication backbones to enable a high degree of integration in multi-core SoCs. Despite their advantages, an important performance limitation in traditional NoCs arises from planar metal interconnect-based multi-hop communications, wherein the data transfer between far-apart blocks causes high latency and power consumption. The latency, power consumption, and interconnect routing problems of NoCs can be simultaneously addressed by replacing multi-hop wired paths with high-bandwidth single-hop long-range wireless links. In this tutorial, we will present an overview of the various wireless NoC (WiNoC) architectures proposed so far designed in traditional 2D IC substrate. After this, we introduce how high bandwidth and low power WiNoC architectures can be designed by incorporating the small-world architecture. We will present detailed performance evaluation and necessary design trade-offs for the small-world WiNoCs with respect to their conventional wireline counterparts. We will also discuss different media access control (MAC) mechanisms and routing protocols used for planar WiNoCs so far. We discuss design of various suitable MACs, including token passing, CDMA, FDMA, and time hopping, among others. To sustain the predicted WiNoC performance, a deadlock-free routing algorithm must be designed. The routing protocol also needs to be simple without incurring excessive power, area and latency overheads. We also present performance evaluation of WiNoCs with respect to various other emerging NoC architectures, like 3D, Photonics and RF-I.

The continuing progress and integration levels in silicon technologies make complete end-user systems on a single chip possible. This massive level of integration makes modern multi-core chips all pervasive in domains ranging from weather forecasting, astronomical data analysis, and biological applications to consumer electronics and smart phones. NoCs have emerged as communication backbones to enable a high degree of integration in multi-core SoCs. Despite their advantages, an important performance limitation in traditional NoCs arises from planar metal interconnect-based multi-hop communications, wherein the data transfer between far-apart blocks causes high latency and power consumption. The latency, power consumption, and interconnect routing problems of NoCs can be simultaneously addressed by replacing multi-hop wired paths with high-bandwidth single-hop long-range wireless links. In this tutorial, we will present an overview of the various wireless NoC (WiNoC) architectures proposed so far designed in traditional 2D IC substrate. After this, we introduce how high bandwidth and low power WiNoC architectures can be designed by incorporating the small-world architecture. We will present detailed performance evaluation and necessary design trade-offs for the small-world WiNoCs with respect to their conventional wireline counterparts. We will also discuss different media access control (MAC) mechanisms and routing protocols used for planar WiNoCs so far. We discuss design of various suitable MACs, including token passing, CDMA, FDMA, and time hopping, among others. To sustain the predicted WiNoC performance, a deadlock-free routing algorithm must be designed. The routing protocol also needs to be simple without incurring excessive power, area and latency overheads. We also present performance evaluation of WiNoCs with respect to various other emerging NoC architectures, like 3D, Photonics and RF-I.

PandePartha Pratim Pande is a Professor and holder of the Boeing Centennial Chair in computer engineering at the school of Electrical Engineering and Computer Science, Washington State University, Pullman, USA. He received his M.S degree in computer science from the National University of Singapore and the Ph.D. degree in electrical and computer engineering from the University of British Columbia, Vancouver, BC, Canada. His current research interests are novel interconnect architectures for multicore chips, on-chip wireless communication networks, and hardware accelerators for biocomputing. He has around 80 publications on these topics. Dr. Pande currently serves on the Editorial Board of IEEE Design and Test (D&T), ACM Journal of Emerging Technologies in Computing Systems (JETC) and Sustainable Computing: Informatics and Systems. He also serves in the program committee of many reputed international conferences. He has won the NSF CAREER award for his research on WiNoCs in 2009. He is the winner of the Anjan Bose outstanding researcher award from the college of engineering, Washington State University in 2013.

 

NojehAlireza Nojeh received his B.S. and M. S. degrees in electrical engineering from Sharif University of Technology. His work there focused on optoelectronic modulators based on interface charge layers. He went on to receive a D.E.A. degree in electronics/optoelectronics from the University of Paris XI - Orsay, where he worked on high electron mobility transistors, and a Ph.D. degree in electrical engineering from Stanford University (2006). There, he worked on carbon nanotubes, focusing on nanoscale electron emitters. He then joined the University of British Columbia, where he is currently an associate professor of electrical and computer engineering. He is also a professional engineer of British Columbia. His research interests are still in nanotechnology, in particular in carbon nanotube devices; interaction of light with nanostructures; electron sources, vacuum electronics and electron microscopy; solid-state electronics; micro/nanofabrication; and modeling and simulation of nanoscale structures. Among his main contributions are the discoveries of the “electron stimulated field-emission” and “heat trap” effects.

IvanovAndré Ivanov is Professor and Head of Electrical and Computer Engineering at UBC with a PhD in 1989 from McGill University. His research interests and contributions have focused on the topics of VLSI design and test, design for testability, fault tolerance, fault modeling and simulation, test generation, built-in self-test, built-in current testing, infrastructure IP for systems on chip, systems on chip design and test, analog and mixed signal design and test, networks on chip, fault diagnosis, design validation, post-silicon debug, and interconnects and on-chip communication paradigms. He has published widely, and is an inventor of four US patents. Over the years, Dr. Ivanov has served on steering, program, and/or organization committees of several international events sponsored by the IEEE Computer Society. He chaired the IEEE Computer Society Test Technology Council (TTTC) for the term 2004-2007. He has served on the Board of Governors of the IEEE Computer Society and on the Board of Governors of the IEEE Technology Management Council. He was Technical Program Chair of the VLSI Test Symposium (VTS) in 2001 and 2002 and the General Chair of VTS in 2003 and 2004. In 2004, Dr. Ivanov founded the 1st IEEE International GHz/Gbps Test Workshop. He has served as Associate Editor for the IEEE Transactions on CAD, and for the IEEE Design and Test of Computers Magazine, and for the Journal of Electronic Test: Theory and Applications (JETTA). He is currently the Editor in Chief of IEEE Design and Test. Dr. Ivanov has served on the Computer Society’s Conference and Tutorials Board and the Technical Activities Board. In 2008, he chaired the Computer Society Fellows Committee. He is a Golden Core Member of the Computer Society, a Fellow of the IEEE, a Fellow of the Canadian Academy of Engineering, a Fellow of the Engineering Institute of Canada, and a Professional Engineer of British Columbia.


 

T2A: Clock Implementation: a question of timing

Gerard M Blair
Avago

Abstract: In digital ASIC design, clocks are complicated by timing. This tutorial looks at clock constraints in timing analysis as the affect the hierarchical design flow and timing validation across process variation. The focus is upon how constraints support construction, from a practical perspective forged over many years working on clock tree implementation. This tutorial would cover the following important topics in clock implementation:

  • Timing with propagated clocks and ideal clocks: background on timing report structure and setup/hold particularly on IO paths, assumption of synchronous design

  • Virtual clocks for IO timing: role to keep path constraints unchanged, standard calculation methods for its latency, problems with values in standard block-models, timing impact in using Max rather than average latency.

  • Refocus on role of virtual-clock latency in hierarchical design; description of improved approach

  • Propagation on pins rather than clock objects to avoid updating constraints after synthesis. Note exception where virtual clock required.

  • Description of the role of float pins in clock tree synthesis

  • Using latency values to: a) anticipate clock-gate-enable timing and b) enable single ETMs for macros.

  • Why memories need a float pin and an early latency

  • Types of variation contrasting global vs local: discussion of transistor and parasitic corners.

  • Demonstration of extent of variation by taking a simple repeater chain and varying the segment drivers; consequence to clock design => need to balance not just delay but also sources of delay, including within macro design.

  • Difference between Setup and Hold closure and how these motivate corners for design sign-off; hold is variation about the mean – setup is from the edge of the curve.

  • Setup is slowest corner: temperature effect (slows interconnect, hastens transistors except when it does not!) – also check FAST wafers if voltage lowered for power saving.

  • Hold is NOT a feature of fast data-paths but rather is dominated by clock skew which is an outcome of variation => worst corners are corners away from where clock optimized; explanation of hold risk from scan reordering and how it is minimized

  • Role of derates (OCV and AOCV) and clock uncertainty; increase of hold uncertainty is catastrophic.

  • Wire design: Signal EM avoidance => wider metal; Cross-talk avoidance (effect of cross-talk on timing in general – on macros in particular) => spacing vs shielding: latency, resource use, power (target skew); Early description to enable tool anticipation of final parasitics and resource allocation

BlairGerard M Blair (SMIEEE) holds degrees in Mathematics and Computer Science from the University of Cambridge and a Doctorate in Electrical Engineering from the University of Edinburgh where he taught for eight years, latterly as Senior Lecturer. His first employment was with European Silicon Structures (ES2) which enabled 1000s of ASIC designs in the late 1980s; he also passed a delightful year at Hitachi’s Central Research Facility in Tokyo. He currently resides in the USA where, after a short time with Hewlett-Packard, he is working as a Distinguished Engineer at Lucent/Agere/LSI/Avago in ASIC Implementation and Methodology Design. He has several patents and IEEE/IEE publications: clocks and clocking have been a strong focus in both his academic and industrial carriers.


T2B: Carbon nanotubes and opportunities for wireless on-chip interconnect

Alireza Nojeh1, Partha P. Pande2, Andre Ivanov1
1Department of Electrical and Computer Engineering
The University of British Columbia, Vancouver BC, Canada
{This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it.}
2School of Electrical Engineering and Computer Science
Washington State University, Pullman WA, USA
This email address is being protected from spambots. You need JavaScript enabled to view it.

Abstract: With the growing sophistication of systems-on-chip and networks-on-chip (NoCs), communication among the various parts of such systems is becoming increasingly difficult and interconnect is presenting one of the main bottlenecks to further scaling and increased integration densities. Indeed, materials innovation and improvements to traditional interconnect schemes may not be sufficient for continuing the scaling trend for much longer, and new paradigms might be required. One such paradigm is that of wireless NoCs, where at least a portion of the interconnect lines are replaced by wireless links. However, to implement this scheme using even the highest available electronic frequencies requires antenna devices with dimensions at least on the millimeter scale, meaning that unacceptably large areas of the chip would be taken by these devices and limiting the number of such wireless links. Going to substantially higher frequencies, that is optical frequencies, where the corresponding wavelengths are in the micro/nano scale and the antennas would thus be much smaller, may represent a viable approach to tackle this challenge.

The optical properties of carbon nanotubes and, indeed, other nanoscale wires, represent an interesting and rich regime of operation. On one hand, given their electronic band structure and typical band gap values, the interband transitions in these devices, like in many other solid-state device, could lead to the generation or absorption of visible or infrared light. On the other hand, these nanoscale wires can be made to lengths on the order of several hundreds of nanometers or micrometers, comparable to the wavelength of the radiation being emitted or absorbed. Therefore, their geometry could play a significant role in the distribution of the electromagnetic wave and how the emitted or absorbed light interacts with them, similar to the situation in radio or microwave antennas (albeit at much shorter wavelengths). In other words, both the quantum nature of light and its wave nature are manifest at the same time, combining the worlds of light-emitting diodes and photodetectors with that of electromagnetic antennas. This leads to a rich set of effects and possibilities. In this tutorial, we will review the optical absorption and emission properties of carbon nanotubes and describe how these properties could potentially enable us to establish a wireless network at the small scale for interconnect applications. Devices could be implemented where the signal generation/detection and antenna functionalities are combined. Other devices may only benefit from a subset of these functionalities enabled by nanotubes. We will also discuss some of the performance benefits that may be achieved through such an approach.

 

NojehAlireza Nojeh received his B.S. and M. S. degrees in electrical engineering from Sharif University of Technology. His work there focused on optoelectronic modulators based on interface charge layers. He went on to receive a D.E.A. degree in electronics/optoelectronics from the University of Paris XI - Orsay, where he worked on high electron mobility transistors, and a Ph.D. degree in electrical engineering from Stanford University (2006). There, he worked on carbon nanotubes, focusing on nanoscale electron emitters. He then joined the University of British Columbia, where he is currently an associate professor of electrical and computer engineering. He is also a professional engineer of British Columbia. His research interests are still in nanotechnology, in particular in carbon nanotube devices; interaction of light with nanostructures; electron sources, vacuum electronics and electron microscopy; solid-state electronics; micro/nanofabrication; and modeling and simulation of nanoscale structures. Among his main contributions are the discoveries of the “electron stimulated field-emission” and “heat trap” effects.

PandePartha Pratim Pande is a Professor and holder of the Boeing Centennial Chair in computer engineering at the school of Electrical Engineering and Computer Science, Washington State University, Pullman, USA. He received his M.S degree in computer science from the National University of Singapore and the Ph.D. degree in electrical and computer engineering from the University of British Columbia, Vancouver, BC, Canada. His current research interests are novel interconnect architectures for multicore chips, on-chip wireless communication networks, and hardware accelerators for biocomputing. He has around 80 publications on these topics. Dr. Pande currently serves on the Editorial Board of IEEE Design and Test (D&T), ACM Journal of Emerging Technologies in Computing Systems (JETC) and Sustainable Computing: Informatics and Systems. He also serves in the program committee of many reputed international conferences. He has won the NSF CAREER award for his research on WiNoCs in 2009. He is the winner of the Anjan Bose outstanding researcher award from the college of engineering, Washington State University in 2013.

IvanovAndré Ivanov is Professor and Head of Electrical and Computer Engineering at UBC with a PhD in 1989 from McGill University. His research interests and contributions have focused on the topics of VLSI design and test, design for testability, fault tolerance, fault modeling and simulation, test generation, built-in self-test, built-in current testing, infrastructure IP for systems on chip, systems on chip design and test, analog and mixed signal design and test, networks on chip, fault diagnosis, design validation, post-silicon debug, and interconnects and on-chip communication paradigms. He has published widely, and is an inventor of four US patents. Over the years, Dr. Ivanov has served on steering, program, and/or organization committees of several international events sponsored by the IEEE Computer Society. He chaired the IEEE Computer Society Test Technology Council (TTTC) for the term 2004-2007. He has served on the Board of Governors of the IEEE Computer Society and on the Board of Governors of the IEEE Technology Management Council. He was Technical Program Chair of the VLSI Test Symposium (VTS) in 2001 and 2002 and the General Chair of VTS in 2003 and 2004. In 2004, Dr. Ivanov founded the 1st IEEE International GHz/Gbps Test Workshop. He has served as Associate Editor for the IEEE Transactions on CAD, and for the IEEE Design and Test of Computers Magazine, and for the Journal of Electronic Test: Theory and Applications (JETTA). He is currently the Editor in Chief of IEEE Design and Test. Dr. Ivanov has served on the Computer Society’s Conference and Tutorials Board and the Technical Activities Board. In 2008, he chaired the Computer Society Fellows Committee. He is a Golden Core Member of the Computer Society, a Fellow of the IEEE, a Fellow of the Canadian Academy of Engineering, a Fellow of the Engineering Institute of Canada, and a Professional Engineer of British Columbia.


 

T3A: Design and Managements of Multiprocessor Systems-on-Chips

 Umit Y. Ogras
School of Electrical, Computer and Energy Engineering
Arizona State University
This email address is being protected from spambots. You need JavaScript enabled to view it.

Abstract: Continuous advances in VLSI technology enable implementation of complex systems ranging from single chip cloud computers to application specific heterogeneous multiprocessor systems-on-chip. Regardless of the application domain, design and implementation of these systems require multidimensional problem solving. Traditional metrics such as thermal design power, processor speed and chip area are not adequate to describe or differentiate modern computing systems. Instead, energy efficiency and performance under specific use cases, or key performance indicators, constitute an array of metrics. Similarly, dynamic power management techniques ensure energy efficiency under workload and parameter variations. This talk will present novel design and management methodologies for VLSI systems.

This talk will present a unified methodology for the design and management of state of the art VLSI systems using examples from both high performance CMP and MpSoC domains. More specifically, the first part will focus on a multidimensional optimization methodology which relies on novel analytical power, performance and area models. The second part of the talk will cover variation-adaptive dynamic power management techniques based on feedback control theory.

OgrasUmit Y. Ogras received his Ph.D. degree in Electrical and Computer Engineering from Carnegie Mellon University in 2007. From 2008 to 2013, he worked as a Research Scientist at the Strategic CAD Laboratories, Intel Corporation. He is currently an Assistant Professor at the School of Electrical, Computer and Energy Engineering, Arizona State University. Dr. Ogras has received include Strategic CAD Labs Research Award, 2012 IEEE Donald O. Pederson Transactions on CAD Best Paper Award, 2011 IEEE VLSI Transactions Best Paper Award and 2008 EDAA Outstanding PhD. Dissertation Award.  His research interests include digital system design, embedded systems, multicore architecture and electronic design automation with particular emphasis on multiprocessor systems-on-chip (MPSoC).

 

 


 

T3B: Recent Advancements in Fiber Optic Transmission Enabled by Highly Integrated Mixed Signal SoC and Advanced Digital Signal Processing

Han Sun
Infinera

Abstract: Mixed signal SoC has always played an important role in long haul, high capacity fiber optic transmission systems. In early days of 10Gbit NRZ transmission, the functions were simple, but implementing decision device, clock recovery and de-multiplexing functions at such high data rate was challenging at the time. In the span of 15 years, the single channel data rate and network capacities have increased 20x, owing to a fundamental change in the way data is modulated and demodulated over the fiber optic channel. Intensity modulation and direct detection has given way to coherent detection and advanced modulation formats such as Polarization-Multiplexed QPSK and higher order QAM. Today, commercial state-of-art single channel data rate have reached 100Gbit/s. 400Gbit/s data rates are being attempted in the laboratory. These astounding achievements are not possible without the parallel advancements in CMOS technology. High speed A/D and D/A converters implemented in CMOS side-by-side with massively parallel, highly dense digital circuits is a key enabler in delivering the network capacities demanded by network operators and consumers.

In this tutorial, we first review the challenges of the fiber optic channel, and introduce the necessary digital signal processing functions that need to be implemented in the SOC. We provide some example implementations of clock recovery, carrier recovery and equalization algorithms. We will also review forward error correction methods adopted in the most state-of-art designs. We conclude by discussing the challenges in designing next generation transceiver ASICs.

 

HanSunHan Sun received the B.Eng. degree in electrical engineering and post-graduate degree in photonics and semiconductor lasers, both from the University of Toronto, Toronto, Ontario, Canada, in 1997 and 1999, respectively. From 2001 to 2009, he was employed with Nortel, Ottawa, Ontario, doing research on future optical transport systems. From 2003 to 2006, he was instrumental in the development of DSP algorithms which led to the World’s first commercial 40Gb optical modem employing Pol-Mux QPSK modulation format. He is currently with Infinera Canada, architecting the next generation transceivers targeting at 100Gb and beyond.

He holds 20 granted US patents and 20 additional submissions. He has authored/co-authored over 27 technical journals papers and conference presentations. His publications have accumulated over 1200 citations. He is a regular reviewer of IEEE Photonic Technology Letters. His research interests include signal processing, receiver equalization, and error correction coding.

 


 

T4A: System-on-Chip Design Using Tri-Gate Technology

Andrew Marshall
University of Texas in Dallas

Abstract: At the cutting edge of silicon IC technology we have seen a move from the planar processes used for the last 50 years, to a new three dimensional approach to device design. State of the art production silicon at the 20nm process node uses silicon Tri-gate devices, and it is expected this will continue at the 14-16nm process geometry nodes. It is thus important to understand the specific design issues associated with system on chip circuit design using Tri-gate technology. This tutorial analyzes the design risks and benefits of using bulk tri-gate compared to conventional planar processes.

andrewAndrew Marshall is a research professor at the University of Texas in Dallas, and an analog and digital IC design expert. His research interests include benchmarking of leading edge and future technologies and low power/high voltage analog circuit development. Dr. Marshall has authored/co-authored approximately 82 patents and 80 papers. He is co-author of the book “SOI Design: Analog, Memory and Digital Techniques” and sole author of “Mismatch and Noise in Modern IC Processes”. Andrew is a Fellow of both the IEEE and Institute of Physics, and Fellow Emeritus of Texas Instruments Incorporated.

 

 

 


 

T4B: Formal Verification in System-on-Chip Design:
Scientific Foundations and Practical Methodology

Wolfgang Kunz, Dominik Stoffel and Joakim Urdahl
Dept. of Electrical & Computer Engineering
University of Kaiserslautern

Abstract: The role of formal techniques in SoC design has constantly increased over the last two decades. Yet, in today’s practice, the extent to which formal techniques are involved in actual design flows varies widely between different industrial settings. In some scenarios, formal techniques are conceded a rather minor role and are viewed as nice-to-have additions to conventional simulation, for example as a tool for “hunting bugs” in corner cases. In other scenarios, more and more responsibility is shifted from simulation to formal techniques. Verification methodologies have emerged that involve formal property checking comprehensively, and in a systematic way.

In this tutorial, we review the scientific foundations of modern formal verification tools. A particular focus will be on demonstrating how basic algorithmic issues and the choice of computational models influence industrial verification methodologies. We report on experiences from large-scale industry projects. A systematic property checking methodology is presented as it has evolved in some parts of the industry.

System-level design flows pose new challenges for formal methods. A formal methodology will be outlined that can contribute to closing the “semantic gap” between the system level and the RTL. Based on formal techniques a perspective is developed how to extend traditional design flows by system-level models, not only for prototyping purposes at the system level but also for reducing design and verification costs at the RTL.

KunzWolfgang 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. In 2001 he joined the Department of Electrical & Computer Engineering at the University of Kaiserslautern.

Wolfgang Kunz conducts research in the area of System-on-Chip design and verification. He has played a leading role in large national research projects in Germany with participation of several international companies, universities and research institutes. Current activities concentrate on industry-strength methodologies for formal design verification. His research group collaborates with Alcatel-Lucent, Audi, Bosch, Infineon and OneSpin Solutions to develop new verification methodologies for Systems-on-Chip and Automotive Systems.

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.

StoffelDominik Stoffel obtained a Dipl.-Ing. degree from the University of Karlsruhe in 1992 and a Ph.D. from the University of Frankfurt in 1999. From 1993 to 1994 he worked as an R&D engineer at Mercedes-Benz in the development of testing methodology for automotive electronics. From 1994 to 1998 he was with the Max-Planck Fault-Tolerant Computing Group in Potsdam, Germany. From 1998 to 2001 he was with the Electronic Design Automation group at the University of Frankfurt, Germany. Since 2001 he is working as a research scientist and lecturer, and since 2012 he is an adjunct professor in the Electronic Design Automation group at the University of Kaiserslautern.

Dominik Stoffel conducts research in the area of design and verification of systems-on-chip. He has a special interest in methodologies and techniques for formal design verification. Dominik Stoffel has received the Award of the German IT Society.

UrdahlJoakim Urdahl is a Ph.D. student in the Electronic Design Automation Group at the University of Kaiserslautern, Germany.

He received a B. Eng. degree from Bergen University College, Norway in 2007. In 2010 he graduated with M. Eng. degree from the Norwegian University of Science and Technology (NTNU) where his thesis was awarded the “microelectronics prize” of 2010 for the best master thesis in the field.

His research interests are in formal hardware verification and design methodologies for systems-on-chip.

Sponsors

MBblue transparent CASnew big trans

Corporate Sponsors

cadence logo Infinera NewLOGOtagline PMS White
Aldec Crescent rgb sm  
top