Proof-Carrying Hardware via IC3

TL;DR

This paper introduces a novel proof-carrying hardware method using IC3, enabling fully automatic and efficient safety proofs for complex sequential circuits, surpassing previous semi-automatic approaches.

Contribution

It presents a new approach employing IC3 for automatic proof generation in proof-carrying hardware, applicable to general sequential circuits.

Findings

Proof validation is several orders of magnitude faster.

Proofs are often smaller than existing PCH methods.

Demonstrates feasibility of automatic PCH for complex circuits.

Abstract

Proof-carrying hardware (PCH) is an approach to achieving safety of dynamically reconfigurable hardware, transferring the idea of proof-carrying code to the hardware domain. Current PCH approaches are, however, either limited to combinational and bounded unfoldings of sequential circuits, or only provide semi-automatic proof generation. We propose a new approach to PCH which employs IC3 as proof generator, making automatic PCH applicable to sequential circuits in their full generality. We demonstrate feasibility of our approach by showing that proof validation is several orders of magnitude faster than original proof generation while (most often) generating smaller proofs than current PCHs.