Speeding Up Image Computation by Using RTL Information
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.
KeywordsModel Check Transition Relation Memory Consumption Reachable State Reachability Analysis
Unable to display preview. Download preview PDF.
- 1.A. Aziz et. al., Texas-97 benchmarks, http://www-cad.EECS.Berkeley.EDU/Respep/Research/Vis/texas-97.
- 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.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.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.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.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.R. D. M. Hunter and T. T. Johnson, Introduction to VHDL, Chapman &amt; Hall, 1996.Google Scholar
- 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.F. Somenzi, CUDD: CU Decision Diagram Package, ftp://vlsi.colorado.edu/pub/.
- 11.D.E. Thomas and P. Moorby, The Verilog Hardware Description Language,Kluwer, 1991.Google Scholar