State pruning for test vector generation for a multiprocessor cache coherence protocol

Ying Chen, Dennis Abts, David J. Lilja

Research output: Contribution to journalConference articlepeer-review

1 Scopus citations


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 [2], 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 new 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.

Original languageEnglish (US)
Pages (from-to)74-77
Number of pages4
JournalProceedings of the International Workshop on Rapid System Prototyping
StatePublished - Oct 18 2004
EventProceedings - 15th IEEE International Workshop on Rapid Systems Prototyping - Geneva, Switzerland
Duration: Jun 28 2004Jun 30 2004


Dive into the research topics of 'State pruning for test vector generation for a multiprocessor cache coherence protocol'. Together they form a unique fingerprint.

Cite this