Cache Formal Cover Scenarios
Add reachability goals for hit, clean miss and dirty eviction paths.
Task
Write three cover properties: a hit, a miss with !victim_dirty, and a miss with victim_dirty followed eventually by writeback_start.
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, cover property
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