HOME       UP       PREV       FURTHER NOTES       NEXT (Is a formal specification complete ?)  

Formally Synthesised Bus Monitor

Dynamic validation: a checker flags protocol violations:

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

(C) 2008-10, DJ Greaves, University of Cambridge, Computer Laboratory.