Quantum Machines Testimonial

Quantum Machines Testimonial

Scalable formal verification for quantum computing hardware

Quantum machines testimonial logo

Project background

Quantum Machines (QM) develops control systems for quantum computers. With their Quantum Orchestration™ Platform, customers can realize the full potential of any qubit, at any scale, in record time. QM’s internal teams include both VLSI design and verification engineers, who work with LUBIS EDA as a trusted partner for formal verification activities.

The challenge

Quantum Machines sought to gain an edge in verifying their product IP. Deploying formal methods at large-scale requires a partner with deep engineering expertise who can keep pace with rapidly evolving RTL and changing project requirements while maintaining rigorous formal standards.

LUBIS EDA contribution

LUBIS EDA supports Quantum Machines with formal verification services across their product IP. The team brings specialist expertise in formal methods, navigates the balance between rapidly evolving RTL and changing project requirements, and deploys formal methods for large-scale design verification.

How the work was done

The cooperation has worked flawlessly at both a personal and professional level since the first engagement in early 2022. LUBIS EDA’s proficiency in deploying formal methods for large-scale design verification, combined with their ability to tackle complex challenges, has made the collaboration a repeatable and reliable part of QM’s verification process.

Results achieved

Since the first engagement, Quantum Machines has extended the business relationship multiple times. LUBIS EDA has consistently delivered formal verification services that give QM an edge in verifying their product IP, with a dedication to quality and a commitment to an error-free process.

Value for Quantum Machines

Quantum Machines views LUBIS EDA as their strategic partner for formal verification and looks forward to working together in future endeavors. The engagement provides access to a team with unparalleled understanding of the engineering intricacies involved, consistently exceeding expectations in delivering top-notch formal verification services

What Our Partners Say

Feedback from industry leaders who have adopted model-driven formal verification methodologies with LUBIS EDA.

When it comes to production-grade and scalable formal verification, LUBIS truly delivers excellence. Their team possesses an unparalleled understanding of the intricacies involved at an engineering level.
Ori Weber
Director of Logic and Manager of Quantum Machines verification activities • Quantum Machines
Outcome Summary

A Trusted Partner for Scalable Formal Verification

The Quantum Machines engagement shows how a consistent, expert-driven formal verification partnership supports hardware teams in verifying complex IP. The collaboration has grown steadily since 2022 and established LUBIS EDA as a strategic partner for Quantum Machines' formal verification activities.

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