Technical blueprint
Technical blueprint
Everything a senior verification engineer needs to vet ChipVerify AI before bringing RTL near it. Three pipelines — Design, Verify, Implement — over a shared engine layer of real open-source tools, feeding honesty-graded evidence. Every verdict is graded (advisory · evidence · record · inventory · tool); never a false clean, pass, proof, or foundry sign-off.
Multi-tenant SaaS · CI-native · PostgreSQL row-level-security tenant isolation · optional SSO/OIDC
System diagram
FastAPI hub, two-queue workers, hardened EDA sandbox.
Browsers, CLI, and the GitHub Action all hit FastAPI over REST. Jobs split by cost class onto Redis/RQ workers, run inside a cap-dropped, rlimit-bounded sandbox, and return artifacts (VCD, reports, readiness summaries) the dashboard can render.
Stack
Built on tools you trust.
Three areas where the version pin and the limits matter: the open EDA pipeline that produces the evidence, the worker sandbox that runs every external tool, and the user-facing feature surface that turns raw tool output into one decision. No vendor EDA license keys; no proprietary lock-in below the dashboard.
EDA pipeline
- Parsers — Slang / pyslang v2 (active default), regex v1 (fail-soft fallback), Surelog/UHDM v3 (readiness path detected; JSON-to-AST adapter in flight)
- Lint — Verible (chipsalliance, pinned static binary) + optional svlint as second-opinion lint only when the binary is executable, both normalized into the same issue evidence
- Simulation — Icarus 12 (iverilog -g2012 -Wall) and Verilator 5 with native line/branch coverage and waveform-to-source debug
- Synthesis lint — Yosys 0.64 (oss-cad-suite) for area/gate estimates, sv2v 0.0.13 for SystemVerilog → Verilog-2005 compatibility, netlistsvg 1.0.2 for schematic highlight
- Formal — SymbiYosys (main branch, tracking yosys 0.64 (oss-cad-suite)) + Z3 for BMC, k-induction, and cover; RISC-V RVFI / riscv-formal scaffold (no ISA-compliance claim)
- Equivalence — EQY via pinned oss-cad-suite (2026-05-06 build, SHA-pinned, isolated under /opt) so the plugin ABI matches its bundled Yosys
- Mutation — MCY for mutation planning and bounded execution when a testbench is supplied
- Reference model — Spike (riscv-isa-sim, master 20feb9c2bf2a, post-v1.1.0) runs supplied RISC-V ELFs with bounded timeout and commit cap; ISA reference trace, not RTL co-sim
- Cocotb — scaffold generator + bounded runnable probe gated on cocotb package, cocotb-config, make, and simulator detection
- Readiness engines — OpenSTA readiness + real multi-corner pre-signoff STA, SystemRDL/PeakRDL preview/fail-soft fallback, CIRCT/firtool FIRRTL ingestion preview, SystemC/Verilator --sc compile-plan readiness, Surfer external waveform handoff
- Pre-flight — FuseSoC .core source-list import (filesets/targets), SDC sanity, timing/constraint readiness, DFT readiness, FPGA portability, IP provenance/SBOM-lite
- Evidence analyzers — synth-vs-sim mismatch, reset / X-convergence, timing-exception candidates (false-path/multicycle/static, with assumptions), macro/wrapper-vs-Liberty/LEF contract, UPF-vs-RTL low-power consistency, waiver revalidation — deterministic evidence, never proofs
Sandboxing & isolation
- Container model — worker runs in dedicated chipverify-worker / chipverify-worker-fast images; JOB_ISOLATION=process is the default, container nesting is opt-in via JOB_ISOLATION=container
- Process limits — subprocess invocations wrapped in rlimits: CPU seconds, address space (AS), file size (FSIZE), and process count (NPROC) — every tool run is a hard wall, not a hint
- Capabilities — cap_drop: ALL on the worker container; no kernel capabilities even before the rlimits apply
- Privileges — no-new-privileges enforced; the worker process cannot setuid or escalate even if a tool subprocess tries
- Filesystem — read-only root FS for the worker container; tmpfs workdir mounted under /var/lib/chipverify/work, cleared on job completion
- PID containment — pids_limit on the container so a fork-bomb in a user-supplied testbench can't starve the host
- Source-safety scan — pre-execution macro-expansion check rejects file-system reads (`$readmemh` to /etc/), unsafe `$system` / `$display` patterns, and deep include nesting before any tool runs
- Rate-limit fail-closed — public unauth endpoints (tt-scan, share-read, password-reset, early-access, quick-analyze) reject when the Redis-backed limiter is unreachable instead of degrading to a per-process bucket
- Atomic billing — record_usage / check_limit are transactional so a failed tool run can't double-bill or skip the cap; cluster-wide via Postgres rows
- Tenant scoping — every persisted row carries tenant_id; cross_tenant_view + the request middleware are the only paths that ever read across tenants, and PostgreSQL row-level-security policies enforce that isolation at the database layer as defense-in-depth
Tool features
- Unified verification score — 0–100 composite of multi-engine evidence with confidence band, 17-tag correlation, and a recommended action verdict
- Closure board — verification plan + versioned waivers + fix-verify loop + schematic highlight overlay; tracks objectives kanban-style
- Evidence maturity — every finding tiered HEURISTIC / PREVIEW / RELIABLE across functional, test-quality, private-policy, and evidence axes
- Per-rule precision badges — calibrated from the outcome ledger (fixed, waived, ignored, false-positive, recurring) so reviewers see how often a rule has been right historically
- Quality tab — area + gate estimate, sv2v compatibility, MCY mutation evidence, RTL security (CWE), VHDL/GHDL readiness
- Advanced engineering (Quality tab) — area/gate estimate, sv2v compatibility, MCY mutation execution, RTL security (CWE), and VHDL/GHDL readiness
- API-forward readiness — RISC-V/RVFI readiness, Spike ISA reference trace, SystemRDL preview, CIRCT readiness, SystemC planning, Surfer handoff metadata, timing/constraints, DFT, IP provenance/SBOM-lite, and FPGA portability have backend services and REST endpoints; some surface only through the API. OpenSTA pre-signoff timing and the floorplan advisor are mounted dashboard panels (Timing and Implement views)
- Waveform intelligence — heuristic VCD summary (likely clocks, resets, grouped signals, transaction markers, protocol hints) instead of a raw text dump; in-browser VCD viewer with 50 MiB cap; GTKWave / Surfer handoff for larger captures
- Auto-docs + register-map — datasheet JSON / Markdown / PDF + registers.json + C header + Python MMIO + Markdown via SystemRDL/PeakRDL
- Protocol packs — APB, AXI-lite, UART decoders with structural checks, SVA monitors, coverage goals, and transaction decoders
- PR-review preview + CI gate — .chipverify.yml policy + GitHub Action + comment-bot; commercial log import for VCS/Xcelium/Questa
- Project lifecycle — project-intelligence map, regression intelligence, optimization advisor, history with staleness flags, HMAC-signed share links + public SVG trust-score badge
Pipeline split
Two queues, one hub. Heavy jobs never starve interactive ones.
Every job is enqueued through Redis/RQ, but ChipVerify routes it onto one of two pools based on expected cost. Fast workers handle analyze, lint, simulation, and github-import. Heavy workers handle synth_lint, formal, assertions, equivalence, lec, cdc, batch_scan, and regression_farm.
The reason for the split is operational, not theoretical: a multi-minute Yosys synth, sby run, or mutation execution cannot be allowed to block the dashboard's next interactive analyze. Separate worker pools, separate concurrency budgets, separate timeouts.
Capability map
Current engines, readiness checks, and evidence layers.
The public architecture page mirrors the product boundary: deterministic engines and advisory readiness checks are surfaced together, but signoff claims stay out of scope.
Execution and open EDA
The worker image runs deterministic open-source engines first, then rolls their evidence into the same project score and report surface.
- Icarus 12 and Verilator 5 simulation, native line/branch coverage, VCD artifacts, and waveform-to-source debug
- Yosys 0.64 synthesis lint, area/gate estimates, sv2v compatibility, netlistsvg structure, and EQY equivalence (oss-cad-suite, SHA-pinned)
- SymbiYosys + Z3 formal checks, RISC-V RVFI / riscv-formal setup readiness, Spike (master 20feb9c2bf2a) ISA reference traces for supplied ELF programs, plus MCY mutation planning and bounded execution when a testbench is available
- Verible plus optional svlint as a second lint opinion normalized into ChipVerify issue evidence
- Cocotb scaffold generator plus a bounded runnable probe gated on cocotb-config detection — produces a transcript, not a passing-test claim
- CIRCT/firtool preview for emitted FIRRTL and Chisel handoff, plus SystemC/C++ compile-plan readiness around Verilator --sc
- FuseSoC `.core` source-list ingestion (filesets/targets parsed; no dependency resolution)
Handoff readiness
New readiness checks are shift-left prechecks for engineering handoff. They are explicit about what they do not replace.
- OpenSTA (sta built from a pinned SHA) checks Liberty/SDC/design inputs for readiness, then runs real multi-corner pre-signoff STA for worst setup/hold slack; it is pre-signoff, not foundry signoff
- Timing and constraint readiness flag wide combinational paths, deep decode cones, logic-derived clocks, missing clocks, and missing IO delays
- DFT readiness catches resetless state, multi-clock sequential blocks, internal high-Z, and generated-clock risks before scan handoff
- FPGA portability highlights vendor primitive lock-in, simulation-only tasks, fabric clocks, and non-portable initialization
- Surfer handoff prepares metadata and local launch hints for large waveform debug while keeping the built-in browser viewer for quick inspection; it does not host a Surfer session
Evidence and provenance
The closure layer now tracks more than raw tool output: it records confidence, maturity, provenance, and reviewer-facing rationale.
- IP provenance / SBOM-lite reports SPDX coverage, vendor or generated source markers, copyleft signals, and ownership evidence
- RISC-V formal readiness reports RVFI coverage, missing retire/register/PC/memory channels, and the upstream-check scaffold without claiming ISA compliance
- Spike ISA reference trace runs supplied RISC-V ELF programs with bounded timeout and commit caps; RTL-vs-Spike comparison is a future track
- Evidence maturity and rule precision calibrate analyzer trust from fixed, waived, ignored, false-positive, and recurring findings — every finding ships HEURISTIC / PREVIEW / RELIABLE tier plus the rule's historical precision
- Deterministic evidence analyzers — synth-vs-sim mismatch, reset / X-convergence, a timing-exception candidate workbench (false-path / multicycle / static, each with stated assumptions), a macro/wrapper-vs-Liberty/LEF pin-contract checker, UPF-vs-RTL isolation/level-shifter consistency, and waiver revalidation; all produce evidence to review, never asserted false paths, proofs, or signoff
- Waiver revalidation re-runs active waivers against the latest evidence so a waiver for a vanished or shifted finding is flagged stale instead of silently suppressing a real issue
- SystemRDL preview emits register docs, C header snippets, Markdown, and IP-XACT-style XML with PeakRDL detection and fail-soft heuristic fallback
- Commercial log import (VCS / Xcelium / Questa), private per-tenant rules, PR review comments, regression intelligence, and coverage-at-risk keep external signals in the same evidence model
User feature surface
What users actually see in the dashboard, on share links, and through the CI gate. Every entry maps to a backend service that is part of the current product surface.
- Closure board — verification plan + versioned waivers + fix-verify loop + schematic highlight overlay; tracks objectives kanban-style
- Unified verification score (0–100) with confidence band, 17-tag correlation, and a recommended action verdict per project
- Auto-docs — datasheet JSON / Markdown / PDF generated from the analyzer evidence, plus register-map exports (registers.json, C header, Python MMIO, Markdown)
- Protocol packs — APB, AXI-lite, and UART transaction decoders with structural checks, SVA monitors, and coverage goals
- Public surface — HMAC-signed share links, SVG trust-score badge for READMEs, GitHub Action + .chipverify.yml CI gate, and the PR comment-bot review preview
- Project lifecycle — project-intelligence map, regression intelligence, optimization advisor, and a history view with explicit staleness flags when inputs drift
Sandboxing & data privacy
Workers are bounded; tenants are isolated.
- Worker container with cap_drop ALL, no-new-privileges, a tmpfs workdir, and POSIX rlimits (CPU / AS / FSIZE / NPROC) applied per job. Process isolation is the default; per-job container isolation is opt-in.
- Default JOB_ISOLATION=process; =container is opt-in once a sidecar / rootless runtime is wired into the compose stack.
- Macro-expansion source-safety scan rejects $system, DPI-C imports, $readmem*, $writemem*, $fopen*, and unsafe `include paths before the parser runs.
- Tenant isolation via tenant_id filtering at the data layer, now backed by PostgreSQL row-level security policies that enforce the same isolation in the database itself (defense-in-depth, not a compliance certification); cross-tenant reads are blocked end-to-end, including in the report and artifact paths.
- Atomic billing (record_usage / check_limit) prevents per-tenant counter corruption under concurrent simulate / explain.
Parser-backend matrix
Slang AST in front, regex behind, Surelog on the readiness path.
| Backend | Default | Status |
|---|---|---|
| Slang / pyslang AST (v2) | yes | active |
| Regex subset (v1) | fallback | fail-soft only |
| Surelog / UHDM (v3) | no | readiness path detects the binary; JSON-to-AST adapter shipping in a follow-up |
Known limits
The constraints we publish on purpose.
This section is for the audit memo. We do not bury caps, preview-only paths, optional-tool paths, or readiness boundaries in fine print.
VCD output cap — 50 MiB
Capped at 50 MiB per simulation by RLIMIT_FSIZE. When the cap is hit, the run is marked truncated and the dashboard surfaces a notice.
Mitigations: narrow $dumpvars scope (e.g. $dumpvars(2, tb.dut)), shorten the simulated time window, or rely on the waveform-intelligence digest (likely clocks/resets, signal groups, transaction markers, advisory warnings) instead of full visual review.
Cocotb — scaffold plus bounded run probe
ChipVerify writes a Cocotb test file plus a Makefile pair tailored to the parsed RTL. The run endpoint checks for the Cocotb package, cocotb-config, make, and the selected simulator before execution.
The dashboard's advanced panel currently uses the safe runnable probe by default. Bounded execution exists behind the API, but full regression management is still outside the product boundary.
Surelog / UHDM v3 parser — readiness path
Readiness path only. The dispatcher detects whether the surelog binary is present on the worker, but the JSON-to-AST adapter has not shipped. The active backend today is the Slang / pyslang v2 parser.
Air-gapped on-prem — partial
Container images, the Compose overlay, the on-prem installer manifest (compose-base + compose-prod-overlay + Caddyfile + .env.example + DEPLOY.md + SECURITY.md + THIRD_PARTY_NOTICES.md + LICENSE), and the trust-pack evidence endpoint all ship today. Helm charts and a one-shot self-install installer are on the roadmap. Talk to us if you need self-install before then.
VHDL — readiness / analyze only
GHDL elaboration check on uploaded .vhd / .vhdl files. This is a readiness signal — full mixed-language Verilog/VHDL verification, GitHub-import filtering for VHDL, and FuseSoC manifest VHDL paths are not wired yet.
Spike — ISA reference trace, not RTL co-simulation
The Spike endpoint accepts a pre-built RISC-V ELF, runs the official riscv-isa-sim reference simulator with bounded timeout and retire cap, and returns structured commit-trace evidence.
Shape A does not compare the trace to RTL, run RISCOF, or claim ISA compliance. RTL-vs-Spike trace diffing and RVFI proof remain follow-up tracks.
MCY mutation coverage — heavy + needs a testbench
Mutation coverage now has a bounded execution path, not just planning. It still requires a working testbench that the mutated design can be diffed against, and each run is limited by mutant count, parallel job count, subprocess timeout, and worker rlimits.
Compute footprint is significantly larger than analyze / lint / sim. Treat MCY as an async engineering action, not a default-on gate for every upload.
sv2v — compatibility conversion, not signoff
Converts modern SystemVerilog constructs to Verilog-2005 so the open-flow tools (iverilog / yosys) can consume the design. The conversion is best-effort and not a guarantee of semantic equivalence — treat it as a compatibility layer, not a signoff path.
Area / gate estimate — early signal, not PPA signoff
Cell-count and gate-equivalent rollup from a Yosys synth pass. Useful as an early design-quality signal during RTL iteration; not a substitute for a real PPA flow with technology library, place-and-route, or static timing analysis.
OpenSTA — real pre-signoff STA + readiness
The sta binary is built from a pinned OpenSTA SHA in the worker image. The readiness gate checks Liberty, SDC, and design inputs; the timing endpoint then runs real multi-corner pre-signoff STA (synthesize → map → per-corner report_checks) and parses worst setup/hold slack and TNS.
It is pre-signoff timing on open educational/research PDKs — not foundry, customer, or vendor STA signoff, and not a PrimeTime/Tempus replacement.
SystemRDL / PeakRDL — preview and fail-soft fallback
SystemRDL support validates uploaded register specs and previews Markdown, C header, and IP-XACT-style metadata. PeakRDL and peakrdl-regblock are detected when installed, but the page remains honest when only the heuristic preview path is available.
CIRCT / firtool — ingestion preview only
CIRCT support detects FIRRTL, CIRCT MLIR, and Chisel source markers, then reports whether firtool is available for a bounded conversion preview. It is not a claim that ChipVerify elaborates Chisel projects, proves RTL equivalence, or signs off generated Verilog.
SystemC — harness and compile-plan readiness
SystemC support checks C++/SystemC source markers, SC_MODULE, sc_main, SystemC install hints, and Verilator --sc availability. It does not execute untrusted C++/SystemC workloads in the hosted cloud path.
Surfer — external waveform handoff
Surfer support prepares artifact metadata, local launch hints, and recommendations for large VCD/FST traces. The built-in browser waveform viewer remains the default quick inspection surface; ChipVerify does not host a Surfer session.
DFT readiness — pre-scan, not DFT signoff
DFT readiness flags resetless state, multiple clock edges in sequential blocks, logic-derived clocks, internal tri-state style, and mixed reset polarity. It does not replace scan insertion, ATPG, fault simulation, or foundry/customer DFT signoff.
FPGA portability — source-level precheck
FPGA portability catches vendor primitive lock-in, fabric clocks, internal high-Z, simulation-only system tasks, and non-portable initialization patterns. It is not vendor synthesis, implementation, bitstream, or timing validation.
IP provenance / SBOM-lite — not legal advice
Provenance checks report missing SPDX identifiers, likely vendor or generated sources, copyleft markers, source type, and ownership evidence. They help prepare security and legal review; they do not replace supplier due diligence or counsel review.
svlint — optional second opinion
svlint runs when the binary is available on PATH. Missing tools, timeouts, and startup failures are reported as engine status, not hidden behind the aggregate score.
EDA toolchain versions
Pinned in the worker image.
These come from backend/Dockerfile. Some tools are pinned (oss-cad-suite, sv2v, Verible, netlistsvg, Spike SHA, OpenSTA SHA); the apt-installed engines (iverilog / yosys / verilator / z3) track Debian and are not version-pinned, so exact versions can drift across image rebuilds.
- Icarus Verilog
- 12 · iverilog -g2012 -Wall
- Verilator
- 5 · native + line/branch coverage
- Yosys
- 0.64 · synthesis lint
- SymbiYosys
- sby main · BMC / k-induction / cover
- Z3
- apt latest · SMT backend
- riscv-formal / RVFI
- PATH/env-detected · readiness scaffold, no ISA signoff claim
- Spike / riscv-isa-sim
- 1.1.1-dev · pinned SHA 20feb9c2bf2a · ISA reference trace
- Verible
- v0.0-4053-g89d4d98a · lint / format
- svlint
- PATH-detected · executable second-opinion lint only when installed
- netlistsvg
- 1.0.2 · schematic highlight
- EQY
- oss-cad-suite pinned · equivalence
- sv2v
- v0.0.13 · SystemVerilog → Verilog-2005 conversion
- MCY
- oss-cad-suite · bounded mutation planning + execution
- GHDL
- oss-cad-suite · VHDL elaboration / readiness
- OpenSTA
- built from pinned SHA 17380215 (sta) · real multi-corner pre-signoff STA + readiness
- PeakRDL
- PATH / Python-detected · SystemRDL preview, heuristic fallback when missing
- CIRCT / firtool
- PATH-detected · FIRRTL conversion preview only, no equivalence claim
- SystemC
- pkg-config / SYSTEMC_HOME detected · compile-plan readiness only
- Surfer
- PATH-detected · external VCD/FST handoff, no hosted session
- Cocotb
- Python package / cocotb-config / simulator detected · scaffold + run probe
- oss-cad-suite
- pinned tarball · source for EQY / MCY / GHDL
Next step
Read the blueprint? Bring real RTL.
Closed beta. Free for individual designers and students. Team for chip startups and labs. Air-gapped Enterprise on request.