Applying a visual specification language to hardware protocol verification

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.