ZettaVerif
Zettabolt's static verification family. Four sign-off quality checkers, LINT, CDC, DFT and TXM, find RTL coding bugs, clock-domain bugs, testability problems and wrong timing exceptions without a single test vector. Catch them early, when they are cheap to fix, not after synthesis or tape-out.
WHY STATIC VERIFICATION?
Find bugs simulation can't see, before they cost a re-spin
Modern SoCs have hundreds of IP blocks, dozens of asynchronous clock domains, millions of scan flops and thousands of timing constraints. Simulation only finds what your testbench exercises, and STA trusts every timing exception you give it, even the wrong ones. Static verification analyses the whole design structurally and formally, so whole classes of bugs are found exhaustively and early.
- LINTIs my RTL clean, synthesizable and free of simulation–synthesis mismatches?
- CDCAre all my clock-domain crossings properly synchronized?
- DFTIs my design testable, and what fault coverage will I reach before DFT insertion?
- TXMAre my false paths and multicycle paths actually correct, or are they hiding real violations?
Where each checker fits in the flow
RTL Lint Checker (LINT)
LINT is the first line of defence for RTL quality. It checks every line of your Verilog and SystemVerilog against a comprehensive ruleset, so the code that reaches simulation, synthesis and your IP customers is clean, consistent and reusable.
How it works: four levels of checking in one run
- 1Parse → Syntax & lint checks
RTL is parsed; language and coding-rule violations are flagged.
- 2AST → Semantic checks
Declarations, usage, widths and connections are checked for meaning, not just syntax.
- 3Synthesize → Synthesizability checks
A fast built-in synthesis step finds constructs that won't synthesize, or will synthesize differently than they simulate.
- 4Netlist → Structural checks
The elaborated netlist is checked for structural issues such as combinational loops and undriven or floating nets.
Rule categories
Comprehensive checks
- A wide range of rulesets confirms RTL meets sign-off quality for syntax, connectivity, efficient synthesis, simulation and reuse.
- Dedicated design-reuse rulesets compatible with industry standards RMM (Reuse Methodology Manual) and STARC.
Ease of use
- Supports Verilog, SystemVerilog and mixed-language designs.
- Reads standard file lists (.f), include paths and defines, so it drops into existing flows.
- Tcl-shell commands make scripting and waiver-list customisation easy.
User-friendly GUI
- Quick message filtering and probing.
- Jump from a violation straight to the source line and schematic.
- Expandable fan-in/fan-out cones for logic tracing.
- Potential error locations are labelled for quick analysis.
Clock Domain Crossing Checker (CDC)
Signals crossing between asynchronous clocks can go metastable, lose data or arrive out of order. These bugs are intermittent, hard to reproduce in simulation and often found only in silicon. CDC finds every crossing in your design and confirms each one is correctly synchronized.
How it works
- Read in library and check.
- Support SDC
- Constraint syntax check
- Constraint consistency check
- Setup checks
- Integrity checks
- Sync/Async checks
- Coherency checks
- Setup checks
- Integrity checks
- Sync/Async checks
- Coherency checks
Issues found are analysed and fixed in RTL, then CDC is re-run until the design is clean and ready for sign-off.
Check categories
Comprehensive checks
- Built-in rules check that CDC constraints are complete.
- Setup, integrity, synchronization and structure rules give sign-off quality results.
Ease of use
- High performance for fast sign-off on large designs.
- Reuses your existing SDC constraints to extract clock domains, with no separate CDC setup language.
- Clock and reset inference fills in domain information automatically.
- Object-oriented messages produce a low-noise report.
- Tcl-shell commands for scripting and waiver lists.
User-friendly GUI
- A GUI built specifically for CDC debug.
- Quick message filtering and probing.
- Locate problem objects in the circuit diagram instantly.
- Key circuit attributes, such as clock domain, are shown visually.
- Incremental GUI with expandable fan-in/fan-out cones.
Design-for-Test Checker (DFT)
Testability problems such as blocked scan chains, uncontrolled clocks and resets, or black boxes, usually surface only after scan insertion or ATPG. Fixing them then means going back to RTL, re-synthesizing and re-inserting. DFT checks testability at RTL, estimates the fault coverage you will reach, and tells you which fixes will raise it, before DFT insertion starts.
Where it fits: across the whole test flow
How it works
- 1Read the design and set up test mode
Read libraries and RTL or netlist, then define clocks, test clocks, test signals, scan-enable and scan chains in a short Tcl constraint file.
- 2Run the rule checks
About 300 rules check clocks, resets, scan, topology, latches, RAMs, tristates and connections. Results are graded ERROR, WARN or INFO.
- 3Estimate coverage and testability
Stuck-at and transition fault coverage and test coverage are calculated, with controllability and observability analysis showing exactly where and why faults can't be tested.
- 4Fix in order of impact
A coverage audit lists each problem with the fault and test coverage you would reach after fixing it, so you fix the biggest wins first.
Check categories
Comprehensive checks
- Testability, stuck-at and transition fault analysis, scan analysis, BIST design analysis and test-compression design analysis.
- Custom checks on clock, reset, test and scan-enable signals. Change the circuit's test state without changing the design.
- A DFT-friendly RTL can cut the design cycle of large IPs by as much as half, with far fewer RTL → DFT → RTL loops.
Fast and scriptable
- A multi-threaded engine runs checks in parallel, so run time drops with every thread you add.
- Run interactively, from an init script that drops you into the shell, or as a batch script that exits when done.
- Shallow learning curve: engineers pick up DFT rules and concepts as they use the tool.
User-friendly GUI
- Violation, design and file trees, with the full rule description one click away.
- Incremental schematic shows exactly where a violation sits in the design.
- Pin, port, instance and net properties on click, plus customisable schematics.
- Search everywhere: rules, objects, schematics and messages.
- "Open in source" jumps straight to the RTL line to fix.
Timing Exception Master (TXM)
STA assumes every path must complete in a single clock cycle. Timing exceptions, meaning false paths, multicycle paths and max/min delays, tell STA where that assumption doesn't apply. But STA can't check whether an exception is correct. It skips every path it is told to skip. TXM is a formal verification tool built for timing exceptions. It proves each one is correct, or shows you the counterexample.
How it works
- 1Timing-exception LINT
The first gate. It flags non-standard SDC, wildcard and path-syntax errors, undefined clocks, and overlaps where the same path gets conflicting exceptions.
- 2Path existence pre-check
Confirms every constrained path actually exists. It flags dangling constraints and paths blocked by black boxes, combinational loops, multi-driven nets or set_disable_timing, and identifies CDC and constant-value paths.
- 3Formal proof
The RTL and SDC are turned into mathematical assertions, and a satisfiability solver proves each false path is truly false and each multicycle path truly meets its cycle count. Any failure comes with a counterexample waveform.
- 4Glitch check
Proves that relaxing the path can't let a glitch propagate in practice. This applies to false paths and to the extended hold window of multicycle paths.
Check categories
Full coverage
- Three engines with 25+ checks: false paths, multicycle paths and timing-exception LINT.
- Covers combinational and sequential false paths, gated clocks and synchronous clocks with any phase difference.
Ease of use
- Reads standard SDC, including files pulled in with the source command. Unsupported options are flagged, not silently dropped.
- A clock-relationship report shows Sync, Async, physically exclusive and logically exclusive clocks, with SDC line numbers. Export it to CSV or HTML.
- Tcl shell and parameters to tune limits, glitch checks and sequential depth.
Sign-off confidence
- Complements PrimeTime and Tempus with a deterministic "proof of no omission".
- Every message points to the SDC file and line number.
- GUI with incremental schematics to debug counterexamples.
Ready to catch RTL, CDC, DFT and timing-exception bugs before tape-out?
