Towards Automatic Property Generation for SoC Security Verification

Formal verification is an emerging technique for validating the soundness of SoC designs and uncover design flaws. However, existing formal solutions heavily rely on verification engineers to manually specify assertion properties, which can be time-consuming but provides no guarantee on the quality or completeness of the property set. In this brief, we move a step towards automatic property generation for SoC security verification. We automatically extract invariant behaviors from functional and security simulation traces and specify them as assertions. We further prove the generated properties to search for property violations to identify design vulnerabilities. Experimental results show the effectiveness of our method in detecting timing channel and stealthy hardware Trojan.