Verifying a gigabit ethernet switch using SMV

ABSTRACT

We use model checking techniques to verify a switching block in a new Gigabit Ethernet switch - BCM5690. Due to its dynamic nature, this block has been traditionally difficult to verify. Formal techniques are far more efficient than simulation for this particular design. Among 26 design errors discovered, 22 are found using formal methods. We then improve our model checking capability to analyze switch latency. We also use induction to avoid state explosion in the model checker.

REFERENCES

• 1: Mark D. Aagaard , Robert B. Jones , Roope Kaivola , Katherine R. Kohatsu , Carl-Johan H. Seger, Formal verification of iterative algorithms in microprocessors, Proceedings of the 37th conference on Design automation, p.201-206, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337388]
• 2: Bob Bentley, Validating the intel pentium 4 microprocessor, Proceedings of the 38th conference on Design automation, p.244-248, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378473]
• 3: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 4: Cadence Berkeley Lab. Cadence SMV. http://www-cad.eecs.berkeley.edu/kenmcmil/smv, 1998.
• 5: P. Chauhan, E. M. Clarke, Y. Lu, and D. Wang. Verifying IP-core based system-on-chip designs. In IEEE ASIC Conference, 1999.
• 6: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 7: Jayant Kadambi , Ian Crayford , Mohan Kalkunte, Gigabit ethernet: migrating to high-bandwidth LANs, Prentice-Hall, Inc., Upper Saddle River, NJ, 1998
• 8: Kenneth L. McMillan, Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.110-121, June 28-July 02, 1998
• 9: Open Source Software Project. Embedded Perl Language. In http://www.ossp.org/pkg/tool/eperl, 1998.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids

General Terms:
Verification

Keywords:
Verification