Chapter 4 quiz

Check yourself: Formal Property Verification (FPV) Basics

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

Q1 Why do experienced engineers write covers before assertions? Covers prove assertions automatically. Covers validate that the environment allows the interesting behaviour, so later proofs are meaningful. Covers are required by the SVA standard. Covers run faster than assertions.

Q2 A counterexample uses period = 1, which the spec forbids. What is the correct response? Change the RTL to handle period = 1. Delete the failing assertion. Add an assumption that forbids loading period = 1, citing the spec. Increase the proof depth.

Q3 Which is NOT one of the three root causes of a counterexample? A design bug A wrong property A missing or wrong assumption The proof depth was too small

Q4 In FPV, who decides the values of top-level inputs? The testbench author. Random number generators seeded by the user. The formal tool, which considers every value allowed by the assumptions. They are always 0 unless driven.

Was this page helpful?

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