Finding Glitches Using Formal Methods

Slides for presentation in Industrial Track at Async 2016 Conference (IEEE International Symposium on Asynchronous Circuits and Systems, May 2016). Authors: Yan Peng, Ian W. Jones, and Mark Greenstreet. The increasing scale and complexity of integrated circuits leads to many departures from a pure, synchronous design methodology. Clock-domain crossings, multi-cycle paths, and circuits for test with long combinational logic delays introduce vulnerabilities for glitch-related failures. Conventional simulation techniques can miss glitches because of the large number of value and timing scenarios. We have tried several commercially available tools but have not found a comprehensive solution. This paper presents a concise statement of what it means for a logic circuit to be “glitch free”. This property can be verified using satisfiability solvers. We present our implementation using the ACL2 theorem proving system and some experimental results. This is the final version of the slides presented at Async 2016. They are a slightly trimmed-down version of the slides that have previously been cleared, OL# 2016-0105.