Efficient suspect selection in unreachable state diagnosis

  • Ryan Berryhill
  • Andreas Veneris


In the modern hardware design cycle, correcting the design when verification reveals a state to be erroneously unreachable can be a time-consuming manual process. Recently-developed algorithms aid the engineer in finding the root cause of the failure in these cases. However, they exhaustively examine every design location to determine a set of possible root causes, potentially requiring substantial runtime. This work develops a novel approach that is applicable to practical diagnosis problems. In contrast to previous approaches, it considers only a portion of the design locations but still finds the complete solution set to the problem. The presented approach proceeds through a series of iterations, each considering a strategically-chosen subset of the design locations (a suspect set) to determine if they are root causes. The results of each iteration inform the choice of suspect set for the next iteration. By choosing the first iteration’s suspect set appropriately, the algorithm is able to find the complete solution set to the problem. Empirical results on industrial designs and standard benchmark designs demonstrate a 15x speedup compared to the previous approach, while considering only 18.7% of the design locations as suspects.


Diagnosis Debug Verification Model checking 

Mathematics Subject Classification (2010)

94C12 68W35 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Berryhill, R., Veneris, A.: Automated Rectification Methodologies to Functional State-Space Unreachability. In: Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, DATE ’15, pp. 1401–1406 (2015)Google Scholar
  2. 2.
    Berryhill, R., Veneris, A.: A Complete Approach to Unreachable State Diagnosability via Property Directed Reachability. In: Proceedings of the 2016 Asia and South Pacific Design Automation Conference, ASP-DAC ’16 (2016)Google Scholar
  3. 3.
    Berryhill, R., Veneris, A.: Efficient Selection of Suspect Sets in Unreachable State Diagnosis. In: Proceedings of the 2016 Int’l Symposium on Artificial Intelligence and Mathematics, ISAIM ’16 (2016)Google Scholar
  4. 4.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. In: Advances in Computers, vol. 58, pp. 118–149 (2003)Google Scholar
  5. 5.
    Bradley, A.: Sat-Based Model Checking without Unrolling. In: Int’l Conf. on Verification, Model Checking, and Abstract Interpretation, pp. 70–87 (2011)Google Scholar
  6. 6.
    Brummayer, R., Biere, A.: Local Two-Level And-Inverter Graph Minimization without Blowup. In: Proceedings of the 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, MEMICS ’06 (2006)Google Scholar
  7. 7.
    Cabodi, G., Loiacono, C., Palena, M., Pasini, P., Patti, D., Quer, S., Vendraminetto, D., Biere, A., Heljanko, K., Baumgartner, J.: Hardware model checking competition 2014: An analysis and comparison of solvers and benchmarks vol. 9 (2016)Google Scholar
  8. 8.
    Eén, N., Mishchenko, A., Brayton, R.: Efficient Implementation of Property Directed Reachability. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, FMCAD ’11, pp. 125–134. FMCAD Inc, Austin (2011)Google Scholar
  9. 9.
    Foster, H.: Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial). In: Int’l Conference on Computer-Aided Verification (CAV), pp. 5–10 (2008)Google Scholar
  10. 10.
    Foster, H.: From Volume to Velocity: The Transforming Landscape in Function Verification. In: Design Verification Conference (2011)Google Scholar
  11. 11.
    Keng, B., Safarpour, S., Veneris, A.: Bounded model debugging. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(11), 1790–1803 (2010). CrossRefGoogle Scholar
  12. 12.
    Keng, B., Veneris, A.: Path-directed abstraction and refinement for sat-based design debugging. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 32(10), 1609–1622 (2013). CrossRefGoogle Scholar
  13. 13.
    Mangassarian, H., Veneris, A., Safarpour, S., Benedetti, M., Smith, D.: A Performance-Driven Qbf-Based on Iterative Logic Array Representation with Applications to Verification, Debug and Test. In: Int’l Conf. on CAD (2007)Google Scholar
  14. 14.
    Mangassarian, H., Le, B., Veneris, A.: Debugging rtl using structural dominance. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 33(1), 153–166 (2014). CrossRefGoogle Scholar
  15. 15. (2007)
  16. 16.
    Safarpour, S., Veneris, A.: Automated design debugging with abstraction and refinement. Trans. Comp. Aided Des. Integ. Cir. Sys. 28(10), 1597–1608 (2009)CrossRefGoogle Scholar
  17. 17.
    Smith, A., Veneris, A., Ali, M.F., Viglas, A.: Fault diagnosis and logic debugging using boolean satisfiability. IEEE Trans. Comput. Aided Design Integr. Circuits Syst. 24(10), 1606–1621 (2005)CrossRefGoogle Scholar
  18. 18.
    Tseitin, G.S.: On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic Part II, 115–125 (1968)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Department of Electrical and Computer EngineeringUniversity of TorontoTorontoCanada

Personalised recommendations