Sciweavers

Share
GLVLSI
2000
IEEE

Speeding up symbolic model checking by accelerating dynamic variable reordering

8 years 10 months ago
Speeding up symbolic model checking by accelerating dynamic variable reordering
Symbolic Model checking is a widely used technique in sequential verification. As the size of the OBDDs and also the computation time depends on the order of the input variables, the verification may only succeed if a well suited variable order is chosen. Since the characteristics of the represented functions are changing, the variable order has to be adapted dynamically. Unfortunately, dynamic reordering strategies are often very time consuming and sometimes do not provide any improvement of the OBDD representation. This paper presents adaptions of reordering techniques originally intended for combinatorial verification to the specific requirements of symbolic model checking. The techniques are orthogonal in the way that they use either structural information about the OBDDs or semantical information about the represented functions. The application of these techniques substantially accelerates the reordering process and makes it possible to finish computations, that are too time...
Christoph Meinel, Christian Stangier
Added 31 Jul 2010
Updated 31 Jul 2010
Type Conference
Year 2000
Where GLVLSI
Authors Christoph Meinel, Christian Stangier
Comments (0)
books