Refill Beat Ordering Property
Prove the four-beat refill index advances monotonically without skipping beats.
Task
When refill_fire occurs and beat_index is below 3, require next-cycle beat_index == past beat_index + 1.
Examples
- Implement the required behavior and preserve it under the stated interface/control conditions.
Constraints
- Keep the implementation deterministic and consistent with the interface contract described in the task.
Concepts to review
formal, cache, refill
Open HDLForge to solve this problem in the interactive editor.
Related problems
- Cache Address Decode — Medium
- Cache Hit Detection — Medium
- Cache Line Store — Hard
- Cache Miss / Refill FSM — Hard
- Four-Beat Refill Counter — Medium