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.
