Every design RTLPreCheck has analyzed, with full metrics.
7 IP blocks from the lowRISC silicon root-of-trust SoC integration: Access Control, ASCON crypto, DMA, Key Manager DPE, Mailbox, SoC Debug Control, SoC Proxy. 59 modules. Input: SystemVerilog only. 27 minutes compute, zero counterexamples.
| IP Block | Modules | Proven | Intent | Actionable |
|---|---|---|---|---|
| Access Control | 2 | 47 | 0 | 0 |
| ASCON Crypto | 5 | 388 | 10 | 5 |
| DMA | 2 | 123 | 6 | 5 |
| Key Manager DPE | 2 | 144 | 8 | 10 |
| Mailbox | 8 | 378 | 14 | 0 |
| SoC Debug Control | 3 | 149 | 8 | 5 |
| SoC Proxy | 2 | 86 | 3 | 0 |
| Shared Primitives | 35 | 751 | 47 | 17 |
87 of 87 structural contract edges discharged. Every cross-module boundary in the design has a proven structural guarantee on the upstream side that satisfies the downstream input requirement.
368 total discharged — 87 structural + 24 cone-of-influence + 257 passthrough
Guard closure: 111 / 139 (79.9%)
12 external inputs — boundary signals driven from outside the analyzed scope. These are the system-level assumptions a SoC integrator carries, not gaps.
Compositional proof at SoC scale. Module-level proofs are not enough — the value comes when their guarantees compose across boundaries. RTLPreCheck produces the full bipartite map: every edge, every family pair, every discharge status.
The tabs below summarize results by pattern and family rather than listing every individual SVA — a single row like “T1/T2 share register family (24 props)” represents 24 assertions following the same reset/update/stable template. This keeps the page readable when a single module proves over a hundred properties. For the full per-property output, machine-readable verification matrix, or a plug-and-play SVA bundle for JasperGold, VC Formal, or other formal solvers, contact taylor@rtlprecheck.com.
All 2066 solver-verified properties across the analyzed modules. 1,552 single-cycle (safety implications, X-checking, parameter constraints) plus 514 temporal (guarded updates, hold conditions, arithmetic updates, liveness, handshake stability). Click a module to expand.
96 verification candidates RTLPreCheck identified from structural analysis. Engineer provides design intent and writes the final assertion. 20 CRITICAL (functional correctness, data integrity) and 76 REQUIRED (protocol compliance, initialization).
42 output signals with zero functional coverage and no X-checking. Logic drives them but no proven assertion covers their behavior. Real verification gaps.
750 informational signals — not verification gaps. Flagged for transparency. An engineer can upgrade any signal to actionable if functional coverage is needed.
Have X-propagation checking but no functional property. Concentrated in CSR adapter outputs (tl_o.d_* sub-fields), interrupt outputs, FIFO depth/error signals, and SRAM arbiter outputs.
Wire-throughs, struct sub-fields, CSR boilerplate. Coverage exists in child modules or these are non-driven informational ports.
Run ID 2026-04-30T08-51-00 · Z3 unbounded k-induction · 27 min compute · 0 counterexamples
130 primitive modules from the lowRISC silicon root-of-trust. Arbiters, FIFOs, counters, alert/escalation protocol, SECDED encoders, LFSRs, edge detectors. Input: SystemVerilog only.
33 Solver-Verified — Z3 proves OT's assertion follows from RTLPreCheck's facts
14 Discovered — intent candidate covers same signals and goal
21 Flagged — coverage scanner explicitly flags the gap
13 Covered Signals — proven properties exist on same signals
81 of 81 design RTL assertions accounted for. 100% coverage visibility.
2 additional OT assertions reference FPV testbench signals not in design RTL — excluded from scope.
All 2327 solver-verified properties across 104 modules. Click a module to expand.
All 136 design intent candidates across 53 modules. Specific signals, specific properties, specific structural evidence.
All 493 output signals with zero functional coverage — explicitly flagged. 7 on the 13 cross-checked core modules; 493 across the full 104-module bench (mostly wire-throughs, struct ports, and auto-generated CSR outputs).
Proven assertion set with solver certificates · Intent candidate report with specific signals · Coverage completeness map for all signal classes · Contract edges and boundary closure data · Per-module diagnostic barcodes for every failure · Deterministic output — same RTL in, same results out
Channel Data Processor from NVIDIA's Deep Learning Accelerator. LUT-based activation functions, floating-point conversion, and post-processing pipeline.
124 modules analyzed across the full CDP hierarchy — 2,023 registers, LUT register banks (333 address-decoded storage elements), HLS floating-point arithmetic libraries (FP16, FP17, FP32 multipliers, adders, converters), interpolation units, NaN detection, and data conversion pipeline. Same binary that verified CDMA. Cold start, zero configuration, reproducible every run.
CDMA moved data without transforming it — 0/0 data signal properties. CDP transforms data through LUT-based activation functions and floating-point conversion. 16/16 data signal properties verified at 100%. RTLPreCheck generates and proves structural properties on data-carrying signals, not just control flow.
41 of 51 memory index bound properties proven. The remaining 10 involve multi-level pointer chains in the LUT control unit where the PDR/IC3 engine is needed to close the induction gap. K-induction alone cannot prove these — the base case holds but the induction step requires an invariant the bounded prover cannot discover. This is a solver limitation, not an RTLPreCheck limitation.
405 unique contract edges discharged across 124 modules. Port connections validated across the full hierarchy (100% netlist completeness). External inputs cataloged as integration boundary candidates. Zero manual assume-guarantee pairs. Port matching over RTL wiring topology using structural geometry. Validated against Slang elaborated IR.
Convolution DMA from NVIDIA's Deep Learning Accelerator. Orchestrates all data movement between external memory and the compute engine.
63 modules analyzed across the full CDMA hierarchy — 5,883 registers, weight/feature/pixel data channels, shared buffer management, DMA mux, and multi-phase sequencing. Cold start, reproducible every run. 940 port connections validated across 3 hierarchy levels (100% netlist completeness). Data plane is N/A because CDMA moves opaque data without transforming values.
Every property was generated from RTL structure alone and proven via k-induction. No specifications, no bind files, no testbench.
| Module | Property Type | Signal / Anchor | Result |
|---|---|---|---|
| cklnqd12 | Signal Activity | Q | PASS_K |
| cklnqd12po4 | Signal Activity | Q | PASS_K |
| an2d4po4 | Signal Activity | Z | PASS_K |
Showing 55 of 373 properties. Full property table available on request.
3 sync integrity checks on dc, img_ctrl, and wg — no CDC sync chain structure found. 3 grant exclusivity checks on RAM logic modules — no arbiter grant signals. 2 decode coverage checks on img_pack and regfile — no structurally defensible decode enable. 1 deadlock freedom check on dc — no self-feedback path. 1 deadlock freedom check on wg — no self-feedback path. BINDING_FAILED = structurally inapplicable. Correct behavior, not a verification gap.
5 RAM logic modules and 1 FIFO module whose registers sit entirely within a parent module's cone of influence. The parent's solver-verified proofs cover the child. Compositionally proven through structural delegation.
Combinational dependency check on wg where the basecase passes at bounded depth but the k-induction step cannot close at unbounded depth. Stronger proof strategies (IC3/PDR) exist for this case.
236 unique contract edges discharged across 63 modules. 940 port connections validated (100% netlist completeness). 193 external inputs cataloged as integration boundary candidates. Zero manual pairs.
Full-featured SPI peripheral from the lowRISC silicon root-of-trust project
25 modules analyzed across the full SPI host hierarchy. Cold start, reproducible every run.
Grant exclusivity checks on modules that lack arbiter-style grant chains. BINDING_FAILED = structurally inapplicable.
876 contract edges automatically discharged across 25 modules. 238 Slang-elaborated wires validated (100% netlist completeness). Zero manual pairs.
SmallBoomV3 from Chipyard
268 modules received automated formal analysis. Every proof ran on an open-source formal solver.
We injected a 3-line microarchitectural bug into BOOM's reorder buffer. When an exception and a branch mispredict arrive on the exact same cycle, a latch permanently blocks the commit pointer. The processor hangs. Simulation never triggers it.
Caught in 17 seconds with a concrete counterexample trace. The formal solver explores every reachable state — no random stimulus, no directed tests needed.
9,084 contract edges automatically discharged across 266 modules. Zero manual pairs.