A New SAT-Based Algorithm for Symbolic Trajectory Evaluation

  • Jan-Willem Roorda
  • Koen Claessen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


We present a new SAT-based algorithm for Symbolic Trajectory Evaluation (STE), and compare it to more established SAT-based techniques for STE.


  1. 1.
    Aagaard, M., Jones, R.B., Melham, T.F., O’Leary, J.W., Seger, C.-J.H.: A methodology for large-scale hardware verification. In: Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design (2000)Google Scholar
  2. 2.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an Alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 454. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
  5. 5.
    Pandey, M., Raimi, R., Bryant, R.E., Abadir, M.S.: Formal verification of content addressable memories using symbolic trajectory evaluation. In: 34th Design Automation Conference (DAC 1997), pp. 167–172. Association for Computing Machinery (1997)Google Scholar
  6. 6.
    Schubert, T.: High level formal verification of next-generation microprocessors. In: Proceedings of the 40th conference on Design automation, pp. 1–6. ACM Press, New York (2003)Google Scholar
  7. 7.
    Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design: An International Journal 6(2), 147–189 (1995)CrossRefGoogle Scholar
  8. 8.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. 9.
    Yang, J., Gil, R., Singerman, E.: SatGSTE: Combining the abstraction of GSTE with the capacity of a SAT solver. In: Designing Correct Circuits (DCC 2004) (2004)Google Scholar
  10. 10.
    Yang, J., Seger, C.-J.H.: Introduction to generalized symbolic trajectory evaluation. In: IEEE International Conference on Computer Design: VLSI in Computers & Processors (ICCD 2001), Washington - Brussels - Tokyo, September 2001, pp. 360–367. IEEE, Los Alamitos (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Jan-Willem Roorda
    • 1
  • Koen Claessen
    • 1
  1. 1.Chalmers University of TechnologySweden

Personalised recommendations