vplan

Instruction file imported from Yoshi19701228/hw-formal-suite (.github/instructions/vplan.instructions.md). Copyright stays with the author.

Verification Plan Workflow

Stage 1 — Spec → Verification Plan

Trigger: "create a verification plan", "検証プランを作って", "#file:spec.txt からプランを作って"

Output YAML format:

dut: <module_name>
spec: <spec_name>

plan:
  - id: VP-001
    priority: critical        # critical / high / medium
    category: protocol        # protocol / safety / data-integrity / liveness / reset
    title: "<short title>"
    description: >
      <1-2 sentences: what must hold and why>
    signals: [sig1, sig2]
    method: assertion         # assertion / scoreboard / cover-only
    bound: 16
    coverage_goals:
      - COV_<NAME>_NORMAL
      - COV_<NAME>_BOUNDARY
      - COV_<NAME>_ERROR

Rules:

• 5–10 items — one per major chapter or feature group, not per signal
• Every item: at least 2 coverage_goals
• critical: protocol correctness, data loss, deadlock
• high: timing constraints, error handling
• medium: boundary conditions, back-to-back transfers
• scoreboard: data value correctness (write→read match)
• assertion: protocol sequencing, timing, state machine
• cover-only: reachability of optional features

Stage 2 — Verification Plan → Assertions

Trigger: "generate assertions from this plan", "このプランからアサーションを生成して", "#file:xxx_vplan.yaml からアサーションを生成して"

For each plan item:

• assertion → property + AST_ + all coverage_goals as COV_
• scoreboard → ghost register + AST_ mismatch + COV_ points
• cover-only → COV_ only, no AST_

Group by VP id:

// ============================================================
// [VP-001] <title>  priority: critical
// ============================================================

Helper logic (counters for bound, ghost registers for scoreboard) → [Helper Logic] section at the top.

Output: single *_assert_fml.sv using the standard single-module format.