Identification of Effective Guidance Hints for Better Design Debugging by Formal Methods

Achieving complete design verification by formal methods remains a daunting goal to date. With advancements in model checkers and other formal techniques, large designs can be verified in a partial or semi-formal manner. However, it is well known that exhaustive exploration of design state space is still prohibitive. In this paper, we revisit the concept of guided state space exploration which holds the promise of complete formal verification. Since it is not trivial to devise guidance strategies in an automatic manner, identification of the guidance hints becomes very crucial for a directed traversal of the state space. This directed traversal can ultimately reduce the time spent in formal verification and also assist in better design debugging. We propose a methodology for identification of such guideposts and utilize them for debugging purpose. Our goal is to achieve faster counter-example generation by the usage of guideposts. Experiments on a complex design show that guidance hints identified with the proposed methodology provide significant gains during model checking for different error traces.