No False Cache Hit
Prove that an invalid line or tag mismatch cannot produce a hit.
Task
Assert !line_valid implies !hit and stored_tag!=request_tag implies !hit.
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, validity
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