Behavioral verification of an ATM switch fabric using implicit abstract state enumeration
Behavioral verification of an ATM switch fabric using implicit abstract state enumeration
复制标题
使用隐式抽象状态枚举对 ATM 交换结构进行行为验证
DOI：
10.1109/iccd.1996.563526
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
E. Cerny
中科院分区：
文献类型：
--
作者：
M. Langevin;S. Tahar;Zijian Zhou;Xiaoyu Song;E. Cerny
针对不受帧大小、信元长度和字宽限制的高级行为规范，研究了剑桥Fairisle异步传输模式(ATM)4×4交换结构RTL硬件实现的等价性验证。验证基于实现和规范的产品机的可达性分析，两者都被建模为抽象状态机(ASM)。多路决策图(MDG)用于编码ASM和可达抽象状态集的输出和转换关系，从而允许隐式抽象状态枚举。由于MDG避免了由数据值引起的模型爆炸，本实验证明了基于MDG的验证作为基于ROBDD的方法的扩展的有效性。
We investigate equivalence checking of the RTL hardware implementation of the Cambridge Fairisle Asynchronous Transfer Mode (ATM) 4 by 4 switch fabric against a high-level behavioral specification which has unrestricted frame size, cell length and word width. The verification is based on the reachability analysis of the product machine of the implementation and the specification, both modeled as Abstract State Machines (ASM). Multiway Decision Graphs (MDG) are used to encode both the output and transition relations of the ASMs and of the set of reachable abstract states, allowing implicit abstract state enumeration. Since MDGs avoid model explosion induced by data values, this experiment demonstrates the effectiveness of MDG-based verification as an extension of ROBDD-based approaches.