PathFinder: A tool for design exploration. (English) Zbl 1010.68769

Brinksma, Ed (ed.) et al., Computer aided verification. 14th international conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2404, 510-514 (2002).
Summary: 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. PathFinder provides a means for the designer to explore, debug and gain insight into the behaviors of the design at a very early stage of the implementation – as soon as their HDL code is written. In the usage paradigm enabled by PathFinder, which we call Design Exploration, the design engineer specifies a behavior of interest; and the tool then finds and demonstrates – graphically – a set of execution traces compliant with the specified behavior, if any exist. When presented with each such execution sequence, the designer is essentially furnished with an insight into the design behavior, and specifically with an example of a concrete scenario in which the behavior of interest occurs. This scenario can then be closely inspected, refined, or abandoned in favor of another scenario.
For the entire collection see [Zbl 0993.00049].


68U99 Computing methodologies and applications
68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)


Zbl 0993.00049


Full Text: Link