The BUSpec Platform for Automated Generation

of Verification Aids for Standard Bus Protocols

A typical verification IP of a Bus protocol such as ARM AMBA or PCI
consists of a set of assertions and associated verification aids such as
test-benches and coverage metrics. While, several languages have been
formalized for specifying assertions (examples include OVA, Sugar, ForSpec,
SVA, etc), the task of writing test-benches that produce protocol compliant
stimuli and coverage monitors that reflect the coverage of the protocol
functionality are also tasks of significant importance.
BUSpec is a platform for high-level specification of a Bus protocol and an
which is the basis of our  methodology for automatically
generating a variety of verification aids that must supplement the set of
assertions in a verification IP.

 BUSpec Language Reference Manual and Tool Description

 BUSpec description for the Example given in paper

 BUSpec description of ARM AMBA AHB Protocol