Correct Safety Critical Hardware Descriptions via Static Analysis and Theorem Proving

We propose a new method for embedding Bluespec SystemVerilog descriptions in PVS's higherorder 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.