# Rtl P5 Verify Policy

> Internal reference: rtl p5 verify policy (agent-loaded; do not invoke).

- Skill: `babyworm/rtl-p5-verify-policy` (Agent Skill)
- Install (CLI): `npx skillmds@latest add babyworm/rtl-p5-verify-policy`
- Raw SKILL.md: https://api.skillmd.com/api/skills/babyworm/rtl-p5-verify-policy/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: babyworm (https://skillmd.com/u/babyworm)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/babyworm/rtl-p5-verify-policy

---


# 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:

```markdown
# 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`:
```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.