Hardware verification: Techniques, methodology and solutions

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Hardware verification has been one of the biggest drivers of formal verification research, and has seen the greatest practical impact of its results. The use of formal techniques has not been uniformly successful here - with equivalence checking widely used, assertion-based verification seeing increased adoption, and general property checking and theorem proving seeing only limited use. I will first examine the reasons for this varied success and show that for efficient techniques to translate to solutions they must be part of an efficient methodology and be scalable. Next I will describe specific efforts addressing each of these critical requirements for the verification of emerging computing systems. A significant barrier in enabling efficient techniques to flow into efficient methodology is the need for human intervention in this process. I argue that in large part this is due to the gap between functional design specification, which is still largely in natural language, and structural design description at the register-transfer level (RTL). This gap is largely filled by humans, leading to a methodology which is error-prone, incomplete and inefficient. To overcome this, we need formal functional specification and a way to bridge the gap from this specification to structural RTL. In this direction I will present a modeling framework with design models at two levels - architectural and microarchitectural. The architectural model provides for a functional specification, and the microarchitectural model connects this to a physical implementation. I will illustrate how this enables greater automation in verification. A major challenge in verification techniques providing scalable solutions is the inherent intractability of the problem. This is only getting worse with increasing complexity and is reflected in the increasing number of bug escapes into silicon. I argue that existing verification solutions need to be augmented with runtime validation techniques, through online error-checking and recovery in hardware. I will illustrate this with examples from emerging multi-core architectures. I will also discuss the complementary roles of formal techniques and runtime validation in a cooperative methodology.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 14th Int. Conf., TACAS 2008 - Held as Part of the Joint European Conf. Theory and Practice of Software, ETAPS 2008 Proceedings
Number of pages1
DOIs
StatePublished - Jul 21 2008
Event"14th International Conference onTools and Algorithms for the Construction and Analysis of Systems, TACAS2008" - Budapest, Hungary
Duration: Mar 29 2008Apr 6 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4963 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other"14th International Conference onTools and Algorithms for the Construction and Analysis of Systems, TACAS2008"
CountryHungary
CityBudapest
Period3/29/084/6/08

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Hardware verification: Techniques, methodology and solutions'. Together they form a unique fingerprint.

Cite this