Chapter 2 quiz

Check yourself: How Formal Engines Think

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

Q1 What does a miter do? It minimises the logic of a circuit. It XORs the outputs of two circuits driven by the same inputs, turning equivalence into "can the XOR be 1?". It removes logic outside the cone of influence. It converts RTL to CNF.

Q2 Which statement about the cone of influence is correct? It contains all logic in the design. It contains only the logic that can affect the signals used by the property; everything else is removed. It only contains combinational logic. It only matters for simulation.

Q3 Why is a reduced ordered BDD useful for equivalence checking? Because it is always small. Because, for a fixed variable order, it is canonical: equivalent functions give identical graphs. Because it does not depend on variable order. Because it can represent analog behaviour.

Q4 BMC with depth 30 finds no counterexample. What can you conclude? The property is proven for all time. The property cannot fail within 30 cycles of reset. The design has fewer than 30 states. The assumptions are wrong.

Q5 Induction fails for a property that is true in all reachable states. What is the usual fix? Remove the property. Add an assumption on the outputs. Add a helper assertion (invariant) that excludes the unreachable states the step started from. Increase the BMC depth to 1000.

Was this page helpful?

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