Name: Carl Seger
Title: Formal Verification of Complex Data-Paths: An Industrial Perspective
Abstract: After caches, most transistors in a modern chip are devoted to wide data-paths. Due to performance and power requirements, these data-paths are often implementing sophisticated algorithms and use complex implementations. As Intel experienced in 1994, a bug in a data-path can be extremely expensive and thus needs to be avoided at almost any cost. At the same time, simulation based verification is extremely poor at verifying data-paths due to the vast data space and thus formal verification is appealing. In this talk we will give a retrospective on the formal verification of complex data-paths that took place at Intel from the mid-1990s until recently. We will discuss the technology that made the effort possible, the tools developed that made it feasible, and the methodology created that made it practical.
Bio: Dr. Carl-Johan (Carl) Seger received his M.Sc. in Engineering Physics from Chalmers University of Technology, Sweden in 1985 and his M. Math and Ph.D. degrees in Computer Science from University of Waterloo, Canada, in 1986 and 1988 respectively. After seven years in academia, ending as associate professor at the University of British Columbia, Canada, he joined Intel Corporation's Strategic CAD Labs in 1995 where he stayed for more than 21 years. At Intel, Dr. Seger drove the development and successful wide deployment of formal verification of Intel's microprocessors. In 2006-2007 has was granted a full year sabbatical from Intel and became an Oliver Smithies lecturer and visiting fellow at Balliol College, Oxford. In 2016, he took early retirement from Intel and joined the Computer Science and Engineering department at Chalmers University of Technology as a WASP Professor. In addition to formal verification of hardware, Dr. Seger's research interests focuses on how to design and verify correct, robust, and secure software/hardware systems for autonomous vehicles and other Internet-of-Things.