Simulation reads an assertion as a checker that watches a run. A proof engine reads the same assertion as extra hardware: each concurrent property becomes a small monitor circuit, stitched to the design into one product model, and the proof asks whether the monitor can reach its fail state. This topic builds that picture, shows how sampling and delay sequences become history registers, and ends with the translation table the rest of the section relies on.
Lesson | After it you can... |
|---|---|
Say what assert, assume and cover each ask about the monitor, and place properties where the open flow accepts them. | |
Read a value at the right edge, use the sampled-value functions, and say exactly what a reset disable does and does not hide. | |
Turn a delay chain, a range or a repetition into shift registers and counters the proof engine accepts. | |
Translate the common operators into their Boolean history forms and check each translation against the textbook meaning. |
Suggested order: top to bottom. The monitor picture first, then the sampling rule that decides which cycle every monitor sees, then sequences as pipelines, then the full translation table. The next topic replays the same ideas on the errors reviewers actually find: overlapped versus non-overlapped, level versus edge, and stability windows.