Talk Title: Harnessing the Power of Formal Verification for the $Trillion Chip Design Industry
Formal verification and model checking in particular is a key technology which is widely used for enabling the fast-growing electronic industry, serving many aspects of our digital lives in communication and computing. The pandemic has helped accelerate the growth of this industry boosted by the global digital orientation and remote collaboration. Analysists estimate that the electronic industry total annual revenue will be doubled by 2030 to reach one Trillion USD. Chip design is the heart of it and spans many areas including handheld devices, computer servers and cloud computing, mobile phones, Artificial Intelligence, Internet-of-things, automotive and variety of embedded systems. Cost of chip design is severely growing on the other hand and the industry consistently looks for solutions to address the productivity gaps. Formal Verification plays a significant role to boost verification productivity by an order of magnitude by unleashing formal applications. It enables many domains in the chip design and implementation cycles including functional, safety and security verification, logic optimization at various levels of design abstractions starting from architectural levels down to implementation for both software and hardware models.
The inherit theoretical complexity of model checking presents a big barrier to scale for such complex systems. In this talk, we will show how the industry explores and exploits various techniques in model checking to make it a practical and scalable technology, including key technological and methodological inflection points that made significant innovations and managed to boost formal. We will highlight innovations and exploitation that the industry produced, including for example the concept of formal apps, democratization of formal, the concept of 100% signoff in arithmetic designs, and equivalence checking. Model checking of software is a growing interest in the chip design industry driven by the fast growth of domain specific architectures like AI and DSP chips and dedicated accelerators, where models are implemented in C++ and model checking is required.
Despite the impressive industrial advancements and successful applications of model checking technologies for chip design, the domain is still very young considering its high expected impact on the industry. Therefore, in this talk we are interested in inspiring the academic community and accelerating research in key challenges through a joint and focused research with the industry. The intent is to boost core model checking algorithms and abstraction research, as well as model checking applications in key verification areas such as cybersecurity, automotive safety, and machine learning algorithms. Recently we have observed a rising research front of quantum computing leveraging formal verification technologies which could have major impact on the scalability and applications of quantum machines. Through collaboration, the academic and industrial communities can hugely influence the pace of innovation in these critical areas.
Dr. Ziyad Hanna is a Corporate Vice President of Cadence Design Systems, and the R&D General Manager of Cadence Israel, leading the company’s technology innovations and business in the area of Electronic Design Automation with focus on software verification technologies and solutions for the worldwide chip design industry. Prior to that, he was the Sr. Vice President and General Manager of Jasper Israel the first startup company that made its way to exit and managed by an Arab Israeli General Manager. Prior to joining Jasper, Ziyad was a senior principal engineer and senior manager at Intel in Israel and the US. A senior IEEE member, Ziyad is very active in the Hi-Tech field and has participated in many international conferences and workshops. He has published more than 30 articles, has 15 patents, and gave hundreds of talks in various fields in computer science. Ziyad received numerous awards including Intel's highest achievement award twice, and Cadence move-the-needle award. He obtained his bachelor’s and master’s degree from Tel Aviv University, and PhD in computer science from Oxford University in England, where he serves as a visiting professor in the computer science department. Ziyad is very active to foster the Hi-Tech in the Arab community in Israel and serves as Co-Chair of the General Council of the Tsofen foundation for the development of Hi-Tech in the Arab community in Israel. Ziyad was ranked number 39 in TheMarker’s 100 most influential people on the Israel life for year 2019, also top the list in the Hi-Tech category. Also, his name was included in the list of the most influential people in Hi-Tech for 2020 in the People and Computers magazine.