Giolit Labs presents
SystemVerilog assertion
formal verifier
Giolit SVA Verifier 1.0
Stop simulating. Start proving.
Simulation checks the input sequences somebody wrote. The Giolit SVA Verifier checks all of them — proof that every SystemVerilog Assertion (SVA) of your RTL hardware holds for every input and every start state, or the exact clock cycle that breaks it.
sva-verify 1.0.0 (trial) · Linux x86-64 · exit codes for CI · C++ SDK · runs offline
SystemVerilog Assertion Verifier
One command. Proof or the breaking cycle.
- Your RTL with assert, assume, cover — IEEE 1800-2017, exactly as you simulate it.
- Three engines race: prover (invariants), explorer (states + lassos), simulator (deep runs).
- PROVED ships a signed certificate; FAILED ships the cycle, waveform and replay testbench.
- Safety margins with 1–5 stars tell you how much slack each proof has.
$ sva-verify --reset=rst --margins 11_margins.sv
PROVED assert margins.a_level
PROVED assert margins.a_latency
Score ★★★☆☆ · Report: cert/certificate.pdf
Proof, not sampling
Every input sequence, of any length, from every start state — checked at once. PROVED is a proof, never a test result.
The exact breaking cycle
FAILED means a concrete run: cycle-by-cycle values, VCD waveform and a replay testbench for your own simulator.
Evidence auditors accept
Signed PDF certificate with the invariant in your signal names, SHA-256 statement, one-script check — no tool needed.
Margins with stars
Know whether each bound holds with room to spare or by a single count: per-bound margins + 1–5 star Resilience Score.
0
wrong answers on 340 benchmark properties
219/231
designs decided — vs 160 EBMC, 104 SymbiYosys
★★★★★
safety margins + Resilience Score per bound
100%
in-house engines — no solver, fully offline
Product tour
Your RTL in. Decision with evidence out.
No test vectors to write, no engines to pick, no project files. Three in-house engines race on the same cycle model — the first to settle a property decides it.
How it works
Your RTL in. Decision with evidence out.
No test vectors to write, no engines to pick, no project files. Three in-house engines race on the same cycle model — watch the prover settle first.
SystemVerilog RTL with SVA
assert, assume, cover — IEEE 1800-2017, as written. No test vectors, no project files.
$ one cycle model · three hunters · verdict the instant it is known
Every engine is built in-house — no external solver, no network, no upload. Your RTL never leaves your machines.
Constrained-random simulation
Checks the sequences somebody wrote.
Common cases get hit. The corner case — the red dot nobody aimed at — ships to emulation, silicon, or your customer.
Giolit SVA proof
Checks all of them. At once.
Every input sequence, of any length, from every start state. When PROVED, there is no sequence that breaks it.
Why chips still fail
The expensive bugs are the sequences nobody simulated.
Constrained-random finds the common bugs. The corner cases are rare by nature — and found late: in emulation, in silicon, or by your customer. Proof finds them on day one, with the run attached.
$ sva-verify --reset=rst 02_counter_bug.sv
FAILED assert counter_bug.p_range
cycle 0 : cnt=15 en=1 rst=1
...
cycle 11 : cnt=10 ✕ violates cnt <= 9
Double grant
Arbiter grants two masters in the same cycle — after one exact request pattern.
Full + empty
FIFO flags full and empty together on a push/pop at the wrap point.
Dropped handshake
Responder drops a request that rises during reset release.
Impossible state
State machine reaches the state everyone swore was unreachable.
Each of these is one sva-verify run away. When the tool says PROVED, no input sequence of any length triggers it. When one exists, you get the run — as a timing diagram, a waveform, and a replay testbench for the tools you already use.
Only in Giolit
Certificates. Margins. Nobody else ships either.
Proof certificates
Evidence your customer can check.
Invariant
In your signal names — holds at first edge, survives every cycle, excludes failure.
PDF certificate
Proofs, waveforms, replay testbenches — signed under your license, opens directly.
SHA-256 statement
Hashes of every design + evidence file, signed with your key.
One-script check
Your customer verifies everything without our tool — and without trusting it.
Inv: b = a ∧ 0 <= b <= 12000000
12M counter values covered by three lines — case split on $initstate, reset, running.
Real proof: lockstep.a_same, document GIO-SVA-94B352394746
Safety margins
A proof says it holds. The margin says by how much.
level <= 4'd12
Never exceeds 9 — margin 3 of 13 values.
##[1:6] ack window
Always answers in exactly 3 cycles — margin 3 cycles of 6.
Giolit Safety Resilience Score: the weakest bound sets the score. High score means headroom against future edits. Zero margin: any change toward the bound turns the verdict.
Real output: sva-verify --reset=rst --margins 11_margins.sv · document GIO-SVA-9564A1822018
Evidence
Measured against SymbiYosys and EBMC.
Same designs, same 20-second budget, every result reproducible from the trial package. This is the chart from the product poster — with the numbers behind it.
Measured, not marketed
All 231 designs with a known answer.
| Suite | Giolit | SymbiYosys | EBMC 6.0 |
|---|---|---|---|
| EBMC regression suite, of 168 | 163 | 55 | 114 |
| SymbiYosys examples, of 63 | 56 | 49 | 46 |
| TACAS 2016 bit-level netlists, of 12 | 4 | 7 | 6 |
| Wrong answers, on 340 properties | 0 | – | – |
| Proof certificate · Safety margins | ✓ · ✓ | – · – | – · – |
Same 20s budget per design for every tool; SymbiYosys with abc pdr, EBMC with a portfolio of its engines (k-induction, IC3, BDD, bounded). EBMC and SymbiYosys decide more of the bit-level TACAS 2016 netlists — their home turf. Every result is reproducible from the Tool Comparison and the results/ folder in the trial package.
Head to head
The only one that hands you the proof.
Only sva-verify backs every proof with a signed certificate — and only sva-verify measures the safety margin. That is not our slogan; it is the measured comparison table from the trial package.
| Capability | Giolit SVA 1.0 | SymbiYosys | EBMC 6.0 | Jasper / VC Formal |
|---|---|---|---|---|
| Designs decided (231 known-answer, same 20s budget) | 219 | 104 | 160 | not measured |
| Wrong answers on 340 properties | 0 | not scored | not scored | not published |
| Signed proof certificate — invariant in your signal names | ✓ | – | – | not advertised |
| Safety margins + 1–5 star Resilience Score | ✓ | – | – | not advertised |
| Covers + liveness decided in the same run | ✓ | separate, limited | engine per run | varies |
| In-house engines — no external solver to install | ✓ | ABC + SMT | SAT + opt. SMT | proprietary |
| Reproducible bundle in the trial (results + reproduce.sh) | ✓ | – | – | – |
| C++ SDK with client examples | ✓ 8 clients | – | – | varies |
| Runs fully offline, RTL never leaves your machines | ✓ | ✓ | ✓ | ✓ |
Measured rows: same designs, same 20s budget; commercial tools were not measured — the Tool Comparison excludes them (no Verific front-end available), so we claim nothing there. Ask any vendor for the same signed, rerunnable evidence bundle — then rerun it.
Example certifications
Real certificates. Signed and licensed — generated this week.
Proof you can hand to an auditor — or the exact failure, step by step, never a false alarm. These four were generated under professional license GIOLIT-PRO-2026-000001: a margins proof, a caught bug, a 6-file SoC integration, and a 12-million-state lockstep proof. Signed content, protection removed so every PDF opens right in your browser.
Detail: each bundle carries the PDF + results.json + proof.json + sources + reproduce.sh; failures add the VCD waveform and replay testbench.
PROVED
Margins block — proved with safety margins
2 PROVED / 0 failed · 0.4s · 11_margins.sv · 5 pages
margin 3 of 13 ★★★☆☆ · ##[1:6] margin 3 ★★★★★ · Score ★★★☆☆
Document GIO-SVA-9564A1822018 · signed · license GIOLIT-PRO-2026-000001
Download PDF
FAILED
Counter bug — found in 12 cycles
1 FAILED with trace + VCD + replay · 0.3s · 02_counter_bug.sv · 5 pages
cycle 11: cnt=10 violates cnt <= 9
Document GIO-SVA-785AAA26C149 · signed · license GIOLIT-PRO-2026-000001
Download PDF
PROVED
SoC integration — 7 files, one certificate
25 PROVED + 6 COVERED · 7 files · 31 properties · 21 pages
2 counters + 2× depth-16 FIFO + pipelines + buffer + margins
Document GIO-SVA-2CAD57A4AC96 · signed · license GIOLIT-PRO-2026-000001
Download PDF
PROVED
Lockstep pair — 12M states, 3-line proof
2 PROVED / 0 failed · 1.5s · 10_lockstep.sv · 5 pages
Inv: $initstate ∨ (a=b=0) ∨ (0≤b≤12M ∧ b=a)
Document GIO-SVA-94B352394746 · signed · license GIOLIT-PRO-2026-000001
Download PDFProduct brochure — 4 pages
Proof story · features · benchmarks · services
The whole pitch in one PDF: why simulation misses the expensive bugs, what each feature does for you, the measured comparison, and verification services.
Download brochureProduct poster — 1 page
Flow diagram · one command · benchmark chart
The single-page sales sheet this page is built from: the three-engine flow, the one command, certificates and margins, and the 219-bar benchmark chart.
Download posterWhat it checks
Every property, one honest verdict.
Each assert, assume, cover and immediate assertion is decided on its own cone of influence — with the method and cause recorded. Covers matter as much as assertions: an assertion is trivially true on a design that can never reach the interesting states.
SVA as written: ##[m:n] [*] [→] |-> |=> s_eventually $past $stable — plus hierarchy, parameters, generate, interfaces, packages, memories and bind.
What it handles
- SVA sequences and properties:
##[m:n], [*], [->], |->, |=>, until, … - Liveness:
s_eventually, k-liveness proofs, lasso counterexamples - Assumptions, covers, immediate assertions,
$past, $stable - Hierarchy, parameters, generate, interfaces, packages, bind
- One global clock or exact multi-clock semantics
- Every engine built in-house: no external solver
No run of the design violates the assertion. A proof, not a test result — backed by an inductive invariant or exhaustive exploration.
Some run violates it. You get the run cycle by cycle, as a VCD waveform and a self-checking replay testbench.
This interesting scenario can happen — witness run included. Covers prove your assertions are not vacuously true.
This cover can never happen: dead logic, or assumptions that over-constrain the inputs. Found before it hides a bug.
A liveness goal is reached on some run (witness shown) but not proved for every run. A hint, not a verdict.
Neither proved nor refuted within the time budget. The reason is printed — plus the standard remedy ladder.
Learn in an afternoon
11 tutorial designs. Each runs in seconds.
First proof: wrap counter, 3 PROVED + 1 COVERED in 0.1s
Reading a counterexample: wraps at 10, FAILED in 12 cycles
Memories + pointer invariants: 5 PROVED + full COVERED
When the property is wrong, not the design: fairness fixed
Timing windows ##[1:3]: in-time PROVED, off-by-one FAILED
Enum FSM: never-both-green PROVED, seeded bug FAILED
Generate + hierarchy: data-width reduction -G W=2
Assumptions: constrained inputs PROVED, unconstrained FAILED
s_eventually: round-robin PROVED, starvation lasso FAILED
Deep proof: 24-bit pair, 3-line invariant, both PROVED
Margins + Resilience Score from one --margins run
socbig_top.sv
Our 7-file SoC integration: 2 counters, 2 depth-16 FIFOs, pipelines, buffer, margins — 25 PROVED + 6 COVERED, 21-page certificate. Our largest verified program — yours can be next.
Fits the way you work
A command, a library, a sign-off gate.
$ sva-verify --reset=rst --timeout=600 --json=sva.json rtl/*.sv
case $? in 0) echo all proved;; 1) echo failures: see sva.json;; esac
$ sva-verify --property fifo.a_ptr_sync --report=cert rtl/*.sv
Exit 0
all proved
Exit 1
failures found
Exit 2
undecided
Exit 3/4
usage / license
C++ SDK — formal becomes part of your flow
libgiolit_sva, _report, _license, _frontend, _backend. Eight client examples ship in the trial — each token is one run:
Assumptions + covers: constrain inputs, prove guarantees, catch over-constraining.
Multiclock: one global clock by default, exact edge semantics with --multiclock.
Hierarchy at scale: parameters, generate, interfaces, packages, bind, memories.
Offline by design: no solver to install, no network, no upload — Linux x86-64.
Services: Giolit engineers write assertions from your spec and deliver proofs + certificates.
Trial terms
System requirements and trial terms: Ubuntu 24.04, 1000 runs, 50 days.
The trial (giolit-sva-verifier-1.0.0-trial.tar.gz) allows 1000 runs within 50 days on one Linux x86-64 computer — Ubuntu 24.04 LTS, LLVM/Clang 18, libc6-dev, libssl3 (LuaLaTeX + qpdf for PDFs). It includes sva-verify, the C++ SDK with 8 client examples, 11 tutorial designs, 218 benchmark verifications with known answers and every result bundle. sva-verify --license shows runs and days left without using a run. Trial PDFs are watermarked and unsigned.
FAQ
SystemVerilog (SVA) Verifier FAQ: proof, margins, trial.
Short answers to the questions every team asks before trusting a formal tool — what PROVED means, what the stars mean, and what the trial includes. No question assumes you already do formal.
What does PROVED actually guarantee?01+
That no input sequence — of any length, from any start state — can violate the assertion, under the documented model (your files and flags, top and parameters, --reset, one global clock unless --multiclock, your assume properties, X/Z treated as 0/1, async resets at the edge). The guarantee is backed by an inductive invariant written in your own signal names, printed in the certificate and checkable by hand.
We only simulate today. Where do we start?02+
Install the trial, copy the 11 tutorial examples, and run sva-verify --reset=rst 01_counter.sv — ALL ASSERTIONS PROVED in 0.1s. Then run 02_counter_bug.sv and watch the exact 12-cycle failure. Bring one small block with 2–3 assertions next; keep simulation for everything else and let proof own the critical properties first.
Do we have to rewrite our SVA?03+
No. The verifier reads IEEE 1800-2017 SystemVerilog with its assertions as they are — sequences, |->/|=>, $past/$stable, disable iff, assume/cover, checkers and bind — via the slang front-end. Properties can live in the design or in a separate file bound with bind.
What happens when a proof fails?04+
You get the failing run cycle by cycle (cycle 0 is the first clock edge, only changed signals printed), the same run as a VCD waveform for GTKWave, and a self-checking replay testbench that fails in Verilator or your simulator in minutes. Check the property first — most first failures are wrong properties, missing resets, or free inputs that need assumptions.
What is the Safety Resilience Score?05+
With --margins, every numeric bound and latency window is tightened step by step and re-proved until one fails; the distance is the margin. The weakest bound sets the 1–5 star score (≥50% five stars, ≥25% four, ≥10% three, >0 two, 0 one star). High score means headroom against future edits; zero margin means any change toward the bound flips the verdict.
How do assumptions and covers fit?06+
assume constrains inputs — state what neighbours promise, and only about inputs. cover proves interesting scenarios can actually happen; an expected COVERED that comes back UNREACHABLE means dead logic or over-constraining assumptions, caught before they hide a real bug. Assume about inputs only, cover what matters.
C Program Verifier or SVA Verifier — which do we need?07+
C code (firmware, drivers, HAL, multi-file projects) goes to the Program Verifier at /verifier; RTL blocks with SystemVerilog assertions go here. Chip teams commonly use both: SVA proofs for the hardware, C proofs for the software running on it.
What is in the trial?08+
giolit-sva-verifier-1.0.0-trial.tar.gz: sva-verify plus libraries, the C++ SDK with 8 client examples, 11 tutorial designs, 218 benchmark verifications with known answers and every result bundle (console output, results.json, reproduce.sh), Tutorial, Product Poster, Tool Comparison, README and License Terms. 1000 runs within 50 days on one Linux x86-64 computer (Ubuntu 24.04, LLVM/Clang 18). Trial PDFs are watermarked and unsigned; sva-verify --license shows runs and days left for free.
Comparing with simulation, SymbiYosys, EBMC and commercial tools+
Why not just simulate more?
More simulation still samples: the next bug hides in the next unsimulated pattern. Proof ends the treadmill for the properties that matter — and every failure replays in your simulator as a waveform plus testbench, so nothing you built is wasted.
What about SymbiYosys and EBMC?
Strong open tools — and the scoreboard is public: 219 vs 160 vs 104 on the same designs with the same budget, 0 wrong answers on 340 properties, every result rerunnable from the trial package. They give verdicts; Giolit adds the signed invariant certificate, the margins and stars, covers with liveness in one run, and support.
And JasperGold / VC Formal?
Not measured here — and we will not claim a win we did not measure. What only Giolit advertises in one run: full SVA with signed checkable certificates, margins with stars, in-house offline engines, a reproducible public benchmark pack, and a C++ SDK. Ask any vendor for the same bundle — then rerun it.
The same proof idea covers your firmware: the Giolit Program Verifier proves C projects free of run-time errors — overflow, memory safety, threads.
Commercial licensing
See your own block proved — start free
Send us a block and its spec: we write or review the assertions with you and show the first proof — or the first run that breaks it. Start with the free 1000-run trial, or talk licensing for your team and CI.