Hardware interview practice
Prove bounded bridge forward progress
A request bridge has two queue entries. The downstream may stall, so liveness needs an explicit fairness contract. A request ID is unique while outstanding but may be reused after its prior request completes. Write a formal property plan for safety, conservation, and bounded completion.
Starting point
Question code
req_valid, req_ready, req_id
out_valid, out_ready, out_id
rsp_valid, rsp_id
reset_n
queue depth = 2Reviewed example
Work through one case
Input
Case 1: One request accepted at cycle 0
Case 2: Two accepted requests
Case 3: A response with an untracked IDExpected output
Case 1: Must complete by cycle 20.
Case 2: May fill the queue, but a third sees req_ready = 0.
Case 3: Fails immediately.The shown result follows by applying this rule: Fairness is written as an assumption, not hidden inside the design assertion. The cases also demonstrate this requirement: Assert every accepted input completes within 20 cycles under the stated assumptions; cover full-queue recovery.
What to cover
Requirements
- Assume every accepted downstream request receives a response within 12 cycles and out_ready is asserted at least once in every four cycles.
- Assert occupancy remains 0 through 2 and accepted requests equal queued plus completed requests.
- Assert that every accepted request instance produces at most one downstream issue and one completion, that neither output nor response appears without an outstanding instance, and that an ID is not reused while still outstanding.
- Assert every accepted input completes within 20 cycles under the stated assumptions; cover full-queue recovery.