Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors
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.
KeywordsModel Checker Clock Cycle Model Reduction Formal Verification Design Error
- 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 1998Google Scholar
- 4.FormalCheck User’s Guide. Bell labs Design Automation, Lucent Technologies, V1.1, 1997Google 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
- 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.