Title :
The BUSpec platform for automated generation of verification aids for standard bus protocols
Author :
Pal, Bhaskar ; Banerjee, Ansuman ; Dasgupta, Pallab ; Chakrabarti, P.P.
Author_Institution :
Dept. of Comput. Sci. & Eng., Indian Inst. of Technol., Kharagpur, India
Abstract :
A typical verification IP (VIP) of a bus protocol such as ARM AMBA or PCI consists of a set of assertions and associated verification aids like test-benches and coverage metrics. While, several languages have been formalized for specifying assertions (examples include OVA, Sugar, ForSpec, SVA, etc), the tasks of writing test-benches that produce protocol compliant stimuli and coverage monitors that reflect the coverage of the protocol functionality are also of significant importance. This paper presents a platform for high-level specification of a bus protocol and an automated methodology for generating a variety of verification aids that must supplement the set of assertions in a VIP.
Keywords :
formal specification; formal verification; protocols; system buses; ARM ANIBA; BUSpec platform; PCI; automated verification aid generation; bus protocols; coverage metrics; high-level specification; test-benches; verification IP; Acquired immune deficiency syndrome; Circuits; Communication standards; Computer science; Master-slave; Protocols; Prototypes; System-on-a-chip; Testing; Writing;
Conference_Titel :
Formal Methods and Models for Co-Design, 2004. MEMOCODE '04. Proceedings. Second ACM and IEEE International Conference on
Print_ISBN :
0-7803-8509-8
DOI :
10.1109/MEMCOD.2004.1459831
