Border-Block Triangular Form and Conjunction Schedule in Image Computation

  • In-Ho Moon
  • Gary D. Hachtel
  • Fabio Somenzi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)


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.


Image Computation Model Check Transition Relation Total Lifetime Symbolic Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    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.Google Scholar
  2. [2]
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.CrossRefGoogle Scholar
  3. [3]
    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.Google Scholar
  4. [4]
    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.Google Scholar
  5. [5]
    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.Google Scholar
  6. [6]
    A. L. Dulmadge and N. S. Mendelsohn. Two algorithms for bipartite graphs. J. Soc. Indust. Appl. Math., 11:183–193,March 1963.Google Scholar
  7. [7]
    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.Google Scholar
  8. [8]
    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.Google Scholar
  9. [9]
    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.Google Scholar
  10. [10]
    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.Google Scholar
  11. [11]
    K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994.Google Scholar
  12. [12]
    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.Google Scholar
  13. [13]
    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.Google Scholar
  14. [14]
    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.Google Scholar
  15. [15]
    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.Google Scholar

Copyright information

© Springer-VerlagBerlin Heidelberg 2000

Authors and Affiliations

  • In-Ho Moon
    • 1
  • Gary D. Hachtel
    • 1
  • Fabio Somenzi
    • 1
  1. 1.Department of Electrical and Computer EngineeringUniversity of Colorado at BoulderUSA

Personalised recommendations