Chapter 6 quiz

Check yourself: FPV for Bug Hunting and Signoff

Pick one answer per question, then press Check answers. Explanations appear after checking. Your best score is saved in this browser.

Q1 What is the key idea behind the tracked-item data check? Model the whole FIFO memory in the testbench. Let the tool choose one arbitrary push and check only that entry — which proves it for every entry. Track only the first push after reset. Compare rdata against wdata on every cycle.

Q2 Why can control properties of the FIFO be proven with WIDTH = 1? Because 1-bit FIFOs are the most common. Because the FIFO never makes decisions based on data values (data independence). Because formal tools ignore data. They cannot — WIDTH must match the real design.

Q3 A mutation (deliberate bug) is injected and every assertion still proves. What does that indicate? The mutation tool is broken. The design is robust. There is a hole in the property set or an over-constraining assumption. The proof depth is too large.

Q4 What makes a bounded proof acceptable for signoff? Any bound over 100 cycles. A documented argument (backed by covers) that the bound reaches all relevant states. Approval from the tool vendor. Bounded proofs are never acceptable.

Was this page helpful?

Tip: select any text on the page before clicking Report and it will be quoted in your report.