Verifying a gigabit ethernet switch using SMV
Verifying a gigabit ethernet switch using SMV
复制标题
使用 SMV 验证千兆位以太网交换机
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Mike Jorda
中科院分区：
文献类型：
--
作者：
Yuan Lu;Mike Jorda
我们使用模型检查技术对新型千兆以太网交换机BCM5690中的交换块进行了验证。由于其动态特性，该区块传统上难以验证。对于这种特殊的设计，形式化的技术要比模拟有效得多。在发现的26个设计错误中，有22个是使用形式化方法发现的。然后，我们改进了模型检查能力来分析交换机延迟。我们还在模型检查器中使用了感应来避免状态爆炸。
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.