Article

Speeding Up Image Computation by Using RTL Information

Authors:

Christoph Meinel,

Christian StangierAuthors Info & Claims

FMCAD '00: Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design

Pages 443 - 454

Published: 01 November 2000 Publication History

Abstract

Image computation is the core operation for optimization and formal verification of sequential systems like controllers or protocols. State exploration techniques based on OBDDs use a partitioned representation of the transition relation to keep the OBDD-sizes manageable. 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.

References

[1]

A. Aziz et. al., Texas-97 benchmarks , http://www-cad.EECS.Berkeley.EDU/Respep/Research/Vis/texas-97.

Google Scholar

[2]

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation , IEEE Transactions on Computers, C-35, 1986, pp. 677-691.

Google Scholar

[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: 10 ²⁰ 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.

Crossref

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.

Crossref

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 & 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/.

Google Scholar

[11]

D.E. Thomas and P. Moorby, The Verilog Hardware Description Language , Kluwer, 1991.

Crossref

Google Scholar

Cited By

View all

Ward DSomenzi FHassoun S(2006)Decomposing image computation for symbolic reachability analysis using control flow informationProceedings of the 2006 IEEE/ACM international conference on Computer-aided design10.1145/1233501.1233662(779-785)Online publication date: 5-Nov-2006
https://dl.acm.org/doi/10.1145/1233501.1233662
Meinel CStangier CGoto S(2001)A new partitioning scheme for improvement of image computationProceedings of the 2001 Asia and South Pacific Design Automation Conference10.1145/370155.370289(97-102)Online publication date: 30-Jan-2001
https://dl.acm.org/doi/10.1145/370155.370289

Recommendations

Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs
DATE '07: Proceedings of the conference on Design, automation and test in Europe

Automated abstraction is the enabling technique for model checking large circuits. Predicate Abstraction is one of the most promising abstraction techniques. It relies on the efficient computation of predicate images and the right choice of predicates. ...
Speeding up Mutual Information Computation Using NVIDIA CUDA Hardware
DICTA '07: Proceedings of the 9th Biennial Conference of the Australian Pattern Recognition Society on Digital Image Computing Techniques and Applications

We present an efficient method for mutual information (MI) computation between images (2D or 3D) for NVIDIA's `compute unified device architecture' (CUDA) compatible devices. Efficient parallelization of MI is particularly challenging on a `graphics ...
Verification of Transaction-Level SystemC models using RTL Testbenches
MEMOCODE '03: Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-Design

System architects working on SoC design havetraditionally been hampered by the lack of a coherentemethodology for architecture evaluation and coverificationof hardware and software. SystemC 2.0facilitates the development of Transaction-Level Models(TLMs)...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

FMCAD '00: Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design

November 2000

537 pages

ISBN:3540412190

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 November 2000

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 25 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ward DSomenzi FHassoun S(2006)Decomposing image computation for symbolic reachability analysis using control flow informationProceedings of the 2006 IEEE/ACM international conference on Computer-aided design10.1145/1233501.1233662(779-785)Online publication date: 5-Nov-2006
https://dl.acm.org/doi/10.1145/1233501.1233662
Meinel CStangier CGoto S(2001)A new partitioning scheme for improvement of image computationProceedings of the 2001 Asia and South Pacific Design Automation Conference10.1145/370155.370289(97-102)Online publication date: 30-Jan-2001
https://dl.acm.org/doi/10.1145/370155.370289

Abstract

References

Cited By

Recommendations

Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs

Speeding up Mutual Information Computation Using NVIDIA CUDA Hardware

Verification of Transaction-Level SystemC models using RTL Testbenches

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Share

Share this Publication link

Share on social media

Affiliations