Assertions

Declarative programming involves writing assertions that hold for all time.

For instance, on an indicator panel never is light A on at the same time as light B.

Assertion-based design (ABD) is an approach that encourages writing assertions as early as possible, preferably before coding/implementation starts.

• Writing assertions at design capture time before detailed coding starts.
• Writing further assertions as coding progresses.
• Structuring testing around assertions.

Assertions are (conjunctions of):

• Imperative (aka immediate) safety checks (like assert.h in C++ and expect in SystemVerilog)

• Coverage checks (log that flow of control has passed a point or a property held).

• Declarative safety properties, that always hold, such as `Never are both the inner and outer door of the airlock open at once unless we are on the ground'. Safety properties normally use the keywords never or always.

• Liveness and deadlock properties (also declarative), such as `If the emergency button is pressed, eventually at least one of the doors will be unlocked.' Liveness properties normally use keywords such as eventually or it will always be possible to.

All four can be proved by formal techniques such as pen and paper, theorem provers and model checkers.

Dynamic validation is simulation (or execution) while checking properties. This can sometimes find safety violations and, with careful construction detect deadlock, but it cannot prove the liveness or that safety wont be violated.

Assertions can be imported from previous designs or other parts of the same design for global consistency.

Formal proof shows up corner case problems not encountered in simulation.

A formally-verified result may be required by the customer.