IBM Israel Research Seminars

Hardware verification is a major limiting factor in modern complex design, with an increasing “verification gap” separating the scale of designs that we can reasonably verify and that we can fabricate. I will argue that a significant contributor to this gap is the limitation of the Register-Transfer-Level (RTL) model for design verification. Higher level models such as SystemC and SystemVerilog aim to raise the level of abstraction to enhance designer productivity. However, overall they are limited as they provide for executable but not analyzable descriptions. Next, I will propose the use of formal analyzable design models at two distinct levels above RTL, the architecture and the microarchitecture level. The key characteristic of these models is that they are based on concurrent units of data computation termed transactions. The architecture level describes the computation/state updates in the transactions and their interaction through shared data. The microarchitecture level adds to this the resource usage in the transactions as well as their interaction based on shared resources. This generalizes the notions of architecture and microarchitecture to beyond programmable processor design. We then illustrate the applicability of these models in a top-down verification methodology which addresses most of the concerns of current methodologies.

Speaker Bio
Sharad Malik received the B. Tech. degree in Electrical Engineering from the Indian Institute of Technology, New Delhi, India in 1985 and the M.S. and Ph.D. degrees in Computer Science from the University of California, Berkeley in 1987 and 1990 respectively.

Currently he is the George Van Ness Lothrop Professor of Engineering and the Director for the Center for Innovation in Engineering Education at Princeton University.

His research spans all aspects of Electronic Design Automation. His current focus areas are the synthesis and verification of digital systems and embedded computer systems.