Verifying a gigabit ethernet switch using SMV
Yuan Lu, Mike Jorda · 2004
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.