manolios@cc.gatech.edu
College of Computing
We introduce collapsed flushing, a new flushing-based refinement
map for automatically verifying safety and liveness properties of
term-level pipelined machine models. We also present a new
method for handling liveness that is both simpler to define and
easier to verify than previous approaches. To empirically
validate collapsed flushing, we ran extensive experiments which
show more than an order-of-magnitude improvement in verification
times over standard flushing. Furthermore, by combining
collapsed flushing with commitment refinement maps, we can
monolithically verify complex pipelined machine models with deep
pipelines---a salient feature of state-of-the-art microprocessor
designs---that previous approaches cannot handle.
PDF (72K) © ACM
|
Last modified: Wed Jan 11 19:49:35 EST 2006
manolios@cc.gatech.edu |
College of Computing |