Efficient Automatic STE Refinement Using Responsibility
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.
- 1.Adams, S., Bjork, M., Melham, T., Seger, C.: Automatic Abstraction in Symbolic Trajectory Evaluation. In: FMCAD 2007 (2007)Google Scholar
- 2.Chen, Y., He, Y., Xie, F., Yang, J.: Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation. In: FMCAD 2007 (2007)Google Scholar
- 3.Chockler, H., Halpern, J.Y., Kupferman, O.: What causes a system to satisfy a specification? In: ACM TOCL (to appear)Google Scholar
- 8.Halpern, J.Y., Pearl, J.: Causes and explanations: A structural-model approach — part 1: Causes. In: Uncertainty in Artificial Intelligence: Proceedings of the Seventeenth Conference (UAI-2001), pp. 194–202. Morgan Kaufmann, San Francisco (2001)Google Scholar
- 9.Hume, D.: A treatise of human nature. John Noon, London (1739)Google Scholar
- 10.Kurshan, R.P.: Computer-Aided Verification of coordinating processes - the automata theoretic approach (1994)Google Scholar
- 13.Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design 6(2) (1995)Google Scholar
- 14.Seger, C.-J.H., Jones, R.B., O’Leary, J.W., Melham, T.F., Aagaard, M., Barrett, C., Syme, D.: An industrially effective environment for formal hardware verification. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems 24(9) (2005)Google Scholar
- 16.Wile, B., Roesner, W., Goss, J.: Comprehensive Functional Verification: The Complete Industry Cycle. Morgan Kaufmann, San Francisco (2005)Google Scholar
- 17.Wilson, J.C.: Symbolic Simulation Using Automatic Abstraction of Internal Node Values. PhD thesis, Stanford University, Dept. of Electrical Engineering (2001)Google Scholar