FIFO Ordering Property
Track one symbolic item and prove that the FIFO cannot reorder it.
Task
Assume tracked_valid identifies an accepted symbolic input. Assert that when tracked_reaches_head is true and a read occurs, the output data equals tracked_data.
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, FIFO, ordering
Open HDLForge to solve this problem in the interactive editor.
Related problems
- Async FIFO Dual-Port Memory — Easy
- Async FIFO Binary Pointers — Medium
- Binary-to-Gray Pointer Conversion — Easy
- Async FIFO Empty Detection — Easy
- Async FIFO Full Detection — Hard