Efficient automatic STE refinement using responsibility

Hana Chockler*, Orna Grumberg, Avi Yadgar

*Corresponding author for this work

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

11 Citations (Scopus)

Abstract

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. The abstraction is derived from a given user specification.

An STE run results in "pass" (1), if the circuit satisfies the specification, 'fail" (0) 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 the 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.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication14th International Conference, TACAS 2008, Part of Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, March 29-April 6, 2008. Proceedings
EditorsCR Ramakrishnan, J Rehof
Place of PublicationBERLIN
PublisherSpringer-Verlag Berlin Heidelberg
Pages233-248
Number of pages16
ISBN (Print)978-3-540-78799-0
DOIs
Publication statusPublished - 2008
Event14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Budapest, Hungary
Duration: 29 Mar 20086 Apr 2008

Publication series

NameLECTURE NOTES IN COMPUTER SCIENCE
PublisherSPRINGER-VERLAG BERLIN
Volume4963
ISSN (Print)0302-9743

Conference

Conference14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Country/TerritoryHungary
CityBudapest
Period29/03/20086/04/2008

Keywords

  • SYMBOLIC TRAJECTORY EVALUATION

Fingerprint

Dive into the research topics of 'Efficient automatic STE refinement using responsibility'. Together they form a unique fingerprint.

Cite this