An Encoding of the Clock Cycle Semantics of Bluespec SystemVerilog in PVS

Abstract

The invention of Hardware Description Languages has given hardware designers access to powerful methods of abstraction and organization, previously only available to software developers.

A high-powered means of examining properties such as reliability, correctness and safety is the creation of formal, mathematical proofs of correctness. One approach to this is the modelling of the artifact in the logic of some deductive system, such as the higher order logic of the Prototype Verification System (PVS). The ambition of this work is to demonstrate a mechanism by which a class of hardware descriptions may be used to generate such models automatically. We further demonstrate the utility of said models, using them to demonstrate non-trivial correctness properties. We also present a method of generating hardware descriptions, logical models, and proofs from a class of tabular specifications.

The language on which this method operates is Bluespec SystemVerilog (BSV), a high-level hardware description language notable for its elegant semantics. The target platform of our translation is the Prototype Verification System (PVS), which features a highly automatic theorem-proving system. The translation algorithm is discussed at length, including the reconciliation of BSV's action-oriented semantic and the Kripke semantics employed by our chosen model in PVS.

Five case studies demonstrate our methodology. In studies one and two, function blocks of the IEC 61131-3 Annex F library are verified against tabular specifications, or generated from the same. The remaining case studies are based on the Shakti RISC-V implementation of the RapidIO subsystem. Our final case study demonstrates progress towards the verification of highly abstract and complex properties over the entire translatable subset of the RapidIO library.