Topics: Assertion-Based Design, Assertion Synthesis to H/W Monitors.
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.
Ideally, assertion-based design (ABD) involves:
Assertions are (conjunctions of):
All three can potentially be proved by formal methods.
Simulation (aka dynamic validation) can sometimes find safety violations and sometimes find deadlock but it cannot prove liveness.
Assertions can be imported from previous designs or other parts of the same design for global consistency.
ABD shows up corner case problems not encountered in simulation.
A formally-verified result may be required by the customer.