Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors

  • Conference paper
  • First Online:

Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 1703))

Abstract

We describe the application of model checking using FormalCheck to an industrial RTL design. It was used as a complement to classical simulation on portions of the chip that involved complex interactions and were difficult to verify by simulation. We also identify certain circuit structures that for a certain type of queries lend themselves to manual model reductions which were not detected by the automatic reduction algorithm. These reductions were instrumental in allowing us to complete the formal verification of the design and to detect two design errors that would have been hard to detect by simulation. We also provide a technique to estimate the length of a random simulation needed to detect a particular design error with a given probability; this length can be used as a measure of its difficulty.

Similar content being viewed by others

Keywords

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.

References

  1. A. Silburt Invited Lecture: ASIC/System Hardware Verification at Nortel: A View from the Trenches.Proceeding of the 9th IFIP WG10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’97), October, 1997, Montreal Canada.

    Google Scholar 

  2. A.J. Camilleri. A role for Theorem Proving in Multi-processor Design.Proceeding of the 10th International Conference on Computer Aided Verification (CAV’98),Vancouver, BC Canada, June/July 1998.

    Google Scholar 

  3. D.L. Dill. What’s Between Simulation and Formal Verification.Proceeding of the 35th Design Automation Conference (DAC’98), San Francisco, CA, USA, June 1998

    Google Scholar 

  4. FormalCheck User’s Guide. Bell labs Design Automation, Lucent Technologies, V1.1, 1997

    Google Scholar 

    Google Scholar 

  5. K. L. McMillan.Symbolic model checking-an approach to the state explosion problem. Ph.D. thesis, SCS, Carnegie Mellon University, 1992. (See also Cadence Design Systems, Inc. www pages.)

    Google Scholar 

  6. 0-In Design Automation, Inc., “Whitebox verification”,http://www.0-in.com/tools.

  7. 0-In Design Automation, Inc., “0-In search,”http://www.0-in.com/tools.

  8. System Science, Inc. (Synopsys, Inc.), “The VERA verification system,”http:// www.systems.com/products/vera.

  9. TransEDA, Inc., “VeriSure-Verilog code coverage tool,”http://www.transeda.com/products. 121 Practical Application of Formal Verification Techniques

  10. Lucent Technologies, “FormalCheck model checker,”http://www.bell-labs.com/org/blda/product.formal.html.

  11. P. Bratley, B.L. Fox, L.E. Schrage,A Guide to Simulation, 2nd Edition, Springer-Verlag, New York, 1986.

    Google Scholar 

  12. L. Devroye,Non-Uniform Random Variate Generation, Springer-Verlag, New York, 1986.

    MATH  Google Scholar 

  13. CheckOff User Guide, Siemens Nixdorf Informations Systemen AG & Abstract Hardware Limited, January, 1996.

    Google Scholar 

  14. Lambda user’s manual, Abstract Hardware limited, 1995.

    Google Scholar 

  15. Verisity Design, Inc. Specman Data Sheet,http://www.verisity.com.

Download references

Author information

Authors and Affiliations

  1. Nortel Semiconductors, Ottawa, Ontario, Canada

    Y. Xu, A. Silburt, A. Coady, Y. Liu & P. Pownall

  2. Dépt.IRO, Université de Montréal, MontréAl, Québec, Canada

    E. Cerny

Authors
  1. Y. Xu

    You can also search for this author inPubMed Google Scholar

  2. E. Cerny

    You can also search for this author inPubMed Google Scholar

  3. A. Silburt

    You can also search for this author inPubMed Google Scholar

  4. A. Coady

    You can also search for this author inPubMed Google Scholar

  5. Y. Liu

    You can also search for this author inPubMed Google Scholar

  6. P. Pownall

    You can also search for this author inPubMed Google Scholar

Editor information

Editors and Affiliations

  1. CMI/Université de Provence, 39, rue Joliot-Curie, F-13453, Marseille Cedex 13, France

    Laurence Pierre

  2. Technische Informatik, Universität Tübingen, Im Sand 13, D-72076, Tübingen, Germany

    Thomas Kropf

Rights and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Xu, Y., Cerny, E., Silburt, A., Coady, A., Liu, Y., Pownall, P. (1999). Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_10

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp