Multiway Decision Graphs for Automated Hardware Verification | Formal Methods in System Design Skip to main content
Springer Nature Link
Log in

Multiway Decision Graphs for Automated Hardware Verification

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Traditional ROBDD-based methods of automated verification suffer from the drawback that they require a binary representation of the circuit. To overcome this limitation we propose a broader class of decision graphs, called Multiway Decision Graphs (MDGs), of which ROBDDs are a special case. With MDGs, a data value is represented by a single variable of abstract type, rather than by 32 or 64 boolean variables, and a data operation is represented by an uninterpreted function symbol. MDGs are thus much more compact than ROBDDs, and this greatly increases the range of circuits that can be verified. We give algorithms for MDG manipulation, and for implicit state enumeration using MDGs. We have implemented an MDG package and provide experimental results.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. F. Van Aelten, S.Y. Liao, J. Allen, and S. Devadas, "Automatic generation and verification of sufficient correctness properties for synchronous processors," in International Conference on Computer-Aided Design, 1992.

  2. S. Bose and A.L. Fisher, "Automatic verification of synchronous circuits using symbolic logic simulation and temporal logic," in Proceedings of the IMEC-IFIP Workshop on Applied Formal Methods for Correct VLSI Design, 1989.

  3. R.E. Bryant, "Graph-based algorithms for boolean function manipulation," IEEE Transactions on Computers, Vol. 35, No. 8, pp. 677–691, Aug. 1986.

    Google Scholar 

  4. R.E. Bryant, D.L. Beatty, and C.-J.H. Seger, "Formal hardware verification by symbolic ternary trajectory evaluation," in 28th ACM/IEEE Design Automation Conference, 1991.

  5. J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill, "Symbolic model checking for sequential circuit verification," IEEE Transactions on Computer-Aided Design, Vol. 13, No. 4, pp. 401–424, April 1994.

    Google Scholar 

  6. J.R. Burch and D.L. Dill, "Automatic verification of pipelined microprocessor control," in Proc. Work. on Computer-Aided Verification, 1994.

  7. A.J. Camilleri, M.J.C. Gordon, and T.F. Melham, "Hardware verification using higher-order logic," in D. Borrione (Ed.), Proceedings of the IFIP WG 10.2 Working Conference: From H.D.L. Descriptions to Guaranteed Correct Circuit Designs, Grenoble, Sept. 1986, North-Holland, 1987.

  8. H. Cho, G. Hachtel, S.-W. Jeong, B. Plessier, E. Schwarz, and F. Somenzi, "ATPG aspects of FSM verification," in International Conference on Computer-Aided Design, 1990.

  9. L. Claesen, F. Proesmans, E. Verlind, and H. De Man, "SFG-Tracing: A methodology for the automatic verification of MOS transistor level implementations from high level behavioral specifications," in P.A. Subrahmanyam(Ed.), International Workshop on Formal Methods in VLSI Design, Miami, Florida, Jan. 1991.

  10. E.M. Clarke, O. Grumberg, and D.E. Long, "Model checking and abstraction," in Proc. 19th ACM Symp. on Principles of Programming Languages, Jan. 1992.

  11. F. Corella, "What holds in a context," Journal of Automated Reasoning, Vol. 10, pp. 79–93, 1993.

    Google Scholar 

  12. F. Corella, "Automated high-level verification against clocked algorithmic specifications," in Proceedings of CHDL 93, April 1993.

  13. F. Corella, "Automated verification of behavioral equivalence for microprocessors," IEEE Transactions on Computers, Vol. 43, No. 1, pp. 115–117, Jan. 1994.

    Google Scholar 

  14. F. Corella, Z. Zhou, X. Song, M. Langevin, and E. Cerny, "Appendix B: Details of the MDG algorithms," Available electronically from the University of Montreal, see http://www.iro.umontreal.ca/labs/lasso/research/ mdgverif/mdgverif eng.html.

  15. O. Coudert, C. Berthet, and J.C. Madre, "Verification of sequential machines using boolean functional vectors," in L. Claesen (Ed.), Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, North-Holland, Nov. 1989, pp. 111–128.

    Google Scholar 

  16. O. Coudert and J.C. Madre, "A unified framework for the formal verification of sequential circuits," in International Conference on Computer-Aided Design, 1990.

  17. D. Cyrluk, S. Rajan, N. Shankar, and M.K. Srivar, "Effective theorem proving for hardware verification," in Second International Conference on Theorem Provers in Circuit Design, 1994.

  18. M. Fujita, "RTL design verification by making use of datapath information," in IEEE International Conference on Computer Design, 1992.

  19. D. Geist and I. Beer, "Efficient Model Checking by Automated Ordering of Transition Relation Partitions," in Proc. Work. on Computer-Aided Verification, 1994.

  20. A.J. Hu and D.L. Dill, "Reducing BDD size by exploiting functional dependencies," in 30th ACM/IEEE Design Automation Conference, 1993, pp. 266–271.

  21. W.A. Hunt, "FM8501: A verified microprocessor," Ph.D. Thesis, University of Texas, Austin, 1985.

    Google Scholar 

  22. J. Joyce, G. Birtwistle, and M. Gordon, "Proving a computer correct in higher order logic, Technical Report 100," University of Cambridge, Computer Laboratory, Dec. 1986.

  23. J.J. Joyce, "Multi-level verification of microprocessor-based systems," Ph.D. Thesis, Technical Report 195, University of Cambridge, Computer Laboratory, May 1990.

  24. R.P. Kurshan, "Analysis of discrete event coordination," in J.W. de Bakker, W.-P. de Roewer, and G. Rozenberg (Eds.), Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems. Springer-Verlag, 1989, Vol. LNCS 430.

  25. M. Langevin and E. Cerny, "Verification of processor-like circuits," in P. Prinetto and E. Camurati (Eds.s), Proc. Work. on Correct Hardware Design Methodologies. North-Holland, June 1991.

  26. M. Langevin and E. Cerny, "Comparing generic state machines," in K.G. Larsen and A. Skou (Eds.), Proc. Work. on Computer-Aided Verification. Springer-Verlag, July 1991, Vol. LNCS 575.

  27. M. Langevin and E. Cerny, "An extended OBDD representation for extended FSMs," in Proc. of EDAC-ETCEUROASIC, 1994.

  28. D.E. Long, Model Checking, Abstraction, and Compositional Verification, Ph.D. Thesis, Carnegie Mellon University, 1993.

  29. M. Payer, T. Filkorn, and P. Warkentin, "Symbolic verification of sequential circuits synthesized with CALLAS," in International Workshop on High-Level Synthesis, Laguna Nigel, California, 1992.

  30. A. Srinivasan, T. Kam, S. Malik, and R.K. Brayton, "Algorithms for discrete function manipulation," in ACM/IEEE 27th Design Automation Conference, 1990.

  31. André Stauffer, Systemes numériques câblés et microprogrammés, Presses Polytechniques Romandes, 1989.

  32. K.J. Supowit and S.J. Friedman, "A new method for verifying sequential circuits," in 23rd Design Automation Conference, 1986, pp. 200–205.

  33. H.J. Touati, H. Savoj, B. Lin, R.K. Brayton, and A. Sangiovanni-Vincentelli, "Implicit state enumeration of finite state machines using BDDs," in International Conference on Computer-Aided Design, 1990.

  34. P. Wolper, "Expressing interesting properties of programs in propositional temporal logic," in Proceedings of the 13th ACM Symposium on Principles of Programming Languages, Jan. 1986.

  35. Z. Zhou, X. Song, F. Corella, E. Cerny, and M. Langevin, "Partitioning transition relations efficiently and automatically," in Proceedings of the Fifth Great Lakes Symposium on VLSI, 1995.

  36. Z. Zhou, X. Song, F. Corella, E. Cerny, and M. Langevin, "Description and verification of RTL designs using multiway decision graphs," in Proceedings of the Conference on Hardware Description Languages, 1995.

Download references

Author information

Authors and Affiliations

  1. Hewlett-Packard Company, Canada

    F. Corella

  2. Nortel Technology, Canada

    Z. Zhou & M. Langevin

  3. Dép. d’I. R.O., Univ.de Montréal, Canada

    X. Song & E. Cerny

Authors
  1. F. Corella
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Z. Zhou
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. X. Song
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. M. Langevin
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. E. Cerny
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Corella, F., Zhou, Z., Song, X. et al. Multiway Decision Graphs for Automated Hardware Verification. Formal Methods in System Design 10, 7–46 (1997). https://doi.org/10.1023/A:1008663530211

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1008663530211

Search

Navigation