The Compositional Far Side of Image Computation

Symbolic image computation is the most fundamental computation in BDD-based sequential system optimization and formal verification. In this paper, we explore the use of over-approximation and BDD minimization with don’t cares during image computation. Our new method, based on the partitioned representation of the transition relation, consists of three phases: First, the model is treated as a set of loosely coupled components, and over-approximate images are computed to minimize the transition relation of each component. A refined overall image is then computed using the simplified transition relation. Finally, the exact image is obtained by a clipping operation that recovers all previous over-approximations. Since BDD minimization employs constraints on the next-state variables of the transition relation, instead of the customary constraints on the present-state variables, we call the resulting method far side image computation. The new method can be implemented on top of any ima...

• Type: Conference
• Year: 2003
• Where: ICCAD
• Authors: Chao Wang, Gary D. Hachtel, Fabio Somenzi
• Keywords: Hardware, ICCAD 2003, Image Computation, Simplified Transition Relation, Transition Relation