Skip to content

Methodology

Research claim

SV-Gap separates two questions that conventional RTL generation benchmarks often conflate:

  1. Functional validity: did the candidate pass the supplied behavioral oracle?
  2. Structural validity: does the candidate satisfy declared structural safety rules under explicit clock/reset/value intent?
  3. Supporting evidence: what do distinct evidence classes such as ordinary lint report without being mistaken for structural CDC/RDC analysis?

Two candidates can be observationally equivalent under a functional testbench while differing in structural validity. We call the resulting measurement failure the structural validity gap: the benchmark's supplied contract and oracle do not identify whether the candidate satisfies the declared structural property. This term is distinct from control-theoretic structural observability.

The primary claim is existential and diagnostic. It does not require an estimate of how frequently the gap occurs in a model or population. A population estimate is a separate follow-on question requiring a sampling frame, clustered analysis, and broader adjudication. See research-scope-v0.2.md.

Primary metric

For candidates whose structural result is determinate:

structural_validity_gap =
  count(functional_pass and structural_fail)
  / count(functional_pass and structural_determinate)

The report must also disclose functional coverage, structural determinacy, tool errors, rule severities, tool versions, and any expert adjudication.

In schema v2, an oracle affects membership only when contributes_to_gap = true. The default profile makes the structural oracle contributing and ordinary lint contextual. A lint failure therefore remains visible but cannot silently redefine the structural-validity gap. Required and optional execution policy is separate from contribution policy.

Evidence policy

  • pass: the configured oracle completed and emitted no failing finding.
  • fail: at least one configured failing rule emitted concrete evidence.
  • compile_error: the candidate was rejected during compilation or elaboration; it is not conflated with a behavioral test failure or tool-infrastructure error.
  • unknown: intent or analyzer coverage was insufficient for a conclusion.
  • tool_error: the checker could not complete successfully.

unknown and tool_error are never counted as structural passes.

Schema v1 has one structural result. Schema v2 has an ordered oracle_results array, and each result includes its class, contribution flag, required flag, backend provenance, findings, diagnostics, and backend-declared coverage. Aggregators normalize v1 into a one-element structural-oracle view.

Reference-oracle policy

The built-in oracle exists to make the evaluation contract executable and to support controlled research fixtures. Every rule must have paired positive and negative fixtures, a stable identifier, source evidence where available, and a plain-language limitation statement. Broader or signoff-grade analysis belongs in independently versioned checker backends. See the finding ID reference for what each stable identifier detects.