DAC 2020 Paper Report: Easy Deadlock Verification and Debug with Advanced Formal Verification
At this year’s Design Automation Conference (DAC), Formal verification was everywhere – in posters, papers, and panel discussions – where new and long-time formal users alike shared their experiences in applying this powerful technology to challenging real-world verification problems. Indicative of this trend was the Best Paper winner, 4.1 Easy Deadlock Verification and Debug with Advanced Formal, by lead authors Laurent Arditi and Vincent Abikhattar of Arm.
At a very high-level, Laurent and Vincent were addressing the same deadlock verification issues and employing the same formal-based methodologies outlined in a prior Verification Horizons article, Deadlock Prevention Made Easy with Formal Verification. To briefly re-cap, there are two deadlock scenarios to look out for:
A – The design gets into a state that it can never escape and there is no sequence of inputs you can give it to dislodge it from that state. This is always a bug that needs to be fixed.
B – The design gets into a state that it can actually escape, but the system might tend to hang-up there anyway. Depending on the system’s requirements, this is not always a design issue that needs to be fixed; but it’s essential to understand the behavioral boundaries of the logic to confirm there won’t be any trouble.
Of course, Arm’s DUTs are seriously large IPs that could find their way into a trillion devices. Specifically, they shared three case studies where formal-based deadlock analysis with Questa PropCheck either found show-stopper bugs, or mathematically proved the absence of deadlock for all time and all inputs.
1 – Instruction Fetch unit FSMs – while these FSMs were designed to be resilient in the face of incorrect or unexpected environment behaviors, and sometimes even support Case B above where the DUT can hang out in a given state, their formal analysis showed inescapable deadlocks. (And apparently the performance exceeded expectations, as “Proof time is a few minutes, with no overhead for also running the unescapable deadlock checks”)
2 – L1 data cache arbiter – in this case “all assertions were proven” – no doubt a big relief to the project team!
3 – Credit based protocol verification – they were able to prove that “no credit is lost”, and there were “a few critical bugs found”
My notes aren’t doing this presentation justice, so I urge you to watch the recording when it becomes available. In the meantime, in the DAC proceedings look for the file “B1094_4_1_Arditi_POSTER_1592757546.pdf”
Until next time, may your power consumption be low, and your throughput be high!
Joe Hupcey III,
for the Questa Formal team
P.S. Full disclosure: myself and my colleague Jeremy Levitt supported Laurent and Vincent by providing feedback on their slide drafts, and they returned the favor by honoring us as co-authors.
