Cache Formal Environment Assumptions
Constrain request behavior for formal cache proofs.
Task
Assume reset is initially active and assume req_valid remains asserted with a stable request address while req_ready is low.
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, assume 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