The Property Generator is a proprietary tool developed by LUBIS EDA to simplify and accelerate formal verification.

It results in correct-by-construction assertions, human readable, and, lastly, removes the need for a review of the assertions.

The verification journey begins with writing a SystemC model that expresses functional intent. This model can be simulated using standard C++ and SystemC techniques, helping designers and verification engineers validate functionality early. The Property Generator then analyzes the model to auto-generate assertions that comprehensively describe the expected behavior.

After generation the assertions are loaded together with the design into a formal tool of your choice or a simulator.

In a typical setup, these assertions must be manually bound to RTL design signals—a process that is time-consuming and error-prone. To address this, the Property Generator integrates an AI-Refinement add-on, powered by Large Language Models (LLMs). These models can interpret both the abstract model and RTL structure, performing the refinement step with high accuracy and minimal user intervention.

What makes our generations special is that we generate assertions to ease proof complexity by generating a large number of simple, focused properties, rather than a few complex ones. These simpler properties are easier to prove individually. Once the design is verified, only the abstract model needs review, significantly reducing sign-off time.

By using our tool, we enable more people to use formal verification and kick-start their formal journey.

More information about objectives, motivation, content and target audience can be found in the attached PDF.