A UVM regression answers one kind of question well: did the design do the right thing for the stimulus we gave it? Some of the most valuable questions in verification are of a different kind. Can this ever happen, for any input? Does every bench that uses this bus check the same protocol rules? Which of last night's 2,000 runs were worth their CPU time? This topic covers the three tools senior engineers reach for beyond the constrained-random bench: formal verification, assertion VIP attached with bind, and automation (including machine learning) built on regression data.
Split a block's verification plan between formal and simulation, say what each one closes, read a bounded and a full proof result, and explain how the two combine at sign-off.
Write a protocol checker as a bound SVA module, report its failures through UVM, control it per test, and reuse it as the assumptions of a formal run.
Tell the real uses of ML in verification from the hype, list the data each one needs, evaluate a tool claim, and build a coverage-based test ranking yourself.
Lesson | The question it answers |
|---|---|
Which of the DMA's rules should be proved instead of simulated, and what does a proof result actually promise? | |
How do protocol checks travel with the RTL into every bench, report through UVM, and become formal assumptions? | |
What can ML really do with regression data today, and what can you automate yourself this week? |