A RECORD OF LUBIS EDA

A RECORD OF LUBIS EDA

To share how LUBIS EDA began, we take you back to 2015. The LUBIS EDA history is rooted in academic research that explored new ways to advance formal verification.

Research Foundations

The idea emerged from research work on Path-Predicate Abstractions (PPA), seeking inspiration for advancing formal verification methods. One of our team members was exploring sound abstraction of RTL designs using formal properties and investigating how these abstract models could guide hardware design from ESL to RTL

At the same time, another part of our team was working on teaching Test-Driven Development (TDD) in software, focusing on ensuring correctness through tests that define behavior before implementation.

Property-Driven Development

This sparked a key insight: apply the principles of TDD to hardware verification by defining the expected behavior up front through formal properties. We called this Property-Driven Development (PDD) — the idea that formal properties should be defined before implementing a design. These properties act as a “basis of truth” guiding both design and verification.

From this philosophy grew our first product concept, the LUBIS Property Generator, a tool designed to automate correct-by-construction generation of formal assertion IP from behavioral models. The Property Generator helps accelerate formal verification by producing human-readable assertions that express intended behavior and simplify proof convergence.

Team and Product Evolution

Since then, we have formed a diverse team committed to applying agile methodologies to hardware development. Our product lineup continues to evolve with this mindset, delivering tools that help teams bring designs to market faster, reduce development costs, and create RTL designs that are correct by construction.

At LUBIS EDA, our vision is to be the first EDA company empowering the industry to move from traditional waterfall processes to Agile Hardware Development, where formal properties and automation play a central role in design and verification.

Training Topics

  1. Abstraction vectors (time, functionality)
  2. AIP for protocols
  3. AIP orchestration
  4. BMC & IPG, invariants
  5. Codestyle
  6. Completeness
  7. Liveness property, safety property
  8. Non-determinism (abstraction technique)
  9. Response generation (abstraction technique)
  10. Scoreboard (abstraction technique)
  11. Signal cutting, blackboxing
  12. State space explosion and mitigation techniques
  13. SVA fundamentals
  14. Whitebox checking, blackbox checking, greybox checking
  15. Witness, vacuity, reachability

Become a leader in formal verification