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 language | English |
---|---|
Title of host publication | Tools and Algorithms for the Construction and Analysis of Systems |
Subtitle of host publication | 14th International Conference, TACAS 2008, Part of Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, March 29-April 6, 2008. Proceedings |
Editors | CR Ramakrishnan, J Rehof |
Place of Publication | BERLIN |
Publisher | Springer-Verlag Berlin Heidelberg |
Pages | 233-248 |
Number of pages | 16 |
ISBN (Print) | 978-3-540-78799-0 |
DOIs | |
Publication status | Published - 2008 |
Event | 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Budapest, Hungary Duration: 29 Mar 2008 → 6 Apr 2008 |
Publication series
Name | LECTURE NOTES IN COMPUTER SCIENCE |
---|---|
Publisher | SPRINGER-VERLAG BERLIN |
Volume | 4963 |
ISSN (Print) | 0302-9743 |
Conference
Conference | 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems |
---|---|
Country/Territory | Hungary |
City | Budapest |
Period | 29/03/2008 → 6/04/2008 |
Keywords
- SYMBOLIC TRAJECTORY EVALUATION