학술논문
State pruning for test vector generation for a multiprocessor cache coherence protocol
Document Type
Conference
Author
Source
Proceedings. 15th IEEE International Workshop on Rapid System Prototyping, 2004. Rapid systems prototyping Rapid System Prototyping, 2004. Proceedings. 15th IEEE International Workshop on. :74-77 2004
Subject
Language
ISSN
1074-6005
Abstract
Verification is extremely important in designing digital systems such as a cache coherence protocol. Generating traces for system verification using a model checker and then using the traces to drive the RTL logic design simulation is an efficient method for debugging. This method has been called the witness string method (Abts and Roberts, 1999), which is based on DFS. We investigate a state pruning method that exploits multiple search heuristics in simultaneous DFS searches to choose the most efficient traces. We distribute the hash table of the entire state space among the simultaneous searches so that they cooperate to avoid redundant state exploration. To evaluate this search algorithm, we implant several protocol bugs in the Stanford DASH cache coherence protocol. Using an IBM Power4 system with the Berkeley Active Message library, we show an improvement in witness strings generation through the state pruning method over a pure DFS and a guided DFS.