Skip to main content

PathFinder: A Tool for Design Exploration

Part of the Lecture Notes in Computer Science book series (LNCS,volume 2404)


In this paper we present a tool called PathFinder, which exploits the power of model checking for developing and debugging newly-written hardware designs. Our tool targets the community of design engineers, who—in contrast to verification engineers—are not versed in formal verification, and therefore have traditionally been distant from the growing industry momentum in the area of model checking.


  • Model Check
  • Timing Diagram
  • Execution Trace
  • Partial Trace
  • Design Exploration

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. N. Amla, E. A. Emerson, R. P. Kurshan, and K. S. Namjoshi. Model checking synchronous timing diagrams. In Formal Methods in Computer-Aided Design, pages 283–298, 2000.

    Google Scholar 

  2. I. Beer, S. Ben-David, C. Eisner, D. Fisman, A. Gringauze, and Y. Rodeh. The temporal logic sugar. In Computer Aided Verification, Proc. 13th International Conference, volume 2102 of Lecture Notes in Computer Science, pages 363–367. Springer, 2001.

    Google Scholar 

  3. S. Ben-David, A. Gringauze, S. Keidar, B. Sterin, and Y. Wolfsthal. Design exploration through model checking. Technical Report H0097, IBM Haifa Research Laboratory, December 2001.

    Google Scholar 

  4. K. Fisler. Timing diagrams: Formalization and algorithmic verification. Journal of Logic, Language and Information, 8(3):323–361, 1999.

    MATH  CrossRef  MathSciNet  Google Scholar 

  5. R. H. Hardin, Z. Har’El, and R. P. Kurshan. COSPAN. In Computer Aided Verification, Proc. 8th International Conference, volume 1102 of Lecture Notes in Computer Science, pages 423–427. Springer, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations


Editor information

Editors and Affiliations

Rights and permissions

Reprints and Permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ben-David, S., Gringauze, A., Sterin, B., Wolfsthal, Y. (2002). PathFinder: A Tool for Design Exploration. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg.

Download citation

  • DOI:

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43997-4

  • Online ISBN: 978-3-540-45657-5

  • eBook Packages: Springer Book Archive