# FV Plan: <block name>

## 1. Scope and goal
- Goal: [design exploration | bug hunting | signoff]
- Configurations: <parameters / defines that will be proven>
- Out of scope (verified elsewhere): <list>

## 2. Design overview
- Interfaces and protocols: <list, with spec references>
- Clocks and resets: <domains, polarities, reset sequence>
- State overview: <FSMs, counters, memories, approx. flop count>

## 3. Requirements and properties
| Req ID | Requirement (spec ref) | Property name(s) | Type (A/M/C) | Status |
|--------|------------------------|------------------|--------------|--------|

## 4. Assumptions
| Name | Meaning | Spec reference | Asserted where? | Reviewed by |
|------|---------|----------------|-----------------|-------------|

## 5. Complexity strategy
- Reductions (parameters, black boxes, cut points) and soundness argument:
- Abstractions (counters, memories):
- Helper invariants:
- Case splits and completeness argument:

## 6. Quality checks and exit criteria
- [ ] All covers reachable (list max depth)
- [ ] No vacuous assertions
- [ ] All assertions proven, or bounded with documented depth argument
- [ ] Mutation campaign: all mutants killed or explained
- [ ] COI / proof-core coverage reviewed; gaps explained
- [ ] Assumption review done
- [ ] Environment in regression

## 7. Results log
| Date | RTL rev | Proven | Bounded (depth) | Failed | Covers hit | Notes |
|------|---------|--------|-----------------|--------|------------|-------|