manolios@cc.gatech.edu
College of Computing
While most of the effort in improving verification times for
pipeline machine verification has focused on faster decision
procedures, we show that the refinement maps used also have a
drastic impact on verification times. We introduce a new
class of refinement maps for pipelined machine verification, and
using the state-of-the-art verification tools UCLID and Siege
we show that one can attain several orders of magnitude
improvements in verification times over the standard
flushing-based refinement maps, even enabling the verification of
machines that are too complex to otherwise automatically verify.
PDF (74K) © ACM
|
Last modified: Sun Feb 27 15:23:32 EST 2005
manolios@cc.gatech.edu |
College of Computing |