Efficient Automatic STE Refinement Using Responsibility

  • Hana Chockler
  • Orna Grumberg
  • Avi Yadgar
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


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. 1.
    Adams, S., Bjork, M., Melham, T., Seger, C.: Automatic Abstraction in Symbolic Trajectory Evaluation. In: FMCAD 2007 (2007)Google Scholar
  2. 2.
    Chen, Y., He, Y., Xie, F., Yang, J.: Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation. In: FMCAD 2007 (2007)Google Scholar
  3. 3.
    Chockler, H., Halpern, J.Y., Kupferman, O.: What causes a system to satisfy a specification? In: ACM TOCL (to appear)Google Scholar
  4. 4.
    Chockler, H., Halpern, J.Y.: Responsibility and blame: a structural-model approach. Journal of Artificial Intelligence Research (JAIR) 22, 93–115 (2004)zbMATHMathSciNetGoogle Scholar
  5. 5.
    Chou, C.-T.: The mathematical foundation of symbolic trajectory evaluation. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 196–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  6. 6.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    Grumberg, O., Schuster, A., Yadgar, A.: 3-Valued Circuit SAT for STE with Automatic Refinement. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 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. 9.
    Hume, D.: A treatise of human nature. John Noon, London (1739)Google Scholar
  10. 10.
    Kurshan, R.P.: Computer-Aided Verification of coordinating processes - the automata theoretic approach (1994)Google Scholar
  11. 11.
    Pandey, M., Raimi, R., Bryant, R.E., Abadir, M.S.: Formal verification of content addressable memories using symbolic trajectory evaluation. DAC 00, 167 (1997)CrossRefGoogle Scholar
  12. 12.
    Roorda, J.-W., Claessen, K.: Sat-based assistance in abstraction refinement for symbolic trajectory evaluation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 175–189. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 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. 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
  15. 15.
    Tzoref, R., Grumberg, O.: Automatic refinement and vacuity detection for symbolic trajectory evaluation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 190–204. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  16. 16.
    Wile, B., Roesner, W., Goss, J.: Comprehensive Functional Verification: The Complete Industry Cycle. Morgan Kaufmann, San Francisco (2005)Google Scholar
  17. 17.
    Wilson, J.C.: Symbolic Simulation Using Automatic Abstraction of Internal Node Values. PhD thesis, Stanford University, Dept. of Electrical Engineering (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Hana Chockler
    • 1
  • Orna Grumberg
    • 2
  • Avi Yadgar
    • 2
  1. 1.IBM ResearchHaifaIsrael
  2. 2.Computer Science Department, Technion HaifaIsrael

Personalised recommendations