Writing SystemVerilog Assertions (SVA) is a must-do task when applying Formal Verification. Not only is this a highly specialized and manual task, but also fulfilling the completeness-criteria and making sure that the full functionality and state-space of the design is covered can be tricky.

We will introduce the Property Generator, a tool that generates a complete set of SystemVerilog Assertions (SVA) from SystemC-based models. This enables formal verification to begin as early as the virtual prototyping phase. It results in correct-by-construction assertions, quick turn- around in case requirement changes, and, lastly, removes the need for human review of the assertions.

We aim to introduce the tool to a wider audience and help people starting their formal verification journey.

By leveraging state-of-the-art compilers, the Property Generator eliminates the need for manual property creation, accelerating verification workflows and reducing review overhead. This workshop demonstrates how behavioral intent, captured in SystemC, can be directly translated into actionable formal properties, leading to bug-free RTL designs with less manual effort and greater confidence.