Formal verification of an ATM switch fabric using multiway decision graphs
Formal verification of an ATM switch fabric using multiway decision graphs
复制标题
使用多路决策图对 ATM 交换结构进行形式化验证
DOI：
10.1109/glsv.1996.497603
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
M. Langevin
中科院分区：
文献类型：
--
作者：
S. Tahar;Zijian Zhou;Xiaoyu Song;E. Cerny;M. Langevin
在本文中，我们提出了我们的结果，正式验证了异步传输模式（ATM）网络交换结构的实现使用一类新的决策图，称为多路决策图（MDG）。我们所考虑的设计在剑桥费尔希尔网络的实际应用中得到了应用。我们在不同的抽象层次上生成了硬件实现的描述。然后，我们根据门级实现的描述对抽象描述模型进行验证。使用这个抽象模型，我们完成了对反映Fairisle ATM交换机结构行为的特定属性的验证。
In this paper we present our results on formally verifying the implementation of an asynchronous transfer mode (ATM) network switching fabric using a new class of decision graphs, called Multiway Decision Graphs (MDG). The design we consider is in use for real applications in the Cambridge Fairisle network. We produced the description of the hardware implementation at different levels of abstraction. We then performed the verification of an abstract description model against the description of the gate-level implementation. Using this abstract model, we accomplished the verification of specific properties that reflect the behavior of the Fairisle ATM switch fabric.