Chapter 5 quiz

Check yourself: Exploring New RTL with Formal

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 main construct used in design exploration? Assumptions Covers Equivalence checks Coverage groups

Q2 How does a formal tool usually present a liveness counterexample? As a single failing cycle. As a prefix followed by a loop of states that repeats forever without the required event. As an infinite simulation log. It cannot produce counterexamples for liveness.

Q3 You add "assume property (!call[1])" to get a specific trace. What should you do with it afterwards? Keep it — more assumptions make proofs faster. Label it as exploration-only and remove it (or get it reviewed) before any signoff use. Convert it into an assertion on call[1]. Nothing; temporary assumptions cannot hide bugs.

Q4 Why convert "eventually served" into "served within K cycles" once K is known? Because liveness properties are not allowed in SVA. Bounded safety properties are usually easier to prove, give shorter counterexamples and state a real performance guarantee. Because covers cannot be used with liveness. There is no advantage.

Was this page helpful?

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