Presentation
Forward Progress Testing: Saftey vs Liveness Assertion
DescriptionFormal verification plays a crucial role in today's Design Verification flows. There's no doubt that Formal verification does tasks that are extremely difficult in Simulation-based verification. One such task is checking forward progress in a System, ensuring that a system eventually reaches a desired state or completes its intended behavior. Forward progress verification guarantees that a system continuously makes progress and avoids getting stuck in an undesirable or deadlock state.
This problem is especially bigger when you are dealing with critical design components in high-performance computing systems. These systems interact with multiple internal/external controllers, where it's not always guaranteed that the drivers will strictly align to spec. Even if it returns unexpected data, for systems running for months it's not a big issue. But if garbage in causes a hang, that's bad because in most cases it's a full system reset needed to get it going.
This paper focuses on the different techniques and methodologies employed to analyze and prove forward progress and its significance in the context of formal verification.
We will discuss various approaches for ensuring forward progress in the design, using Liveness and Safety assertions both, and later examine how and where each assertion type should be used. with some case studies that demonstrate the application of forward progress checks and the type of critical issues it has found in the designs.
This problem is especially bigger when you are dealing with critical design components in high-performance computing systems. These systems interact with multiple internal/external controllers, where it's not always guaranteed that the drivers will strictly align to spec. Even if it returns unexpected data, for systems running for months it's not a big issue. But if garbage in causes a hang, that's bad because in most cases it's a full system reset needed to get it going.
This paper focuses on the different techniques and methodologies employed to analyze and prove forward progress and its significance in the context of formal verification.
We will discuss various approaches for ensuring forward progress in the design, using Liveness and Safety assertions both, and later examine how and where each assertion type should be used. with some case studies that demonstrate the application of forward progress checks and the type of critical issues it has found in the designs.
Event Type
Engineering Track Poster
TimeMonday, June 245:00pm - 6:00pm PDT
LocationLevel 2 Exhibit Hall
Back-End Design
Embedded Systems
Front-End Design
IP