Assertions proved for every input, or broken with a short trace.
Lumina Formal reads the same sources as Lumina Lint and Lumina Sim, compiles every concurrent assertion, assumption and cover into checker logic, and runs three engines on them. Every counterexample is replayed in Lumina Sim, so a failure it reports is one the simulator confirms.
From the Lumina Formal getting-started guide
- BMC
- finds the shortest failure
- k-induction
- proves
- IC3/PDR
- proves with an invariant
- Replayed
- every counterexample, in simulation
What Lumina Formal does
Three engines, in turn
Bounded model checking looks for the shortest failure, k-induction proves what it can, and IC3/PDR builds an inductive invariant for the rest, or finds a failure deeper than the bound.
Counterexamples you can trust
A testbench drives the design as the counterexample does, and the simulator's own assertion engine must report the same failure. One that does not replay is never reported as a confirmed bug.
Every clock interleaving
With several clock inputs, each step is any set of clock edges, so every order in which the clocks can tick is checked.
X means any value
Undriven signals, unreset flops and x constants are free values, so a proof holds for every value an X could take.
The SVA you write
Sequences, implication, disable iff, $past, $rose, $stable, $onehot and the rest, with unbounded repetition and goto operators checked by automata.
Liveness
s_eventually and strong sequences are proved too; a failure is shown as a lasso, a path on which an obligation stays pending forever.
CDC and multicycle proofs
Crossings flagged by Lumina CDC and multicycle paths in your constraints are proved on the same design model.
Honest about limits
A construct it cannot check yet is reported UNSUPPORTED with the reason, never silently passed.
What a result means
- PROVED
Holds for every input sequence from reset, with the engine that proved it
- FAILED at step n
A counterexample with every input at every step, and the simulation replay's verdict
- No failure up to step k
BMC found none and the proofs did not conclude
- COVERED at step n
The cover property can be reached, with the trace that reaches it
- UNSUPPORTED
The property uses a construct not checked yet; the reason is given
Properties checked
- Directives
assert property, assume property, cover property, in modules and their instances
- Sequences
##n, ##[m:n], [*n], [*m:n], and, or, intersect, throughout, within, first_match
- Properties
|->, |=>, #-#, #=#, not, and, or, iff, implies, if/else, nexttime, always [m:n], s_eventually
- Functions
$past, $rose, $fell, $stable, $changed, $onehot, $onehot0, $countones
- Unbounded
##[m:$], [*m:$], goto [->n] and non-consecutive [=n] repetition, by automata
- Reset
disable iff and default disable iff, asynchronous as IEEE 1800 defines
Frequently asked
What is formal verification?
A mathematical check that a property of the design holds for every possible input sequence, not only for the ones a testbench happens to drive. When it does not hold, the tool gives the exact sequence of inputs that breaks it.
How is it different from simulation?
Simulation shows that the design works for the tests you ran. Formal shows that an assertion can never fail, or finds the shortest way to make it fail. The two complement each other: Lumina replays every formal counterexample in simulation.
Do I need to write new properties?
No. Lumina Formal checks the concurrent assertions, assumptions and covers already in your SystemVerilog code. The same assertions are checked in simulation.
What happens with constructs it does not support yet?
The property is reported as UNSUPPORTED with the reason. Nothing is skipped silently or reported as proved.
Run your own design on Lumina first.
We are working with a small group of design teams before release. You run your real designs; we fix what you find, and your cases become part of the tests every build must pass.