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 [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 language | English (US) |
|---|---|
| Pages (from-to) | 74-77 |
| Number of pages | 4 |
| Journal | Proceedings of the International Workshop on Rapid System Prototyping |
| State | Published - 2004 |
| Event | Proceedings - 15th IEEE International Workshop on Rapid Systems Prototyping - Geneva, Switzerland Duration: Jun 28 2004 → Jun 30 2004 |