Toward more efficient formal strategies for deadlock

By TDF Editor |  No Comments  |  Posted: January 29, 2020
Topics/Categories: Blog Topics, Verification  |  Tags: , , , , , ,  | Organizations:

Deadlock is one of those problems that is well established but has remained a persistent challenge.

Whether the issue manifests itself as a total or ‘true’ deadlock, or as one from which a device can eventually escape though only after some time, it is nearly impossible to detect using simulation alone.

More recently, formal verification has been applied to the task. Specifically, users have sought to apply two analytical concepts, as a recent posting on the Verification Academy explains, but not without difficulty.

“‘Liveness’ properties are used to specify that something good will eventually happen. ‘Safety’ properties state that something bad will never happen,” the article explains. “Unfortunately, there is a big caveat to manually employing these techniques with a mix of properties and constraints: you really have to know what you are doing. And even then, it can be a tedious and error-prone manual process often involving many lengthy iterations.”

For example, while there is a language available to apply these formal strategies to total deadlocks – Computational-Tree Logic (CTL) – it is largely used in academia and there is a significant learning curve for engineers more familiar with, say, SystemVerilog Assertions (SVA). Nevertheless, CTL provides the most definitive deadlock check.

Meanwhile, while a more familiar, commercially supported and SVA/PSL-related language – Linear-Temporal Logic (LTL)  – that can be used to address hanging-but-not-total deadlocks, its practical use involves a lot of manual effort and, typically, multiple formal runs to identify constraints that may be missing from the CTL-based check and thereby whittle down the deadlock problem.

The obvious next step is automation and the article describes how techniques that incorporate CTL and LTL algortihms in the context of a more familiar formal infrastructure have recently been added to Questa PropCheck.

The article describes a work flow that builds upon deadlock properties from SVA to incorporate the algorithms with liveness and safety objectives.

Questa contains a number of formal apps that can help to overcome similar and often tricky tasks, if attempted manually. Learn more about some of those here.

 

Leave a Comment

PLATINUM SPONSORS

Synopsys Cadence Design Systems Mentor - A Siemens Business
View All Sponsors