Using formal techniques to debug the AMBA system-on-chip bus protocol Export

@inproceedings{citeulike:2353677, abstract = {System-on-chip (SoC) designs use bus protocols for high performance data transfer among the intellectual property (IP) cores. These protocols incorporate advanced features such as pipelining, burst and split transfers. In this paper, we describe a case study in formally verifying a widely used SoC bus protocol: the advanced micro-controller bus architecture (AMBA) protocol from ARM. In particular, we develop a formal specification of the AMBA protocol. We then employ model checking, a state space exploration based formal verification technique, to verify crucial design invariants. The presence of pipelining and split transfer in the AMBA protocol gives rise to interesting corner cases, which are hard to detect via informal reasoning. Using the SMV model checker, we have detected a potential bus starvation scenario in the AMBA protocol. Such scenarios demonstrate the inherent intricacies in designing pipelined bus protocols.}, author = {Roychoudhury, A. and Mitra, T. and Karri, S. R.}, booktitle = {Design, Automation and Test in Europe Conference and Exhibition, 2003}, citeulike-article-id = {2353677}, citeulike-linkout-0 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1253709}, journal = {Design, Automation and Test in Europe Conference and Exhibition, 2003}, keywords = {amba, arm, formal-methods, on-chip-communication}, pages = {828--833}, posted-at = {2008-02-08 15:31:43}, priority = {2}, title = {Using formal techniques to debug the AMBA system-on-chip bus protocol}, url = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1253709}, year = {2003} }

TY - CONF ID - citeulike:2353677 L3 - citeulike-article-id:2353677 N2 - System-on-chip (SoC) designs use bus protocols for high performance data transfer among the intellectual property (IP) cores. These protocols incorporate advanced features such as pipelining, burst and split transfers. In this paper, we describe a case study in formally verifying a widely used SoC bus protocol: the advanced micro-controller bus architecture (AMBA) protocol from ARM. In particular, we develop a formal specification of the AMBA protocol. We then employ model checking, a state space exploration based formal verification technique, to verify crucial design invariants. The presence of pipelining and split transfer in the AMBA protocol gives rise to interesting corner cases, which are hard to detect via informal reasoning. Using the SMV model checker, we have detected a potential bus starvation scenario in the AMBA protocol. Such scenarios demonstrate the inherent intricacies in designing pipelined bus protocols. JF - Design, Automation and Test in Europe Conference and Exhibition, 2003 EP - 833 TI - Using formal techniques to debug the AMBA system-on-chip bus protocol T2 - Design, Automation and Test in Europe Conference and Exhibition, 2003 SP - 828 KW - amba KW - arm KW - formal-methods KW - on-chip-communication AU - Roychoudhury, A AU - Mitra, T AU - Karri, SR PY - 2003/// UR - http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1253709 ER -