The paper considers the co-ordination and control of flexible, independently driven, multiaxis, high-speed machinery in which mechanical complexity has been exchanged for sophistication in control. The control of such machines is a hybrid control problem and the paper addresses the specification and design of the discrete event part of the controller. It focuses on the design of synchronisation logic for the event-driven real-time co-ordination and synchronisation of the machine. For such time-critical and system-critical applications, it is imperative that system behaviour is fully understood and unambiguous. The paper proposes a method for inferring system behaviour and performing formal verification of machine systems specified using a subset of the industry standard IEC 1131 sequential function charts (SFC). It shows how an SFC-based design can be translated to an equivalent Petri net model, thereby allowing Petri net theory and analysis techniques to probe its behaviour and verify its functionality. The approach is demonstrated by considering the design of synchronisation logic for a prototype six-axis high-speed packaging machine which incorporates both time-critical and system-critical functions.