...
SAT
...
Based
...
Design
...
Debugging
...
Propositional
...
Satisfiability
...
(SAT)
...
is
...
seeing
...
increasing
...
use
...
in
...
design
...
verification.
...
One
...
usage
...
scenario
...
involves
...
encoding
...
a
...
verification
...
task
...
as
...
an
...
instance
...
of
...
SAT
...
with
...
the
...
formula
...
representing
...
erroneous
...
conditions.
...
Thus,
...
verification
...
involves
...
proving
...
that
...
this
...
instance
...
is
...
unsatisfiable,
...
i.e.,
...
that
...
there
...
are
...
no
...
erroneous
...
conditions.
...
If
...
this
...
is
...
not
...
the
...
case,
...
then
...
a
...
satisfying
...
assignment
...
provides
...
a
...
“counter-example”
...
which
...
can
...
then
...
be
...
used
...
to
...
debug
...
the
...
design.
...
In
...
an
...
alternate
...
use
...
of
...
SAT
...
for
...
design
...
debugging,
...
the
...
specification
...
is
...
inconsistent
...
with
...
the
...
behavior,
...
and
...
therefore
...
yields
...
an
...
inconsistent
...
SAT
...
instance.
...
There
...
are
...
two
...
separate
...
scenarios
...
where
...
such
...
an
...
inconsistency
...
arises.
...
In
...
the
...
first,
...
you
...
have
...
an
...
implementation
...
which
...
does
...
not
...
satisfy
...
its
...
point-wise
...
specification
...
(i.e.,
...
test-cases
...
fail).
...
In
...
the
...
second,
...
you
...
have
...
the
...
golden
...
model
...
for
...
the
...
implementation
...
and
...
the
...
observed
...
behavior
...
does
...
not
...
adhere
...
to
...
it.
...
In
...
either
...
scenario,
...
the
...
unsatisfiable
...
SAT
...
instance
...
can
...
then
...
be
...
diagnosed
...
to
...
pin-point
...
the
...
fault.
...
This
...
diagnosis
...
uses
...
the
...
notion
...
of
...
correction
...
sets,
...
which
...
is
...
intimately
...
tied
...
to
...
the
...
notion
...
of
...
unsatisfiable
...
subsets
...
(aka
...
cores)
...
and
...
the
...
MAX-SAT
...
problem.
...
In
...
this
...
talk,
...
I
...
will
...
cover
...
design
...
debugging
...
using
...
correction
...
sets
...
and
...
show
...
its
...
application
...
in
...
hardware
...
logic
...
design
...
debugging,
...
software
...
debugging
...
and
...
finally
...
silicon
...
debugging
...
(aka
...
post-silicon
...
validation).
...
Silicon
...
debugging
...
poses
...
difficult
...
challenges
...
due
...
to
...
limited
...
design
...
observability.
...
I
...
will
...
show
...
how
...
the
...
notion
...
of
...
the
...
“backbone”
...
of
...
a
...
satisfiable
...
SAT
...
instance
...
is
...
useful
...
in
...
maximizing
...
information
...
flow
...
in
...
this
...
limited
...
observability
...
context.
...
Sharad Malik, Princeton University
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 Electrical Engineering at Princeton University.
His research focuses on design methodology and design automation for computing systems. He is the Director of the FCRP Gigascale Systems Research Center, a multi-university effort directed towards addressing chip/package-scale system design challenges with a ten year horizon. His research in functional timing analysis and propositional satisfiability has been widely used in industrial electronic design automation tools.
He has received the NSF Young Investigator Award (1994), the CAV Award (2009, for fundamental contributions to the development of high-performance Boolean satisfiability solvers) as well as several best paper and teaching awards. He serves/has served on the program committees of leading conferences and editorial boards of leading journals. He is a fellow of the IEEE. He has published numerous papers, book chapters and a book (Static Timing Analysis for Embedded Software) describing his research.
| Attachments | ||
|---|---|---|
|