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

  • Y. Xu
  • E. Cerny
  • A. Silburt
  • A. Coady
  • Y. Liu
  • P. Pownall
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


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.


Model Checker Clock Cycle Model Reduction Formal Verification Design Error 
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.


  1. 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. 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. 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 1998Google Scholar
  4. 4.
    FormalCheck User’s Guide. Bell labs Design Automation, Lucent Technologies, V1.1, 1997Google Scholar
  5. 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. 6.
    0-In Design Automation, Inc., “Whitebox verification”,
  7. 7.
    0-In Design Automation, Inc., “0-In search,”
  8. 8.
    System Science, Inc. (Synopsys, Inc.), “The VERA verification system,” http://
  9. 9.
    TransEDA, Inc., “VeriSure-Verilog code coverage tool,” 121 Practical Application of Formal Verification Techniques
  10. 10.
    Lucent Technologies, “FormalCheck model checker,”
  11. 11.
    P. Bratley, B.L. Fox, L.E. Schrage, A Guide to Simulation, 2nd Edition, Springer-Verlag, New York, 1986.Google Scholar
  12. 12.
    L. Devroye, Non-Uniform Random Variate Generation, Springer-Verlag, New York, 1986.zbMATHGoogle Scholar
  13. 13.
    CheckOff User Guide, Siemens Nixdorf Informations Systemen AG & Abstract Hardware Limited, January, 1996.Google Scholar
  14. 14.
    Lambda user’s manual, Abstract Hardware limited, 1995.Google Scholar
  15. 15.
    Verisity Design, Inc. Specman Data Sheet,

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Y. Xu
    • 1
  • E. Cerny
    • 2
  • A. Silburt
    • 1
  • A. Coady
    • 1
  • Y. Liu
    • 1
  • P. Pownall
    • 1
  1. 1.Nortel SemiconductorsOntarioCanada
  2. 2.Dépt.IROUniversité de MontréalQuébecMontréAlCanada

Personalised recommendations