Formal Cover Goals
Use cover properties to prove interesting states are reachable, not merely safe.
Task
Add cover goals for a full FIFO state and for two consecutive successful ready/valid transfers.
Examples
- Implement the required behavior and preserve it under the stated control conditions.
Constraints
- Use synthesizable SystemVerilog unless this stage is verification-only.
Concepts to review
formal, cover property, reachability
Open HDLForge to solve this problem in the interactive editor.
Related problems
- Formal Reset Assumptions — Medium
- FIFO Safety Properties — Hard
- FIFO Ordering Property — Hard
- Arbiter Mutual Exclusion — Medium
- Bounded Arbiter Liveness — Hard