the compositional far side of image computation
Symbolic image computation is the most fundamental computationin BDD-based sequential system optimization and formal verification.In this paper, we explore the use of over-approximationand BDD minimization with dont cares during image computation.Our new method, based on the partitioned representation ofthe transition relation, consists of three phases: First, the model istreated as a set of loosely coupled components, and over-approximateimages are computed to minimize the transition relation ofeach component. A refined overall image is then computed usingthe simplified transition relation. Finally, the exact image isobtained by a clipping operation that recovers all previous over-approximations.Since BDD minimization employs constraints on thenext-state variables of the transition relation, instead of the customaryconstraints on the present-state variables, we call the resultingmethod far side image computation.The new method can be implemented on top of any image computationalgorithm that is based on the partitioned transition relation.(For example, IWLS95, MLP, and Fine-Grain.)We demonstrate the effectiveness of our approach by experimentson models ranging from easy to hard: The new method wins significantlyover the best known algorithms so far in both CPU timeand memory usage, especially on the hard models.
image computation symbolic binary decision diagrams model checking