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 …