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

Formally Synthesised Bus Monitor

A bus monitor is a typical example of dynamic validation: it is a checker that flags protocol violations:

For implementation in silicon, or if we are using an old simulator (e.g. a Verilog interpreter) that does not provide PSL or other temporal logic, the assertions can be compiled to an RTL checker automaton.

A bus monitor connects to the net-level bus in RTL or silicon. (TLM formal monitoring is also being developed.)

The monitor can keep statistics as well as detect protocol violations.

Example of checker synthesis from a formal spec: »www.cl.cam.ac.uk/research/srg/han/hprls/orangepath/transactors and Bus Monitors

6: (C) 2012-17, DJ Greaves, University of Cambridge, Computer Laboratory.