Architecture

SV-Gap separates functional execution from independently versioned evidence producers. Schema v2 records every producer as a distinct oracle result.

manifest + RTL
   |
   +-- functional commands/import --------> FunctionalResult
   |
   +-- structural oracle (Yosys/Naja) ----> OracleResult[class=structural]
   +-- bounded properties (Yosys SAT) ----> OracleResult[class=temporal|protocol]
   +-- synthesized reference miter -------> OracleResult[class=equivalence]
   +-- ordinary lint (Verilator) ---------> OracleResult[class=lint]
   `-- other configured evidence ---------> OracleResult[class=...]
                                              |
                                              v
                                     EvaluationReport v2
                                     + gap membership
                                     + configured-contract status
                                     + per-oracle coverage
                                     + versions/diagnostics/artifacts

This prevents a lint-clean result from overwriting a CDC/RDC failure, and it prevents an unavailable optional tool from being silently reported as a pass.

Manifest boundary

The manifest is the reproducibility boundary. Relative paths resolve from its directory. Clock and reset relationships are declared, never inferred merely from different signal names.

Schema v1 remains accepted and maps its single [structural] table to one compatibility oracle. Schema v2 uses ordered [[oracles]] records:

schema_version = "2.0"
candidate_id = "candidate-a"

[design]
top = "top"
sources = ["design.sv"]

[functional]
commands = [
  ["iverilog", "-g2012", "-o", "${SVGAP_BUILD}/sim.vvp", "design.sv", "tb.sv"],
  ["vvp", "${SVGAP_BUILD}/sim.vvp"],
]

[[oracles]]
id = "reference-structure"
class = "structural"
backend = "reference-yosys"
contributes_to_gap = true
required = true

[[oracles]]
id = "ordinary-lint"
class = "lint"
backend = "lint-verilator"
contributes_to_gap = false
required = false

[intent]
asynchronous_groups = [["source"], ["destination"]]
cdc_reconvergence = "forbid_independent"
x_policy = "strict"

[[intent.clocks]]
name = "source"
port = "src_clk"

[[intent.clocks]]
name = "destination"
port = "dst_clk"

[[intent.crossings]]
source = "event_toggle"
destination = "event_pulse"
protocol = "pulse"
min_sync_stages = 2

[output]
report = "build/report.json"

required = false means tool absence is retained as tool_error evidence but does not make the command fail. contributes_to_gap = false means the result is contextual evidence and cannot create a gap member. A v2 manifest requires at least one contributing oracle; that oracle may be structural, temporal, protocol, equivalence, or a plugin-defined evidence class.

The complete syntax example is schemas/manifest-v2.example.toml.

Report boundary

Schema v1 emits the legacy top-level structural result. Schema v2 emits oracle_results and deliberately omits that top-level field:

{
  "schema_version": "2.0",
  "functional": {"status": "pass"},
  "oracle_results": [
    {
      "oracle_id": "reference-structure",
      "oracle_class": "structural",
      "status": "fail",
      "contributes_to_gap": true,
      "required": true,
      "coverage": {"rules": ["REF-CDC-001"]}
    },
    {
      "oracle_id": "ordinary-lint",
      "oracle_class": "lint",
      "status": "pass",
      "contributes_to_gap": false,
      "required": false,
      "coverage": {"ruleset": "--Wall"}
    }
  ],
  "contract_status": "open",
  "gap_member": true
}

The actual schema requires the remaining backend, finding, diagnostic, version, and timestamp fields. Gap membership is:

functional == pass
AND any(oracle.contributes_to_gap AND oracle.status == fail)

contract_status is the positive counterpart used by campaigns. It is closed only when functional evidence passes, every required oracle passes, and every required observed-coverage goal reports requirements_met != false. Required failures produce open; missing or bounded-out evidence produces incomplete; required tool failures produce tool_error. Gap membership is retained unchanged for longitudinal compatibility.

Backend boundary

A backend exposes stable name and version values and implements either:

check(manifest) -> CheckResult

or the schema-v2-aware form:

check(manifest, oracle_config) -> CheckResult
coverage(manifest, oracle_config) -> dict

It returns pass, fail, unknown, or tool_error. Missing required intent or unsupported analysis must not become pass.

Built-in reference oracle

reference-yosys elaborates RTL with Yosys and implements 17 controlled recognizers across these classes:

• baseline CDC (REF-CDC-001 through 003);
• pulse, toggle, handshake, reconvergence, and async-FIFO CDC (REF-CDC-004 through 008);
• declared synchronizer depth (REF-META-001);
• reset release, independent reset domains, reset gating, and reset reconvergence (REF-RDC-001 through 004);
• output-reachable un-reset state, X-masking control flow, selective reset, and memory initialization (REF-XPROP-001 through 004).

See the finding ID reference for exact activation conditions. These are reference shapes with paired fixtures, not a signoff deck.

reference-naja independently reproduces the original CDC/RDC/X subset using Naja's in-process SNL graph. It exposes its supported rules in coverage metadata and returns unknown when newer intent classes are requested.

Lint evidence

lint-verilator and lint-verible run ordinary source lint as the separate lint evidence class. Their coverage metadata records the ruleset and the frozen RDC calibration result: neither default configuration detected the RDC mechanism in the 14 functionally passing REF-RDC-001 cases. This makes lint useful evidence without relabeling it as structural CDC/RDC analysis.

Temporal, protocol, and equivalence evidence

formal-yosys reads candidate RTL plus manifest-named formal property sources, lowers clocked properties through clk2fflogic, honors assumptions, and runs a bounded Yosys SAT proof. The rule ID, property top, bound, and message are explicit oracle options. Its coverage says proof_scope = "bounded"; it does not claim unbounded liveness or production formal signoff. A property harness can name non_vacuity_signal, set non_vacuity_depth, and require require_non_vacuity = true; a proof pass then closes only if Yosys also finds a bounded witness reaching that signal. Proof scripts, logs, counterexamples, and reachability witnesses are retained with SHA-256 digests in artifacts for both passing and failing oracle outcomes.

equivalence-yosys separately synthesizes the supplied reference and candidate views, builds a Yosys miter, and proves its comparison assertion for the configured bound. The current controlled fixtures are combinational. A larger bound is still only bounded, zero-initialized sequential comparison—not industrial four-state or state-mapped sequential equivalence.

The temporal/equivalence benchmark audit explains why these classes are separate from finite functional simulation and ordinary lint.