Dynamic Scheduling and Clustering in Symbolic Image Computation

The core computation in BDD-based symbolic synthesis and verification is forming the image and pre-image of sets of states under the transition relation characterizing the sequential behavior of the design. Computing an image or a pre-image consists of ordering the latch transition relations, clustering them and eventually re-ordering the clusters. Existing algorithms are mainly limited by memory resources. To make them as efficient as possible, we address a set of heuristics with the main target of minimizing the memory used during image computation. They include a dynamic heuristic to order the latch relations, a dynamic framework to cluster them, and the application of conjunctive partitioning during image computation. We provide and integrate a set of algorithms and we report references and comparisons with recent work. Experimental results are given to demonstrate the efficiency and robustness of the approach.

• Type: Conference
• Year: 2002
• Where: DATE
• Authors: Gianpiero Cabodi, Paolo Camurati, Stefano Quer
• Keywords: DATE 2002, Hardware, Image Computation, Latch Transition Relations, Transition Relations