Property Generator: simple generation of Formal Assertion IP

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 autocompile assertions that comprehensively describe the expected behavior. Afterwards, the assertions are loaded together with the RTL 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 many simple, focused properties, rather than a few complex ones. These properties are easier to prove individually, increasing convergence. Once the design is verified, only the abstract model needs review, significantly reducing sign-off time.

Dr. Tobias Ludwig is the CEO and co-founder of LUBIS EDA, a company specializing in electronic design automation (EDA) tools and formal verification consulting. He earned his Ph.D. in Electronic Design Automation from the University of Technology Kaiserslautern in 2021. During his doctoral studies, Dr. Ludwig identified inefficiencies in traditional formal verification processes within the semiconductor industry. This insight led him to work on an automated EDA software solution aimed at enhancing development processes and ensuring high-quality, efficient outcomes. Collaborating with Dr. Michael Schwarz and Dr. Max Birtel, he co-founded LUBIS EDA to advance formal verification in the semiconductor industry. Under Tobias’ leadership, LUBIS EDA has focused on automating formal verification to uncover simulation-resistant and corner-case bugs in high-risk silicon designs. The company integrates cutting-edge tools and AI techniques to make formal verification more accessible and effective.