Correct Safety Critical Hardware Descriptions via Static Analysis and Theorem Proving
Nicholas Moore, Mark Lawford · 2017
We propose a new method for embedding Bluespec SystemVerilog descriptions in PVS's higher-order proof logic. In contrast to previous embeddings, our approach accepts a greater subset of BSV and provides a far greater degree of automation. Our custom software tool transforms the action-oriented semantics of BSV to a state-centric Kripke structure, enabling automated theorem proving. We demonstrate our verification technique by applying it to one of the function blocks of the IEC 61131-3 standard for PLCs.