In this video, Joe Hupcey ask to Hirak Roy of the Questa Formal team about how Mentor’s PropCheck formal tool efficiently maps its engines to the customer's available compute resources, how the algorithm orchestration architecture gives users’ predictable, linear scalability of compute resource consumption, and how compute resources can be freed up on-the-fly as the properties are proven over the course of the formal analysis.