DescriptionQ830
Q830DVArchQualcommASIC interview problem
Prove bounded bridge forward progress
TechniquesDVArchFormal
DifficultyHard
TopicAssertions and Formal
LanguageSystemVerilog
Requirements4 checkpoints
01
Problem
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 declarationSystemVerilog
req_valid, req_ready, req_id
out_valid, out_ready, out_id
rsp_valid, rsp_id
reset_n
queue depth = 2Example input and output
Use this case to check your interpretationInput
Case 1: One request accepted at cycle 0
Case 2: Two accepted requests
Case 3: A response with an untracked IDOutput
Case 1: Must complete by cycle 20.
Case 2: May fill the queue, but a third sees req_ready = 0.
Case 3: Fails immediately.Explanation
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.
02
Requirements (4)
- 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.