PathFinder: A tool for design exploration. 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.

References in zbMATH (referenced in 1 article , 1 standard article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Ben-David, Shoham; Gringauze, Anna; Sterin, Baruch; Wolfsthal, Yaron: PathFinder: A tool for design exploration (2002)