A property library pays for itself when the same rule is checked on the other face of an interface, at another size or in another mode. It fails when the library is wrong about roles, when the sizes it was proved at are too small to show the faults, or when its rule table has rules with no cover. This topic builds one checker used on two faces of the bridge, proves a parameterised design at several sizes and modes, and ends with the rule tables of three running designs checked mechanically.
Lesson | After it you can... |
|---|---|
Write one checker with a role parameter and instantiate it as an assumption on one face and an assertion on the other. | |
Prove at the sizes and modes that expose faults, and state the depth a bounded run needs. | |
Keep a rule table whose asserts and antecedent covers are checked against the design files. |
Suggested order: top to bottom. The checker is the unit of reuse, parameters and modes are the axis of reuse, and the rule tables record what the library covers.
The rule is owed by the block that drives a face and assumed by the block that receives it. An assertion on a free input fails at once; an assumption on an output prunes the design.