| | Hardware Verification: Methodology, Techniques and Solutions
Sharad Malik
Citation
Sharad Malik. "Hardware Verification: Methodology, Techniques and Solutions". Talk or presentation, 4, April, 2008; Keynote address by Sharad Malik.
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. Electronic downloads
- HTML
Sharad Malik. <a
href="http://www.gigascale.org/pubs/1298.html"><i>Hardware
Verification: Methodology, Techniques and
Solutions</i></a>, Talk or presentation, 4,
April, 2008; Keynote address by Sharad Malik.
- Plain text
Sharad Malik. "Hardware Verification: Methodology,
Techniques and Solutions". Talk or presentation, 4, April,
2008; Keynote address by Sharad Malik.
- BibTeX
@presentation{Malik08_HardwareVerificationMethodologyTechniquesSolutions,
author = {Sharad Malik},
title = {Hardware Verification: Methodology, Techniques and
Solutions},
day = {4},
month = {April},
year = {2008},
note = {Keynote address by Sharad Malik.},
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. },
URL = {http://www.gigascale.org/pubs/1298.html}
}
Posted by Allen Hopkins on 16 May 2008..
Notice:
This material is presented to ensure timely dissemination of scholarly
and technical work. Copyright and all rights therein are retained by
authors or by other copyright holders. All persons copying this
information are expected to adhere to the terms and constraints
invoked by each author's copyright.
| |
