A Case Study in the Automated Translation of BSV Hardware to PVS Formal Logic with Subsequent Verification

We previously developed a method of formal hardware verification that automatically translates hardware descriptions encoded in Bluespec SystemVerilog (BSV) into the formal logic of Prototype Verification System (PVS) to allow verification of system properties. This paper reports on an extension of our translation tool, BAPIP, that refines the semantic model to cover more Bluespec language constructs and optimizes the translation to PVS to address scalability to allow applicability of the method to real-world hardware examples as demonstrated by a case study of the Shakti RISC-V project’s implementation of the RapidIO data packet passing communication protocol. In particular we verify the encoding of byte masks in outgoing memory read requests.