Please use this identifier to cite or link to this item: https://doi.org/10.1109/DATE.2003.1253709
Title: Using formal techniques to debug the AMBA system-on-chip bus protocol
Authors: Roychoudhury, A. 
Mitra, T. 
Karri, S.R.
Issue Date: 2003
Source: Roychoudhury, A.,Mitra, T.,Karri, S.R. (2003). Using formal techniques to debug the AMBA system-on-chip bus protocol. Proceedings -Design, Automation and Test in Europe, DATE : 828-833. ScholarBank@NUS Repository. https://doi.org/10.1109/DATE.2003.1253709
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. © 2003 IEEE.
Source Title: Proceedings -Design, Automation and Test in Europe, DATE
URI: http://scholarbank.nus.edu.sg/handle/10635/78417
ISSN: 15301591
DOI: 10.1109/DATE.2003.1253709
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

53
checked on Mar 7, 2018

Page view(s)

30
checked on Mar 9, 2018

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.