Assertion IP (AIP) for Improved Design Verification

Over the years design reuse methodology created a market for Semiconductor IP (SIP), now with formal techniques there’s a need for Assertion IP (AIP). Where each AIP is a reusable and configurable verification component used in hardware design to detect protocol and functional violations in a Design Under Test (DUT).  LUBIS EDA is focused on formal services and tools, so I received an update on their approach to developing these AIPs and detecting corner-case bugs in high-risk IPs.

Before I jump into the details of the approach that LUBIS EDA uses, let’s first review how simulation-based verification differs from formal verification. With simulation an engineer is writing stimulus to cover all the known states of a design, hoping that the coverage is high enough. With formal verification the formal tool figures out all the possible paths from inputs to outputs within a design.

One approach used by LUBIS EDA is their in-house property generator, which works at the Electronic System Level (ESL) rather than Register Transfer Level (RTL). This enables them to deliver verification services that are faster, higher quality and more efficient. The property generator enables you to go from an abstract model to your AIP in a matter of minutes, which is a huge leap in verification productivity. Here’s what that flow looks like: first the abstract model is parsed and analyzed by the property generator, then the formal verification IP is created as System Verilog Assertions (SVA). These assertions check your design intent and provide full coverage of the functional behavior.

Your abstract model at the ESL level is written in C++ or SystemC and can be simulated to verify its behavior, the Property Generator reads in that code and generates the AIP for you. The assertions are then bound to your RTL design through the refinement step which is supported by Large Language Models (LLMs) for a faster result.  The assertions are human-readable and correct-by-construction, so you don’t need to have a dedicated assertion review session. Run your favorite formal tool in this flow and then look for any failures.

One example for applying this AIP approach is for cryptographic hash functions like SHA-512. The following shows the C++ model on the left and the property that is generated on the right that covers a portion of the model.

Summary

How does this approach make formal verification more efficient? Verification engineers can apply formal approaches by manually writing assertions. Manually writing formal assertions take time, error prone and requires expertise, so automating this step saves you engineering time and effort.

The generated Assertion IP (AIP) covers every possible scenario and stimuli to guarantee a bug-free design. This approach is also quite useful to help you verify blocks of logic or even complex IP cores.

Is your project under enormous time pressure and would you like to leverage the benefits of such an efficient approach? Then you should consider LUBIS EDA’s consulting services to achieve first-class SoC design quality. If you want to carry out your project yourself, there are also courses on formal verification that could help you work faster. LUBIS EDA’s website also has many useful blog articles on using formal verification techniques.

To take the next step, just contact the team at LUBIS EDA.

Related Blogs

• LUBIS EDA at the 2025 Design Automation Conference #62DAC
• CEO Interview: Tobias Ludwig of LUBIS EDA