Formally Synthesised Bus Monitor

Dynamic validation: a checker flags protocol violations:

• Safety violations are indicated straightaway,
• Liveness properties can be noted as they are satisfied.

If we have a simulator (e.g. a Verilog interpreter) that does not understand temporal logic, the assertions can be compiled to an RTL checker automaton.

A bus monitor connects to the net-level bus.

For a liveness property we can indicate whether it has been tested at least once and also whether there is a pending condition that yet to be satisfied.

Monitor can keep statistics as well as detect protocol violations.

Can it be synthesised from a formal spec ? »www.cl.cam.ac.uk/research/srg/han/hprls/orangepath/transactors and Bus Monitors