WRITING FORMAL PROPERTIES IS COMPLICATED? LET US DEMOCRATISE PROPERTY CREATION!

Today, formal verification is mostly used for bug hunting. Writing formal properties is time consuming and requires a certain level of expertise. The performance of formal tools increased drastically within the last decade. Trends like increasing design complexity, safety and security requirements (e.g. ISO 26262) lead to an increasing usage of formal to verify the chips. Wouldn’t it be great to democratise property creation?

Our Vision is to democratise property creation to enable a wider audience to use formal to their benefit. LUBIS EDA provides toolings and services that allow your company to automatically generate Verification IP (VIP).

The flow starts with parsing a Transaction Level Model (e.g. SystemC or any other DSL). The parsed model is processed by LUBIS CONCILIUM and LUBIS VERITAS and the Verification IP is generated for our customers.

The VIP is a set of System Verilog Assertions (SVA). The properties are configurable regarding timing and bit-accuracy and can be adapted to any existing or new RTL design. Proving all generated properties ensures that the functional behaviour specified by the TLM model is implemented correctly. You get a correct-by-construction RTL design.

We conducted two case studies on industrial designs. Let us take a closer look:


Analysing the posted numbers, we can conduct two things:

1. Many properties
2. Fast runtime

Our aim is to generate many properties, that are easy to understand, easy to debug and circumvent a complexity blow-up of the formal tool.

Now its time to go get a coffee.
While you’re getting the coffee:
imagine a world that allows you to incrementally build your RTL.

When you’re back at your work desk, imagine that the recent RTL changes are already verified with our VIP.

Get in contact with us and be part of the next innovation in chip design!

Best
Tobias