A property is a contract written in logic. The commonest failure of a first formal run is not a design bug but a property that cannot fail: a trigger that never fires, a comparison against the design's own expression, a width that throws the failing case away. The proof then passes and means nothing. This topic builds one habit: read each requirement sentence, ask five questions about it, write the property, then break the design on purpose and read the counterexample.
Lesson | After it you can... |
|---|---|
Ask the five questions, write the property with the right window, count answers one to one, and show a cover that its trigger can fire. | |
Layer a local stage check under an end-to-end check and say which one names the broken stage. | |
Prove data integrity by following one free item instead of building a scoreboard. | |
Size, sign and start a property so that large values, negative values and the first cycle are checked. |
Suggested order: top to bottom. The five questions come first because every later lesson uses them; layering decides where each property lives; tracked items need both; widths and initial state are the quiet ways a good property goes blind. For the SVA language itself see the SystemVerilog course: only the forms the front end accepts are used here.
Whether its trigger can fire (an antecedent cover), and whether it compares the design with an independent expectation instead of with its own expression. Then plant a fault the property should catch.