Chapter 1 quiz

Check yourself: Welcome to Formal Verification

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 fundamental difference between simulation and formal property verification? Formal runs faster test vectors than simulation. Simulation checks the input sequences you drive; formal considers all legal input sequences. Formal only works on gate-level netlists. Simulation cannot use assertions.

Q2 In the credit counter example, why did the formal tool find the bug so easily? Because the testbench was written to target zero credits. Because the inputs were left unconstrained, so the tool was free to send dec when credits were 0. Because the counter was only 4 bits wide. Because the cover property forced the failure.

Q3 What is an assumption in formal verification? A property the tool tries to violate. A behaviour the tool tries to reach to prove it is possible. A constraint that restricts the inputs to legal behaviour. A comment explaining the design intent.

Q4 A tool reports "bounded proof to 25 cycles" for an assertion. What does that mean? The assertion is proven for all time. The assertion failed at cycle 25. No violation exists within 25 cycles of reset, but longer traces were not ruled out. The design has exactly 25 reachable states.

Q5 Which block is typically the best first candidate for formal property verification? A 64-bit floating-point multiplier. A round-robin arbiter with request/grant handshakes. A complete SoC with CPU and software. An analog PLL.

Was this page helpful?

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