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.