Formal Verification Sign-Off: Frequently Asked Questions
Answers to the questions we hear most from engineering teams and procurement contacts.
About LUBIS EDA
LUBIS EDA provides formal verification sign-off as a service for digital IP and SoCs. We take block-level RTL designs through a structured, end-to-end process: verification planning, property development, formal environment setup, convergence, and a documented sign-off report. Our focus is on finding simulation-resistant and corner-case bugs and giving teams the confidence to tape out critical designs on schedule.
LUBIS EDA was founded in 2020. Our team brings a combined 100+ years of hands-on formal verification experience, with engineers holding master’s degrees and PhDs in the field. To date we have completed 325+ formal verification projects.
As digital designs grow in complexity, simulation alone can no longer reliably find corner-case bugs within a reasonable schedule. Formal verification closes that gap, but only when executed with the right methodology and expertise. We started LUBIS EDA to make high-quality formal sign-off accessible to any team building critical digital IP, regardless of whether they have in-house formal specialists or not.
Most vendors offer engineers on a time-and-materials basis. LUBIS EDA combines specialist execution with a proven delivery structure: a layered team model, a sign-off maturity flow, and reusable verification artifacts — so you get consistent, traceable results rather than a one-off consulting engagement. We are 100% focused on formal verification, which means depth of expertise that generalist vendors cannot match.
Yes. Our case studies and success stories are available on our website at lubis-eda.com/case-studies. We work with many of the world’s top semiconductor companies, including clients in the Fortune 25. We are not able to disclose all engagements publicly, but we can connect you with a reference client upon request. Public engagements you can find at https://lubis-eda.com/lubis-eda-testimonials/
Yes. We work with all major formal verification tools on the market, including Synopsys VC Formal, Cadence Jasper, and Siemens Questa Formal / OneSpin. Our Assertion IPs and verification flows are compatible across tools, so we can integrate into your existing EDA environment rather than requiring you to change it.
How Formal Verification Works
Simulation verifies that your design behaves correctly under the scenarios you thought to test. Formal verification proves that certain behaviors cannot occur, regardless of input sequence. Simulation-resistant corner-case bugs (race conditions, protocol violations, and multi-cycle state-machine anomalies) live in scenarios that no testbench will ever reach. Across 325+ formal verification sign-off projects, our engineers have found 900+ real bugs that simulation missed, including critical findings just weeks before tape-out.
Formal verification is valuable for any team working on digital designs, regardless of company size. As soon as you have RTL and specification, formal verification can add value. It is particularly critical when you are working on high-risk blocks on the tape-out critical path, when simulation coverage has plateaued, or when the design complexity is rising faster than your ability to hire deep formal expertise.
An Assertion IP is a reusable, self-contained package of SystemVerilog Assertions (SVA) that checks the behavior of a specific design block or protocol. It contains the checkers, constraints, and cover points needed to formally verify a block’s requirements. Our AIPs are delivered as part of every engagement and are designed to be reusable — you can integrate them into your regression flow to catch regressions in future design iterations.
For most blocks, we aim for 100% proof coverage at sign-off where proof complexity allows. Coverage encompasses property coverage (are all required behaviors checked?), stimuli coverage (are all interesting scenarios reachable?), and dead-code analysis. Together these confirm that if the design broke, at least one property would catch it.
In a design that has not been formally verified before, the first bug can often be found within the first day of running properties. In more mature designs that have already undergone some verification, finding bugs requires deeper analysis. The time-to-first-bug depends on design maturity and the nature of the block, but formal consistently finds issues that simulation would have missed entirely.
Proof runtime is highly block-specific. Some proofs close in minutes; others take hours; some converge over days. Certain properties in deeply sequential designs may never fully converge, in which case we use bounded model checking and coverage analysis to establish defensible confidence within defined bounds. We do not use runtime as the primary metric, we use the depth of the bounds reached and coverage results to make the sign-off decision.
The Sign-Off Process
Formal verification sign-off is a structured, documented conclusion to a formal verification engagement, not just a green result on a proof dashboard. Sign-off means that all of the following conditions are satisfied:
- All checkers are proven within agreed bounds, or failing for a confirmed design bug.
- All intended behaviors are covered, confirmed reachable via cover points.
- All constraints and assumptions are reviewed and justified.
- Non-converging proofs have been addressed through bound analysis.
- A formal sign-off report is delivered with full traceability.
This gives you a reproducible, defensible record, not just a passing run.
For designs where full exhaustive proof is not achievable due to complexity, we use bounded model checking combined with cover-point analysis. We check whether the achieved proof depth covers the most interesting and safety-critical behaviors, and we document any remaining open items with a clear risk assessment. This allows a principled sign-off decision even without 100% unbounded proof.
Coverage metrics in formal verification tell you how much your property set exercises the design. This includes property coverage (which parts of the design are checked by at least one property), stimuli coverage (which design states and transitions have been reached), and dead-code analysis (which parts of the design can never be activated). High coverage means that if a bug existed in that part of the design, your properties would catch it.
We find real bugs. Across 325+ formal verification sign-off projects, our engineers have uncovered 900+ confirmed design bugs: including corner-case failures, protocol violations, incorrect exception handling, and unreachable states that had been present in production-bound RTL for months. Formal is not just a quality seal; it is an active bug-finding methodology.
at does a typical project flow look like?
- Every project follows a five-phase delivery model:
- Request: you provide the RTL, specification, and design context.
- Plan: we align on verification targets, scope, milestones, and sign-off criteria.
- Prep: we build the formal environment: abstractions, constraints, and an initial property set.
- Execute: we drive convergence, investigate failing properties, and provide regular progress updates.
Working With Us
To kick off a project we need: the RTL of the target block, the design specification, and a few sessions with the responsible designer to clarify intent, known risks, and open questions. We handle everything from there. You do not need in-house formal expertise or your own formal tool licenses to get started.
If you already have a formal verification expert in-house, the most efficient start is to review the blocks they have pre-selected and dive directly into the technical details and verification strategy for each one. If you are new to formal, we recommend starting with a single high-risk block, one that is on your tape-out critical path or one where simulation coverage has plateaued. We will help you scope the effort and define realistic sign-off targets before committing to a full engagement.
We recommend starting as soon as the first version of the RTL is available. The earlier formal verification begins, the lower the cost of fixing bugs and the lower the risk of schedule impact. Waiting until close to tape-out limits the depth of coverage you can achieve and increases the chance of findings landing too late to fix cleanly.
Yes. Block selection is one of the highest-value early conversations we have with new clients. We help you identify the blocks where formal verification delivers the most ROI: typically control logic, protocol interfaces, arbiters, and other blocks with deep corner-case behavior that is difficult to reach in simulation. We can prioritize based on your tape-out schedule and risk profile.
All of our projects run remotely. We work through regular structured sync-ups with your engineering team, typically weekly, to review progress, discuss questions, and align on any changes in scope or specification. You receive on-the-spot bug reports as findings are confirmed, and weekly progress updates. Your team does not need to be available constantly; we operate asynchronously and escalate only when a designer conversation is truly required.
We support multiple secure transfer methods. You can provide access to a private repository on any platform (GitHub, GitLab, internal Bitbucket), upload files to our secure SFTP server, or share via a secure corporate file exchange if your policy requires it. We treat all design data as strictly confidential and do not use it for any purpose other than the contracted verification work.
Not necessarily. By default, we run all formal jobs on our own servers using our own tool licenses. This means you do not need to provide us with access to your internal servers unless your security policy or design sensitivity requires the work to be done on your infrastructure. In that case, we can either connect via VPN to your existing servers and licenses or run the engagement as a fully managed service where LUBIS EDA hosts everything and no vendor contracts are required on your side. In both cases, collaboration is facilitated through version control. We highly recommend setting up a private Git repository for timely updates and traceability, though customers are free to use a system they prefer.
Yes. You will have regular sync-ups directly with the project engineer and the formal project lead. The project engineer handles day-to-day development and is typically present in all technical meetings. The team is fixed for the duration of the project to ensure continuity and consistent context.
Project Execution & Deliverables
The formal project lead and the assigned verification engineer define the verification plan, targets, and strategy together, then present them to your contact person (typically the responsible designer or verification lead) for alignment. The project engineer then carries out the property development according to the plan. You do not need to write assertions, that is our job. However, your designer’s input on design intent and edge cases is essential during the planning and prep phases.
We derive constraints from the specification and from discussions with your designer. Throughout the planning and prep phases, we identify all necessary assumptions, review them with you, and make sure they are clearly documented and justified. Any constraint that restricts the formal environment must be traceable back to a design requirement — we do not apply assumptions silently.
Yes, upon request. When we know upfront that you want to reuse the properties in simulation, we write them in a simulation-friendly way. Some formal-only constraints (such as cut constraints or abstract models) are not directly portable to simulation, but the functional checkers and many of the constraint assumptions can be made compatible. Just let us know this requirement at the start of the project.
Design changes are a normal part of formal verification projects. When you provide a new RTL version, we re-run the existing property set against it, update any assertions or constraints affected by the change, and inform you of the impact on the verification plan and timeline. Changes are most straightforward when caught early; later changes can require re-verification of previously closed properties, which we flag and handle transparently.
When a property fails, we first determine whether the failure indicates a genuine design bug or a property/constraint issue. If it is a design bug, we analyze the counterexample, classify the severity, and write a detailed bug report including the waveform, the violated behavior, and the conditions that trigger it. You receive the waveform report and can load the waveform in any compatible tool to inspect the failure yourself. Genuine bugs are tracked throughout the project and resolved with your design team.
At the end of an engagement you receive:
- All developed SystemVerilog Assertions (checkers, covers, and constraints).
- A formal sign-off report with proof results, coverage analysis, and a sign-off recommendation.
- Load scripts and configuration files for the formal tool of your choice.
- Full documentation of the Assertion IP, including scope, assumptions, and known limitations.
- Reusable artifacts as agreed, these can be integrated into your regression flow for ongoing protection.
Yes. Many of our clients engage us for ongoing multi-block verification programs, full-chip sign-off strategies, or retainer-based engagements. We can run parallel dedicated teams across multiple blocks and plan capacity in advance. Both fixed-price and subscription models are available for longer-term programs.
Tools & Infrastructure
We use all major formal verification tools available in the market, including Synopsys VC Formal, Cadence JasperGold, and Siemens Questa Formal (formerly OneSpin). We are tool agnostic — our Assertion IPs and verification flows are compatible across platforms, and we work with whichever tool fits your existing EDA infrastructure.
We develop our Assertion IPs in SystemVerilog Assertions (SVA). We work with designs written in Verilog, SystemVerilog, and VHDL.
We have developed our own protocol checkers and Assertion IPs for a wide range of standard protocols. In cases where a client specifically requires the vendor-supplied VIP (for example, for traceability or existing flow compatibility), we can use that instead. The choice is yours.
Yes, if the RTL is encrypted using a format supported by the formal tool in use (such as IEEE P1735-compliant encryption), we can work with it directly. Please let us know the encryption method upfront so we can confirm compatibility.
Generally no. We run all formal jobs on our own servers with our own licenses. You will only need a tool license yourself if you want to run the formal properties independently after delivery, for example, to re-verify the design after RTL changes. You do need a simulator or viewer to inspect the waveforms we provide as part of bug reports. On infrastructure, customers can either leverage their existing tool licenses and servers, with our engineers connecting via VPN, or opt for our fully managed service, where LUBIS EDA hosts everything and no vendor contracts are required on your side. In both cases, we highly recommend setting up a private Git repository for timely updates and version control, though you’re free to use a system you prefer.
FormalOS is LUBIS EDA’s comprehensive formal verification orchestration platform—connecting methodology, execution, automation, and reporting into a unified approach that improves predictability throughout the verification lifecycle. FormalOS is built on the lessons we’ve learned across more than 325 successful formal verification projects worldwide, and it empowers our team to deliver consistent, structured results, at scale, on a foreseeable sign-off timeline.
By default, we run formal jobs on our own servers. The intellectual property of the design remains entirely yours, we do not modify the design, and all design data is handled confidentially under our NDA. If your security policy requires work to be performed on your own servers, we can accommodate that as well.
Block Types & Scope
We have experience across a wide range of block types, including:
- Control logic: arbiters, schedulers, state machines, and bus controllers.
- Memory subsystems: cache controllers, memory controllers, FIFOs, and buffers.
- Protocol interfaces: AXI, AHB, AXI-Stream, PCIe, Ethernet, and custom protocols.
- Compute cores: RISC-V processors, AI/ML accelerators, and datapath units.
- Interconnects: routers, bridges, crossbars, and network-on-chip elements.
If your block type is not listed, reach out — we can advise on feasibility.
Our primary scope is block-level and IP-level verification, which is where formal delivers the best convergence and ROI. The sweet spot are blocks with input-to-output latency under approximately 30 cycles. We can extend to larger subsystems using abstraction techniques, but this requires additional planning and scoping. Full SoC-level formal is only practical with aggressive block-level abstractions.
Yes. Data integrity is a standard part of any functional verification engagement that involves data flow. We verify that data is correctly transmitted, transformed, or stored and that no corruption or loss can occur under formally proven conditions.
For block-level work, we typically need a high-level understanding of the system one or two levels above the target block, enough to understand interface contracts, clock domains, and reset behavior. This is usually covered in the initial design briefing. We do not need access to the full SoC to verify an individual block effectively.
Formal techniques are closely related to those used in functional safety (ISO 26262) and security analysis. If you have specific safety or security requirements, contact us to discuss what is within scope.
Pricing & Engagement Models
We offer two primary engagement models:
- Fixed Price: we scope the effort per block, estimate the required work, and deliver for a defined price. This model gives you cost certainty upfront and is well-suited for well-specified blocks with stable RTL.
- Subscription: a recurring engagement model suited for teams with ongoing or multi-block verification needs. Resources are allocated over time, providing flexibility for iterative or pipeline-style verification programs.
Both models include a dedicated team, structured delivery milestones, and the same quality of output. We will recommend the model that best fits your timeline and planning horizon.
Pricing depends on the block complexity, estimated effort, timeline, and the engagement model chosen. For fixed-price projects, we review the RTL and specification before providing a detailed estimate. For subscriptions, pricing is based on the number of allocated engineer-days per period. We always provide a rough estimate before any commitment so you can plan your budget.
Yes. Fixed-price projects carry a scoping premium because we absorb the risk of effort overruns. Subscription models typically offer a lower effective rate per engineer-day in exchange for a commitment to a longer engagement. The right choice depends on how predictable your design inputs are and how much schedule flexibility you need.
We are structured to accommodate changes. When a design or specification change occurs, we assess the impact on the verification plan and communicate it to you clearly, including any effect on timeline or deliverables. Smaller changes (such as RTL bugfixes) are typically absorbed within the existing plan. Larger scope changes (such as redesigned interfaces) are handled through a plan revision. We aim for transparency throughout, so there are no surprises at sign-off.
Standalone trainings are possible, however, from experience we prefer an embedded training approach as part of a joint engagement. This provides the opportunity to work on a design your team knows. Our engineers work alongside yours, sharing methodology, reviewing property strategies, and transferring knowledge directly on your own designs. This applies to both formal verification engineers and those newer to formal methods.