Abstract
Conjunction scheduling in image computation consists of clustering the parts of a transition relation and ordering the clusters, so that the size of the BDDs for the intermediate results of image computation stay small. We present an approach based on the analysis and permutation of the dependence matrix of the transition relation. Our algorithm computes a bordered-block lower triangular form of the matrix that heuristically minimizes the active lifetime of variables, that is, the number of conjunctions in which the variables participate. The ordering procedure guides a clustering algorithm based on the affinity of the transition relation parts. The ordering procedure is then applied again to define the cluster conjunction schedule.Our experimental results show the effectiveness of the new algorithm.
This work was supported in part by SRC contract 98-DJ-620 and NSF grant CCR-99-71195.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. K. Brayton et al. VIS: A system for verification and synthesis. In T. Henzinger and R. Alur, editors, Eighth Conference on Computer Aided Verification (CAV’96), pages 428–432. Springer-Verlag, Rutgers University, 1996. LNCS 1102.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In Proceedings of the Design Automation Conference, pages 403–407, San Francisco, CA, June 1991.
H. Cho, G. D. Hachtel, S.-W. Jeong, B. Plessier, E. Schwarz, and F. Somenzi. ATPG aspects of FSM verification. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 134–137,November 1990.
O. Coudert, C. Berthet, and J. C. Madre. Verification of sequential machines using boolean functional vectors. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied FormalMethods for Correct VLSI Design, pages 111–128, Leuven, Belgium, November 1989.
A. L. Dulmadge and N. S. Mendelsohn. Two algorithms for bipartite graphs. J. Soc. Indust. Appl. Math., 11:183–193,March 1963.
D. Geist and I. Beer. Efficient model checking by automated ordering of transition relation partitions. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV’94), pages 299–310, Berlin, 1994. Springer-Verlag. LNCS 818.
E. Hellerman and D. C. Rarick. The partitioned preassigned pivot procedure (P4). In D. J. Rose and R. A. Willoughby, editors, SparseMatrices and Their Applications, pages 67–76. Plenum Press, New York, 1972.
R. Hojati, S. C. Krishnan, and R. K. Brayton. Early quantification and partitioned transition relations. In Proceedings of the International Conference on Computer Design, pages 12–19, Austin, TX, October 1996.
S.-W. Jeong, B. Plessier, G. D. Hachtel, and F. Somenzi. Variable ordering and selection for FSM traversal. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 476–479, Santa Clara, CA, November 1991.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994.
I.-H. Moon. Efficient Reachability Algorithms in Symbolic Model Checking. PhD thesis, University of Colorado at Boulder, Department of Electrical and Computer Engineering, July 2000.
I.-H. Moon, J. H. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the Design Automation Conference, pages 23–28, Los Angeles, CA, June 2000.
R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. Presented at IWLS95, Lake Tahoe, CA., May 1995.
H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit enumeration of finite state machines using BDD’s. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 130–133,November 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-VerlagBerlin Heidelberg
About this paper
Cite this paper
Moon, IH., Hachtel, G.D., Somenzi, F. (2000). Border-Block Triangular Form and Conjunction Schedule in Image Computation. In: Hunt, W.A., Johnson, S.D. (eds) Formal Methods in Computer-Aided Design. FMCAD 2000. Lecture Notes in Computer Science, vol 1954. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40922-X_6
Download citation
DOI: https://doi.org/10.1007/3-540-40922-X_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41219-9
Online ISBN: 978-3-540-40922-9
eBook Packages: Springer Book Archive