Chapter 8 quiz

Check yourself: Formal Equivalence Verification

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

Q1 Why does combinational FEV scale to whole-chip netlists? Because netlists are simpler than RTL. Because mapping state elements reduces the problem to many small combinational comparisons between flops. Because it only checks outputs. Because it uses simulation internally.

Q2 A register was moved from after an adder to before it (retiming). Which kind of equivalence check is needed? Combinational Sequential None — retiming is always safe Connectivity

Q3 After scan insertion, FEV reports mismatches on many flops. What is the most likely cause? Synthesis bugs everywhere. Scan enable is not constrained to functional mode, so the scan path is compared against RTL that has none. The RTL has X assignments. The clock is not defined.

Q4 In a conditional equivalence check, why must the qualifier (valid) also be compared unconditionally? It is not necessary. Otherwise a design that never asserts valid would pass all qualified data checks vacuously. Because tools require it syntactically. To speed up the proof.

Was this page helpful?

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