Dirty Eviction Ordering Property
Prove dirty misses write back the victim before refill starts.
Task
When miss && victim_dirty occurs, assert writeback_start occurs before refill_start. Use a bounded two-step sequence.
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, writeback
Open HDLForge to solve this problem in the interactive editor.
Related problems
- Writeback Result Select — Easy
- Cache Address Decode — Medium
- Cache Hit Detection — Medium
- Cache Line Store — Hard
- Cache Miss / Refill FSM — Hard