rtl-p5-verify-policy

name	rtl-p5-verify-policy
description	Internal reference: rtl p5 verify policy (agent-loaded; do not invoke).
user-invocable	false

Phase 5 Verification Policy

Three-Stage Architecture

Stage 1 (Module): Each module independently verified in parallel across 9 categories. Stage 2 (Top): System-level verification after ALL modules graduate. Stage 3 (Final): Compliance review + summary generation.

Core principle: Module-level verification first, top-level only after module graduation (criteria: Module Graduation Gate below). Only graduated modules participate in top-level integration. This prevents wasting top-level sim time on modules with known bugs.

Verification Categories

Applied at both module-level (Stage 1) and top-level (Stage 2). Agent/sub-orchestrator routing per category is OWNED by the p5-verify-orchestrator agent prompt ("Verification Categories" table).

V1: Lint (final comprehensive)
V2: SVA Completion + Formal
V3: CDC/RDC Analysis
V4: Protocol Compliance (if bus interfaces)
V5: Functional Regression (Tier 3/4)
V6: Coverage Analysis
V7: Performance Verification
V8: Synthesizability + PPA Estimation
V9: Code Review + Refactoring

Parallelism Model (Stage 1 per module)

Parallel Group A: V1(Lint) + V2(SVA/Formal) + V3(CDC) + V4(Protocol) + V8(Synth Est.)
Sequential: V5(Functional) starts after V1 pass (lint-clean required for sim)
Incremental: V6(Coverage) starts as V5 data arrives
Sequential: V7(Performance) after V5 pass (functional correctness required)
Final: V9(Code Review) after V1-V8 results inform review scope

Overlap Rules

• Stage 1 modules are fully independent → all modules run simultaneously; a module that passes all Group A checks starts Group B immediately without waiting for other modules
• Within a module, Groups A/B/C progress as dependencies are met
• Stage 2 starts as soon as ALL modules graduate (not before)
• Stage 3 starts after Stage 2 completes

Module Graduation Gate

A module graduates when ALL 9 checks pass. The per-check criteria are stated ONCE, normatively, in "Final Checklist — Stage 1 (Per Module)" below (PARTIAL_PASS accepted for V5 AC-level checks — WARNING, not FAIL).

On FAIL: invoke rtl-p4s-bugfix (feedback loop, max 2 per module). After fix, re-verify ONLY the failed categories (not all 9).

AC-Level Module Graduation (when applicable)

When structured acceptance_criteria (with ac_id) exist in iron-requirements: Module graduation (Stage 1):

• VERIFIED or FORMAL ac_ids: PASS
• PARTIAL Critical/High ac_ids: WARNING — module graduates but flagged for Stage 3 closure
• UNTESTED Critical/High ac_ids: FAIL — module does not graduate
• NOT_VERIFIABLE ac_ids (verifiable: false): excluded from gate

Stage 3 audit (final, pre-P6): per "Requirement Traceability Gate (P6 Entry Blocker)" below and Final Checklist Stage 3 (no Critical/High ac_id UNTESTED or PARTIAL). When no structured AC: existing REQ-level graduation applies.

Top-Level Gate

All top-level checks PASS → proceed to Stage 3. On FAIL → classify and fix:

• UNIT_FIX: single module issue → rtl-p4s-bugfix → re-verify module → re-graduate → re-verify top
• INTEGRATION_FIX: cross-module issue → fix → re-verify affected checks
• DESIGN_FIX: architecture issue → STOP, escalate to user

Per-Module Verification Tracker Schema

Per-module JSON with fields: module, status (initial "pending"), checks object with one key per category — v1_lint, v2_sva_formal, v3_cdc, v4_protocol (allows "n/a"), v5_functional, v6_coverage, v7_performance, v8_synth_est, v9_code_review — each initialized "pending", plus feedback_loops (count, initial 0) and graduated (bool, initial false).

Functional Verification Scenario Splitting (V5)

Long test suites split by scenario category:

Category	Description	Typical Vector Count
basic	Normal operation, happy path	50-100
corner_case	Boundary conditions, edge cases	100-200
stress	Maximum throughput, back-to-back, full FIFO	200-500
error_handling	Invalid inputs, error injection, recovery	50-100

Each scenario category runs as independent parallel agent. Multi-seed regression per scenario (5 seeds default: 1, 42, 123, 1337, 65536). Total: M modules × S scenarios × 5 seeds = massive parallelism. Early termination: >5% failure rate → halt and report.

For very large modules, further split by feature within each category.

SVA Iterative Refinement

Minimum 3 rounds: Draft → Strengthen → Harden.

• SymbiYosys requires Verilog DUT input. Run sv2v --write=formal/{module}_v2v.v explicitly on DUT RTL only before SBY, then verify the output file exists and is non-empty.
• Full concurrent SVA assets are commercial-formal only for this flow. Do not pass them through sv2v; generate a Yosys-compatible procedural harness for OSS SBY.
• .sby config references copied basenames for _v2v.v and *_formal_harness.sv.
• On counterexample: waveform-analyzer diagnoses

Coverage Targets

Post-exclusion targets: line ≥ 90%, toggle ≥ 80%, FSM ≥ 70% (normative statement: Final Checklist Stage 1, V6 items).

Iterative coverpoint refinement (minimum 3 rounds). Generate additional tests for HIGH priority gaps. Re-run regression for new tests. When convergence is detected (2 consecutive iterations with < 0.5% improvement), apply Coverage Exclusion Protocol per rtl-p5s-coverage-policy: classify unreachable bins, generate exclusion files, document in reviews/phase-5-verify/{module}-coverage-exclusions.md, and report both raw and post-exclusion numbers.

Synthesis Estimation Policy (ASIC TSMC 28nm)

Both Module-level (V8) and Top-level (T8):

1. constraint-writer generates SDC (MANDATORY — before synthesis)
2. run_syn.sh — handles tool selection and sv2v conversion internally (Layer 2). --skip-if-unavailable is permitted only for an explicitly requested exploratory estimate, never for synthesis signoff or module graduation.
3. Synthesis scope depends on tool tier (per syn-tool-profiles):
   • Tier 1 (commercial): full synthesis + timing + area + PPA
   • Tier 2 (oss/Yosys): latch detection + unmapped cells + basic area (NAND2-FO2 gate eq)
   • Tier 3 (none): SKIPPED with WARNING. This is allowed only for exploratory estimation; synthesis signoff and module graduation remain blocked until a synthesis-capable tool runs and passes.
4. Area reported in NAND2-FO2 gate equivalents (area_um2 / 0.798) when available

Module-level (Stage 1 V8): → Always: synthesis estimation with NanGate45 + NAND2 gate count → SDC: per-module clock/IO constraints

Top-level (Stage 2 T8): → Always: full synthesis estimation with NanGate45 + SDC → User requested full synthesis? → additionally export netlist + JSON report → Area metric: ALWAYS NAND2-FO2 gate equivalents (NOT LUTs, NOT raw cell count)

Parallelism Budget

Cap concurrent verification agents at ~20-30 via run_in_background regardless of theoretical parallelism.

Feedback Loop Classification

Failure Type	Scope	Fix Approach	Re-verify
UNIT_FIX (lint)	Single module V1	rtl-coder fix	V1 only
UNIT_FIX (SVA)	Single module V2	rtl-p4s-bugfix	V2 only
UNIT_FIX (CDC)	Single module V3	rtl-coder add sync	V3 only
UNIT_FIX (sim)	Single module V5	rtl-p4s-bugfix	V5 + V6
INTEGRATION_FIX	Cross-module	rtl-p4s-bugfix	Affected Vx + Stage 2
DESIGN_FIX	Architecture	STOP → user	All (after upper phase fix)

Independent UNIT_FIX failures in different modules: fix in parallel. Same-module failures: fix sequentially within a single task. INTEGRATION_FIX: always sequential (cross-module dependencies).

UARCH_FIX (P5→P3 Feedback Path)

When P5 verification reveals a μArch-level issue that cannot be fixed in RTL alone (e.g., pipeline balance infeasible, missing metadata in FIFO struct, architectural throughput bottleneck):

1. Classify as UARCH_FIX → STOP current P5 verification for affected module
2. Generate reviews/phase-5-verify/uarch-feedback-{module}.md with:
   • Root cause analysis (why RTL fix is insufficient)
   • Affected P3 uarch spec section(s)
   • Proposed uarch change
3. Escalate to user for P3 uarch document update
4. After P3 update → P4 RTL re-implementation → P5 re-verification

Feedback Loop Decision Recording

Every feedback loop iteration MUST produce a decision record at .rat/scratch/phase-5/feedback-loop-decision-{N}.md with:

# Feedback Loop Decision #{N}
- Module: {module}
- Check: V{x} ({category})
- Classification: UNIT_FIX | INTEGRATION_FIX | DESIGN_FIX | UARCH_FIX
- Root cause: {description}
- Fix applied: {description of change}
- Alternatives considered: {rejected options with rationale}
- Affected artifacts: {list of modified files}
- Re-verification scope: {which checks to re-run}

This enables post-mortem analysis of verification efficiency and identifies recurring patterns that should become preventive rules.

Integration with rat-auto-design

When invoked from rat-auto-design, state is tracked in .rat/state/rat-auto-design-state.json:

{
  "current_phase": 5,
  "completed_sub_phases": ["stage-1-module-a", ...],
  "pending_sub_phases": ["stage-2-integration", "stage-3-compliance"],
  "fix_history": [
    {"sub_phase": "stage-1-v2", "module": "module_a", "fix_count": 1, "status": "resolved"}
  ]
}

This enables resume: re-read state and continue from next pending sub-phase.

UVM Verification (Optional)

If commercial simulator available and UVM mandated, invoke /rtl-agent-team:rtl-p5s-uvm-verify alongside V5. UVM is NOT a replacement for cocotb regression — both provide complementary coverage.

Escalation & Stop Conditions

• Module feedback loop exhausted (2 cycles for same check) → escalate to user with findings
• DESIGN_FIX detected (architecture-level issue) → IMMEDIATE STOP, escalate to user
• Coverage persistently below target after 3 rounds → escalate to rtl-architect
• Performance deficit >20% → escalate to rtl-architect for pipeline review
• Synthesis estimation shows infeasible design → escalate to user with PPA report
• Multiple modules fail same check type → systematic issue, escalate to rtl-architect
• Stage 2 integration FAIL with >3 bugs → escalate to rtl-architect for interface review
• CDC failures where root cause is uncertain clock relationship/clock gating/muxing → escalate to clock-architect + cdc-reviewer before next fix loop
• Tool not installed → eda-runner provides instructions, halt affected check

Final Checklist

Stage 1 (Per Module)

• V1: lint PASS (verilator --lint-only -Wall + slang --lint-only)
• V2: SVA formal — all properties proved or justified timeout (3+ refinement rounds)
• V3: CDC — zero VIOLATION, CAUTIONs justified
• V4: protocol PASS or n/a
• V5: functional — all scenarios × all seeds PASS
• V6: post-exclusion coverage targets met (line ≥ 90%, toggle ≥ 80%, FSM ≥ 70%)
• V6: raw coverage reported alongside post-exclusion numbers
• V6: exclusion record approved (if exclusions applied; standard categories auto-approved by coverage-analyst, non-standard user-approved)
• V7: performance — all metrics within 10% of BFM baseline
• V8: synthesizable — no latches, PPA estimate in NAND2-FO2 gate count (NanGate45/28nm)
• V9: code review — no critical findings, refactoring applied if needed
• All modules graduated

Stage 2 (Top-Level)

• T1: top-level lint PASS
• T2: system SVA formal PASS
• T3: system CDC PASS (zero VIOLATION)
• T4: system protocol PASS
• T5: integration test (Tier 4) PASS
• T6: system post-exclusion coverage targets met, raw coverage reported
• T6: system exclusion record approved (if exclusions applied; non-standard require user approval)
• T7: system performance within spec
• T8: ASIC 28nm synthesis estimation saved (NanGate45, NAND2-FO2, SDC applied)
• T9: top-level code review — no critical findings

Stage 3 (Final)

• reviews/phase-5-verify/requirement-traceability.md saved
• reviews/phase-5-verify/e2e-traceability.md saved
• reviews/phase-5-verify/traceability-audit.md saved with verdict PASS
• Zero Critical/High priority UNTESTED or PARTIAL requirements/ac_ids (when structured AC exists)
• AC-level traceability audit: no Critical/High ac_id UNTESTED or PARTIAL (must be VERIFIED/FORMAL)
• reviews/phase-5-verify/final-compliance.md saved with verdict PASS
• docs/phase-5-verify/phase-5-summary.md generated
• docs/phase-5-verify/ reports collected
• All feedback loops resolved (max 2 per module per check)

Requirement Traceability Gate (P6 Entry Blocker)

Stage 3 includes a Formal Traceability Audit that gates P6 entry:

• Every Critical/High priority requirement in iron-requirements.json must have status VERIFIED (simulation test with assertion) or FORMAL (SVA proof)
• PARTIAL Critical/High requirements at Stage 1 module graduation produce WARNING (proceed)
• PARTIAL Critical/High requirements at Stage 3 final audit produce FAIL and block P6 entry (must upgrade to VERIFIED or FORMAL)
• UNTESTED or PARTIAL Critical/High requirements produce FAIL and block P6 entry (PARTIAL must be upgraded to VERIFIED or FORMAL)
• The traceability-audit.md verdict must be PASS for final-compliance.md to pass

This ensures no Critical/High requirement ships without at least one verification artifact.