{'fraction_non_alphanumeric': 0.010906040268456376, 'fraction_numerical': 0.0016778523489932886, 'mean_word_length': 5.2460732984293195, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
State Pruning for Generating Efficient Test Vectors

The previously proposed witness string method [2] generates traces for system verification using a model checker and then uses the traces to drive the RTL logic design simulation. This paper extends the depth first search (DFS) used in the original witness string method with a state pruning method that exploits multiple search heuristics in simultaneous searches where each DFS uses a different heuristic. The hash table of the entire state space is distributed among the simultaneous searches so that they cooperate to avoid redundant state exploration. To evaluate this new search algorithm, we implanted several protocol bugs in the Stanford DASH cache coherence protocol model. We also evaluated the Counter benchmark that models the state space of a general application. Using an IBM Power4 multiprocessor system with the Berkeley Active Message library, we show that this new method of state pruning produces quantitatively better witness strings compared to both pure and guided DFS. The state pruning method proposed in this study is motivated from the problems in digital system design and then extended to general verification.