Before any metric can be understood, the run itself must be visible: what is compiled, what drives the design, what a task and an engine and a depth are, what the report says, and where the proved model differs from the simulated one. This topic walks that flow in vendor-neutral terms, with one complete harness, one depth pair, one report parser, and one fidelity table.
Lesson | After it you can... |
|---|---|
Build a complete harness: free inputs, reset, assumptions, assertions, covers, and parameters. | |
Predict what changing depth, engine, time, or splitting properties does to a run. | |
Parse a generic report into proven, counterexample, and inconclusive counts without misfiling. | |
Name where the proved model differs from simulation and what that costs. |
Suggested order: top to bottom. Build the harness, learn the run controls, read the report, then distrust the model in exactly the right places.
Inconclusive: it is neither a proof nor a counterexample, and filing it elsewhere corrupts the signoff.