Abstract

A non-trivial subset of Bluespec SystemVerilog (BSV) is embedded in the higher order logic of the PVS theorem prover. Owing to the clean semantics of BSV , application of monadic techniques leads to a surprisingly elegant embedding, in which hardware designs are translated into logic almost verbatim, preserving types and language constructs. The resulting specifications are compatible with the built-in model checker of PVS , which can automatically prove an important class of temporal logic theorems, and can also be used in conjunction with the powerful proof strategies of PVS , including automatic predicate abstraction, to verify a broader class of properties than can be achieved with model checking alone. Furthermore, the above BSV subset is also embedded in the specification language of the SAL model checker, which provides a diverse array of fully-automated verification techniques.

Bluespec SystemVerilog is a hardware description language based on the guarded action model of concurrency. It has an elegant semantics, which has previously been shown to support design verification by hand proof: to date, however, little work has been conducted on the application of automated reasoning to BSV designs.