Efficient Automatic STE Refinement Using Responsibility
Professor Orna Grumberg ( Technion )
- 16:00 29th May 2008 ( week 6, Trinity Term 2008 )Lecture Theatre B
Symbolic Trajectory Evaluation (STE) is a powerful technique for
hardware model checking. It is based on 3-valued symbolic
simulation, using 0,1, and X (``unknown''). X is used to
abstract away values of circuit nodes, thus reducing memory and
runtime of STE runs.
An STE run results in ``pass'', if the circuit
satisfies the specification, ``fail'' if the circuit
falsifies it, and ``unknown'' (X), if the abstraction is
too coarse to determine either of the two. In the latter case,
refinement is needed:
The X values of some of the abstracted inputs should be replaced.
The main difficulty is to choose an appropriate subset of these
inputs that will help to eliminate the ``unknown'' STE
result, while avoiding an unnecessary increase in memory and
runtime. The common approach to this problem is to manually choose
these inputs.
This work suggests a novel approach to automatic refinement for
STE, which is based on the notion of ``responsibility''. For
each input with X value we compute its ``Degree of
Responsibility'' (DoR) to the ``unknown'' STE result. We
then refine those inputs whose DoR is maximal.
We implemented an efficient algorithm, which is linear in the size
of the circuit, for computing an approximate DoR of inputs. We
used it for refinements for STE on several circuits and
specifications. Our experimental results show that DoR is a very
useful device for choosing inputs for refinement. In comparison
with previous works on automatic refinement, our computation of
the refinement set is faster, STE needs fewer refinement
iterations and uses less overall memory and time.
This is a joint work with Hana Chockler and Avi Yadgar.
--------------------------------------------------------
Bio:
Orna Grumberg received her B.Sc.(1976), M.Sc (1978). and Ph.D. (1984) from the Computer Science Department at the Technion - Israel Institute of Technology. Since 1984 she is a faculty member there.
During 1985-1987 she held a postdoctoral position in Ed Clarke's Verification Group at Carnegie-Mellon University. Since then she spends every summer at CMU as a visiting researcher in this group. In 1992 she was on sabbatical in Bell Laboratories.
Her interests include model checking of hardware and software systems, abstraction-refinement, modularity, symmetry and vacuity in model checking, 3-valued abstraction-refinement, distributed model checking, SAT solvers, model checking games, and symbolic trajectory evaluation (STE).
Together with Ed Clarke and Doron Peled she is the co-author of the book "Model Checking'', published by MIT Press in 1999.
She is on the editorial board of Information and Computation and Formal methods in System Design. She served on numerous program committees of conferences and workshops. She chaired the Computed-Aided Verification (CAV) conference in 1997 and co-chaired the TACAS conference in 2007. She is on the directory board of the NATO summer school in Marktoberdorf (blue series).
hardware model checking. It is based on 3-valued symbolic
simulation, using 0,1, and X (``unknown''). X is used to
abstract away values of circuit nodes, thus reducing memory and
runtime of STE runs.
An STE run results in ``pass'', if the circuit
satisfies the specification, ``fail'' if the circuit
falsifies it, and ``unknown'' (X), if the abstraction is
too coarse to determine either of the two. In the latter case,
refinement is needed:
The X values of some of the abstracted inputs should be replaced.
The main difficulty is to choose an appropriate subset of these
inputs that will help to eliminate the ``unknown'' STE
result, while avoiding an unnecessary increase in memory and
runtime. The common approach to this problem is to manually choose
these inputs.
This work suggests a novel approach to automatic refinement for
STE, which is based on the notion of ``responsibility''. For
each input with X value we compute its ``Degree of
Responsibility'' (DoR) to the ``unknown'' STE result. We
then refine those inputs whose DoR is maximal.
We implemented an efficient algorithm, which is linear in the size
of the circuit, for computing an approximate DoR of inputs. We
used it for refinements for STE on several circuits and
specifications. Our experimental results show that DoR is a very
useful device for choosing inputs for refinement. In comparison
with previous works on automatic refinement, our computation of
the refinement set is faster, STE needs fewer refinement
iterations and uses less overall memory and time.
This is a joint work with Hana Chockler and Avi Yadgar.
--------------------------------------------------------
Bio:
Orna Grumberg received her B.Sc.(1976), M.Sc (1978). and Ph.D. (1984) from the Computer Science Department at the Technion - Israel Institute of Technology. Since 1984 she is a faculty member there.
During 1985-1987 she held a postdoctoral position in Ed Clarke's Verification Group at Carnegie-Mellon University. Since then she spends every summer at CMU as a visiting researcher in this group. In 1992 she was on sabbatical in Bell Laboratories.
Her interests include model checking of hardware and software systems, abstraction-refinement, modularity, symmetry and vacuity in model checking, 3-valued abstraction-refinement, distributed model checking, SAT solvers, model checking games, and symbolic trajectory evaluation (STE).
Together with Ed Clarke and Doron Peled she is the co-author of the book "Model Checking'', published by MIT Press in 1999.
She is on the editorial board of Information and Computation and Formal methods in System Design. She served on numerous program committees of conferences and workshops. She chaired the Computed-Aided Verification (CAV) conference in 1997 and co-chaired the TACAS conference in 2007. She is on the directory board of the NATO summer school in Marktoberdorf (blue series).
Share this:
