Assertion-First Hardware Design and Formal Verification Services

Generative AI has transformed software development, enabling entire applications to be built in minutes. But despite similar progress in AI-generated RTL, hardware verification remains a major bottleneck. RTL can be produced quickly, yet proving its correctness is extraordinarily difficult. This has revived a long-standing but historically unattainable idea, namely, a complete set of formal properties. Hardware design in RTL should begin with Assertion IP that precisely define the intended behavior of the design, rather than generated after the fact. For decades, this approach was out of reach. Today, the landscape has shifted, making assertion-first hardware design increasingly viable.

Tobias Ludwig, CEO of LUBIS EDA addressed this very topic at the Verification Futures Conference recently held in Austin, Texas. His talk covered how the company is moving the industry toward this long-awaited direction.

AI Can Generate RTL But Verification Is Still the Bottleneck

AI-generated RTL may look plausible, but correctness in hardware is a hard requirement. Chips must work under every possible condition, and AI systems trained on similar datasets often share similar failure patterns. Using AI to verify AI does not eliminate risk but rather compounds it. Verification continues to dominate engineering cost and schedule because ensuring correctness requires precise, formalized intent. Assertion IP provides that precision, but historically it has been too difficult to produce at scale.

Assertion IP: What Hardware Design Should Have Started With

Assertion IP captures design intent in its most accurate form. It describes how the design must behave across states, cycles, inputs, and transitions. In an ideal process, assertions would come first, serving as the specification against which RTL is implemented and proven. This would eliminate ambiguity and allow mathematical verification throughout development.

Why Hardware Has Not Started From Assertions

Creating a complete assertion set manually was impractical. Writing hundreds or thousands of assertions by hand was slow and error-prone. High-level modeling languages were inconsistent, lacked structure and were difficult to analyze. Property generation tools did not exist. And Formal Verification engines lacked the computational strength to handle the depth and complexity of real IP blocks.

While waiting for tools capable of generating Assertion IP automatically, the industry’s culture centered on “RTL-first,” with assertions treated as an afterthought rather than the foundation.

What Has Changed Now

The situation has changed dramatically. High-level model analysis engines can now extract states, transitions, invariants, and dataflow from C++/SystemC models. Automated property generation tools can transform these models into complete assertion suites that capture timing behavior, and correctness requirements. Formal verification engines have grown powerful enough to handle deep pipelines, cryptographic algorithms, and large state spaces. AI assistance now makes creating structured models easier, allowing engineers to translate natural-language intent into analyzable code. Together, these breakthroughs make assertion-first design far more practical than ever before.

Where LUBIS EDA Fits In: Opening the Window to Assertion-First Design

LUBIS EDA is turning this renewed possibility into a practical methodology. Its technology automatically generates comprehensive Assertion IP from high-level executable models, bridging the gap between abstract model and RTL implementation. Through refinement techniques that align abstract models with cycle-accurate RTL, LUBIS ensures that properties reflect bit-level reality.

Alongside the company’s formal verification services, LUBIS EDA provides training that help teams adopt assertion-driven workflows and achieve formal sign-off on complex blocks. As AI accelerates RTL generation, LUBIS EDA’s model-first, property-driven approach becomes essential for ensuring correctness and preventing hidden bugs.

Summary

For the first time, hardware teams can move toward a design process where intent is explicit, properties are complete and RTL correctness is provable from the start. This paradigm is now within reach thanks to advances in modeling, property generation, formal tools, and AI support. LUBIS EDA is helping the industry make this transition, prying open the door to a future where hardware design can begin with formal assertion IP.

To learn more, visit www.lubis-eda.com