ABSTRACT :
Formally specifying protocols in Live Sequence Charts (LSCs) and verifying that a register
transfer level implementation meets this formal specification can alleviate the protocol
verification problem. LSCs compactly represent communication between system agents in a
visual format that is easy to learn and use. By adding hardware-specific features to LSCs
and showing a reduction to a previously defined formal semantics, this research provides a
language that can be used to formally specify hardware protocols by engineers not highly
trained in formal methods. This work further lightens the burden of formality on the verification
engineer by developing a tool, lscAssert, which inputs a LSC specification and outputs a series
of properties ready for model checking. Finally, the work includes a demonstration that LSCs
can adequately specify industrial protocols, such as the Virtual Component Interface Standard
and the Peripheral Component Interconnect and that the method identifies design flaws by
presenting a series of verification case studies.
No comments:
Post a Comment