An Efficient Rewriting Framework for Trace Coverage of Symmetric Systems

  • Flavio M. De PaulaEmail author
  • Arvind Haran
  • Brad Bingham
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)


Verification coverage is an important metric in any hardware verification effort. Coverage models are proposed as a set of events the hardware may exhibit, intended to be possible under a test scenario. At the system level, these events each correspond to a visited state or taken transition in a transition system that represents the underlying hardware. A more sophisticated approach is to check that tests exercise specific sequences of events, corresponding to traces through the transition system. However, such trace-based coverage models are inherently expensive to consider in practice, as the number of traces is exponential in trace length. We present a novel framework that combines the approaches of conservative abstraction with rewriting to construct a concise trace-based coverage model of a class of parameterized symmetric systems. First, we leverage both symmetry and rewriting to construct abstractions that can be tailored by users’ defined rewriting. Then, under this abstraction, a coverage model for a larger system can be generated from traces for a smaller system. This coverage model is of tractable size, is tractable to generate, and can be used to identify coverage-holes in large systems. Our experiments on the cache coherence protocol implementation from the multi-billion transistors IBM POWER™ Processor demonstrate the viability and effectiveness of this approach.



The authors thank Viresh Paruthi and Jesse Bingham for valuable suggestions that helped with clarity of this paper.


  1. 1.
    Miller, J.C., Maloney, C.J.: Systematic mistake analysis of digital computer programs. Commun. ACM 6(2), 58–63 (1963)CrossRefzbMATHGoogle Scholar
  2. 2.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411–420. IEEE (1999)Google Scholar
  3. 3.
    Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 327–341. Springer, Heidelberg (2002). CrossRefGoogle Scholar
  4. 4.
    Ziv, A.: Cross-product functional coverage measurement with temporal properties-based assertions. In: DATE, p. 10834. IEEE (2003)Google Scholar
  5. 5.
    Chockler, H., Kupferman, O., Vardi, M.: Coverage metrics for formal verification. STTT 8(4–5), 373–386 (2006)CrossRefzbMATHGoogle Scholar
  6. 6.
    Piziali, A.: Functional Verification Coverage Measurement and Analysis, 1st edn. Springer Publishing Company Incorporated, New York (2004). Google Scholar
  7. 7.
    Czemerinski, H., Braberman, V., Uchitel, S.: Behaviour abstraction coverage as black-box adequacy criteria. In: ICST, pp. 222–231. IEEE (2013)Google Scholar
  8. 8.
    Castillos, K.C., Dadeau, F., Julliand, J.: Coverage criteria for model-based testing using property patterns. In: Proceedings of 9th MBT Workshop, pp. 29–43 (2014)Google Scholar
  9. 9.
    Papamarcos, M.S., Patel, J.H.: A low-overhead coherence solution for multiprocessors with private cache memories. In: Proceedings of 11th Annual International Symposium on Computer Architecture, pp. 348–354. ACM, New York (1984)Google Scholar
  10. 10.
    Shen, J., Abraham, J.A.: An RTL abstraction technique for processor microarchitecture validation and test generation. J. Electron. Test. 16, 67–81 (2000)CrossRefGoogle Scholar
  11. 11.
    Chou, Ching-Tsun, Mannava, Phanindra K., Park, Seungjoon: A simple method for parameterized verification of cache coherence protocols. In: Hu, Alan J., Martin, Andrew K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382–398. Springer, Heidelberg (2004). CrossRefGoogle Scholar
  12. 12.
    Book, R.V., Otto, F.: String-Rewriting Systems. Springer, New York (1993). CrossRefzbMATHGoogle Scholar
  13. 13.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRefzbMATHGoogle Scholar
  14. 14.
    Sinharoy, B., et al.: IBM POWER7 multicore server processor. IBM J. Res. Dev. 55(3), 191–219 (2011)CrossRefGoogle Scholar
  15. 15.
    Starke, W.J., et al.: The cache and memory subsystems of the IBM POWER8 processor. IBM J. Res. Dev. 59(1), 3:1–3:13 (2015)CrossRefGoogle Scholar
  16. 16.
    Cragon, H.G.: Memory Systems and Pipelined Processors. Jones and Bartlett Publishers, Burlington (1996)Google Scholar
  17. 17.
    Shimizu, K., et. al.: Verification of the cell broadband engine; processor. In: Proceedings of 43rd Annual DAC, pp. 338–343. ACM (2006)Google Scholar
  18. 18.
    Ludden, J.M., et al.: Functional verification of the POWER4 microprocessor and POWER4 multiprocessor system. IBM J. Res. Dev. 46(1), 53–76 (2002)CrossRefGoogle Scholar
  19. 19.
    Adir, A., et al.: Genesys-pro: innovations in test program generation for functional processor verification. IEEE Des. Test Comput. 21(2), 84–93 (2004)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Flavio M. De Paula
    • 1
    Email author
  • Arvind Haran
    • 1
  • Brad Bingham
    • 1
  1. 1.IBM CorporationAustinUSA

Personalised recommendations