OpenCollate

Catch SoC collateral drift before tapeout.

OpenCollate builds one provenance-preserving design contract from RTL, implementation, constraints, power intent, register descriptions, circuit netlists, and package collateral. It then reports contradictions in design language. It is local-first, scriptable, and open source.

ERROR OC4001  uart/irq_o has conflicting directions: RTL, CDL, DEF, IP-XACT, LEF = output; Liberty = input.
  --> rtl/uart.sv:8:24 [rtl.default] = output
  --> lib/uart.lib:39:9 [liberty.tt] = input
  help: Correct the direction in the outlying collateral or the canonical contract.

Beta software: OpenCollate 0.3.0 is intended for evaluation, collateral review, and CI experiments. Its Python API, schema, and diagnostic surface can still change before 1.0. It is not a signoff tool and does not replace simulation, formal verification, STA, CDC/RDC, DRC, LVS, extraction, or implementation-tool validation.

Development improvements after v0.3.0

A current checkout additionally provides optional bounded Z3 Boolean checks beyond the default truth-table input limit; guarded Boolean obligations with replayable, content-bound receipts; complete frozen-snapshot drift review; and self-contained interactive HTML reports. These are not included in the older v0.3.0 release tag shown below.

python -m pip install -e ".[formal]"
opencollate formal check examples/formal/obligations.json --output receipt.json
opencollate formal replay examples/formal/obligations.json receipt.json
opencollate check --format html --output review.html
opencollate contract diff baseline.oc.json current.oc.json --output drift.json

See symbolic verification for enabling the optional backend on RTL/Liberty checks and its exact two-valued scope. See contract and HTML review for full snapshot coverage, incomplete-analysis exit statuses, and offline report controls. Public synthetic benchmarks and real-file regression tests document tested capability, not superiority over all proprietary tools or signoff qualification.

Install

OpenCollate requires Python 3.11 or newer.

python -m pip install "git+https://github.com/ajayasai/OpenCollate.git@v0.3.0"
opencollate --version

OpenCollate is not yet published on PyPI. To work from a checkout:

python -m pip install -e ".[dev]"

Thirty-second tour

Run the generated demonstration:

opencollate demo

Or run the repository’s synthetic, deliberately inconsistent UART across all thirteen supported view kinds:

opencollate check examples/uart/opencollate.toml

The full-stack example imports SystemVerilog, Liberty, LEF, CSV, IP-XACT, SystemRDL, declarative connectivity intent, SDC, UPF, a C register header, CDL, DEF, and experimental structural GDSII. It is expected to return status 1 with exactly OC4001, OC4301, and OC5003. See the UART walkthrough.

0.3.0 support matrix

“Structural” means OpenCollate imports facts needed for consistency checks; it does not implement the complete language or the analysis normally performed by its native tool.

View	0.3.0 Beta support	Deliberate boundary
Verilog/SystemVerilog	pyslang preprocessing, parsing, and elaboration; modules, ports, parameters, dimensions, includes, defines, hierarchy, and small continuous-assignment Boolean functions	No behavioral or sequential equivalence; unsupported ports and unresolved shapes remain explicit
Liberty	Libraries, cells, pins, buses, bundles, types, pg_pin, roles, directions, ranges, and small Boolean functions	Timing, power, noise, and characterization table contents are skipped
LEF	Macro/pin interface, direction, use, and declared bus naming	Geometry, vias, obstructions, and antenna/vendor properties are skipped
CSV	Component-pin and package-map profiles, configurable columns, ranges/per-bit rows, roles, directions, pads, balls, and signals	It is not a general spreadsheet importer; ambiguous identity columns must be mapped
IP-XACT	IEEE 1685 2009/2014/2022 components, ports, vectors/arrays, parameters, interfaces/port maps, memory maps, registers, and fields	No XSD validation, schema fetching, or external definition expansion
SystemRDL 2.0	Ordered explicit units through systemrdl-compiler; selected top, nested maps/regfiles, arrays, addresses, widths, access, fields, and resets	Perl preprocessing and source includes are rejected; no RTL/UVM/software/document generation or behavioral verification
Connectivity CSV	Required/forbidden transparent RTL paths across assignments, hierarchy, net aliases, and simple primitives, with collision-free escaped names, bit identity/reversal, known inversion, waypoints/exclusions, witnesses, cuts, and fail-closed tainted frontiers	Bounded static graph analysis only; no temporal, conditional, sequential, mode-aware, or formal proof
SDC	Non-executing Tcl tokenizer; static queries, clocks, generated clocks, I/O delays, false paths, and multicycle paths	Tcl control flow, arbitrary commands, and environment-dependent substitution are not executed
UPF	Non-executing structural subset for design/scope, domains, supplies, isolation, retention, level shifting, switches, and power states	It is not a UPF interpreter or power-intent signoff engine; dynamic Tcl is not executed
C register headers	Conventional base/address/offset and field position/mask/width/reset integer macros	No C preprocessor, conditional-build selection, compiler, or arbitrary macro execution
CDL/SPICE	Subcircuits, explicit pin metadata, connectivity, globals, models, M/R/C/L/X structure, and continuations	No simulation, parameter evaluation, device-model validation, or electrical equivalence
DEF 5.8	DESIGN, COMPONENTS, PINS, NETS, SPECIALNETS, placement, connectivity, hierarchy, and bus naming	Routes and geometry are skipped; DEF pins do not imply package-ball/die-pad mappings
GDSII (experimental)	Bounded native big-endian stream parsing for cells, inferred/selected tops, SREF/AREF hierarchy, transforms, and text labels; selected labels can become unknown-shape ports only through explicit layer/type filters	Polygon/path/node/box geometry is never materialized or verified; no DRC, LVS, extraction, connectivity inference, or implicit label-to-pin guessing

Read the exact supported syntax and limits. The installed build is authoritative:

opencollate capabilities

Every fact is known, unknown, unsupported, tainted, or not applicable. Parser recovery never turns an unestablished fact into an apparent pass.

What OpenCollate checks

The 74-rule 0.3.0 catalog covers:

• Configuration, parser completeness, unsupported constructs, and tainted scopes.
• Component and port identity, inventory, direction, role, shape, range, and ordering.
• Small combinational RTL/Liberty Boolean equivalence.
• Die-pad, package-ball, and logical-signal mappings from explicit mapping sources.
• SDC objects and clocks against statically elaborated RTL.
• UPF object references and duplicate or missing power-intent objects.
• IP-XACT interface-to-physical-port maps.
• IP-XACT, SystemRDL, and C-header register addresses, widths, fields, access, resets, and layout.
• Declarative required/forbidden RTL connectivity, width, bit ordering, known polarity, waypoints, and excluded nodes inside the transparent static subset.
• DEF endpoints against the elaborated RTL hierarchy.
• GDSII structure and explicitly selected text-label port inventory through the common component contract; geometry is not checked.

See the rule catalog. Inconclusive evidence produces a completeness or not-applicable diagnostic; absence of a mismatch is not proof of equivalence.

Source-bound clock-cycle verification (development)

The current checkout additionally provides sequential check and sequential replay for a strict single-clock RTL subset. It reads source RTL rather than trusting manually translated formulas, preserves nonblocking updates/reset/enable semantics, and distinguishes inductively proven properties from finite-depth clean checks. Counterexamples are independently replayed, and receipts bind source content, assumptions and translation. Unsupported HDL is rejected.

python -m pip install -e ".[formal]"
opencollate sequential check examples/sequential/request.json --output receipt.json

See exact semantics, source subset, proof boundaries and test evidence. This is not full SystemVerilog, SVA, multi-clock verification or tapeout signoff.

Independently checkable proof certificates (development)

Generate source-bound safety evidence whose receiver does not need a SAT/SMT solver:

python -m pip install -e ".[certificates]"
opencollate sequential certify examples/sequential/request.json --output proof.json
opencollate sequential verify-certificate examples/sequential/request.json proof.json

The receiver re-reads current RTL, rebuilds separate bit-blasted base/induction obligations, checks every RUP proof addition, and replays reachable guard witnesses. Solver-returned UNSAT and recomputed hashes are not accepted as proof. Ordinary Z3 receipts remain unchanged; use these commands explicitly. The trusted frontend, encoding and Python kernel are not formally verified, and the documented single-clock, two-valued RTL subset still applies. See proof certificates, exact trust boundary and reproducible tests.

Hierarchical controller verification (development)

Sequential checks and independently checked certificates now share an elaborated module/generate frontend, including ordinary case, packed integral enums, and conservatively checked always_comb blocks. Blocking reads use the current procedural value; clocked nonblocking reads use old state. Possible latches, read-before-write blocks and wildcard/unique/priority cases fail explicitly. The complete instantiated model is validated before per-property solver reduction.

opencollate sequential check examples/controller/request.json --output controller.json
opencollate sequential certify examples/controller/request.json --output certificate.json
opencollate sequential verify-certificate examples/controller/request.json certificate.json
opencollate sequential check examples/hierarchy/request.json --no-cone --output full.json

The certificate receiver regenerates full-model CNF and checks RUP evidence without a solver; property-cone reduction is used by the Z3 check/replay path, not silently assumed by the receiver. See controller semantics and hierarchy and exact reduction. This remains a bounded supported hardware subset, not general SystemVerilog simulation equivalence or a signoff replacement.

Manifest-bound multi-file builds (development)

Sequential checks and solver-free proof receivers now accept explicit headers, include directories and build defines through a request's preprocess object. Native slang handles supported macro expansion and conditional compilation; exact source snapshots prevent undeclared disk-file shadowing and stale header evidence.

opencollate sequential check examples/preprocessed/request.json --output receipt.json
opencollate sequential certify examples/preprocessed/request.json --output proof.json
opencollate sequential verify-certificate examples/preprocessed/request.json proof.json

This is a single ordered compilation unit, not unrestricted preprocessing or a sandbox. Computed includes, token pasting and ambiguous declared includes are rejected. See manifest semantics and safety boundaries.

Commands

opencollate check [CONFIG] [--jobs N]       # default: opencollate.toml, one parser worker
opencollate review [CONFIG] --baseline REPORT
opencollate report diff BASELINE CURRENT
opencollate check -c path/to/config.toml
opencollate demo [--output-dir DIR]
opencollate init [PATH]
opencollate capabilities [--json]
opencollate explain CODE
opencollate schema [report|contract|diff] [--output PATH]
opencollate contract build [CONFIG] --output contract.oc.json
opencollate contract migrate LEGACY --output contract.v2.oc.json

Status	Meaning
0	The command completed and no unwaived error-level violations were found
1	The check completed and found unwaived violations
2	Configuration, input, parser, output, or internal failure prevented a trustworthy result

demo returns 0 by default because its inconsistencies are intentional; use demo --strict-exit to propagate its check status. Read exit codes before CI integration. Use baseline review to gate only new or changed findings while retaining fatal-analysis semantics.

Design contract, not pairwise spaghetti

Each importer emits parser-neutral observations with source provenance and fact state. Resolution groups them into canonical identities; rules consume those identities and retain evidence from every view.

RTL / Liberty / LEF / CDL / DEF / GDSII / IP-XACT / SystemRDL
                    │
CSV / connectivity intent / SDC / UPF / C headers
                    ▼
        observations + provenance
                    ▼
     canonical components, ports, registers
                    ▼
 rules → terminal / JSON / Markdown / SARIF / contract JSON

Inspect the exact contract being checked:

opencollate contract build examples/uart/opencollate.toml --output contract.oc.json

Newly generated schema-version-2 contracts persist canonical components, ports, and registers plus integrity-checked snapshots of every parser-neutral observation family: clocks, interfaces, hierarchy and references, package mappings, constraint/power metadata, registers, connectivity, view attributes, completeness, and tainted scopes. Version-1 contracts remain readable and can be migrated without inventing facts they never stored. Read the architecture, canonical contract, and diagnostic model.

Versioned extension platform

Installed packages can add collateral parsers through the opencollate.parsers entry-point group and semantic checks through opencollate.checkers. Registrations declare extension API version 1, provider/version provenance, aliases, and filename suffixes. They cannot silently shadow built-in formats. Parser crashes become fatal, whole-view-tainted OC9001 observations; checker discovery or execution crashes become fatal OC9002 diagnostics.

opencollate capabilities --json  # exact built-in/plugin ownership and failures

See the extension API for packaging, runtime registration, compatibility, configuration forwarding, deterministic conflict handling, and the plugin trust boundary. Set OPENCOLLATE_DISABLE_PLUGINS=1 when a hermetic run must ignore installed entry points.

Incremental and supervised checks (development)

Reuse unchanged parser observations without reusing a previous verdict:

opencollate check --cache-dir .opencollate-cache --cache-stats
opencollate guard --wall-seconds 60 --status-output guard-status.json -- check --cache-dir .opencollate-cache --format json --output report.json

The cache keys file bytes, options and implementation/dependency identity. Rules, contracts and waiver dates are checked every time. Unknown preprocessing dependencies and external plugins are deliberately uncached. The external guard rejects crashes, hangs and abnormal zero exits rather than accepting incomplete analysis. Neither feature is an authentication mechanism or an OS security sandbox. See incremental and guarded checks for POSIX resource limits, Windows restrictions, cache trust, and reproducible benchmarks.

Security and privacy

OpenCollate treats configuration and collateral as untrusted input. SDC and UPF are tokenized as static text; Tcl is never started. C macro and IP-XACT integer expressions use small bounded evaluators, not compilers or eval. IP-XACT rejects DTD/entity declarations and never fetches a schema. SystemRDL Perl tags/includes are rejected before compilation, and connectivity intent is bounded declarative data rather than a property language. CDL/SPICE is never simulated; DEF/LEF geometry is skipped structurally; and GDSII geometry records are bounded and discarded without polygon construction.

OpenCollate has no telemetry, account, upload, or network-reporting feature. Reports and contracts still contain design names, paths, connectivity, expressions, and normalized parser metadata and must be protected like source collateral. Read the security model and privacy statement.

No-signoff positioning

A clean OpenCollate report means only that enabled rules found no contradiction in facts they could establish. It does not certify correctness, completeness, manufacturability, timing, electrical behavior, power intent, or tapeout readiness. Review OC1102–OC1105, unknowns, tainted scopes, configuration participation, and parser coverage before relying on any result.

Project

• Roadmap
• Competitive evidence
• Public benchmarks
• Contributing
• Governance
• Support
• Security policy
• Changelog

OpenCollate is licensed under the Apache License 2.0.