Speeding Up Image Computation by using RTL Information

Christoph Meinel and Christian Stangier

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


Image computation is the core operation for optimization and formal verification of sequential systems like controllers or protocols. State exploration techniques based on OBDDs use a partitioned representation of the transition relation to keep the OBDD-sizes manageable. This paper presents a new approach that significantly increases the quality of the partitioning of the transition relation of controllers given in the hardware description language Verilog. The heuristic has been successfully applied to reachability analysis and symbolic model checking of real life designs, resulting in a significant reduction both in CPU time and memory consumption.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:37
Maintainer sjohnson@cs.indiana.edu.
Start Conference Manager
Conference Systems