WP_Term Object
(
    [term_id] => 24576
    [name] => LUBIS EDA
    [slug] => lubis-eda
    [term_group] => 0
    [term_taxonomy_id] => 24576
    [taxonomy] => category
    [description] => 
    [parent] => 157
    [count] => 2
    [filter] => raw
    [cat_ID] => 24576
    [category_count] => 2
    [category_description] => 
    [cat_name] => LUBIS EDA
    [category_nicename] => lubis-eda
    [category_parent] => 157
)
            
LUBIS EDA SemiWiki Banner
WP_Term Object
(
    [term_id] => 24576
    [name] => LUBIS EDA
    [slug] => lubis-eda
    [term_group] => 0
    [term_taxonomy_id] => 24576
    [taxonomy] => category
    [description] => 
    [parent] => 157
    [count] => 2
    [filter] => raw
    [cat_ID] => 24576
    [category_count] => 2
    [category_description] => 
    [cat_name] => LUBIS EDA
    [category_nicename] => lubis-eda
    [category_parent] => 157
)

Automating Formal Verification

Automating Formal Verification
by Daniel Payne on 01-30-2025 at 10:00 am

Key Takeaways

  • LUBIS EDA, founded in 2020, focuses on automating formal verification to improve reliability in high-risk silicon designs.
  • Their cloud-based product, LUBIS-on-cloud, simplifies setup processes and enables quick bug detection supported by AI.
  • In 2023, LUBIS EDA successfully completed over 50 projects, uncovering more than 250 bugs, indicating an effective verification process.

Formal verification methods are being adopted at a fast pace as a complement to traditional verification methods like functional simulation for IP blocks in SoC designs. I had a video meeting with Max Birtel, co-founder of LUBIS EDA and learned more about their history, products and vision. This company started recently in 2020 to bring formal products to market, based on their experience providing verification services and then productizing their formal apps.

Their vision is to automate formal verification, which reveals hard to find bugs and makes high risk silicon designs more reliable. With a team of 35 people based in Germany, they provide expert training and support through consulting and a formal bootcamp, plus their technology provides automated setup and SVA assertion generation, finally with automated verification it simplifies complex bug detection with AI-driven tools.

VIP has been customized for common designs like RISC-V and AMBA protocols. They even have a cloud-based product, dubbed LUBIS-on-cloud, which means no software to install. In 2023 the company completed over 50 projects, with more than 250 bugs reported, taking typically under 30 days per block. Common blocks like limiters, memories and arbiters required 10 to 25 days. Control logic like AXI to X, routers and CHI took 25 to 50 days. Caches that were pipelined or RMW were validated in 25 to 40 days. Compute cores – Crypto, RISC-V, Image and Tensors took 10 to 50 days.

The LUBIS-on-cloud product takes your RTL code, then runs an App that controls a formal engine (Cadence, Siemens, Synopsys), which produces a bug report that a verification engineer reviews to finally make bug fixes. Here’s the flow for verifying a RISC-V processor, which takes very little training or experience with formal tools. You would see your first bug report within an hour.

LUBIS on cloud min

An example open-source RISC-V processor was uploaded, setup was automatic, then the App was run to start formal verification. Bugs were reported and details of the bug displayed, so that an RTL engineer could find and fix the bug. There were even waveforms shown to help in the debug process. AI is used to explain the bug in English, speeding the debug.

AI debug min
AI Debug

Using these apps to control the formal engines makes it easier for an un-trained engineer to use a formal approach, shortening the verification effort.

Cloud Demo

It was refreshing to see a live EDA demo on a RISC-V processor, and login was with Microsoft. The first run of the formal app revealed that 5 bugs were found.

demo 3 min
Status of formal runs

Max clicked on a bug to see why the run had failed, and it reported which signal had a mismatch between expected and actual values, along with waveforms.

Bug report details
Bug report details

For this block the test failed within 2 minutes, and the tool provides the counter example. You can either debug with the provided waveforms or choose to download the SV testbench to replicate the bug in your own UVM environment. An engineer still must manually fix the bug, then re-run the formal app until it passes to complete verification.

Summary

The focused engineering group at LUBIS EDA has made using formal verification tools quite automated and easy to use with the app approach, and the AI-based debug report really makes understanding what caused the bug explicit. Evaluating the cloud-based tool looks straight forward and intuitive

I also discovered where the company name LUBIS came from, it’s a mixture of the founder’s names: Ludwig, Bittel, Shwartz.

Related Blogs
Share this post via:

Comments

There are no comments yet.

You must register or log in to view/post comments.