In two years’ time, ASML transitioned to next-generation formal tooling. 5000+ models were migrated and 400+ engineers were trained, without impacting running development activities and machine performance.
ASML’s lithography machines consist of thousands of hardware components that must be optimally utilized. This is achieved by the embedded software running on the systems. The software is divided into independently developed components that execute in parallel and asynchronously communicate via interfaces. As the combined behavior quickly becomes very complex, achieving precise control and coordination of all the software components is a major challenge. To stay on top of the ever-growing complexity and minimize integration issues, ASML adopted component-based software engineering and formal verification, in a methodology referred to as formal software engineering (FSE).
FSE enables engineers to divide large systems into smaller subsystems that communicate via formal interfaces. These formal interfaces capture interface requirements, which include both structural (syntax) and behavioral (semantics) properties, and components are automatically verified against them. Unlike testing, formal verification exhaustively explores all possible system behavior. To achieve that in a reasonable time, this methodology promotes the design of loosely coupled and modular components, while guaranteeing correct integration. Additionally, the interface requirements can be used to improve communication with other teams and disciplines.
This article is exclusively available to premium members of Bits&Chips. Already a premium member? Please log in. Not yet a premium member? Become one for just €20 for the first year and enjoy all the benefits.
