Speeding Up Image Computation by Using RTL Information

  • Christoph Meinel
  • Christian Stangier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)


Image computation is the core operation for optimization and formal verification of sequential systems like controllers or proto- cols. State exploration techniques based on OBDDs use a partitioned representation of the transition relation to keep the OBDD-sizes man- ageable. This paper presents a new approach that significantly increases the quality of the partitioning of the transition relation of controllers given in the hardware description language Verilog. The heuristic has been successfully applied to reachability analysis and symbolic model checking of real life designs, resulting in a significant reduction both in CPU time and memory consumption.


Model Check Transition Relation Memory Consumption Reachable State Reachability Analysis 
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.
  2. 2.
    R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, C-35, 1986, pp. 677–691.CrossRefGoogle Scholar
  3. 3.
    J. R. Burch, E. M. Clarke, D. E. Long, Symbolic Model Checking with partitioned transition relations, Proc. of Int. Conf. on VLSI, 1991.Google Scholar
  4. 4.
    J. R. Burch, E. M. Clarke, D. L. Dill, L. J. Hwang and K. L. McMillan, Symbolic model checking: 1020 states and beyond, Proc. of LICS, 1990, pp. 428–439.Google Scholar
  5. 5.
    R. K. Brayton, G. D. Hachtel, A. L. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. A. Edwards, S. P. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, T. Villa, VIS: A System for Verification and Synthesis, Proc. of Computer Aided Verification CAV’96, 1996, pp. 428–432.Google Scholar
  6. 6.
    O. Coudert, C. Berthet and J. C. Madre, Verification of Synchronous Machines using Symbolic Execution, Proc. of Workshop on Automatic Verification Methods for Finite State Machines, LNCS 407, Springer, 1989, pp. 365–373.Google Scholar
  7. 7.
    D. Geist and I. Beer, Efficient Model Checking by Automated Ordering of Transition Relation Partitions, Proc. of Computer Aided Verification CAV’94, 1994, pp. 294–310.Google Scholar
  8. 8.
    R. D. M. Hunter and T. T. Johnson, Introduction to VHDL, Chapman &amt; Hall, 1996.Google Scholar
  9. 9.
    R. K. Ranjan, A. Aziz, R. K. Brayton, C. Pixley and B. Plessier, Efficient BDD Algorithms for Synthesizing and Verifying Finite State Machines, Proc.of Int.Workshop on Logic Synthesis (IWLS’95), 1995.Google Scholar
  10. 10.
    F. Somenzi, CUDD: CU Decision Diagram Package,
  11. 11.
    D.E. Thomas and P. Moorby, The Verilog Hardware Description Language,Kluwer, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Christoph Meinel
    • 1
  • Christian Stangier
    • 1
  1. 1.FB InformatikUniversity of TrierUSA

Personalised recommendations