Abstract. Complementary to the systems and software focus of the conference,
this presentation will be about chips and the progress that has been made in
their functional verification. Common ground will be high-level, still cycleaccurate,
state-based models of hardware functionalities called Abstract RT. RT
stands for register transfer descriptions of hardware such as VHDL or Verilog.
An Abstract RT model is a formal specification which permits an automated
formal comparison with its implementation, thus detecting any functional
discrepancy between code and formal specification.
The first part of the presentation will sketch the big picture: Moore‘s Law still
holds and permits building huge chips comprising up to hundreds of millions of
gates. Under the constraints of shrinking budgets and development times, these
so-called systems-on-chip (SoC) can no longer be developed from scratch but
must largely be assembled from pre-designed, pre-verified design components
such as processors, controllers, a plethora of peripherals and large amounts of
memories. Therefore, getting a SoC right depends to a large extent on the quality
of these design components – IP for short. At stake are critical errors making it
into silicon. These may cost millions of Euros due to delayed market entry,
additional engineering and re-production efforts. Hence, the lion’s share of
today’s verification efforts goes into the functional verification of such IP.