| Many verification engineers find it difficult to write specifications with formal specification languages like Linear Temporal Logic (LTL) and Computational Tree Logic (CTL). This difficulty is one of the reasons that formal methods are not widely accepted. As a solution to this problem, we propose Protocol Live Sequence Charts (PLSCs) as a formal specification language and claim that PLSCs are not only expressive enough but also conceptually accessible for use in widespread hardware protocol compliance verification. Previous work in this area uses PLSCs to specify the Virtual Component Interface (VCI), a system-on-chip communication standard developed by the Virtual Socket Interface Alliance (VSIA), and the Peripheral Component Interconnect (PCI), a complex industrial standard. This research strengthens the PLSC language by adding a concurrency model, which enables PLSCs to specify pipelining in protocols. To bolster our claim about expressiveness of the PLSCs language, this research also specifies the ARMRTM AMBA Advanced Extensible Interface (AXI) and the IntelRTM ItaniumRTM Bus Protocol, which are among the most complex industrial hardware protocols at present, using the concurrency model. |
